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:29;
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:29;
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:64
.= Zero_Tran . [0,(t . (Head s))] by A2, MCART_1:64
.= [1,0,1] by A2, A9, Th38, MCART_1:64 ;
then A12: offset (TRAN s) = 1 by MCART_1:64;
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:7;
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:64
.= 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:64
.= [4,1,(- 1)] by A16, Th38, MCART_1:64 ;
then A18: offset (TRAN [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))]) = - 1 by MCART_1:64;
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:7;
h1 < h + 2 by XREAL_1:8;
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:64
.= Zero_Tran . [p1,(t . (Head [p1,h1,t]))] by MCART_1:64
.= Zero_Tran . [1,(t . h1)] by MCART_1:64
.= [2,1,1] by A8, A4, A20, Def13, Th38 ;
then A22: offset (TRAN [p1,h1,t]) = 1 by MCART_1:64;

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:64
.= Zero_Tran . [p2,((Tape-Chg (t,h1,T)) . (Head [p2,i2,(Tape-Chg (t,h1,T))]))] by MCART_1:64
.= [3,0,(- 1)] by A23, MCART_1:64 ;
then A26: offset (TRAN [p2,i2,(Tape-Chg (t,h1,T))]) = - 1 by MCART_1:64;
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:64
.= Tape-Chg ((Tape-Chg (t,h1,T)),i2,((TRAN [p2,i2,(Tape-Chg (t,h1,T))]) `2)) by MCART_1:64
.= Tape-Chg ((Tape-Chg (t,h1,T)),i2,F) by A25, MCART_1:64 ;
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:64
.= [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))] by A26, A7, MCART_1:64 ;
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:64
.= 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:64
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T) by A17, MCART_1:64 ;
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:64
.= [4,h,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T))] by A18, A5, MCART_1:64 ;
Tape-Chg ((s `3),(Head s),((TRAN s) `2)) = Tape-Chg (t,(Head s),((TRAN s) `2)) by A2, MCART_1:64
.= Tape-Chg (t,h,((TRAN s) `2)) by A2, MCART_1:64
.= Tape-Chg (t,h,F) by A11, MCART_1:64
.= 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:64
.= [p1,h1,t] by A2, A12, MCART_1:64 ;
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:64
.= Tape-Chg (t,h1,((TRAN [p1,h1,t]) `2)) by MCART_1:64
.= Tape-Chg (t,h1,T) by A21, MCART_1:64 ;
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:64
.= [p2,i2,(Tape-Chg (t,h1,T))] by A22, MCART_1:64 ;
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:64
.= 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:64; :: 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:64;
(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