reconsider F = 0 as Symbol of ZeroTuring by Lm9;
let s be All-State of ZeroTuring ; :: thesis: for t being Tape of ZeroTuring
for head being Element of NAT
for f being FinSequence of NAT st len f >= 1 & s = [0 ,head,t] & t storeData <*head*> ^ f holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,0 *> )
let t be Tape of ZeroTuring ; :: thesis: for head being Element of NAT
for f being FinSequence of NAT st len f >= 1 & s = [0 ,head,t] & t storeData <*head*> ^ f holds
( s is Accept-Halt & (Result s) `2 = head & (Result s) `3 storeData <*head,0 *> )
let h be Element of NAT ; :: thesis: for f being FinSequence of NAT st len f >= 1 & s = [0 ,h,t] & t storeData <*h*> ^ f holds
( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,0 *> )
let f be FinSequence of NAT ; :: thesis: ( len f >= 1 & s = [0 ,h,t] & t storeData <*h*> ^ f implies ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,0 *> ) )
assume that
A1: len f >= 1 and
A2: s = [0 ,h,t] and
A3: t storeData <*h*> ^ f ; :: thesis: ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,0 *> )
reconsider s3 = s `3 as Tape of ZeroTuring ;
reconsider h1 = h + 1 as Element of INT by INT_1:def 2;
set m = f /. 1;
set n = (h + (f /. 1)) + 2;
A4: h < h1 by XREAL_1:31;
reconsider p1 = 1 as State of ZeroTuring by Lm8;
A5: h1 + (- 1) = h ;
set s1 = [p1,h1,t];
reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;
A6: h1 < i2 by XREAL_1:31;
reconsider T = 1 as Symbol of ZeroTuring by Lm9;
A7: i2 + (- 1) = h1 ;
set t1 = Tape-Chg t,h1,T;
set t2 = Tape-Chg (Tape-Chg t,h1,T),i2,F;
set t3 = Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T;
A8: t is_1_between h,(h + (f /. 1)) + 2 by A1, A3, Th25;
then A9: t . h = 0 by Def13;
then (Tape-Chg t,h1,T) . h = 0 by A4, Th30;
then (Tape-Chg (Tape-Chg t,h1,T),i2,F) . h = 0 by A4, A6, Th30;
then A10: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T) . h = 0 by A4, Th30;
A11: TRAN s = Zero_Tran . [(s `1 ),(s3 . (Head s))] by Def20
.= Zero_Tran . [0 ,(s3 . (Head s))] by A2, MCART_1:68
.= Zero_Tran . [0 ,(t . (Head s))] by A2, MCART_1:68
.= [1,0 ,1] by A2, A9, Th38, MCART_1:68 ;
then A12: offset (TRAN s) = 1 by MCART_1:68;
set Rs = (Computation s) . (((1 + 1) + 1) + 1);
reconsider p3 = 3 as State of ZeroTuring by Lm8;
A13: (h + 1) + 1 = (h + 0 ) + 2 ;
A14: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T) . (h + 1) = 1 by Th30;

A15: now

let k be Integer; :: thesis: ( h < k & k < (h + 0 ) + 2 implies (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T) . k = 1 )
assume ( h < k & k < (h + 0 ) + 2 ) ; :: thesis: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T) . k = 1
then ( h + 1 <= k & k <= h + 1 ) by A13, INT_1:20;
hence (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T) . k = 1 by A14, XXREAL_0:1; :: thesis: verum

end;

