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 A1: ( s = [0 ,h,t] & t storeData <*h,n*> ) ; :: thesis: ( s is Accept-Halt & (Result s) `2 = h & (Result s) `3 storeData <*h,(n + 1)*> )
then A2: ( t . h = 0 & t . ((h + n) + 2) = 0 & ( for i being Integer st h < i & i < (h + n) + 2 holds
t . i = 1 ) ) by Th20;
reconsider s3 = s `3 as Tape of SuccTuring ;
reconsider F = 0 as Symbol of SuccTuring by Lm6;
reconsider T = 1 as Symbol of SuccTuring by Lm6;
A3: 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, A2, Th34, MCART_1:68 ;
A4: 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 A3, MCART_1:68
.= t by A2, Th28 ;
reconsider p1 = 1 as State of SuccTuring by Lm5;
reconsider h1 = h + 1 as Element of INT by INT_1:def 2;
A5: offset (TRAN s) = 1 by A3, MCART_1:68;
set s1 = [p1,h1,t];
A6: Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),t] by A1, A4, Lm7
.= [1,((Head s) + (offset (TRAN s))),t] by A3, MCART_1:68
.= [p1,h1,t] by A1, A5, MCART_1:68 ;
A7: h < h1 by XREAL_1:31;
h <= h + n by NAT_1:11;
then A8: h + 2 <= (h + n) + 2 by XREAL_1:9;
A9: h1 < h + 2 by XREAL_1:10;
then A10: h1 < (h + n) + 2 by A8, XXREAL_0:2;
reconsider s3 = [p1,h1,t] `3 as Tape of SuccTuring ;
set t1 = Tape-Chg t,h1,T;
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 A2, A7, 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 A2, A8, A9, 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 A1, A12, Th20 ;
:: thesis: verum
end;
end;
end;
end;
A13: 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 A1, A7, A10, Th20, Th34 ;
A14: 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 A13, MCART_1:68 ;
A15: offset (TRAN [p1,h1,t]) = 1 by A13, MCART_1:68;
reconsider p1 = 1 as State of SuccTuring by Lm5;
reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;
set s2 = [p1,i2,(Tape-Chg t,h1,T)];
A16: Following [p1,h1,t] = [((TRAN [p1,h1,t]) `1 ),((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg t,h1,T)] by A14, Lm7
.= [1,((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg t,h1,T)] by A13, MCART_1:68
.= [p1,i2,(Tape-Chg t,h1,T)] by A15, MCART_1:68 ;
A17: the Tran of SuccTuring . [p1,1] = [p1,1,1] by Def18, Th34;
A18: p1 <> the AcceptS of SuccTuring by Def18;
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 A19: ( (h + 1) + 1 <= i & i < ((h + 1) + 1) + n ) ; :: thesis: (Tape-Chg t,h1,T) . i = 1
h1 < h1 + 1 by XREAL_1:31;
then h1 < i by A19, XXREAL_0:2;
then h < i by A7, XXREAL_0:2;
hence (Tape-Chg t,h1,T) . i = 1 by A11, A19; :: thesis: verum
end;
then A20: (Computation [p1,i2,(Tape-Chg t,h1,T)]) . n = [p1,(((h + 1) + 1) + n),(Tape-Chg t,h1,T)] by A17, A18, Lm4;
reconsider nk = (h1 + 1) + n as Element of INT by INT_1:def 2;
set sn = [p1,nk,(Tape-Chg t,h1,T)];
reconsider sn3 = [p1,nk,(Tape-Chg t,h1,T)] `3 as Tape of SuccTuring ;
A21: 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 ;
set t2 = Tape-Chg (Tape-Chg t,h1,T),nk,T;
A22: h1 + 1 <= ((h + 1) + 1) + n by NAT_1:11;
h1 < h1 + 1 by XREAL_1:31;
then A23: h1 < (h1 + 1) + n by A22, XXREAL_0:2;
then A24: h < (h1 + 1) + n by A7, XXREAL_0:2;
A25: ( (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 A7, 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 A26: ( h < i & 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, A26, 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;
A29: 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 A21, MCART_1:68 ;
A30: offset (TRAN [p1,nk,(Tape-Chg t,h1,T)]) = 1 by A21, MCART_1:68;
set i3 = (((h + 1) + 1) + n) + 1;
reconsider n3 = (((h + 1) + 1) + n) + 1 as Element of INT by INT_1:def 2;
reconsider p2 = 2 as State of SuccTuring by Lm5;
reconsider p3 = 3 as State of SuccTuring by Lm5;
set sm = [p2,n3,(Tape-Chg (Tape-Chg t,h1,T),nk,T)];
A31: 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 A29, 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 A21, MCART_1:68
.= [p2,n3,(Tape-Chg (Tape-Chg t,h1,T),nk,T)] by A30, MCART_1:68 ;
reconsider sm3 = [p2,n3,(Tape-Chg (Tape-Chg t,h1,T),nk,T)] `3 as Tape of SuccTuring ;
A32: the Symbols of SuccTuring = {0 ,1} by Def18;
A33: 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 A32, 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;
A34: 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 A33, MCART_1:68 ;
set t3 = Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F;
A35: 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 A34, MCART_1:68 ;
A36: offset (TRAN [p2,n3,(Tape-Chg (Tape-Chg t,h1,T),nk,T)]) = - 1 by A34, MCART_1:68;
A37: n3 + (- 1) = ((h + 1) + 1) + n ;
set sp3 = [p3,nk,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)];
A38: 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 A35, 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 A34, MCART_1:68
.= [p3,nk,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)] by A36, A37, MCART_1:68 ;
A39: (h1 + 1) + n < (((h + 1) + 1) + n) + 1 by XREAL_1:31;
A40: ( (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 A24, A25, A39, 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 A41: ( h < i & i < (h + (n + 1)) + 2 ) ; :: thesis: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F) . i = 1
then i + 1 <= (h + (n + 1)) + 2 by INT_1:20;
then A42: 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 A41, Th30
.= 1 by A25, A41, A42 ; :: thesis: verum
end;
end;
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)] );
A43: S1[ 0 ] by Def8;
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
assume A46: 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)]
A47: h + k < (h + k) + 1 by XREAL_1:31;
set k3 = nk - k;
reconsider ik = nk - k as Element of INT by INT_1:def 2;
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 ;
h + k < nk + 0 by A46, A47, XXREAL_0:2;
then A48: h - 0 < nk - k by XREAL_1:23;
h >= 0 by NAT_1:2;
then reconsider ii = nk - k as Element of NAT by A48, INT_1:16, XXREAL_0:2;
nk <= nk + k by INT_1:19;
then A49: nk - k <= nk by XREAL_1:22;
now
(h + n) + 2 < ((h + n) + 2) + 1 by XREAL_1:31;
hence ii < (h + (n + 1)) + 2 by A49, XXREAL_0:2; :: thesis: verum
end;
then A50: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F) . ii = 1 by A40, A48;
A51: now
thus 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 ; :: thesis: verum
end;
A52: now
thus 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 ; :: thesis: verum
end;
A53: offset (TRAN [p3,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)]) = - 1 by A51, MCART_1:68;
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, A46, A47, 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 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 A51, MCART_1:68
.= [3,((nk - k) + (- 1)),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)] by A53, 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;
reconsider hh = h as Element of INT by INT_1:def 2;
set j1 = (1 + 1) + n;
set sp5 = [p3,hh,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)];
A54: h + ((1 + 1) + n) = nk ;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A43, 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 A54
.= [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 A40, Th34, MCART_1:68 ;
A58: 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 A40, Th28 ;
A59: offset (TRAN [p3,hh,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F)]) = 0 by A57, MCART_1:68;
thus 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 A58, 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 A59, MCART_1:68 ; :: thesis: verum
end;
set Rs = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)));
(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 A6, Th12
.= (Computation ((Computation [p1,i2,(Tape-Chg t,h1,T)]) . ((n + 1) + 1))) . (((1 + 1) + n) + 1) by A16, 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 A20, A31, A38, Def8;
then A60: (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 A61: ((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 A62: Result s = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) by A61, Def10;
hence (Result s) `2 = h by A60, MCART_1:68; :: thesis: (Result s) `3 storeData <*h,(n + 1)*>
A63: (Result s) `3 = Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F by A60, A62, MCART_1:68;
Tape-Chg (Tape-Chg (Tape-Chg t,h1,T),nk,T),n3,F is_1_between h,(h + (n + 1)) + 2 by A40, Def13;
hence (Result s) `3 storeData <*h,(n + 1)*> by A63, Th19; :: thesis: verum