reconsider F = 0 as Symbol of SuccTuring by Lm6;
let s be All-State of SuccTuring; 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_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )
let t be 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_3 = head & (Result s) `3_3 storeData <*head,(n + 1)*> )
let h, n be Element of NAT ; ( s = [0,h,t] & t storeData <*h,n*> implies ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> ) )
assume that
A1:
s = [0,h,t]
and
A2:
t storeData <*h,n*>
; ( s is Accept-Halt & (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> )
A3:
t . h = 0
by A2, Th17;
set i3 = (((h + 1) + 1) + n) + 1;
reconsider h1 = h + 1 as Element of INT by INT_1:def 2;
reconsider p1 = 1 as State of SuccTuring by Lm5;
A4:
(h1 + 1) + n < (((h + 1) + 1) + n) + 1
by XREAL_1:29;
h <= h + n
by NAT_1:11;
then A5:
h + 2 <= (h + n) + 2
by XREAL_1:7;
A6:
h1 < h + 2
by XREAL_1:8;
then A7:
h1 < (h + n) + 2
by A5, XXREAL_0:2;
reconsider p2 = 2 as State of SuccTuring by Lm5;
reconsider i2 = h1 + 1 as Element of INT by INT_1:def 2;
reconsider nk = (h1 + 1) + n as Element of INT by INT_1:def 2;
reconsider hh = h as Element of INT by INT_1:def 2;
reconsider n3 = (((h + 1) + 1) + n) + 1 as Element of INT by INT_1:def 2;
reconsider T = 1 as Symbol of SuccTuring by Lm6;
set t1 = Tape-Chg (t,h1,T);
A8:
h < h1
by XREAL_1:29;
A9:
t . ((h + n) + 2) = 0
by A2, Th17;
A10:
( (Tape-Chg (t,h1,T)) . h = 0 & (Tape-Chg (t,h1,T)) . ((h + n) + 2) = 0 & ( for i being Integer st h < i & i < (h + n) + 2 holds
(Tape-Chg (t,h1,T)) . i = 1 ) )
proof
thus
(Tape-Chg (t,h1,T)) . h = 0
by A3, A8, Th26;
( (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 A9, A5, A6, Th26;
for i being Integer st h < i & i < (h + n) + 2 holds
(Tape-Chg (t,h1,T)) . i = 1
end;
A12:
for i being Integer st (h + 1) + 1 <= i & i < ((h + 1) + 1) + n holds
(Tape-Chg (t,h1,T)) . i = 1
reconsider s3 = s `3_3 as Tape of SuccTuring ;
A15: TRAN s =
Succ_Tran . [(s `1_3),(s3 . (Head s))]
by Def17
.=
Succ_Tran . [0,(s3 . (Head s))]
by A1
.=
Succ_Tran . [0,(t . (Head s))]
by A1
.=
[1,0,1]
by A1, A3, Th30
;
then A16:
offset (TRAN s) = 1
;
set s1 = [p1,h1,t];
reconsider s3 = [p1,h1,t] `3_3 as Tape of SuccTuring ;
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 A15
.=
t
by A3, Th24
;
then A17: Following s =
[((TRAN s) `1_3),((Head s) + (offset (TRAN s))),t]
by A1, Lm7
.=
[1,((Head s) + (offset (TRAN s))),t]
by A15
.=
[p1,h1,t]
by A1, A16
;
A18: TRAN [p1,h1,t] =
Succ_Tran . [([p1,h1,t] `1_3),(s3 . (Head [p1,h1,t]))]
by Def17
.=
Succ_Tran . [p1,(s3 . (Head [p1,h1,t]))]
.=
Succ_Tran . [p1,(t . (Head [p1,h1,t]))]
.=
Succ_Tran . [1,(t . h1)]
.=
[1,1,1]
by A2, A8, A7, Th17, Th30
;
then A19:
offset (TRAN [p1,h1,t]) = 1
;
reconsider p1 = 1 as State of SuccTuring by Lm5;
set s2 = [p1,i2,(Tape-Chg (t,h1,T))];
Tape-Chg (([p1,h1,t] `3_3),(Head [p1,h1,t]),((TRAN [p1,h1,t]) `2_3)) =
Tape-Chg (t,(Head [p1,h1,t]),((TRAN [p1,h1,t]) `2_3))
.=
Tape-Chg (t,h1,((TRAN [p1,h1,t]) `2_3))
.=
Tape-Chg (t,h1,T)
by A18
;
then A20: Following [p1,h1,t] =
[((TRAN [p1,h1,t]) `1_3),((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg (t,h1,T))]
by Lm7
.=
[1,((Head [p1,h1,t]) + (offset (TRAN [p1,h1,t]))),(Tape-Chg (t,h1,T))]
by A18
.=
[p1,i2,(Tape-Chg (t,h1,T))]
by A19
;
reconsider p3 = 3 as State of SuccTuring by Lm5;
set sn = [p1,nk,(Tape-Chg (t,h1,T))];
set t2 = Tape-Chg ((Tape-Chg (t,h1,T)),nk,T);
set t3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F);
( the Tran of SuccTuring . [p1,1] = [p1,1,1] & p1 <> the AcceptS of SuccTuring )
by Def17, Th30;
then A21:
(Computation [p1,i2,(Tape-Chg (t,h1,T))]) . n = [p1,(((h + 1) + 1) + n),(Tape-Chg (t,h1,T))]
by A12, Lm4;
( h1 + 1 <= ((h + 1) + 1) + n & h1 < h1 + 1 )
by NAT_1:11, XREAL_1:29;
then A22:
h1 < (h1 + 1) + n
by XXREAL_0:2;
A23:
( (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 A8, A10, A22, Th26;
for i being Integer st h < i & i <= (h + n) + 2 holds
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i = 1
hereby verum
let i be
Integer;
( h < i & i <= (h + n) + 2 implies (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1 )assume that A24:
h < i
and A25:
i <= (h + n) + 2
;
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1per cases
( i <> (h + n) + 2 or i = (h + n) + 2 )
;
suppose A26:
i <> (h + n) + 2
;
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . b1 = 1then A27:
i < (h + n) + 2
by A25, XXREAL_0:1;
thus (Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . i =
(Tape-Chg (t,h1,T)) . i
by A26, Th26
.=
1
by A10, A24, A27
;
verum end; end;
end;
end;
set sp3 = [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];
set sm = [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))];
reconsider sm3 = [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `3_3 as Tape of SuccTuring ;
A28:
the Symbols of SuccTuring = {0,1}
by Def17;
A29:
now Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)]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 A28, TARSKI:def 2;
suppose
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3 = 1
;
Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)]end; suppose
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3 = 0
;
Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . n3)] = [p3,0,(- 1)]end; end; end;
A30: 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_3),(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]
by Def17
.=
Succ_Tran . [2,(sm3 . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]
.=
Succ_Tran . [2,((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)) . (Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))]
.=
[p3,0,(- 1)]
by A29
;
then A31:
offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) = - 1
;
set j1 = (1 + 1) + n;
set sp5 = [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))];
defpred S1[ Nat] means ( h + $1 <= nk implies (Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . $1 = [3,(nk - $1),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] );
reconsider sn3 = [p1,nk,(Tape-Chg (t,h1,T))] `3_3 as Tape of SuccTuring ;
A32:
h + ((1 + 1) + n) = nk
;
set Rs = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)));
A33: TRAN [p1,nk,(Tape-Chg (t,h1,T))] =
Succ_Tran . [([p1,nk,(Tape-Chg (t,h1,T))] `1_3),(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]
by Def17
.=
Succ_Tran . [p1,(sn3 . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]
.=
Succ_Tran . [p1,((Tape-Chg (t,h1,T)) . (Head [p1,nk,(Tape-Chg (t,h1,T))]))]
.=
[2,1,1]
by A10, Th30
;
then A34:
offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]) = 1
;
A35:
h < (h1 + 1) + n
by A8, A22, XXREAL_0:2;
A36:
( (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 A35, A23, A4, Th26;
( (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 Th26;
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 verum
let i be
Integer;
( h < i & i < (h + (n + 1)) + 2 implies (Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = 1 )assume that A37:
h < i
and A38:
i < (h + (n + 1)) + 2
;
(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . i = 1
i + 1
<= (h + (n + 1)) + 2
by A38, INT_1:7;
then A39:
i <= ((h + (n + 1)) + 2) - 1
by XREAL_1:19;
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 A38, Th26
.=
1
by A23, A37, A39
;
verum
end;
end;
then A40:
Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F) is_1_between h,(h + (n + 1)) + 2
;
Tape-Chg (([p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))] `3_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_3)) =
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_3))
.=
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_3))
.=
Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)
by A30
;
then A41: 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_3),((Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) + (offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by Lm7
.=
[p3,((Head [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]) + (offset (TRAN [p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by A30
.=
[p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by A31
;
Tape-Chg (([p1,nk,(Tape-Chg (t,h1,T))] `3_3),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3)) =
Tape-Chg ((Tape-Chg (t,h1,T)),(Head [p1,nk,(Tape-Chg (t,h1,T))]),((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3))
.=
Tape-Chg ((Tape-Chg (t,h1,T)),nk,((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `2_3))
.=
Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)
by A33
;
then A42: Following [p1,nk,(Tape-Chg (t,h1,T))] =
[((TRAN [p1,nk,(Tape-Chg (t,h1,T))]) `1_3),((Head [p1,nk,(Tape-Chg (t,h1,T))]) + (offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]))),(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]
by Lm7
.=
[2,((Head [p1,nk,(Tape-Chg (t,h1,T))]) + (offset (TRAN [p1,nk,(Tape-Chg (t,h1,T))]))),(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]
by A33
.=
[p2,n3,(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T))]
by A34
;
A43:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A44:
S1[
k]
;
S1[k + 1]
now ( h + (k + 1) <= nk implies (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))] )reconsider ik =
nk - k as
Element of
INT by INT_1:def 2;
set k3 =
nk - k;
A45:
h + k < (h + k) + 1
by XREAL_1:29;
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_3 as
Tape of
SuccTuring ;
nk <= nk + k
by INT_1:6;
then A46:
nk - k <= nk
by XREAL_1:20;
assume A47:
h + (k + 1) <= nk
;
(Computation [p3,nk,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) . (k + 1) = [3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]then
h + k < nk + 0
by A45, XXREAL_0:2;
then A48:
h - 0 < nk - k
by XREAL_1:21;
reconsider ii =
nk - k as
Element of
NAT by A48, INT_1:3;
(h + n) + 2
< ((h + n) + 2) + 1
by XREAL_1:29;
then
ii < (h + (n + 1)) + 2
by A46, XXREAL_0:2;
then A49:
(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)) . ii = 1
by A36, A48;
A50:
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_3),(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]
by Def17
.=
Succ_Tran . [p3,(tt . (Head [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]
.=
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))]))]
.=
[3,1,(- 1)]
by A49, Th30
;
then A51:
offset (TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = - 1
;
A52:
Tape-Chg (
([p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_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_3)) =
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_3))
.=
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_3))
.=
Tape-Chg (
(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),
(nk - k),
T)
by A50
.=
Tape-Chg (
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),
n3,
F)
by A49, Th24
;
hereby 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 A44, A47, A45, Def7, XXREAL_0:2
.=
[((TRAN [p3,ik,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1_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 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 A50
.=
[3,((nk - k) + (- 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by A51
.=
[3,(nk - (k + 1)),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
;
verum
end; end;
hence
S1[
k + 1]
;
verum
end;
A53:
S1[ 0 ]
by Def7;
for k being Nat holds S1[k]
from NAT_1:sch 2(A53, A43);
then A54: (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 A32
.=
[p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
;
A55:
now Following [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] = [4,(h + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]reconsider tt =
[p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_3 as
Tape of
SuccTuring ;
A56:
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_3),(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]
by Def17
.=
Succ_Tran . [3,(tt . (Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))]
.=
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))]))]
.=
[4,0,0]
by A36, Th30
;
then A57:
offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) = 0
;
Tape-Chg (
([p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] `3_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_3)) =
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_3))
.=
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_3))
.=
Tape-Chg (
(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)),
h,
F)
by A56
.=
Tape-Chg (
(Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),
n3,
F)
by A36, Th24
;
hence Following [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))] =
[((TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) `1_3),((Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by Lm7
.=
[4,((Head [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]) + (offset (TRAN [p3,hh,(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]))),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by A56
.=
[4,(h + 0),(Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F))]
by A57
;
verum end;
(Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1))) =
(Computation ((Computation s) . (1 + 1))) . (((n + 1) + 1) + (((1 + 1) + n) + 1))
by Th10
.=
(Computation (Following ((Computation s) . 1))) . (((n + 1) + 1) + (((1 + 1) + n) + 1))
by Def7
.=
(Computation (Following [p1,h1,t])) . (((n + 1) + 1) + (((1 + 1) + n) + 1))
by A17, Th9
.=
(Computation ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . ((n + 1) + 1))) . (((1 + 1) + n) + 1)
by A20, Th10
.=
(Computation (Following ((Computation [p1,i2,(Tape-Chg (t,h1,T))]) . (n + 1)))) . (((1 + 1) + n) + 1)
by Def7
;
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 A21, A42, A41, Def7;
then A58:
(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 A54, A55, Def7;
then A59: ((Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)))) `1_3 =
4
.=
the AcceptS of SuccTuring
by Def17
;
hence
s is Accept-Halt
; ( (Result s) `2_3 = h & (Result s) `3_3 storeData <*h,(n + 1)*> )
then A60:
Result s = (Computation s) . ((1 + 1) + (((n + 1) + 1) + (((1 + 1) + n) + 1)))
by A59, Def9;
hence
(Result s) `2_3 = h
by A58; (Result s) `3_3 storeData <*h,(n + 1)*>
(Result s) `3_3 = Tape-Chg ((Tape-Chg ((Tape-Chg (t,h1,T)),nk,T)),n3,F)
by A58, A60;
hence
(Result s) `3_3 storeData <*h,(n + 1)*>
by A40, Th16; verum