xÎL(M₁)                                                                                          hipótese

$wÎA₁ $aÎG₁^* (q₁,x,Z₁)├_M1^*(w,L,a)                                             def. L(M)

$wÎA₁ $aÎG₁^* (q₁,x,Z₁Z₂)├_M1^*(w,L,aZ₂)                                      def. ├_M

$wÎA₁ $aÎG₁^* (q₁,x,Z₁Z₂)├_M2^*(w,L,aZ₂)                                      def. d₂ em M₂

$wÎA₁ $aÎG₁^* (q₂,x,Z₂)├_M2 (q₁,x,Z₁Z₂)├_M2^*(w,L,aZ₂)├_M2(f,L,aZ₂)├_M2^*(f,L,L) def.d₂ em M₂

$fÎQ₂  (q₂,x,Z₂)├_M2^*(f,L,L)                                                            def. ├_M^* e def. M₂

xÎN(M₂)                                                                                          def. N(M)

xÎN(M₁)                                                                                          hipótese

$wÎQ₁ (q₁,x,Z₁)├_M1^*(w,L,L)                                                         def. N(M)

$wÎQ₁ (q₁,x,Z₁Z₂)├_M1^*(w,L,Z₂)                                                     def. ├_M

$wÎQ₁ (q₁,x,Z₁Z₂)├_M2^*(w,L,Z₂)                                                     def. d₂ em M₂

$wÎQ₁ (q₂,x,Z₂)├_M2 (q₁,x,Z₁Z₂)├_M2^*(w,L,Z₂)├_M2 (f,L,Z₂)           def. d₂ em M₂

(q₂,x,Z₂)├_M2^*(f,L,Z₂)                                                                       def. ├_M^* e def. M₂

$wÎA₂ $aÎG₂^* (q₁,x,Z₂)├_M1^*(w,L,a)                                              Lógicapredicados                 

xÎL(M₂)                                                                                           def. L(M)

xÎN(M₁)                                                                                          hipótese

$wÎQ₁ (q₁,x,Z₁)├_M1^*(w,L,L)                                                         def. L(M)

$wÎQ₁ (q₁,x,Z₁Z₂)├_M1^*(w,L,Z₂)                                                    def. ├_M

$wÎQ₁ (q₁,x,Z₁Z₂)├_M2^*(w,L,Z₂)                                                    def. d₂ em M₂

$wÎQ₁ (q₂,x,Z₂)├_M2 (q₁,x,Z₁Z₂)├_M2^*(w,L,Z₂)├_M2 (f,L,Z₂)          def. d₂ em M₂

(q₂,x,Z₂)├_M2^*(f,L,Z₂)                                                                      def. ├_M^* e def. M₂

$wÎA₂ $aÎG₂^* (q₁,x,Z₂)├_M1^*(w,L,a)                                             Lógica predicados                 

xÎL(M₂)                                                                                          def. N(M)

xÎL(M₁)                                                                                           hipótese

$wÎA₁ $aÎG₁^* (q₁,x,Z₁)├_M1^*(w,L,a)                                              def. N(M)

$wÎA₁ $aÎG₁^* (q₁,x,Z₁Z₂)├_M1^*(w,L,aZ₂)                                       def. ├_M

$wÎA₁ $aÎG₁^* (q₁,x,Z₁Z₂)├_M2^*(w,L,aZ₂)                                       def. d₂ em M₂

$wÎA₁ $aÎG₁^* (q₂,x,Z₂)├_M2 (q₁,x,Z₁Z₂)├_M2^*(w,L,aZ₂)├_M2(f,L,aZ₂)├_M2^*(f,L,L) def.d₂ em M₂

$fÎQ₂  (q₂,x,Z₂)├_M2^*(f,L,L)                                                            def. ├_M^* e def. M₂

xÎN(M₂)                                                                                          def. L(M)