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;

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 ;

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

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

(Tape-Chg (t,h1,T)) . (h + 1) = 1
by Th26;(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;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

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)]

set s2 = [p2,i2,(Tape-Chg (t,h1,T))];A22:
the Symbols of ZeroTuring = {0,1}
by Def19;

end;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