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 ) )
proof
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
hereby :: thesis: verum
let i be Integer; :: thesis: ( h < i & i < (h + n) + 2 implies (Tape-Chg (t,h1,T)) . b1 = 1 )
assume A11: ( h < i & i < (h + n) + 2 ) ; :: thesis: (Tape-Chg (t,h1,T)) . b1 = 1
per cases ( h1 = i or h1 <> i ) ;
suppose h1 = i ; :: thesis: (Tape-Chg (t,h1,T)) . b1 = 1
hence (Tape-Chg (t,h1,T)) . i = 1 by Th26; :: thesis: verum
end;
suppose h1 <> i ; :: thesis: (Tape-Chg (t,h1,T)) . b1 = 1
hence (Tape-Chg (t,h1,T)) . i = t . i by Th26
.= 1 by A2, A11, Th17 ;
:: thesis: verum
end;
end;
end;
end;
A12: for i being Integer st (h + 1) + 1 <= i & i < ((h + 1) + 1) + n holds
(Tape-Chg (t,h1,T)) . i = 1
proof
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;
reconsider s3 = s `3_3 as Tape of SuccTuring ;
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
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
hereby :: thesis: verum
let i be Integer; :: thesis: ( h < i & i <= (h + n) + 2 implies (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1 )
assume that
A24: h < i and
A25: i <= (h + n) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1
per cases ( i <> (h + n) + 2 or i = (h + n) + 2 ) ;
suppose A26: i <> (h + n) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1
then A27: i < (h + n) + 2 by A25, XXREAL_0:1;
thus (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = (Tape-Chg (t,h1,T)) . i by A26, Th26
.= 1 by A10, A24, A27 ; :: thesis: verum
end;
suppose i = (h + n) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1
hence (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = 1 by Th26; :: thesis: verum
end;
end;
end;
end;
set sp3 = [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];
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)]
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;
suppose (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3 = 1 ; :: thesis: Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)]
hence Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)] by Th30; :: thesis: verum
end;
suppose (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3 = 0 ; :: thesis: Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)]
hence Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)] by Th30; :: thesis: verum
end;
end;
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
.= 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 S1[ 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 ) )
proof
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
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;
end;
then A40: Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) is_1_between h,(h + (n + 1)) + 2 ;
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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A44: S1[k] ; :: thesis: S1[k + 1]
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))] )
reconsider 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 ;
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;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A53: S1[ 0 ] by Def7;
for k being Nat holds S1[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))] ;
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))]
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;
(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
.= (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