let s be All-State of SumTuring ; :: thesis: for t being Tape of SumTuring
for head, n1, n2 being Element of NAT st s = [0 ,head,t] & t storeData <*head,n1,n2*> holds
( s is Accept-Halt & (Result s) `2 = 1 + head & (Result s) `3 storeData <*(1 + head),(n1 + n2)*> )
let t be Tape of SumTuring ; :: thesis: for head, n1, n2 being Element of NAT st s = [0 ,head,t] & t storeData <*head,n1,n2*> holds
( s is Accept-Halt & (Result s) `2 = 1 + head & (Result s) `3 storeData <*(1 + head),(n1 + n2)*> )
let h, n1, n2 be Element of NAT ; :: thesis: ( s = [0 ,h,t] & t storeData <*h,n1,n2*> implies ( s is Accept-Halt & (Result s) `2 = 1 + h & (Result s) `3 storeData <*(1 + h),(n1 + n2)*> ) )
assume A1: ( s = [0 ,h,t] & t storeData <*h,n1,n2*> ) ; :: thesis: ( s is Accept-Halt & (Result s) `2 = 1 + h & (Result s) `3 storeData <*(1 + h),(n1 + n2)*> )
reconsider s3 = s `3 as Tape of SumTuring ;
reconsider F = 0 as Symbol of SumTuring by Lm2;
reconsider T = 1 as Symbol of SumTuring by Lm2;
A2: TRAN s = Sum_Tran . [(s `1 ),(s3 . (Head s))] by Def15
.= Sum_Tran . [0 ,(s3 . (Head s))] by A1, MCART_1:68
.= Sum_Tran . [0 ,(t . (Head s))] by A1, MCART_1:68
.= Sum_Tran . [0 ,(t . h)] by A1, MCART_1:68
.= [0 ,0 ,1] by A1, Th17, Th22 ;
A3: t . h = 0 by A1, Th22;
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 A2, MCART_1:68
.= t by A3, Th28 ;
reconsider p0 = 0 as State of SumTuring by Lm1;
reconsider h1 = h + 1 as Element of INT by INT_1:def 2;
A5: offset (TRAN s) = 1 by A2, MCART_1:68;
set s1 = [p0,h1,t];
A6: Following s = [((TRAN s) `1 ),((Head s) + (offset (TRAN s))),t] by A1, A4, Lm3
.= [0 ,((Head s) + (offset (TRAN s))),t] by A2, MCART_1:68
.= [p0,h1,t] by A1, A5, MCART_1:68 ;
reconsider s3 = [p0,h1,t] `3 as Tape of SumTuring ;
A7: ( t . h = 0 & t . ((h + n1) + 2) = 0 & t . (((h + n1) + n2) + 4) = 0 & ( for i being Integer st h < i & i < (h + n1) + 2 holds
t . i = 1 ) & ( for i being Integer st (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 holds
t . i = 1 ) ) by A1, Th22;
A8: h < h1 by XREAL_1:31;
h <= h + n1 by NAT_1:11;
then A9: h + 2 <= (h + n1) + 2 by XREAL_1:9;
A10: h1 < h + 2 by XREAL_1:10;
then A11: h1 < (h + n1) + 2 by A9, XXREAL_0:2;
A12: ((h + 1) + 1) + n1 = (h + n1) + 2 ;
set t1 = Tape-Chg t,h1,F;
h <= h + (n1 + n2) by NAT_1:11;
then A13: h + 4 <= ((h + n1) + n2) + 4 by XREAL_1:9;
A14: (Tape-Chg t,h1,F) . h1 = 0 by Th30;
A15: ( (Tape-Chg t,h1,F) . h = 0 & (Tape-Chg t,h1,F) . ((h + n1) + 2) = 0 & (Tape-Chg t,h1,F) . (((h + n1) + n2) + 4) = 0 & ( for i being Integer st h1 < i & i < ((h + 1) + 1) + n1 holds
(Tape-Chg t,h1,F) . i = 1 ) & ( for i being Integer st (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg t,h1,F) . i = 1 ) )
proof
thus (Tape-Chg t,h1,F) . h = 0 by A7, A8, Th30; :: thesis: ( (Tape-Chg t,h1,F) . ((h + n1) + 2) = 0 & (Tape-Chg t,h1,F) . (((h + n1) + n2) + 4) = 0 & ( for i being Integer st h1 < i & i < ((h + 1) + 1) + n1 holds
(Tape-Chg t,h1,F) . i = 1 ) & ( for i being Integer st (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg t,h1,F) . i = 1 ) )
thus (Tape-Chg t,h1,F) . ((h + n1) + 2) = 0 by A7, A9, A10, Th30; :: thesis: ( (Tape-Chg t,h1,F) . (((h + n1) + n2) + 4) = 0 & ( for i being Integer st h1 < i & i < ((h + 1) + 1) + n1 holds
(Tape-Chg t,h1,F) . i = 1 ) & ( for i being Integer st (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg t,h1,F) . i = 1 ) )
h1 < h + 4 by XREAL_1:10;
hence (Tape-Chg t,h1,F) . (((h + n1) + n2) + 4) = 0 by A7, A13, Th30; :: thesis: ( ( for i being Integer st h1 < i & i < ((h + 1) + 1) + n1 holds
(Tape-Chg t,h1,F) . i = 1 ) & ( for i being Integer st (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg t,h1,F) . i = 1 ) )
hereby :: thesis: for i being Integer st (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg t,h1,F) . i = 1
let i be Integer; :: thesis: ( h1 < i & i < ((h + 1) + 1) + n1 implies (Tape-Chg t,h1,F) . i = 1 )
assume A16: ( h1 < i & i < ((h + 1) + 1) + n1 ) ; :: thesis: (Tape-Chg t,h1,F) . i = 1
then A17: h < i by A8, XXREAL_0:2;
thus (Tape-Chg t,h1,F) . i = t . i by A16, Th30
.= 1 by A1, A12, A16, A17, Th22 ; :: thesis: verum
end;
hereby :: thesis: verum
let i be Integer; :: thesis: ( (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 implies (Tape-Chg t,h1,F) . i = 1 )
assume A18: ( (h + n1) + 2 < i & i < ((h + n1) + n2) + 4 ) ; :: thesis: (Tape-Chg t,h1,F) . i = 1
hence (Tape-Chg t,h1,F) . i = t . i by A11, Th30
.= 1 by A1, A18, Th22 ;
:: thesis: verum
end;
end;
A19: TRAN [p0,h1,t] = Sum_Tran . [([p0,h1,t] `1 ),(s3 . (Head [p0,h1,t]))] by Def15
.= Sum_Tran . [p0,(s3 . (Head [p0,h1,t]))] by MCART_1:68
.= Sum_Tran . [p0,(t . (Head [p0,h1,t]))] by MCART_1:68
.= Sum_Tran . [0 ,(t . h1)] by MCART_1:68
.= [1,0 ,1] by A1, A8, A11, Th17, Th22 ;
A20: Tape-Chg ([p0,h1,t] `3 ),(Head [p0,h1,t]),((TRAN [p0,h1,t]) `2 ) = Tape-Chg t,(Head [p0,h1,t]),((TRAN [p0,h1,t]) `2 ) by MCART_1:68
.= Tape-Chg t,h1,((TRAN [p0,h1,t]) `2 ) by MCART_1:68
.= Tape-Chg t,h1,F by A19, MCART_1:68 ;
A21: offset (TRAN [p0,h1,t]) = 1 by A19, MCART_1:68;
reconsider p1 = 1 as State of SumTuring by Lm1;
reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;
set s2 = [p1,i2,(Tape-Chg t,h1,F)];
A22: Following [p0,h1,t] = [((TRAN [p0,h1,t]) `1 ),((Head [p0,h1,t]) + (offset (TRAN [p0,h1,t]))),(Tape-Chg t,h1,F)] by A20, Lm3
.= [1,((Head [p0,h1,t]) + (offset (TRAN [p0,h1,t]))),(Tape-Chg t,h1,F)] by A19, MCART_1:68
.= [p1,i2,(Tape-Chg t,h1,F)] by A21, MCART_1:68 ;
A23: the Tran of SumTuring . [p1,1] = [p1,1,1] by Def15, Th17;
A24: p1 <> the AcceptS of SumTuring by Def15;
A25: for i being Integer st (h + 1) + 1 <= i & i < ((h + 1) + 1) + n1 holds
(Tape-Chg t,h1,F) . i = 1
proof
let i be Integer; :: thesis: ( (h + 1) + 1 <= i & i < ((h + 1) + 1) + n1 implies (Tape-Chg t,h1,F) . i = 1 )
assume A26: ( (h + 1) + 1 <= i & i < ((h + 1) + 1) + n1 ) ; :: thesis: (Tape-Chg t,h1,F) . i = 1
h1 < h1 + 1 by XREAL_1:31;
then h1 < i by A26, XXREAL_0:2;
hence (Tape-Chg t,h1,F) . i = 1 by A15, A26; :: thesis: verum
end;
reconsider nk = (h1 + 1) + n1 as Element of INT by INT_1:def 2;
set sn = [p1,nk,(Tape-Chg t,h1,F)];
reconsider sn3 = [p1,nk,(Tape-Chg t,h1,F)] `3 as Tape of SumTuring ;
A27: now
thus TRAN [p1,nk,(Tape-Chg t,h1,F)] = Sum_Tran . [([p1,nk,(Tape-Chg t,h1,F)] `1 ),(sn3 . (Head [p1,nk,(Tape-Chg t,h1,F)]))] by Def15
.= Sum_Tran . [p1,(sn3 . (Head [p1,nk,(Tape-Chg t,h1,F)]))] by MCART_1:68
.= Sum_Tran . [p1,((Tape-Chg t,h1,F) . (Head [p1,nk,(Tape-Chg t,h1,F)]))] by MCART_1:68
.= [2,1,1] by A15, Th17, MCART_1:68 ; :: thesis: verum
end;
set t2 = Tape-Chg (Tape-Chg t,h1,F),nk,T;
A28: h1 + 1 <= ((h + 1) + 1) + n1 by NAT_1:11;
A29: h1 < h1 + 1 by XREAL_1:31;
then A30: h1 < (h1 + 1) + n1 by A28, XXREAL_0:2;
A31: ( (Tape-Chg (Tape-Chg t,h1,F),nk,T) . h1 = 0 & (Tape-Chg (Tape-Chg t,h1,F),nk,T) . (((h + n1) + n2) + 4) = 0 & ( for i being Integer st h1 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1 ) )
proof
thus (Tape-Chg (Tape-Chg t,h1,F),nk,T) . h1 = 0 by A14, A28, A29, Th30; :: thesis: ( (Tape-Chg (Tape-Chg t,h1,F),nk,T) . (((h + n1) + n2) + 4) = 0 & ( for i being Integer st h1 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1 ) )
h + n1 <= (h + n1) + n2 by NAT_1:11;
then A32: ((h + 1) + 1) + n1 <= ((h + n1) + n2) + 2 by A12, XREAL_1:9;
((h + n1) + n2) + 2 < ((h + n1) + n2) + 4 by XREAL_1:10;
hence (Tape-Chg (Tape-Chg t,h1,F),nk,T) . (((h + n1) + n2) + 4) = 0 by A15, A32, Th30; :: thesis: for i being Integer st h1 < i & i < ((h + n1) + n2) + 4 holds
(Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1
hereby :: thesis: verum
let i be Integer; :: thesis: ( h1 < i & i < ((h + n1) + n2) + 4 implies (Tape-Chg (Tape-Chg t,h1,F),nk,T) . b1 = 1 )
assume A33: ( h1 < i & i < ((h + n1) + n2) + 4 ) ; :: thesis: (Tape-Chg (Tape-Chg t,h1,F),nk,T) . b1 = 1
per cases ( i < ((h + 1) + 1) + n1 or i = ((h + 1) + 1) + n1 or i > ((h + 1) + 1) + n1 ) by XXREAL_0:1;
suppose A34: i < ((h + 1) + 1) + n1 ; :: thesis: (Tape-Chg (Tape-Chg t,h1,F),nk,T) . b1 = 1
hence (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = (Tape-Chg t,h1,F) . i by Th30
.= 1 by A15, A33, A34 ;
:: thesis: verum
end;
suppose i = ((h + 1) + 1) + n1 ; :: thesis: (Tape-Chg (Tape-Chg t,h1,F),nk,T) . b1 = 1
hence (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1 by Th30; :: thesis: verum
end;
suppose A35: i > ((h + 1) + 1) + n1 ; :: thesis: (Tape-Chg (Tape-Chg t,h1,F),nk,T) . b1 = 1
hence (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = (Tape-Chg t,h1,F) . i by Th30
.= 1 by A15, A33, A35 ;
:: thesis: verum
end;
end;
end;
end;
A36: Tape-Chg ([p1,nk,(Tape-Chg t,h1,F)] `3 ),(Head [p1,nk,(Tape-Chg t,h1,F)]),((TRAN [p1,nk,(Tape-Chg t,h1,F)]) `2 ) = Tape-Chg (Tape-Chg t,h1,F),(Head [p1,nk,(Tape-Chg t,h1,F)]),((TRAN [p1,nk,(Tape-Chg t,h1,F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg t,h1,F),nk,((TRAN [p1,nk,(Tape-Chg t,h1,F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg t,h1,F),nk,T by A27, MCART_1:68 ;
A37: offset (TRAN [p1,nk,(Tape-Chg t,h1,F)]) = 1 by A27, MCART_1:68;
set i3 = (((h + 1) + 1) + n1) + 1;
reconsider n3 = (((h + 1) + 1) + n1) + 1 as Element of INT by INT_1:def 2;
reconsider p2 = 2 as State of SumTuring by Lm1;
set sm = [p2,n3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)];
A38: Following [p1,nk,(Tape-Chg t,h1,F)] = [((TRAN [p1,nk,(Tape-Chg t,h1,F)]) `1 ),((Head [p1,nk,(Tape-Chg t,h1,F)]) + (offset (TRAN [p1,nk,(Tape-Chg t,h1,F)]))),(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A36, Lm3
.= [2,((Head [p1,nk,(Tape-Chg t,h1,F)]) + (offset (TRAN [p1,nk,(Tape-Chg t,h1,F)]))),(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A27, MCART_1:68
.= [p2,n3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A37, MCART_1:68 ;
A39: the Tran of SumTuring . [p2,1] = [p2,1,1] by Def15, Th17;
A40: p2 <> the AcceptS of SumTuring by Def15;
for i being Integer st (((h + 1) + 1) + n1) + 1 <= i & i < ((((h + 1) + 1) + n1) + 1) + (n2 + 1) holds
(Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1
proof
let i be Integer; :: thesis: ( (((h + 1) + 1) + n1) + 1 <= i & i < ((((h + 1) + 1) + n1) + 1) + (n2 + 1) implies (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1 )
assume A41: ( (((h + 1) + 1) + n1) + 1 <= i & i < ((((h + 1) + 1) + n1) + 1) + (n2 + 1) ) ; :: thesis: (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1
nk < (((h + 1) + 1) + n1) + 1 by XREAL_1:31;
then h1 < (((h + 1) + 1) + n1) + 1 by A30, XXREAL_0:2;
then h1 < i by A41, XXREAL_0:2;
hence (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i = 1 by A31, A41; :: thesis: verum
end;
then A42: (Computation [p2,n3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) . (n2 + 1) = [2,(((h + n1) + n2) + 4),(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A39, A40, Lm4;
set i4 = ((h + n1) + n2) + 4;
reconsider n4 = ((h + n1) + n2) + 4 as Element of INT by INT_1:def 2;
set sp2 = [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)];
reconsider sn3 = [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] `3 as Tape of SumTuring ;
A43: TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] = Sum_Tran . [([p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] `1 ),(sn3 . (Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))] by Def15
.= Sum_Tran . [p2,(sn3 . (Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))] by MCART_1:68
.= Sum_Tran . [p2,((Tape-Chg (Tape-Chg t,h1,F),nk,T) . (Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))] by MCART_1:68
.= [3,0 ,(- 1)] by A31, Th17, MCART_1:68 ;
set j3 = (((h + n1) + n2) + 4) - 1;
A44: now
A45: Tape-Chg ([p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] `3 ),(Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]),((TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `2 ) = Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),(Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]),((TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),(((h + n1) + n2) + 4),((TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),(((h + n1) + n2) + 4),F by A43, MCART_1:68
.= Tape-Chg (Tape-Chg t,h1,F),nk,T by A31, Th28 ;
A46: offset (TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) = - 1 by A43, MCART_1:68;
A47: (((h + n1) + n2) + 4) + (- 1) = (((h + n1) + n2) + 4) - 1 ;
thus Following [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] = [((TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `1 ),((Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) + (offset (TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))),(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A45, Lm3
.= [3,((Head [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) + (offset (TRAN [p2,n4,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))),(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A43, MCART_1:68
.= [3,((((h + n1) + n2) + 4) - 1),(Tape-Chg (Tape-Chg t,h1,F),nk,T)] by A46, A47, MCART_1:68 ; :: thesis: verum
end;
reconsider p3 = 3 as State of SumTuring by Lm1;
reconsider m3 = (((h + n1) + n2) + 4) - 1 as Element of INT by INT_1:def 2;
set sp3 = [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)];
reconsider sn3 = [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] `3 as Tape of SumTuring ;
A48: h1 < h + 3 by XREAL_1:10;
A49: (h + 4) - 1 <= (((h + n1) + n2) + 4) - 1 by A13, XREAL_1:11;
then h1 < (((h + n1) + n2) + 4) - 1 by A48, XXREAL_0:2;
then A50: (Tape-Chg (Tape-Chg t,h1,F),nk,T) . ((((h + n1) + n2) + 4) - 1) = 1 by A31, XREAL_1:148;
A51: now
thus TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] = Sum_Tran . [([p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] `1 ),(sn3 . (Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))] by Def15
.= Sum_Tran . [p3,(sn3 . (Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))] by MCART_1:68
.= Sum_Tran . [p3,((Tape-Chg (Tape-Chg t,h1,F),nk,T) . (Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))] by MCART_1:68
.= [4,0 ,(- 1)] by A50, Th17, MCART_1:68 ; :: thesis: verum
end;
set t3 = Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F;
A52: ( (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . h1 = 0 & (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . ((((h + n1) + n2) + 4) - 1) = 0 & ( for i being Integer st h1 < i & i < (((h + n1) + n2) + 4) - 1 holds
(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . i = 1 ) )
proof
thus (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . h1 = 0 by A31, A48, A49, Th30; :: thesis: ( (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . ((((h + n1) + n2) + 4) - 1) = 0 & ( for i being Integer st h1 < i & i < (((h + n1) + n2) + 4) - 1 holds
(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . i = 1 ) )
thus (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . ((((h + n1) + n2) + 4) - 1) = 0 by Th30; :: thesis: for i being Integer st h1 < i & i < (((h + n1) + n2) + 4) - 1 holds
(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . i = 1
hereby :: thesis: verum
let i be Integer; :: thesis: ( h1 < i & i < (((h + n1) + n2) + 4) - 1 implies (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . i = 1 )
assume A53: ( h1 < i & i < (((h + n1) + n2) + 4) - 1 ) ; :: thesis: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . i = 1
then A54: i < ((h + n1) + n2) + 4 by XREAL_1:148, XXREAL_0:2;
thus (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . i = (Tape-Chg (Tape-Chg t,h1,F),nk,T) . i by A53, Th30
.= 1 by A31, A53, A54 ; :: thesis: verum
end;
end;
A55: Tape-Chg ([p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] `3 ),(Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]),((TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `2 ) = Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),(Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]),((TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),((TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F by A51, MCART_1:68 ;
A56: offset (TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) = - 1 by A51, MCART_1:68;
set j2 = ((((h + n1) + n2) + 4) - 1) - 1;
A57: ((((h + n1) + n2) + 4) - 1) + (- 1) = ((((h + n1) + n2) + 4) - 1) - 1 ;
reconsider p4 = 4 as State of SumTuring by Lm1;
reconsider m2 = ((((h + n1) + n2) + 4) - 1) - 1 as Element of INT by INT_1:def 2;
set sp4 = [p4,m2,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)];
A58: now
thus Following [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)] = [((TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) `1 ),((Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) + (offset (TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A55, Lm3
.= [4,((Head [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]) + (offset (TRAN [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A51, MCART_1:68
.= [p4,m2,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A56, A57, MCART_1:68 ; :: thesis: verum
end;
defpred S1[ Element of NAT ] means ( h + $1 < ((((h + n1) + n2) + 4) - 1) - 1 implies (Computation [p4,m2,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) . $1 = [4,((((((h + n1) + n2) + 4) - 1) - 1) - $1),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] );
A59: S1[ 0 ] by Def8;
A60: 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 A61: S1[k] ; :: thesis: S1[k + 1]
now
assume A62: h + (k + 1) < ((((h + n1) + n2) + 4) - 1) - 1 ; :: thesis: (Computation [p4,m2,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) . (k + 1) = [4,((((((h + n1) + n2) + 4) - 1) - 1) - (k + 1)),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]
A63: h + k < (h + k) + 1 by XREAL_1:31;
set k3 = (((((h + n1) + n2) + 4) - 1) - 1) - k;
reconsider ik = (((((h + n1) + n2) + 4) - 1) - 1) - k as Element of INT by INT_1:def 2;
set sk = [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)];
reconsider tt = [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] `3 as Tape of SumTuring ;
h1 + k < (((((h + n1) + n2) + 4) - 1) - 1) + 0 by A62;
then A64: h1 - 0 < (((((h + n1) + n2) + 4) - 1) - 1) - k by XREAL_1:23;
h1 >= 0 by NAT_1:2;
then reconsider ii = (((((h + n1) + n2) + 4) - 1) - 1) - k as Element of NAT by A64, INT_1:16, XXREAL_0:2;
((((h + n1) + n2) + 4) - 1) - 1 <= (((((h + n1) + n2) + 4) - 1) - 1) + k by INT_1:19;
then (((((h + n1) + n2) + 4) - 1) - 1) - k <= ((((h + n1) + n2) + 4) - 1) - 1 by XREAL_1:22;
then (((((h + n1) + n2) + 4) - 1) - 1) - k < (((h + n1) + n2) + 4) - 1 by XREAL_1:148, XXREAL_0:2;
then A65: (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . ii = 1 by A52, A64;
A66: now
thus TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] = Sum_Tran . [([p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] `1 ),(tt . (Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))] by Def15
.= Sum_Tran . [p4,(tt . (Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))] by MCART_1:68
.= Sum_Tran . [p4,((Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . (Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))] by MCART_1:68
.= [4,1,(- 1)] by A65, Th17, MCART_1:68 ; :: thesis: verum
end;
A67: now
thus Tape-Chg ([p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] `3 ),(Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]),((TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `2 ) = Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F),(Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]),((TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F),((((((h + n1) + n2) + 4) - 1) - 1) - k),((TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F),((((((h + n1) + n2) + 4) - 1) - 1) - k),T by A66, MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F by A65, Th28 ; :: thesis: verum
end;
A68: offset (TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) = - 1 by A66, MCART_1:68;
thus (Computation [p4,m2,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) . (k + 1) = Following [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A61, A62, A63, Def8, XXREAL_0:2
.= [((TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `1 ),((Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) + (offset (TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A67, Lm3
.= [4,((Head [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) + (offset (TRAN [p4,ik,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A66, MCART_1:68
.= [4,(((((((h + n1) + n2) + 4) - 1) - 1) - k) + (- 1)),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A68, MCART_1:68
.= [4,((((((h + n1) + n2) + 4) - 1) - 1) - (k + 1)),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
set j1 = (n1 + n2) + 1;
A69: (((((h + n1) + n2) + 4) - 1) - 1) - 1 = h + ((n1 + n2) + 1) ;
set sp5 = [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)];
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A59, A60);
 then A70: (Computation [p4,m2,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) . ((n1 + n2) + 1) = [4,((((((h + n1) + n2) + 4) - 1) - 1) - ((n1 + n2) + 1)),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A69, XREAL_1:148
.= [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] ;
A71: now
reconsider tt = [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] `3 as Tape of SumTuring ;
A72: TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] = Sum_Tran . [([p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] `1 ),(tt . (Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))] by Def15
.= Sum_Tran . [4,(tt . (Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))] by MCART_1:68
.= Sum_Tran . [4,((Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F) . (Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))] by MCART_1:68
.= [5,0 ,0 ] by A52, Th17, MCART_1:68 ;
A73: Tape-Chg ([p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] `3 ),(Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]),((TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `2 ) = Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F),(Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]),((TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F),h1,((TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `2 ) by MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F),h1,F by A72, MCART_1:68
.= Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F by A52, Th28 ;
A74: offset (TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) = 0 by A72, MCART_1:68;
thus Following [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] = [((TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) `1 ),((Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) + (offset (TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A73, Lm3
.= [5,((Head [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]) + (offset (TRAN [p4,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)]))),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A72, MCART_1:68
.= [5,(h1 + 0 ),(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A74, MCART_1:68 ; :: thesis: verum
end;
set Rs = (Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1));
(Computation s) . (1 + 1) = Following ((Computation s) . 1) by Def8
.= [p1,i2,(Tape-Chg t,h1,F)] by A6, A22, Th12 ;
then (Computation s) . (((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) = (Computation [p1,i2,(Tape-Chg t,h1,F)]) . ((((n1 + 1) + (n2 + 1)) + 1) + 1) by Th13;
then A75: (Computation s) . (((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) = Following ((Computation [p1,i2,(Tape-Chg t,h1,F)]) . (((n1 + 1) + (n2 + 1)) + 1)) by Def8
.= Following (Following ((Computation [p1,i2,(Tape-Chg t,h1,F)]) . ((n1 + 1) + (n2 + 1)))) by Def8
.= Following (Following ((Computation ((Computation [p1,i2,(Tape-Chg t,h1,F)]) . (n1 + 1))) . (n2 + 1))) by Th13 ;
now
(Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1)) = (Computation (Following (Following ((Computation ((Computation [p1,i2,(Tape-Chg t,h1,F)]) . (n1 + 1))) . (n2 + 1))))) . (((n1 + n2) + 1) + 1) by A75, Th13
.= (Computation (Following (Following ((Computation (Following ((Computation [p1,i2,(Tape-Chg t,h1,F)]) . n1))) . (n2 + 1))))) . (((n1 + n2) + 1) + 1) by Def8 ;
hence (Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1)) = (Computation (Following [p3,m3,(Tape-Chg (Tape-Chg t,h1,F),nk,T)])) . (((n1 + n2) + 1) + 1) by A23, A24, A25, A38, A42, A44, Lm4; :: thesis: verum
end;
then A76: (Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1)) = [5,h1,(Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F)] by A58, A70, A71, Def8;
then A77: ((Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1))) `1 = 5 by MCART_1:68
.= the AcceptS of SumTuring by Def15 ;
hence s is Accept-Halt by Def9; :: thesis: ( (Result s) `2 = 1 + h & (Result s) `3 storeData <*(1 + h),(n1 + n2)*> )
then A78: Result s = (Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1)) by A77, Def10;
hence (Result s) `2 = 1 + h by A76, MCART_1:68; :: thesis: (Result s) `3 storeData <*(1 + h),(n1 + n2)*>
A79: (Result s) `3 = Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F by A76, A78, MCART_1:68;
Tape-Chg (Tape-Chg (Tape-Chg t,h1,F),nk,T),((((h + n1) + n2) + 4) - 1),F is_1_between h1,(h1 + (n1 + n2)) + 2 by A52, Def13;
hence (Result s) `3 storeData <*(1 + h),(n1 + n2)*> by A79, Th19; :: thesis: verum