let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
let s be 0 -started State of SCMPDS; for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
let I be halt-free shiftable Program of SCMPDS; for a being Int_position
for i being Integer
for X being set st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
let a be Int_position ; for i being Integer
for X being set st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
let i be Integer; for X being set st ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) holds
( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
let X be set ; ( ( for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ) implies ( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P ) )
set b = DataLoc ((s . a),i);
set WHL = while<0 (a,i,I);
set pWHL = stop (while<0 (a,i,I));
set pI = stop I;
set i1 = (a,i) >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
defpred S1[ Element of NAT ] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= $1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( while<0 (a,i,I) is_closed_on t,Q & while<0 (a,i,I) is_halting_on t,Q );
assume A2:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) )
; ( while<0 (a,i,I) is_closed_on s,P & while<0 (a,i,I) is_halting_on s,P )
A3:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
now let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( while<0 (a,i,I) is_closed_on b2,b3 & while<0 (a,i,I) is_halting_on b2,b3 )let Q be
Instruction-Sequence of
SCMPDS;
( - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( while<0 (a,i,I) is_closed_on b1,b2 & while<0 (a,i,I) is_halting_on b1,b2 ) )T:
Initialize t = t
by MEMSTR_0:44;
assume A5:
- (t . (DataLoc ((s . a),i))) <= k + 1
;
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( while<0 (a,i,I) is_closed_on b1,b2 & while<0 (a,i,I) is_halting_on b1,b2 ) )assume A6:
for
x being
Int_position st
x in X holds
t . x = s . x
;
( t . a = s . a implies ( while<0 (a,i,I) is_closed_on b1,b2 & while<0 (a,i,I) is_halting_on b1,b2 ) )assume A7:
t . a = s . a
;
( while<0 (a,i,I) is_closed_on b1,b2 & while<0 (a,i,I) is_halting_on b1,b2 )per cases
( t . (DataLoc ((s . a),i)) >= 0 or t . (DataLoc ((s . a),i)) < 0 )
;
suppose A8:
t . (DataLoc ((s . a),i)) < 0
;
( while<0 (a,i,I) is_closed_on b1,b2 & while<0 (a,i,I) is_halting_on b1,b2 )A12:
(IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i))
by A2, A6, A7, A8, T;
A13:
0 in dom (stop (while<0 (a,i,I)))
by COMPOS_1:36;
A15:
not
DataLoc (
(s . a),
i)
in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
A16:
while<0 (
a,
i,
I)
= ((a,i) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by SCMPDS_4:15;
set t2 =
Initialize t;
set Q2 =
Q +* (stop I);
set t3 =
Initialize t;
set Q3 =
Q +* (stop (while<0 (a,i,I)));
set t4 =
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),1);
set Q4 =
Q +* (stop (while<0 (a,i,I)));
A19:
stop I c= Q +* (stop I)
by FUNCT_4:25;
A20:
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(0 + 1)) =
Following (
(Q +* (stop (while<0 (a,i,I)))),
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),0)))
by EXTPRO_1:3
.=
Following (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t))
by EXTPRO_1:2
.=
Exec (
((a,i) >=0_goto ((card I) + 2)),
(Initialize t))
by A16, SCMPDS_6:11
;
for
a being
Int_position holds
(Initialize t) . a = (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)) . a
by A20, SCMPDS_2:57;
then A22:
DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1))
by SCMPDS_4:8;
XX:
while<0 (
a,
i,
I)
c= stop (while<0 (a,i,I))
by AFINSQ_1:74;
stop (while<0 (a,i,I)) c= Q +* (stop (while<0 (a,i,I)))
by FUNCT_4:25;
then A23:
while<0 (
a,
i,
I)
c= Q +* (stop (while<0 (a,i,I)))
by XX, XBOOLE_1:1;
Shift (
I,1)
c= while<0 (
a,
i,
I)
by Lm2;
then A24:
Shift (
I,1)
c= Q +* (stop (while<0 (a,i,I)))
by A23, XBOOLE_1:1;
set m2 =
LifeSpan (
(Q +* (stop I)),
(Initialize t));
set t5 =
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),
(LifeSpan ((Q +* (stop I)),(Initialize t))));
set Q5 =
Q +* (stop (while<0 (a,i,I)));
set l1 =
(card I) + 1;
A25:
IC (Initialize t) = 0
by MEMSTR_0:def 8;
set m3 =
(LifeSpan ((Q +* (stop I)),(Initialize t))) + 1;
set t6 =
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1));
set Q6 =
Q +* (stop (while<0 (a,i,I)));
set t7 =
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1));
set Q7 =
Q +* (stop (while<0 (a,i,I)));
(card I) + 1
< (card I) + 2
by XREAL_1:6;
then A26:
(card I) + 1
in dom (while<0 (a,i,I))
by Th7;
A27:
IExec (
I,
Q,
(Initialize t))
= Result (
(Q +* (stop I)),
(Initialize t))
by SCMPDS_4:def 5;
A28:
I is_closed_on t,
Q
by A2, A6, A7, A8;
then A29:
I is_closed_on Initialize t,
Q +* (stop I)
by SCMPDS_6:24;
I is_halting_on t,
Q
by A2, A6, A7, A8;
then A30:
Q +* (stop I) halts_on Initialize t
by SCMPDS_6:def 3;
(Q +* (stop I)) +* (stop I) halts_on Initialize (Initialize t)
by A30, FUNCT_4:25, FUNCT_4:98;
then A32:
I is_halting_on Initialize t,
Q +* (stop I)
by SCMPDS_6:def 3;
not
a in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
then (Initialize t) . (DataLoc (((Initialize t) . a),i)) =
(Initialize t) . (DataLoc ((s . a),i))
by A7, FUNCT_4:11
.=
t . (DataLoc ((s . a),i))
by A15, FUNCT_4:11
;
then A33:
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)) =
succ (IC (Initialize t))
by A8, A20, SCMPDS_2:57
.=
0 + 1
by A25
;
then A34:
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = (card I) + 1
by A19, A32, A29, A22, A24, SCMPDS_7:18;
A35:
(Q +* (stop (while<0 (a,i,I)))) /. (IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (while<0 (a,i,I)))) . (IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))))
by PBOOLE:143;
A36:
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))
= Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),
(LifeSpan ((Q +* (stop I)),(Initialize t))))
by EXTPRO_1:4;
then A37:
CurInstr (
(Q +* (stop (while<0 (a,i,I)))),
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) =
(Q +* (stop (while<0 (a,i,I)))) . ((card I) + 1)
by A19, A32, A29, A33, A22, A24, A35, SCMPDS_7:18
.=
(while<0 (a,i,I)) . ((card I) + 1)
by A26, A23, GRFUNC_1:2
.=
goto (- ((card I) + 1))
by Th8
;
A38:
DataPart (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = DataPart (Comput ((Q +* (stop (while<0 (a,i,I)))),(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t)))))
by A19, A32, A29, A33, A22, A24, SCMPDS_7:18;
then A39:
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a =
(Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a
by SCMPDS_4:8
.=
(Result ((Q +* (stop I)),(Initialize t))) . a
by A30, EXTPRO_1:23
.=
s . a
by A7, A2, A6, A8, A27, T
;
A41:
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)) =
Following (
(Q +* (stop (while<0 (a,i,I)))),
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))))
by EXTPRO_1:3
.=
Exec (
(goto (- ((card I) + 1))),
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))))
by A37
;
then IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) =
ICplusConst (
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))),
(0 - ((card I) + 1)))
by SCMPDS_2:54
.=
0
by A34, A36, SCMPDS_7:1
;
then A42:
Initialize (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) = Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))
by MEMSTR_0:46;
A43:
now let x be
Int_position ;
( x in X implies (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x )assume A44:
x in X
;
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x(Comput ((Q +* (stop (while<0 (a,i,I)))),(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x =
(Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x
by A38, SCMPDS_4:8
.=
(Result ((Q +* (stop I)),(Initialize t))) . x
by A30, EXTPRO_1:23
.=
(IExec (I,Q,(Initialize t))) . x
by SCMPDS_4:def 5
.=
t . x
by A2, A6, A7, A8, A44, T
.=
s . x
by A6, A44
;
hence
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x
by A36, A41, SCMPDS_2:54;
verum end; (Comput ((Q +* (stop (while<0 (a,i,I)))),(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i)) =
(Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i))
by A38, SCMPDS_4:8
.=
(Result ((Q +* (stop I)),(Initialize t))) . (DataLoc ((s . a),i))
by A30, EXTPRO_1:23
.=
(IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i))
by SCMPDS_4:def 5
;
then A46:
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i)) = (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i))
by A36, A41, SCMPDS_2:54;
A47:
now
- ((Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i))) < - (t . (DataLoc ((s . a),i)))
by A12, A46, XREAL_1:24;
then A48:
- ((Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i))) < k + 1
by A5, XXREAL_0:2;
assume
- ((Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i))) > k
;
contradictionhence
contradiction
by A48, INT_1:7;
verum end; A50:
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . a =
(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a
by A41, SCMPDS_2:54
.=
s . a
by A39, EXTPRO_1:4
;
then A51:
while<0 (
a,
i,
I)
is_closed_on Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)),
Q +* (stop (while<0 (a,i,I)))
by A4, A43, A47, A42;
now let k be
Element of
NAT ;
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),b1)) in dom (stop (while<0 (a,i,I)))per cases
( k < ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 or k >= ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 )
;
suppose
k < ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1
;
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),b1)) in dom (stop (while<0 (a,i,I)))then A52:
k <= (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1
by INT_1:7;
hereby verum
per cases
( k <= LifeSpan ((Q +* (stop I)),(Initialize t)) or k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 )
by A52, NAT_1:8;
suppose A53:
k <= LifeSpan (
(Q +* (stop I)),
(Initialize t))
;
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) in dom (stop (while<0 (a,i,I)))hereby verum
per cases
( k = 0 or k <> 0 )
;
suppose
k <> 0
;
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) in dom (stop (while<0 (a,i,I)))then consider kn being
Nat such that A54:
k = kn + 1
by NAT_1:6;
reconsider kn =
kn as
Element of
NAT by ORDINAL1:def 12;
reconsider lm =
IC (Comput ((Q +* (stop I)),(Initialize t),kn)) as
Element of
NAT ;
kn < k
by A54, XREAL_1:29;
then
kn < LifeSpan (
(Q +* (stop I)),
(Initialize t))
by A53, XXREAL_0:2;
then
(IC (Comput ((Q +* (stop I)),(Initialize t),kn))) + 1
= IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),1)),kn))
by A19, A32, A29, A33, A22, A24, SCMPDS_7:16;
then A56:
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) = lm + 1
by A54, EXTPRO_1:4;
IC (Comput ((Q +* (stop I)),(Initialize t),kn)) in dom (stop I)
by A28, SCMPDS_6:def 2;
then
lm < card (stop I)
by AFINSQ_1:66;
then
lm < (card I) + 1
by COMPOS_1:55;
then A57:
lm + 1
<= (card I) + 1
by INT_1:7;
(card I) + 1
< (card I) + 3
by XREAL_1:6;
then
lm + 1
< (card I) + 3
by A57, XXREAL_0:2;
then
lm + 1
< card (stop (while<0 (a,i,I)))
by Lm1;
hence
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) in dom (stop (while<0 (a,i,I)))
by A56, AFINSQ_1:66;
verum end; suppose A58:
k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1
;
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) in dom (stop (while<0 (a,i,I)))
(card I) + 1
in dom (stop (while<0 (a,i,I)))
by A26, COMPOS_1:62;
hence
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) in dom (stop (while<0 (a,i,I)))
by A19, A32, A29, A33, A22, A24, A36, A58, SCMPDS_7:18;
verum end; end; suppose
k >= ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1
;
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),b1)) in dom (stop (while<0 (a,i,I)))then consider nn being
Nat such that A59:
k = (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + nn
by NAT_1:10;
reconsider nn =
nn as
Element of
NAT by ORDINAL1:def 12;
Q +* (stop (while<0 (a,i,I))) = (Q +* (stop (while<0 (a,i,I)))) +* (stop (while<0 (a,i,I)))
by FUNCT_4:93;
then
Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
k)
= Comput (
((Q +* (stop (while<0 (a,i,I)))) +* (stop (while<0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))),
nn)
by A42, A59, EXTPRO_1:4;
hence
IC (Comput ((Q +* (stop (while<0 (a,i,I)))),(Initialize t),k)) in dom (stop (while<0 (a,i,I)))
by A51, SCMPDS_6:def 2;
verum end; end; hence
while<0 (
a,
i,
I)
is_closed_on t,
Q
by SCMPDS_6:def 2;
while<0 (a,i,I) is_halting_on t,QRR:
Q +* (stop (while<0 (a,i,I))) = (Q +* (stop (while<0 (a,i,I)))) +* (stop (while<0 (a,i,I)))
by FUNCT_4:93;
while<0 (
a,
i,
I)
is_halting_on Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)),
Q +* (stop (while<0 (a,i,I)))
by A4, A50, A43, A47, A42;
then
Q +* (stop (while<0 (a,i,I))) halts_on Comput (
(Q +* (stop (while<0 (a,i,I)))),
(Initialize t),
(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))
by A42, RR, SCMPDS_6:def 3;
then
Q +* (stop (while<0 (a,i,I))) halts_on Initialize t
by EXTPRO_1:22;
hence
while<0 (
a,
i,
I)
is_halting_on t,
Q
by SCMPDS_6:def 3;
verum end; end;
hence
S1[
k + 1]
;
verum
end;
A60:
S1[ 0 ]
proof
let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( while<0 (a,i,I) is_closed_on t,Q & while<0 (a,i,I) is_halting_on t,Q )let Q be
Instruction-Sequence of
SCMPDS;
( - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( while<0 (a,i,I) is_closed_on t,Q & while<0 (a,i,I) is_halting_on t,Q ) )
assume
- (t . (DataLoc ((s . a),i))) <= 0
;
( ex x being Int_position st
( x in X & not t . x = s . x ) or not t . a = s . a or ( while<0 (a,i,I) is_closed_on t,Q & while<0 (a,i,I) is_halting_on t,Q ) )
then
- (t . (DataLoc ((s . a),i))) <= - 0
;
then A61:
t . (DataLoc ((s . a),i)) >= 0
by XREAL_1:24;
assume
for
x being
Int_position st
x in X holds
t . x = s . x
;
( not t . a = s . a or ( while<0 (a,i,I) is_closed_on t,Q & while<0 (a,i,I) is_halting_on t,Q ) )
assume
t . a = s . a
;
( while<0 (a,i,I) is_closed_on t,Q & while<0 (a,i,I) is_halting_on t,Q )
hence
(
while<0 (
a,
i,
I)
is_closed_on t,
Q &
while<0 (
a,
i,
I)
is_halting_on t,
Q )
by A61, Th9;
verum
end;
A62:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A60, A3);