連立一次方程式のためのマクロ推論規則

Subst' 規則

A[y/y] ≡ A を使う。

   y = C

 -----------[Subst']

  A = A[C/y]

代入法の原理

Subt'とSymm, Tranを使う。

  A = B   y = C

 -----------------[Ass]

  A[C/y] = B[C/y]

左変型規則と右変形規則

  A = B

 --------[Left:A = A']

  A' = B

  A = B

 --------[Right:B = B']

  A = B'

連続等式変型

   A  [S = S']

 = A' [T = T']

 = A''
よって、A = A''

  S = S'

 ------------------[Subst]

  A[S/x] = A[S'/x]

  (A = A')               T = T'

                --------------------[Subst]

                 A'[T/X] = A'[T'/x]

                (A' = A'')

 -------------------------------[Tran]

  A = A''