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_3 = head & (Result s) `3_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_3 = head & (Result s) `3_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_3 = h & (Result s) `3_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_3 = h & (Result s) `3_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_3 = h & (Result s) `3_3 storeData <*h,0*> )
reconsider s3 = s `3_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;
set s1 = [p1,h1,t];
reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;
A5: h1 < i2 by XREAL_1:29;
reconsider T = 1 as Symbol of ZeroTuring by Lm9;
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);
A6: t is_1_between h,(h + (f /. 1)) + 2 by A1, A3, Th22;
then A7: t . h = 0 ;
then (Tape-Chg (t,h1,T)) . h = 0 by A4, Th26;
then (Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)) . h = 0 by A4, A5, Th26;
then A8: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T)) . h = 0 by A4, Th26;
A9: TRAN s = Zero_Tran . [(s `1_3),(s3 . (Head s))] by Def19
.= Zero_Tran . [0,(s3 . (Head s))] by A2
.= Zero_Tran . [0,(t . (Head s))] by A2
.= [1,0,1] by A2, A7, Th33 ;
then A10: offset (TRAN s) = 1 ;
set Rs = (Computation s) . (((1 + 1) + 1) + 1);
reconsider p3 = 3 as State of ZeroTuring by Lm8;
A11: (h + 1) + 1 = (h + 0) + 2 ;
A12: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T)) . (h + 1) = 1 by Th26;

A13: now :: thesis: for k being Integer st h < k & k < (h + 0) + 2 holds
(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T)) . k = 1

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 A11, INT_1:7;
hence (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T)) . k = 1 by A12, XXREAL_0:1; :: thesis: verum

end;

(Tape-Chg (t,h1,T)) . (h + 1) = 1 by Th26;
then A14: (Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)) . (h + 1) = 1 by A5, Th26;
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_3 as Tape of ZeroTuring ;
A15: 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_3),(s33 . (Head [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))]))] by Def19
.= Zero_Tran . [p3,(s33 . (Head [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))]))]
.= Zero_Tran . [p3,((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)) . (Head [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))]))]
.= [4,1,(- 1)] by A14, Th33 ;
then A16: offset (TRAN [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))]) = - 1 ;
reconsider p2 = 2 as State of ZeroTuring by Lm8;
reconsider s13 = [p1,h1,t] `3_3 as Tape of ZeroTuring ;
h <= h + (f /. 1) by NAT_1:11;
then A17: h + 2 <= (h + (f /. 1)) + 2 by XREAL_1:7;
h1 < h + 2 by XREAL_1:8;
then A18: h1 < (h + (f /. 1)) + 2 by A17, XXREAL_0:2;
A19: TRAN [p1,h1,t] = Zero_Tran . [([p1,h1,t] `1_3),(s13 . (Head [p1,h1,t]))] by Def19
.= Zero_Tran . [p1,(s13 . (Head [p1,h1,t]))]
.= Zero_Tran . [p1,(t . (Head [p1,h1,t]))]
.= Zero_Tran . [1,(t . h1)]
.= [2,1,1] by A6, A4, A18, Th33 ;
then A20: offset (TRAN [p1,h1,t]) = 1 ;

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

A22: the Symbols of ZeroTuring = {0,1} by Def19;

per cases ( (Tape-Chg (t,h1,T)) . i2 = 1 or (Tape-Chg (t,h1,T)) . i2 = 0 ) by A22, 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 Th33; :: 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 Th33; :: thesis: verum

end;

end;

end;

set s2 = [p2,i2,(Tape-Chg (t,h1,T))];
reconsider s23 = [p2,i2,(Tape-Chg (t,h1,T))] `3_3 as Tape of ZeroTuring ;
A23: TRAN [p2,i2,(Tape-Chg (t,h1,T))] = Zero_Tran . [([p2,i2,(Tape-Chg (t,h1,T))] `1_3),(s23 . (Head [p2,i2,(Tape-Chg (t,h1,T))]))] by Def19
.= Zero_Tran . [p2,(s23 . (Head [p2,i2,(Tape-Chg (t,h1,T))]))]
.= Zero_Tran . [p2,((Tape-Chg (t,h1,T)) . (Head [p2,i2,(Tape-Chg (t,h1,T))]))]
.= [3,0,(- 1)] by A21 ;
then A24: offset (TRAN [p2,i2,(Tape-Chg (t,h1,T))]) = - 1 ;
Tape-Chg (([p2,i2,(Tape-Chg (t,h1,T))] `3_3),(Head [p2,i2,(Tape-Chg (t,h1,T))]),((TRAN [p2,i2,(Tape-Chg (t,h1,T))]) `2_3)) = Tape-Chg ((Tape-Chg (t,h1,T)),(Head [p2,i2,(Tape-Chg (t,h1,T))]),((TRAN [p2,i2,(Tape-Chg (t,h1,T))]) `2_3))
.= Tape-Chg ((Tape-Chg (t,h1,T)),i2,((TRAN [p2,i2,(Tape-Chg (t,h1,T))]) `2_3))
.= Tape-Chg ((Tape-Chg (t,h1,T)),i2,F) by A23 ;
then A25: Following [p2,i2,(Tape-Chg (t,h1,T))] = [((TRAN [p2,i2,(Tape-Chg (t,h1,T))]) `1_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 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 A23
.= [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))] by A24 ;
reconsider p3 = 3 as State of ZeroTuring by Lm8;
A26: Tape-Chg (([p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))] `3_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_3)) = 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_3))
.= 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_3))
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T) by A15 ;
set s3 = [p3,h1,(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F))];
A27: 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_3),((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 A26, 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 A15
.= [4,h,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T))] by A16 ;
Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)) = Tape-Chg (t,(Head s),((TRAN s) `2_3)) by A2
.= Tape-Chg (t,h,((TRAN s) `2_3)) by A2
.= Tape-Chg (t,h,F) by A9
.= t by A7, Th24 ;
then A28: Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),t] by A2, Lm10
.= [1,((Head s) + (offset (TRAN s))),t] by A9
.= [p1,h1,t] by A2, A10 ;
Tape-Chg (([p1,h1,t] `3_3),(Head [p1,h1,t]),((TRAN [p1,h1,t]) `2_3)) = Tape-Chg (t,(Head [p1,h1,t]),((TRAN [p1,h1,t]) `2_3))
.= Tape-Chg (t,h1,((TRAN [p1,h1,t]) `2_3))
.= Tape-Chg (t,h1,T) by A19 ;
then A29: Following [p1,h1,t] = [((TRAN [p1,h1,t]) `1_3),((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 A19
.= [p2,i2,(Tape-Chg (t,h1,T))] by A20 ;
A30: (Computation s) . (((1 + 1) + 1) + 1) = Following ((Computation s) . ((1 + 1) + 1)) by Def7
.= Following (Following ((Computation s) . (1 + 1))) by Def7
.= Following (Following (Following ((Computation s) . 1))) by Def7
.= [4,h,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T))] by A28, A29, A25, A27, Th9 ;
then A31: ((Computation s) . (((1 + 1) + 1) + 1)) `1_3 = 4
.= the AcceptS of ZeroTuring by Def19 ;
hence s is Accept-Halt ; :: thesis: ( (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,0*> )
then A32: Result s = (Computation s) . (((1 + 1) + 1) + 1) by A31, Def9;
hence (Result s) `2_3 = h by A30; :: thesis: (Result s) `3_3 storeData <*h,0*>
A33: (Result s) `3_3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T) by A30, A32;
(Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)) . i2 = 0 by Th26;
then (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T)) . i2 = 0 by A5, Th26;
then Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),i2,F)),h1,T) is_1_between h,(h + 0) + 2 by A8, A13;
hence (Result s) `3_3 storeData <*h,0*> by A33, Th16; :: thesis: verum