reconsider F = 0 as Symbol of SuccTuring by Lm6;

let s be All-State of SuccTuring; :: thesis: for t being Tape of SuccTuring

for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )

let t be Tape of SuccTuring; :: thesis: for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )

let h, n be Element of NAT ; :: thesis: ( s = [0,h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> ) )

assume that

A1: s = [0,h,t] and

A2: t storeData <*h,n*> ; :: thesis: ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> )

A3: t . h = 0 by A2, Th17;

set i3 = (((h + 1) + 1) + n) + 1;

reconsider h1 = h + 1 as Element of INT by INT_1:def 2;

reconsider p1 = 1 as State of SuccTuring by Lm5;

A4: (h1 + 1) + n < (((h + 1) + 1) + n) + 1 by XREAL_1:29;

h <= h + n by NAT_1:11;

then A5: h + 2 <= (h + n) + 2 by XREAL_1:7;

A6: h1 < h + 2 by XREAL_1:8;

then A7: h1 < (h + n) + 2 by A5, XXREAL_0:2;

reconsider p2 = 2 as State of SuccTuring by Lm5;

reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;

reconsider nk = (h1 + 1) + n as Element of INT by INT_1:def 2;

reconsider hh = h as Element of INT by INT_1:def 2;

reconsider n3 = (((h + 1) + 1) + n) + 1 as Element of INT by INT_1:def 2;

reconsider T = 1 as Symbol of SuccTuring by Lm6;

set t1 = Tape-Chg (t,h1,T);

A8: h < h1 by XREAL_1:29;

A9: t . ((h + n) + 2) = 0 by A2, Th17;

A10: ( (Tape-Chg (t,h1,T)) . h = 0 & (Tape-Chg (t,h1,T)) . ((h + n) + 2) = 0 & ( for i being Integer st h < i & i < (h + n) + 2 holds

(Tape-Chg (t,h1,T)) . i = 1 ) )

(Tape-Chg (t,h1,T)) . i = 1

A15: TRAN s = Succ_Tran . [(s `1_3),(s3 . (Head s))] by Def17

.= Succ_Tran . [0,(s3 . (Head s))] by A1

.= Succ_Tran . [0,(t . (Head s))] by A1

.= [1,0,1] by A1, A3, Th30 ;

then A16: offset (TRAN s) = 1 ;

set s1 = [p1,h1,t];

reconsider s3 = [p1,h1,t] `3_3 as Tape of SuccTuring ;

Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)) = Tape-Chg (t,(Head s),((TRAN s) `2_3)) by A1

.= Tape-Chg (t,h,((TRAN s) `2_3)) by A1

.= Tape-Chg (t,h,F) by A15

.= t by A3, Th24 ;

then A17: Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),t] by A1, Lm7

.= [1,((Head s) + (offset (TRAN s))),t] by A15

.= [p1,h1,t] by A1, A16 ;

A18: TRAN [p1,h1,t] = Succ_Tran . [([p1,h1,t] `1_3),(s3 . (Head [p1,h1,t]))] by Def17

.= Succ_Tran . [p1,(s3 . (Head [p1,h1,t]))]

.= Succ_Tran . [p1,(t . (Head [p1,h1,t]))]

.= Succ_Tran . [1,(t . h1)]

.= [1,1,1] by A2, A8, A7, Th17, Th30 ;

then A19: offset (TRAN [p1,h1,t]) = 1 ;

reconsider p1 = 1 as State of SuccTuring by Lm5;

set s2 = [p1,i2,(Tape-Chg (t,h1,T))];

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

then A20: 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 Lm7

.= [1,((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg (t,h1,T))] by A18

.= [p1,i2,(Tape-Chg (t,h1,T))] by A19 ;

reconsider p3 = 3 as State of SuccTuring by Lm5;

set sn = [p1,nk,(Tape-Chg (t,h1,T))];

set t2 = Tape-Chg ((Tape-Chg (t,h1,T)),nk,T);

set t3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F);

( the Tran of SuccTuring . [p1,1] = [p1,1,1] & p1 <> the AcceptS of SuccTuring ) by Def17, Th30;

then A21: (Computation [p1,i2,(Tape-Chg (t,h1,T))]) . n = [p1,(((h + 1) + 1) + n),(Tape-Chg (t,h1,T))] by A12, Lm4;

( h1 + 1 <= ((h + 1) + 1) + n & h1 < h1 + 1 ) by NAT_1:11, XREAL_1:29;

then A22: h1 < (h1 + 1) + n by XXREAL_0:2;

A23: ( (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . h = 0 & ( for i being Integer st h < i & i <= (h + n) + 2 holds

(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = 1 ) )

set sm = [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))];

reconsider sm3 = [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `3_3 as Tape of SuccTuring ;

A28: the Symbols of SuccTuring = {0,1} by Def17;

.= Succ_Tran . [2,(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]

.= Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]

.= [p3,0,(- 1)] by A29 ;

then A31: offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) = - 1 ;

set j1 = (1 + 1) + n;

set sp5 = [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];

defpred S_{1}[ Nat] means ( h + $1 <= nk implies (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . $1 = [3,(nk - $1),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] );

reconsider sn3 = [p1,nk,(Tape-Chg (t,h1,T))] `3_3 as Tape of SuccTuring ;

A32: h + ((1 + 1) + n) = nk ;

set Rs = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)));

A33: TRAN [p1,nk,(Tape-Chg (t,h1,T))] = Succ_Tran . [([p1,nk,(Tape-Chg (t,h1,T))] `1_3),(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))] by Def17

