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_3 = 1 + head & (Result s) `3_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_3 = 1 + head & (Result s) `3_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_3 = 1 + h & (Result s) `3_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_3 = 1 + h & (Result s) `3_3 storeData <*(1 + h),(n1 + n2)*> )
A3: t . ((h + n1) + 2) = 0 by A2, Th19;
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;
set s1 = [p0,h1,t];
A8: t . h = 0 by A2, Th19;
h <= h + n1 by NAT_1:11;
then A9: h + 2 <= (h + n1) + 2 by XREAL_1:7;
A10: t . (((h + n1) + n2) + 4) = 0 by A2, Th19;
h <= h + (n1 + n2) by NAT_1:11;
then A11: h + 4 <= ((h + n1) + n2) + 4 by XREAL_1:7;
then A12: ( h1 < h + 3 & (h + 4) - 1 <= (((h + n1) + n2) + 4) - 1 ) by XREAL_1:8, XREAL_1:9;
A13: h1 < h + 2 by XREAL_1:8;
then A14: h1 < (h + n1) + 2 by A9, XXREAL_0:2;
A15: t . h = 0 by A2, Th19;
A16: ( (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 A15, A4, Th26; :: 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, A9, A13, Th26; :: 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 A10, A11, Th26; :: 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
A17: h1 < i and
A18: i < ((h + 1) + 1) + n1 ; :: thesis: (Tape-Chg (t,h1,F)) . i = 1
A19: h < i by A4, A17, XXREAL_0:2;
thus (Tape-Chg (t,h1,F)) . i = t . i by A17, Th26
.= 1 by A2, A5, A18, A19, Th19 ; :: 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
A20: (h + n1) + 2 < i and
A21: i < ((h + n1) + n2) + 4 ; :: thesis: (Tape-Chg (t,h1,F)) . i = 1
thus (Tape-Chg (t,h1,F)) . i = t . i by A14, A20, Th26
.= 1 by A2, A20, A21, Th19 ; :: thesis: verum
end;
end;
A22: 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
A23: (h + 1) + 1 <= i and
A24: i < ((h + 1) + 1) + n1 ; :: thesis: (Tape-Chg (t,h1,F)) . i = 1
h1 < h1 + 1 by XREAL_1:29;
then h1 < i by A23, XXREAL_0:2;
hence (Tape-Chg (t,h1,F)) . i = 1 by A16, A24; :: thesis: verum
end;
set t3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F);
A25: (Tape-Chg (t,h1,F)) . h1 = 0 by Th26;
A26: ( (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 A25, A7, Th26; :: 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 A27: ((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 A16, A27, Th26; :: 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
A28: h1 < i and
A29: 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 A30: 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 Th26
.= 1 by A16, A28, A30 ;
:: 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 Th26; :: thesis: verum
end;
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 Th26
.= 1 by A16, A29, A31 ;
:: thesis: verum
end;
end;
end;
end;
A32: ( (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 A26, A12, Th26; :: 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 Th26; :: 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
A33: h1 < i and
A34: 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
A35: i < ((h + n1) + n2) + 4 by A34, 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 A34, Th26
.= 1 by A26, A33, A35 ; :: thesis: verum
end;
end;
then A36: 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 ;
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_3 as Tape of SumTuring ;
A37: TRAN [p1,nk,(Tape-Chg (t,h1,F))] = Sum_Tran . [([p1,nk,(Tape-Chg (t,h1,F))] `1_3),(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,F))]))] by Def14
.= Sum_Tran . [p1,(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,F))]))]
.= Sum_Tran . [p1,((Tape-Chg (t,h1,F)) . (Head [p1,nk,(Tape-Chg (t,h1,F))]))]
.= [2,1,1] by A16, Th14 ;
then A38: offset (TRAN [p1,nk,(Tape-Chg (t,h1,F))]) = 1 ;
reconsider sn3 = [p2,n4,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))] `3_3 as Tape of SumTuring ;
A39: 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_3),(sn3 . (Head [p2,n4,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]))] by Def14
.= Sum_Tran . [p2,(sn3 . (Head [p2,n4,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]))]
.= Sum_Tran . [p2,((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)) . (Head [p2,n4,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]))]
.= [3,0,(- 1)] by A26, Th14 ;
then A40: offset (TRAN [p2,n4,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]) = - 1 ;
Tape-Chg (([p2,n4,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))] `3_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_3)) = 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_3))
.= 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_3))
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),(((h + n1) + n2) + 4),F) by A39
.= Tape-Chg ((Tape-Chg (t,h1,F)),nk,T) by A26, Th24 ;
then A41: 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_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 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 A39
.= [3,((((h + n1) + n2) + 4) - 1),(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))] by A40 ;
Tape-Chg (([p1,nk,(Tape-Chg (t,h1,F))] `3_3),(Head [p1,nk,(Tape-Chg (t,h1,F))]),((TRAN [p1,nk,(Tape-Chg (t,h1,F))]) `2_3)) = Tape-Chg ((Tape-Chg (t,h1,F)),(Head [p1,nk,(Tape-Chg (t,h1,F))]),((TRAN [p1,nk,(Tape-Chg (t,h1,F))]) `2_3))
.= Tape-Chg ((Tape-Chg (t,h1,F)),nk,((TRAN [p1,nk,(Tape-Chg (t,h1,F))]) `2_3))
.= Tape-Chg ((Tape-Chg (t,h1,F)),nk,T) by A37 ;
then A42: Following [p1,nk,(Tape-Chg (t,h1,F))] = [((TRAN [p1,nk,(Tape-Chg (t,h1,F))]) `1_3),((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 A37
.= [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))] by A38 ;
reconsider s3 = s `3_3 as Tape of SumTuring ;
A43: TRAN s = Sum_Tran . [(s `1_3),(s3 . (Head s))] by Def14
.= Sum_Tran . [0,(s3 . (Head s))] by A1
.= Sum_Tran . [0,(t . (Head s))] by A1
.= Sum_Tran . [0,(t . h)] by A1
.= [0,0,1] by A2, Th14, Th19 ;
then A44: offset (TRAN s) = 1 ;
A45: h1 < (h1 + 1) + n1 by A7, XXREAL_0:2;
A46: 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
A47: (((h + 1) + 1) + n1) + 1 <= i and
A48: 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 A45, XXREAL_0:2;
then h1 < i by A47, XXREAL_0:2;
hence (Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)) . i = 1 by A26, A48; :: 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[ 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 Def14, Th14;
then A49: (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 A46, Lm4;
h1 < (((h + n1) + n2) + 4) - 1 by A12, XXREAL_0:2;
then A50: (Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)) . ((((h + n1) + n2) + 4) - 1) = 1 by A26, XREAL_1:146;
reconsider sn3 = [p3,m3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))] `3_3 as Tape of SumTuring ;
A51: 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_3),(sn3 . (Head [p3,m3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]))] by Def14
.= Sum_Tran . [p3,(sn3 . (Head [p3,m3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]))]
.= Sum_Tran . [p3,((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)) . (Head [p3,m3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]))]
.= [4,0,(- 1)] by A50, Th14 ;
then A52: offset (TRAN [p3,m3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))]) = - 1 ;
A53: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A54: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( h + (k + 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))]) . (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))] )
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_3 as Tape of SumTuring ;
assume A55: 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 A56: h1 - 0 < (((((h + n1) + n2) + 4) - 1) - 1) - k by XREAL_1:21;
reconsider ii = (((((h + n1) + n2) + 4) - 1) - 1) - k as Element of NAT by A56, INT_1:3;
((((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 A57: (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F)) . ii = 1 by A32, A56;
A58: 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_3),(tt . (Head [p4,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]))] by Def14
.= Sum_Tran . [p4,(tt . (Head [p4,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]))]
.= 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))]))]
.= [4,1,(- 1)] by A57, Th14 ;
then A59: offset (TRAN [p4,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]) = - 1 ;
A60: Tape-Chg (([p4,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))] `3_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_3)) = 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_3))
.= 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_3))
.= 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 A58
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F) by A57, Th24 ;
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 A54, A55, Def7, XXREAL_0:2
.= [((TRAN [p4,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]) `1_3),((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, 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 A58
.= [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 A59
.= [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;
A61: S1[ 0 ] by Def7;
for k being Nat holds S1[k] from NAT_1:sch 2(A61, A53);
 then A62: (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_3 as Tape of SumTuring ;
A63: TRAN [p0,h1,t] = Sum_Tran . [([p0,h1,t] `1_3),(s3 . (Head [p0,h1,t]))] by Def14
.= Sum_Tran . [p0,(s3 . (Head [p0,h1,t]))]
.= Sum_Tran . [p0,(t . (Head [p0,h1,t]))]
.= Sum_Tran . [0,(t . h1)]
.= [1,0,1] by A2, A4, A14, Th14, Th19 ;
then A64: offset (TRAN [p0,h1,t]) = 1 ;
Tape-Chg (([p3,m3,(Tape-Chg ((Tape-Chg (t,h1,F)),nk,T))] `3_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_3)) = 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_3))
.= 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_3))
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F) by A51 ;
then A65: 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_3),((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 A51
.= [p4,m2,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))] by A52 ;
A66: now :: thesis: Following [p4,h1,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))] = [5,(h1 + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]
reconsider tt = [p4,h1,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))] `3_3 as Tape of SumTuring ;
A67: 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_3),(tt . (Head [p4,h1,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]))] by Def14
.= Sum_Tran . [4,(tt . (Head [p4,h1,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]))]
.= 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))]))]
.= [5,0,0] by A32, Th14 ;
then A68: offset (TRAN [p4,h1,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))]) = 0 ;
Tape-Chg (([p4,h1,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))] `3_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_3)) = 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_3))
.= 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_3))
.= Tape-Chg ((Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F)),h1,F) by A67
.= Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F) by A32, Th24 ;
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_3),((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 A67
.= [5,(h1 + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F))] by A68 ;
:: thesis: verum
end;
Tape-Chg (([p0,h1,t] `3_3),(Head [p0,h1,t]),((TRAN [p0,h1,t]) `2_3)) = Tape-Chg (t,(Head [p0,h1,t]),((TRAN [p0,h1,t]) `2_3))
.= Tape-Chg (t,h1,((TRAN [p0,h1,t]) `2_3))
.= Tape-Chg (t,h1,F) by A63 ;
then A69: Following [p0,h1,t] = [((TRAN [p0,h1,t]) `1_3),((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 A63
.= [p1,i2,(Tape-Chg (t,h1,F))] by A64 ;
Tape-Chg ((s `3_3),(Head s),((TRAN s) `2_3)) = Tape-Chg (t,(Head s),((TRAN s) `2_3)) by A1
.= Tape-Chg (t,h,((TRAN s) `2_3)) by A1
.= Tape-Chg (t,h,F) by A43
.= t by A8, Th24 ;
then A70: Following s = [((TRAN s) `1_3),((Head s) + (offset (TRAN s))),t] by A1, Lm3
.= [0,((Head s) + (offset (TRAN s))),t] by A43
.= [p0,h1,t] by A1, A44 ;
(Computation s) . (1 + 1) = Following ((Computation s) . 1) by Def7
.= [p1,i2,(Tape-Chg (t,h1,F))] by A70, A69, Th9 ;
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 Th10;
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 Def7
.= Following (Following ((Computation [p1,i2,(Tape-Chg (t,h1,F))]) . ((n1 + 1) + (n2 + 1)))) by Def7
.= Following (Following ((Computation ((Computation [p1,i2,(Tape-Chg (t,h1,F))]) . (n1 + 1))) . (n2 + 1))) by Th10 ;
then A71: (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 Th10
.= (Computation (Following (Following ((Computation (Following ((Computation [p1,i2,(Tape-Chg (t,h1,F))]) . n1))) . (n2 + 1))))) . (((n1 + n2) + 1) + 1) by Def7 ;
( the Tran of SumTuring . [p1,1] = [p1,1,1] & p1 <> the AcceptS of SumTuring ) by Def14, Th14;
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 A22, A42, A49, A41, A71, Lm4;
then A72: (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 A65, A62, A66, Def7;
then A73: ((Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1))) `1_3 = 5
.= the AcceptS of SumTuring by Def14 ;
hence s is Accept-Halt ; :: thesis: ( (Result s) `2_3 = 1 + h & (Result s) `3_3 storeData <*(1 + h),(n1 + n2)*> )
then A74: Result s = (Computation s) . ((((((n1 + 1) + (n2 + 1)) + 1) + 1) + (1 + 1)) + (((n1 + n2) + 1) + 1)) by A73, Def9;
hence (Result s) `2_3 = 1 + h by A72; :: thesis: (Result s) `3_3 storeData <*(1 + h),(n1 + n2)*>
(Result s) `3_3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,F)),nk,T)),((((h + n1) + n2) + 4) - 1),F) by A72, A74;
hence (Result s) `3_3 storeData <*(1 + h),(n1 + n2)*> by A36, Th16; :: thesis: verum