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:31;
h <= h + n by NAT_1:11;
then A5: h + 2 <= (h + n) + 2 by XREAL_1:9;
A6: h1 < h + 2 by XREAL_1:10;
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:31;
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:31;
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:68
.= Succ_Tran . [0 ,(t . (Head s))] by A1, MCART_1:68
.= [1,0 ,1] by A1, A3, Th34, MCART_1:68 ;
then A17: offset (TRAN s) = 1 by MCART_1:68;
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:68
.= Tape-Chg t,h,((TRAN s) `2 ) by A1, MCART_1:68
.= Tape-Chg t,h,F by A16, MCART_1:68
.= 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:68
.= [p1,h1,t] by A1, A17, MCART_1:68 ;
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:68
.= Succ_Tran . [p1,(t . (Head [p1,h1,t]))] by MCART_1:68
.= Succ_Tran . [1,(t . h1)] by MCART_1:68
.= [1,1,1] by A2, A9, A7, Th20, Th34 ;
then A20: offset (TRAN [p1,h1,t]) = 1 by MCART_1:68;
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:68
.= Tape-Chg t,h1,((TRAN [p1,h1,t]) `2 ) by MCART_1:68
.= Tape-Chg t,h1,T by A19, MCART_1:68 ;
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:68
.= [p1,i2,(Tape-Chg t,h1,T)] by A20, MCART_1:68 ;
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:31;
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:68
.= 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:68
.= [p3,0 ,(- 1)] by A30, MCART_1:68 ;
then A32: offset (TRAN [p2,n3,(Tape-Chg (Tape-Chg t,h1,T),nk,T)]) = - 1 by MCART_1:68;
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:68
.= Succ_Tran . [p1,((Tape-Chg t,h1,T) . (Head [p1,nk,(Tape-Chg t,h1,T)]))] by MCART_1:68
.= [2,1,1] by A11, Th34, MCART_1:68 ;
then A35: offset (TRAN [p1,nk,(Tape-Chg t,h1,T)]) = 1 by MCART_1:68;
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:20;
then A40: i <= ((h + (n + 1)) + 2) - 1 by XREAL_1:21;
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:68
.= 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:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F by A31, MCART_1:68 ;
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:68
.= [p3,nk,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)] by A32, A8, MCART_1:68 ;
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:68
.= Tape-Chg (Tape-Chg t,h1,T),nk,((TRAN [p1,nk,(Tape-Chg t,h1,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg t,h1,T),nk,T by A34, MCART_1:68 ;
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:68
.= [p2,n3,(Tape-Chg (Tape-Chg t,h1,T),nk,T)] by A35, MCART_1:68 ;
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:31;
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:19;
then A47: nk - k <= nk by XREAL_1:22;
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:23;
h >= 0 by NAT_1:2;
then reconsider ii = nk - k as Element of NAT by A49, INT_1:16, XXREAL_0:2;
(h + n) + 2 < ((h + n) + 2) + 1 by XREAL_1:31;
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:68
.= 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:68
.= [3,1,(- 1)] by A50, Th34, MCART_1:68 ;
then A52: offset (TRAN [p3,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)]) = - 1 by MCART_1:68;
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:68
.= 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:68
.= Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F),(nk - k),T by A51, MCART_1:68
.= 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:68
.= [3,((nk - k) + (- 1)),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)] by A52, MCART_1:68
.= [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:68
.= 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:68
.= [4,0 ,0 ] by A37, Th34, MCART_1:68 ;
then A58: offset (TRAN [p3,hh,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)]) = 0 by MCART_1:68;
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:68
.= 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:68
.= Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F),h,F by A57, MCART_1:68
.= 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:68
.= [4,(h + 0 ),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)] by A58, MCART_1:68 ;
:: 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:68
.= 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:68; :: 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:68;
hence (Result s) `3 storeData <*h,(n + 1)*> by A41, Th19; :: thesis: verum