(Tape-Chg t,h1,T) . (h + 1) = 1 by Th30;
then A16: (Tape-Chg (Tape-Chg t,h1,T),i2,F) . (h + 1) = 1 by A6, Th30;
set s3 = [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)];
reconsider s33 = [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)] `3 as Tape of ZeroTuring ;
A17: TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)] = Zero_Tran . [([p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)] `1 ),(s33 . (Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]))] by Def20
.= Zero_Tran . [p3,(s33 . (Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]))] by MCART_1:68
.= Zero_Tran . [p3,((Tape-Chg (Tape-Chg t,h1,T),i2,F) . (Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]))] by MCART_1:68
.= [4,1,(- 1)] by A16, Th38, MCART_1:68 ;
then A18: offset (TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) = - 1 by MCART_1:68;
reconsider p2 = 2 as State of ZeroTuring by Lm8;
reconsider s13 = [p1,h1,t] `3 as Tape of ZeroTuring ;
h <= h + (f /. 1) by NAT_1:11;
then A19: h + 2 <= (h + (f /. 1)) + 2 by XREAL_1:9;
h1 < h + 2 by XREAL_1:10;
then A20: h1 < (h + (f /. 1)) + 2 by A19, XXREAL_0:2;
A21: TRAN [p1,h1,t] = Zero_Tran . [([p1,h1,t] `1 ),(s13 . (Head [p1,h1,t]))] by Def20
.= Zero_Tran . [p1,(s13 . (Head [p1,h1,t]))] by MCART_1:68
.= Zero_Tran . [p1,(t . (Head [p1,h1,t]))] by MCART_1:68
.= Zero_Tran . [1,(t . h1)] by MCART_1:68
.= [2,1,1] by A8, A4, A20, Def13, Th38 ;
then A22: offset (TRAN [p1,h1,t]) = 1 by MCART_1:68;

A23: now

A24: the Symbols of ZeroTuring = {0 ,1} by Def20;

per cases ( (Tape-Chg t,h1,T) . i2 = 1 or (Tape-Chg t,h1,T) . i2 = 0 ) by A24, TARSKI:def 2;

suppose (Tape-Chg t,h1,T) . i2 = 1 ; :: thesis: Zero_Tran . [2,((Tape-Chg t,h1,T) . i2)] = [3,0 ,(- 1)]

hence Zero_Tran . [2,((Tape-Chg t,h1,T) . i2)] = [3,0 ,(- 1)] by Th38; :: thesis: verum

end;

suppose (Tape-Chg t,h1,T) . i2 = 0 ; :: thesis: Zero_Tran . [2,((Tape-Chg t,h1,T) . i2)] = [3,0 ,(- 1)]

hence Zero_Tran . [2,((Tape-Chg t,h1,T) . i2)] = [3,0 ,(- 1)] by Th38; :: thesis: verum

end;

end;

end;

