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 = head & (Result s) `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 = head & (Result s) `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 = h & (Result s) `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 = h & (Result s) `3 storeData <*h,(n + 1)*> )
A3: t . h = 0 by A2, Th20;
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;
A8: n3 + (- 1) = ((h + 1) + 1) + n ;
set t1 = Tape-Chg (t,h1,T);
A9: h < h1 by XREAL_1:29;
A10: t . ((h + n) + 2) = 0 by A2, Th20;
A11: ( (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, A9, Th30; :: 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 A10, A5, A6, Th30; :: 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 A12: ( 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 Th30; :: thesis: verum
end;
suppose h1 <> i ; :: thesis: (Tape-Chg (t,h1,T)) . b1 = 1
hence (Tape-Chg (t,h1,T)) . i = t . i by Th30
.= 1 by A2, A12, Th20 ;
:: thesis: verum
end;
end;
end;
end;
A13: 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
A14: (h + 1) + 1 <= i and
A15: i < ((h + 1) + 1) + n ; :: thesis: (Tape-Chg (t,h1,T)) . i = 1
h1 < h1 + 1 by XREAL_1:29;
then h1 < i by A14, XXREAL_0:2;
then h < i by A9, XXREAL_0:2;
hence (Tape-Chg (t,h1,T)) . i = 1 by A11, A15; :: thesis: verum
end;
reconsider s3 = s `3 as Tape of SuccTuring ;
A16: TRAN s = Succ_Tran . [(s `1),(s3 . (Head s))] by Def18
.= Succ_Tran . [0,(s3 . (Head s))] by A1, MCART_1:64
.= Succ_Tran . [0,(t . (Head s))] by A1, MCART_1:64
.= [1,0,1] by A1, A3, Th34, MCART_1:64 ;
then A17: offset (TRAN s) = 1 by MCART_1:64;
set s1 = [p1,h1,t];
reconsider s3 = [p1,h1,t] `3 as Tape of SuccTuring ;
Tape-Chg ((s `3),(Head s),((TRAN s) `2)) = Tape-Chg (t,(Head s),((TRAN s) `2)) by A1, MCART_1:64
.= Tape-Chg (t,h,((TRAN s) `2)) by A1, MCART_1:64
.= Tape-Chg (t,h,F) by A16, MCART_1:64
.= t by A3, Th28 ;
then A18: Following s = [((TRAN s) `1),((Head s) + (offset (TRAN s))),t] by A1, Lm7
.= [1,((Head s) + (offset (TRAN s))),t] by A16, MCART_1:64
.= [p1,h1,t] by A1, A17, MCART_1:64 ;
A19: TRAN [p1,h1,t] = Succ_Tran . [([p1,h1,t] `1),(s3 . (Head [p1,h1,t]))] by Def18
.= Succ_Tran . [p1,(s3 . (Head [p1,h1,t]))] by MCART_1:64
.= Succ_Tran . [p1,(t . (Head [p1,h1,t]))] by MCART_1:64
.= Succ_Tran . [1,(t . h1)] by MCART_1:64
.= [1,1,1] by A2, A9, A7, Th20, Th34 ;
then A20: offset (TRAN [p1,h1,t]) = 1 by MCART_1:64;
reconsider p1 = 1 as State of SuccTuring by Lm5;
set s2 = [p1,i2,(Tape-Chg (t,h1,T))];
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 A19, MCART_1:64 ;
then A21: Following [p1,h1,t] = [((TRAN [p1,h1,t]) `1),((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 A19, MCART_1:64
.= [p1,i2,(Tape-Chg (t,h1,T))] by A20, MCART_1:64 ;
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 Def18, Th34;
then A22: (Computation [p1,i2,(Tape-Chg (t,h1,T))]) . n = [p1,(((h + 1) + 1) + n),(Tape-Chg (t,h1,T))] by A13, Lm4;
( h1 + 1 <= ((h + 1) + 1) + n & h1 < h1 + 1 ) by NAT_1:11, XREAL_1:29;
then A23: h1 < (h1 + 1) + n by XXREAL_0:2;
A24: ( (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 A9, A11, A23, Th30; :: 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
A25: h < i and
A26: 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 A27: i <> (h + n) + 2 ; :: thesis: (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1
then A28: i < (h + n) + 2 by A26, XXREAL_0:1;
thus (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = (Tape-Chg (t,h1,T)) . i by A27, Th30
.= 1 by A11, A25, A28 ; :: 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 Th30; :: 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 as Tape of SuccTuring ;
A29: the Symbols of SuccTuring = {0,1} by Def18;
A30: now
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 A29, 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 Th34; :: 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 Th34; :: thesis: verum
end;
end;
end;
A31: 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),(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))] by Def18
.= Succ_Tran . [2,(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))] by MCART_1:64
.= Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))] by MCART_1:64
.= [p3,0,(- 1)] by A30, MCART_1:64 ;
then A32: offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) = - 1 by MCART_1:64;
set j1 = (1 + 1) + n;
set sp5 = [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];
defpred S1[ Element of 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 as Tape of SuccTuring ;
A33: h + ((1 + 1) + n) = nk ;
set Rs = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)));
A34: TRAN [p1,nk,(Tape-Chg (t,h1,T))] = Succ_Tran . [([p1,nk,(Tape-Chg (t,h1,T))] `1),(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))] by Def18
.= Succ_Tran . [p1,(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))] by MCART_1:64
.= Succ_Tran . [p1,((Tape-Chg (t,h1,T)) . (Head [p1,nk,(Tape-Chg (t,h1,T))]))] by MCART_1:64
.= [2,1,1] by A11, Th34, MCART_1:64 ;
then A35: offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]) = 1 by MCART_1:64;
A36: h < (h1 + 1) + n by A9, A23, XXREAL_0:2;
A37: ( (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 A36, A24, A4, Th30; :: 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 Th30; :: 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
A38: h < i and
A39: 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 A39, INT_1:7;
then A40: 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 A39, Th30
.= 1 by A24, A38, A40 ; :: thesis: verum
end;
end;
then A41: Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) is_1_between h,(h + (n + 1)) + 2 by Def13;
Tape-Chg (([p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `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)) = 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)) by MCART_1:64
.= 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)) by MCART_1:64
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A31, MCART_1:64 ;
then A42: 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),((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 A31, MCART_1:64
.= [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A32, A8, MCART_1:64 ;
Tape-Chg (([p1,nk,(Tape-Chg (t,h1,T))] `3),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2)) = Tape-Chg ((Tape-Chg (t,h1,T)),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2)) by MCART_1:64
.= Tape-Chg ((Tape-Chg (t,h1,T)),nk,((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2)) by MCART_1:64
.= Tape-Chg ((Tape-Chg (t,h1,T)),nk,T) by A34, MCART_1:64 ;
then A43: Following [p1,nk,(Tape-Chg (t,h1,T))] = [((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `1),((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 A34, MCART_1:64
.= [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] by A35, MCART_1:64 ;
A44: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A45: S1[k] ; :: thesis: S1[k + 1]
now
reconsider ik = nk - k as Element of INT by INT_1:def 2;
set k3 = nk - k;
A46: 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 as Tape of SuccTuring ;
nk <= nk + k by INT_1:6;
then A47: nk - k <= nk by XREAL_1:20;
assume A48: 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 A46, XXREAL_0:2;
then A49: h - 0 < nk - k by XREAL_1:21;
h >= 0 by NAT_1:2;
then reconsider ii = nk - k as Element of NAT by A49, INT_1:3, XXREAL_0:2;
(h + n) + 2 < ((h + n) + 2) + 1 by XREAL_1:29;
then ii < (h + (n + 1)) + 2 by A47, XXREAL_0:2;
then A50: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ii = 1 by A37, A49;
A51: 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),(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by Def18
.= Succ_Tran . [p3,(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by MCART_1:64
.= 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))]))] by MCART_1:64
.= [3,1,(- 1)] by A50, Th34, MCART_1:64 ;
then A52: offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = - 1 by MCART_1:64;
A53: Tape-Chg (([p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `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)) = 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)) by MCART_1:64
.= 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)) by MCART_1:64
.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),(nk - k),T) by A51, MCART_1:64
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A50, Th28 ;
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 A45, A48, A46, Def8, XXREAL_0:2
.= [((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1),((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 A53, 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 A51, MCART_1:64
.= [3,((nk - k) + (- 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A52, MCART_1:64
.= [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;
A54: S1[ 0 ] by Def8;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A54, A44);
 then A55: (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 A33
.= [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] ;
A56: now
reconsider tt = [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3 as Tape of SuccTuring ;
A57: 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),(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by Def18
.= Succ_Tran . [3,(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))] by MCART_1:64
.= 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))]))] by MCART_1:64
.= [4,0,0] by A37, Th34, MCART_1:64 ;
then A58: offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = 0 by MCART_1:64;
Tape-Chg (([p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `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)) = 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)) by MCART_1:64
.= 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)) by MCART_1:64
.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),h,F) by A57, MCART_1:64
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A37, Th28 ;
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),((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 A57, MCART_1:64
.= [4,(h + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] by A58, MCART_1:64 ;
:: 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 Th13
.= (Computation (Following ((Computation s) . 1))) . (((n + 1) + 1) + (((1 + 1) + n) + 1)) by Def8
.= (Computation (Following [p1,h1,t])) . (((n + 1) + 1) + (((1 + 1) + n) + 1)) by A18, Th12
.= (Computation ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . ((n + 1) + 1))) . (((1 + 1) + n) + 1) by A21, Th13
.= (Computation (Following ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . (n + 1)))) . (((1 + 1) + n) + 1) by Def8 ;
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 A22, A43, A42, Def8;
then A59: (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 A55, A56, Def8;
then A60: ((Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)))) `1 = 4 by MCART_1:64
.= the AcceptS of SuccTuring by Def18 ;
hence s is Accept-Halt by Def9; :: thesis: ( (Result s) `2 = h & (Result s) `3 storeData <*h,(n + 1)*> )
then A61: Result s = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) by A60, Def10;
hence (Result s) `2 = h by A59, MCART_1:64; :: thesis: (Result s) `3 storeData <*h,(n + 1)*>
(Result s) `3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) by A59, A61, MCART_1:64;
hence (Result s) `3 storeData <*h,(n + 1)*> by A41, Th19; :: thesis: verum