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