set s2 = [p2,i2,(Tape-Chg t,h1,T)];
reconsider s23 = [p2,i2,(Tape-Chg t,h1,T)] `3 as Tape of ZeroTuring ;
A25: TRAN [p2,i2,(Tape-Chg t,h1,T)] = Zero_Tran . [([p2,i2,(Tape-Chg t,h1,T)] `1 ),(s23 . (Head [p2,i2,(Tape-Chg t,h1,T)]))] by Def20
.= Zero_Tran . [p2,(s23 . (Head [p2,i2,(Tape-Chg t,h1,T)]))] by MCART_1:68
.= Zero_Tran . [p2,((Tape-Chg t,h1,T) . (Head [p2,i2,(Tape-Chg t,h1,T)]))] by MCART_1:68
.= [3,0 ,(- 1)] by A23, MCART_1:68 ;
then A26: offset (TRAN [p2,i2,(Tape-Chg t,h1,T)]) = - 1 by MCART_1:68;
Tape-Chg ([p2,i2,(Tape-Chg t,h1,T)] `3 ),(Head [p2,i2,(Tape-Chg t,h1,T)]),((TRAN [p2,i2,(Tape-Chg t,h1,T)]) `2 ) = Tape-Chg (Tape-Chg t,h1,T),(Head [p2,i2,(Tape-Chg t,h1,T)]),((TRAN [p2,i2,(Tape-Chg t,h1,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg t,h1,T),i2,((TRAN [p2,i2,(Tape-Chg t,h1,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg t,h1,T),i2,F by A25, MCART_1:68 ;
then A27: Following [p2,i2,(Tape-Chg t,h1,T)] = [((TRAN [p2,i2,(Tape-Chg t,h1,T)]) `1 ),((Head [p2,i2,(Tape-Chg t,h1,T)]) + (offset (TRAN [p2,i2,(Tape-Chg t,h1,T)]))),(Tape-Chg (Tape-Chg t,h1,T),i2,F)] by Lm10
.= [3,((Head [p2,i2,(Tape-Chg t,h1,T)]) + (offset (TRAN [p2,i2,(Tape-Chg t,h1,T)]))),(Tape-Chg (Tape-Chg t,h1,T),i2,F)] by A25, MCART_1:68
.= [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)] by A26, A7, MCART_1:68 ;
reconsider p3 = 3 as State of ZeroTuring by Lm8;
A28: Tape-Chg ([p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)] `3 ),(Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]),((TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) `2 ) = Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),(Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]),((TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,((TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T by A17, MCART_1:68 ;
set s3 = [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)];
A29: Following [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)] = [((TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) `1 ),((Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) + (offset (TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T)] by A28, Lm10
.= [4,((Head [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]) + (offset (TRAN [p3,h1,(Tape-Chg (Tape-Chg t,h1,T),i2,F)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T)] by A17, MCART_1:68
.= [4,h,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T)] by A18, A5, MCART_1:68 ;
Tape-Chg (s `3 ),(Head s),((TRAN s) `2 ) = Tape-Chg t,(Head s),((TRAN s) `2 ) by A2, MCART_1:68
.= Tape-Chg t,h,((TRAN s) `2 ) by A2, MCART_1:68
.= Tape-Chg t,h,F by A11, MCART_1:68
.= t by A9, Th28 ;
then A30: Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),t] by A2, Lm10
.= [1,((Head s) + (offset (TRAN s))),t] by A11, MCART_1:68
.= [p1,h1,t] by A2, A12, MCART_1:68 ;
Tape-Chg ([p1,h1,t] `3 ),(Head [p1,h1,t]),((TRAN [p1,h1,t]) `2 ) = Tape-Chg t,(Head [p1,h1,t]),((TRAN [p1,h1,t]) `2 ) by MCART_1:68
.= Tape-Chg t,h1,((TRAN [p1,h1,t]) `2 ) by MCART_1:68
.= Tape-Chg t,h1,T by A21, MCART_1:68 ;
then A31: Following [p1,h1,t] = [((TRAN [p1,h1,t]) `1 ),((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg t,h1,T)] by Lm10
.= [2,((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg t,h1,T)] by A21, MCART_1:68
.= [p2,i2,(Tape-Chg t,h1,T)] by A22, MCART_1:68 ;
A32: (Computation s) . (((1 + 1) + 1) + 1) = Following ((Computation s) . ((1 + 1) + 1)) by Def8
.= Following (Following ((Computation s) . (1 + 1))) by Def8
.= Following (Following (Following ((Computation s) . 1))) by Def8
.= [4,h,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T)] by A30, A31, A27, A29, Th12 ;
then A33: ((Computation s) . (((1 + 1) + 1) + 1)) `1 = 4 by MCART_1:68
.= the AcceptS of ZeroTuring by Def20 ;
hence s is Accept-Halt by Def9; :: thesis: ( (Result s) `2 = h & (Result s) `3 storeData <*h,0 *> )
then A34: Result s = (Computation s) . (((1 + 1) + 1) + 1) by A33, Def10;
hence (Result s) `2 = h by A32, MCART_1:68; :: thesis: (Result s) `3 storeData <*h,0 *>
A35: (Result s) `3 = Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T by A32, A34, MCART_1:68;
(Tape-Chg (Tape-Chg t,h1,T),i2,F) . i2 = 0 by Th30;
then (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T) . i2 = 0 by A6, Th30;
then Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),i2,F),h1,T is_1_between h,(h + 0 ) + 2 by A10, A15, Def13;
hence (Result s) `3 storeData <*h,0 *> by A35, Th19; :: thesis: verum