.= Succ_Tran . [p1,(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]

.= Succ_Tran . [p1,((Tape-Chg (t,h1,T)) . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]

.= [2,1,1] by A10, Th30 ;

then A34: offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]) = 1 ;

A35: h < (h1 + 1) + n by A8, A22, XXREAL_0:2;

A36: ( (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . h = 0 & (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ((h + (n + 1)) + 2) = 0 & ( for k being Integer st h < k & k < (h + (n + 1)) + 2 holds

(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . k = 1 ) )

Tape-Chg (([p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `3_3),(Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]),((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `2_3)) = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),(Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]),((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A30 ;

then A41: Following [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] = [((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `1_3),((Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) + (offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by Lm7

.= [p3,((Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) + (offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A30

.= [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A31 ;

Tape-Chg (([p1,nk,(Tape-Chg (t,h1,T))] `3_3),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3)) = Tape-Chg ((Tape-Chg (t,h1,T)),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3))

.= Tape-Chg ((Tape-Chg (t,h1,T)),nk,((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3))

.= Tape-Chg ((Tape-Chg (t,h1,T)),nk,T) by A33 ;

then A42: Following [p1,nk,(Tape-Chg (t,h1,T))] = [((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `1_3),((Head [p1,nk,(Tape-Chg (t,h1,T))]) + (offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]))),(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by Lm7

.= [2,((Head [p1,nk,(Tape-Chg (t,h1,T))]) + (offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]))),(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by A33

.= [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by A34 ;

A43: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Def7;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A53, A43);

then A54: (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . ((1 + 1) + n) = [3,(nk - ((1 + 1) + n)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A32

.= [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] ;

.= (Computation (Following ((Computation s) . 1))) . (((n + 1) + 1) + (((1 + 1) + n) + 1)) by Def7

.= (Computation (Following [p1,h1,t])) . (((n + 1) + 1) + (((1 + 1) + n) + 1)) by A17, Th9

.= (Computation ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . ((n + 1) + 1))) . (((1 + 1) + n) + 1) by A20, Th10

.= (Computation (Following ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . (n + 1)))) . (((1 + 1) + n) + 1) by Def7 ;

then (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) = (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (((1 + 1) + n) + 1) by A21, A42, A41, Def7;

then A58: (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) = [4,h,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A54, A55, Def7;

then A59: ((Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)))) `1_3 = 4

.= the AcceptS of SuccTuring by Def17 ;

hence s is Accept-Halt ; :: thesis: ( (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> )

then A60: Result s = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) by A59, Def9;

hence (Result s) `2_3 = h by A58; :: thesis: (Result s) `3_3 storeData <*h,(n + 1)*>

(Result s) `3_3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A58, A60;

hence (Result s) `3_3 storeData <*h,(n + 1)*> by A40, Th16; :: thesis: verum

let s be All-State of SuccTuring; :: thesis: for t being Tape of SuccTuring

for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )

let t be Tape of SuccTuring; :: thesis: for head, n being Element of NAT st s = [0,head,t] & t storeData <*head,n*> holds

( s is Accept-Halt & (Result s) `2_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )

let h, n be Element of NAT ; :: thesis: ( s = [0,h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> ) )

assume that

A1: s = [0,h,t] and

A2: t storeData <*h,n*> ; :: thesis: ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> )

A3: t . h = 0 by A2, Th17;

set i3 = (((h + 1) + 1) + n) + 1;

reconsider h1 = h + 1 as Element of INT by INT_1:def 2;

reconsider p1 = 1 as State of SuccTuring by Lm5;

A4: (h1 + 1) + n < (((h + 1) + 1) + n) + 1 by XREAL_1:29;

h <= h + n by NAT_1:11;

then A5: h + 2 <= (h + n) + 2 by XREAL_1:7;

A6: h1 < h + 2 by XREAL_1:8;

then A7: h1 < (h + n) + 2 by A5, XXREAL_0:2;

reconsider p2 = 2 as State of SuccTuring by Lm5;

reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;

reconsider nk = (h1 + 1) + n as Element of INT by INT_1:def 2;

reconsider hh = h as Element of INT by INT_1:def 2;

reconsider n3 = (((h + 1) + 1) + n) + 1 as Element of INT by INT_1:def 2;

reconsider T = 1 as Symbol of SuccTuring by Lm6;

set t1 = Tape-Chg (t,h1,T);

A8: h < h1 by XREAL_1:29;

A9: t . ((h + n) + 2) = 0 by A2, Th17;

A10: ( (Tape-Chg (t,h1,T)) . h = 0 & (Tape-Chg (t,h1,T)) . ((h + n) + 2) = 0 & ( for i being Integer st h < i & i < (h + n) + 2 holds

(Tape-Chg (t,h1,T)) . i = 1 ) )

proof

A12:
for i being Integer st (h + 1) + 1 <= i & i < ((h + 1) + 1) + n holds
thus
(Tape-Chg (t,h1,T)) . h = 0
by A3, A8, Th26; :: thesis: ( (Tape-Chg (t,h1,T)) . ((h + n) + 2) = 0 & ( for i being Integer st h < i & i < (h + n) + 2 holds

(Tape-Chg (t,h1,T)) . i = 1 ) )

thus (Tape-Chg (t,h1,T)) . ((h + n) + 2) = 0 by A9, A5, A6, Th26; :: thesis: for i being Integer st h < i & i < (h + n) + 2 holds

(Tape-Chg (t,h1,T)) . i = 1

end;(Tape-Chg (t,h1,T)) . i = 1 ) )

thus (Tape-Chg (t,h1,T)) . ((h + n) + 2) = 0 by A9, A5, A6, Th26; :: thesis: for i being Integer st h < i & i < (h + n) + 2 holds

(Tape-Chg (t,h1,T)) . i = 1

hereby :: thesis: verum

let i be Integer; :: thesis: ( h < i & i < (h + n) + 2 implies (Tape-Chg (t,h1,T)) . b_{1} = 1 )

assume A11: ( h < i & i < (h + n) + 2 ) ; :: thesis: (Tape-Chg (t,h1,T)) . b_{1} = 1

end;assume A11: ( h < i & i < (h + n) + 2 ) ; :: thesis: (Tape-Chg (t,h1,T)) . b

(Tape-Chg (t,h1,T)) . i = 1

proof

reconsider s3 = s `3_3 as Tape of SuccTuring ;
let i be Integer; :: thesis: ( (h + 1) + 1 <= i & i < ((h + 1) + 1) + n implies (Tape-Chg (t,h1,T)) . i = 1 )

assume that

A13: (h + 1) + 1 <= i and

A14: i < ((h + 1) + 1) + n ; :: thesis: (Tape-Chg (t,h1,T)) . i = 1

h1 < h1 + 1 by XREAL_1:29;

then h1 < i by A13, XXREAL_0:2;

then h < i by A8, XXREAL_0:2;

hence (Tape-Chg (t,h1,T)) . i = 1 by A10, A14; :: thesis: verum

end;assume that

A13: (h + 1) + 1 <= i and

A14: i < ((h + 1) + 1) + n ; :: thesis: (Tape-Chg (t,h1,T)) . i = 1

h1 < h1 + 1 by XREAL_1:29;

then h1 < i by A13, XXREAL_0:2;

then h < i by A8, XXREAL_0:2;

hence (Tape-Chg (t,h1,T)) . i = 1 by A10, A14; :: thesis: verum

A15: TRAN s = Succ_Tran . [(s `1_3),(s3 . (Head s))] by Def17

.= Succ_Tran . [0,(s3 . (Head s))] by A1

.= Succ_Tran . [0,(t . (Head s))] by A1

.= [1,0,1] by A1, A3, Th30 ;

then A16: offset (TRAN s) = 1 ;

set s1 = [p1,h1,t];

reconsider s3 = [p1,h1,t] `3_3 as Tape of SuccTuring ;

Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)) = Tape-Chg (t,(Head s),((TRAN s) `2_3)) by A1

.= Tape-Chg (t,h,((TRAN s) `2_3)) by A1

.= Tape-Chg (t,h,F) by A15

.= t by A3, Th24 ;

then A17: Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),t] by A1, Lm7

.= [1,((Head s) + (offset (TRAN s))),t] by A15

.= [p1,h1,t] by A1, A16 ;

A18: TRAN [p1,h1,t] = Succ_Tran . [([p1,h1,t] `1_3),(s3 . (Head [p1,h1,t]))] by Def17

.= Succ_Tran . [p1,(s3 . (Head [p1,h1,t]))]

.= Succ_Tran . [p1,(t . (Head [p1,h1,t]))]

.= Succ_Tran . [1,(t . h1)]

.= [1,1,1] by A2, A8, A7, Th17, Th30 ;

then A19: offset (TRAN [p1,h1,t]) = 1 ;

reconsider p1 = 1 as State of SuccTuring by Lm5;

set s2 = [p1,i2,(Tape-Chg (t,h1,T))];

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

then A20: 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 Lm7

.= [1,((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg (t,h1,T))] by A18

.= [p1,i2,(Tape-Chg (t,h1,T))] by A19 ;

reconsider p3 = 3 as State of SuccTuring by Lm5;

set sn = [p1,nk,(Tape-Chg (t,h1,T))];

set t2 = Tape-Chg ((Tape-Chg (t,h1,T)),nk,T);

set t3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F);

( the Tran of SuccTuring . [p1,1] = [p1,1,1] & p1 <> the AcceptS of SuccTuring ) by Def17, Th30;

then A21: (Computation [p1,i2,(Tape-Chg (t,h1,T))]) . n = [p1,(((h + 1) + 1) + n),(Tape-Chg (t,h1,T))] by A12, Lm4;

( h1 + 1 <= ((h + 1) + 1) + n & h1 < h1 + 1 ) by NAT_1:11, XREAL_1:29;

then A22: h1 < (h1 + 1) + n by XXREAL_0:2;

A23: ( (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . h = 0 & ( for i being Integer st h < i & i <= (h + n) + 2 holds

(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = 1 ) )

proof

set sp3 = [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];
thus
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . h = 0
by A8, A10, A22, Th26; :: thesis: for i being Integer st h < i & i <= (h + n) + 2 holds

(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = 1

end;(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = 1

hereby :: thesis: verum

let i be Integer; :: thesis: ( h < i & i <= (h + n) + 2 implies (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b_{1} = 1 )

assume that

A24: h < i and

A25: i <= (h + n) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b_{1} = 1

end;assume that

A24: h < i and

A25: i <= (h + n) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b

per cases
( i <> (h + n) + 2 or i = (h + n) + 2 )
;

end;

set sm = [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))];

reconsider sm3 = [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `3_3 as Tape of SuccTuring ;

A28: the Symbols of SuccTuring = {0,1} by Def17;

A29: now :: thesis: Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)]end;

A30: TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] =
Succ_Tran . [([p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `1_3),(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]
by Def17
per cases
( (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3 = 1 or (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3 = 0 )
by A28, TARSKI:def 2;

end;

.= Succ_Tran . [2,(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]

.= Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]

.= [p3,0,(- 1)] by A29 ;

then A31: offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) = - 1 ;

set j1 = (1 + 1) + n;

set sp5 = [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];

defpred S

reconsider sn3 = [p1,nk,(Tape-Chg (t,h1,T))] `3_3 as Tape of SuccTuring ;

A32: h + ((1 + 1) + n) = nk ;

set Rs = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)));

A33: TRAN [p1,nk,(Tape-Chg (t,h1,T))] = Succ_Tran . [([p1,nk,(Tape-Chg (t,h1,T))] `1_3),(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))] by Def17

.= Succ_Tran . [p1,(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]

.= Succ_Tran . [p1,((Tape-Chg (t,h1,T)) . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]

.= [2,1,1] by A10, Th30 ;

then A34: offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]) = 1 ;

A35: h < (h1 + 1) + n by A8, A22, XXREAL_0:2;

A36: ( (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . h = 0 & (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ((h + (n + 1)) + 2) = 0 & ( for k being Integer st h < k & k < (h + (n + 1)) + 2 holds

(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . k = 1 ) )

proof

then A40:
Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) is_1_between h,(h + (n + 1)) + 2
;
thus
(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . h = 0
by A35, A23, A4, Th26; :: thesis: ( (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ((h + (n + 1)) + 2) = 0 & ( for k being Integer st h < k & k < (h + (n + 1)) + 2 holds

(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . k = 1 ) )

thus (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ((h + (n + 1)) + 2) = 0 by Th26; :: thesis: for k being Integer st h < k & k < (h + (n + 1)) + 2 holds

(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . k = 1

end;(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . k = 1 ) )

thus (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ((h + (n + 1)) + 2) = 0 by Th26; :: thesis: for k being Integer st h < k & k < (h + (n + 1)) + 2 holds

(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . k = 1

hereby :: thesis: verum

let i be Integer; :: thesis: ( h < i & i < (h + (n + 1)) + 2 implies (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = 1 )

assume that

A37: h < i and

A38: i < (h + (n + 1)) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = 1

i + 1 <= (h + (n + 1)) + 2 by A38, INT_1:7;

then A39: i <= ((h + (n + 1)) + 2) - 1 by XREAL_1:19;

thus (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i by A38, Th26

.= 1 by A23, A37, A39 ; :: thesis: verum

end;assume that

A37: h < i and

A38: i < (h + (n + 1)) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = 1

i + 1 <= (h + (n + 1)) + 2 by A38, INT_1:7;

then A39: i <= ((h + (n + 1)) + 2) - 1 by XREAL_1:19;

thus (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i by A38, Th26

.= 1 by A23, A37, A39 ; :: thesis: verum

Tape-Chg (([p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `3_3),(Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]),((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `2_3)) = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),(Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]),((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A30 ;

then A41: Following [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] = [((TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) `1_3),((Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) + (offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by Lm7

.= [p3,((Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) + (offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A30

.= [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A31 ;

Tape-Chg (([p1,nk,(Tape-Chg (t,h1,T))] `3_3),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3)) = Tape-Chg ((Tape-Chg (t,h1,T)),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3))

.= Tape-Chg ((Tape-Chg (t,h1,T)),nk,((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3))

.= Tape-Chg ((Tape-Chg (t,h1,T)),nk,T) by A33 ;

then A42: Following [p1,nk,(Tape-Chg (t,h1,T))] = [((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `1_3),((Head [p1,nk,(Tape-Chg (t,h1,T))]) + (offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]))),(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by Lm7

.= [2,((Head [p1,nk,(Tape-Chg (t,h1,T))]) + (offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]))),(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by A33

.= [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by A34 ;

A43: for k being Nat st S

S

proof

A53:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A44: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A44: S

now :: thesis: ( h + (k + 1) <= nk implies (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (k + 1) = [3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] )

hence
Sreconsider ik = nk - k as Element of INT by INT_1:def 2;

set k3 = nk - k;

A45: h + k < (h + k) + 1 by XREAL_1:29;

set sk = [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];

reconsider tt = [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3 as Tape of SuccTuring ;

nk <= nk + k by INT_1:6;

then A46: nk - k <= nk by XREAL_1:20;

assume A47: h + (k + 1) <= nk ; :: thesis: (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (k + 1) = [3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]

then h + k < nk + 0 by A45, XXREAL_0:2;

then A48: h - 0 < nk - k by XREAL_1:21;

reconsider ii = nk - k as Element of NAT by A48, INT_1:3;

(h + n) + 2 < ((h + n) + 2) + 1 by XREAL_1:29;

then ii < (h + (n + 1)) + 2 by A46, XXREAL_0:2;

then A49: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ii = 1 by A36, A48;

A50: TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = Succ_Tran . [([p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `1_3),(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by Def17

.= Succ_Tran . [p3,(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= Succ_Tran . [p3,((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= [3,1,(- 1)] by A49, Th30 ;

then A51: offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = - 1 ;

A52: Tape-Chg (([p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3),(Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3)) = Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(nk - k),((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(nk - k),T) by A50

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A49, Th24 ;

end;set k3 = nk - k;

A45: h + k < (h + k) + 1 by XREAL_1:29;

set sk = [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];

reconsider tt = [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3 as Tape of SuccTuring ;

nk <= nk + k by INT_1:6;

then A46: nk - k <= nk by XREAL_1:20;

assume A47: h + (k + 1) <= nk ; :: thesis: (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (k + 1) = [3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]

then h + k < nk + 0 by A45, XXREAL_0:2;

then A48: h - 0 < nk - k by XREAL_1:21;

reconsider ii = nk - k as Element of NAT by A48, INT_1:3;

(h + n) + 2 < ((h + n) + 2) + 1 by XREAL_1:29;

then ii < (h + (n + 1)) + 2 by A46, XXREAL_0:2;

then A49: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ii = 1 by A36, A48;

A50: TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = Succ_Tran . [([p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `1_3),(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by Def17

.= Succ_Tran . [p3,(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= Succ_Tran . [p3,((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= [3,1,(- 1)] by A49, Th30 ;

then A51: offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = - 1 ;

A52: Tape-Chg (([p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3),(Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3)) = Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(nk - k),((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(nk - k),T) by A50

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A49, Th24 ;

hereby :: thesis: verum

thus (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (k + 1) =
Following [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by A44, A47, A45, Def7, XXREAL_0:2

.= [((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1_3),((Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A52, Lm7

.= [3,((Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A50

.= [3,((nk - k) + (- 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A51

.= [3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] ; :: thesis: verum

end;.= [((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1_3),((Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A52, Lm7

.= [3,((Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A50

.= [3,((nk - k) + (- 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A51

.= [3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] ; :: thesis: verum

for k being Nat holds S

then A54: (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . ((1 + 1) + n) = [3,(nk - ((1 + 1) + n)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A32

.= [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] ;

A55: now :: thesis: Following [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = [4,(h + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]

(Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) =
(Computation ((Computation s) . (1 + 1))) . (((n + 1) + 1) + (((1 + 1) + n) + 1))
by Th10
reconsider tt = [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3 as Tape of SuccTuring ;

A56: TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = Succ_Tran . [([p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `1_3),(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by Def17

.= Succ_Tran . [3,(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= Succ_Tran . [3,((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= [4,0,0] by A36, Th30 ;

then A57: offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = 0 ;

Tape-Chg (([p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3),(Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3)) = Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),h,((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),h,F) by A56

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A36, Th24 ;

hence Following [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = [((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1_3),((Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by Lm7

.= [4,((Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A56

.= [4,(h + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A57 ;

:: thesis: verum

end;A56: TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = Succ_Tran . [([p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `1_3),(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by Def17

.= Succ_Tran . [3,(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= Succ_Tran . [3,((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]

.= [4,0,0] by A36, Th30 ;

then A57: offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = 0 ;

Tape-Chg (([p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3),(Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3)) = Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]),((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),h,((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `2_3))

.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),h,F) by A56

.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A36, Th24 ;

hence Following [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = [((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1_3),((Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by Lm7

.= [4,((Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A56

.= [4,(h + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A57 ;

:: thesis: verum

.= (Computation (Following ((Computation s) . 1))) . (((n + 1) + 1) + (((1 + 1) + n) + 1)) by Def7

.= (Computation (Following [p1,h1,t])) . (((n + 1) + 1) + (((1 + 1) + n) + 1)) by A17, Th9

.= (Computation ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . ((n + 1) + 1))) . (((1 + 1) + n) + 1) by A20, Th10

.= (Computation (Following ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . (n + 1)))) . (((1 + 1) + n) + 1) by Def7 ;

then (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) = (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (((1 + 1) + n) + 1) by A21, A42, A41, Def7;

then A58: (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) = [4,h,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A54, A55, Def7;

then A59: ((Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)))) `1_3 = 4

.= the AcceptS of SuccTuring by Def17 ;

hence s is Accept-Halt ; :: thesis: ( (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> )

then A60: Result s = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) by A59, Def9;

hence (Result s) `2_3 = h by A58; :: thesis: (Result s) `3_3 storeData <*h,(n + 1)*>

(Result s) `3_3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A58, A60;

hence (Result s) `3_3 storeData <*h,(n + 1)*> by A40, Th16; :: thesis: verum