let s be 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 s . (DataLoc ((s . a),i)) < 0 & card I > 0 & ( for t being State 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,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) holds
IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s)))
let I be halt-free shiftable Program of SCMPDS; for a being Int_position
for i being Integer
for X being set st s . (DataLoc ((s . a),i)) < 0 & card I > 0 & ( for t being State 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,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) holds
IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s)))
let a be Int_position ; for i being Integer
for X being set st s . (DataLoc ((s . a),i)) < 0 & card I > 0 & ( for t being State 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,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) holds
IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s)))
let i be Integer; for X being set st s . (DataLoc ((s . a),i)) < 0 & card I > 0 & ( for t being State 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,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) holds
IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s)))
let X be set ; ( s . (DataLoc ((s . a),i)) < 0 & card I > 0 & ( for t being State 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,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) implies IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s))) )
set b = DataLoc ((s . a),i);
set WHL = while<0 (a,i,I);
set pWHL = stop (while<0 (a,i,I));
set s1 = (Initialize s) +* (stop (while<0 (a,i,I)));
set ps = ProgramPart s;
I1:
(Initialize s) +* (stop (while<0 (a,i,I))) = s +* (Initialize (stop (while<0 (a,i,I))))
by COMPOS_1:125;
set i1 = (a,i) >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A1:
s . (DataLoc ((s . a),i)) < 0
; ( not card I > 0 or ex t being State 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 & not ( (IExec (I,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) or IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s))) )
set Es = IExec (I,s);
set bj = DataLoc (((IExec (I,s)) . a),i);
set sI = (Initialize s) +* (stop I);
set m1 = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2;
set s2 = (Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)));
set m2 = LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))));
I2:
(Initialize s) +* (stop I) = s +* (Initialize (stop I))
by COMPOS_1:125;
I3:
(Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))) = (IExec (I,s)) +* (Initialize (stop (while<0 (a,i,I))))
by COMPOS_1:125;
assume A2:
card I > 0
; ( ex t being State 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 & not ( (IExec (I,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) ) or IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s))) )
assume A3:
for t being State 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,t)) . a = t . a & (IExec (I,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) )
; IExec ((while<0 (a,i,I)),s) = IExec ((while<0 (a,i,I)),(IExec (I,s)))
then
while<0 (a,i,I) is_halting_on s
by A2, Th15;
then A4:
ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) halts_on (Initialize s) +* (stop (while<0 (a,i,I)))
by SCMPDS_6:def 3;
A5:
Initialize (stop I) c= (Initialize s) +* (stop I)
by I2, FUNCT_4:26;
A6:
for x being Int_position st x in X holds
s . x = s . x
;
then
I is_halting_on s
by A1, A3;
then A7:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by SCMPDS_6:def 3;
I4:
(Initialize ((Initialize s) +* (stop I))) +* (stop I) = ((Initialize s) +* (stop I)) +* (Initialize (stop I))
by COMPOS_1:125;
(Initialize s) +* (stop I) = (Initialize ((Initialize s) +* (stop I))) +* (stop I)
by A5, I4, FUNCT_4:79;
then
ProgramPart (((Initialize s) +* (stop I)) +* (Initialize (stop I))) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I)
by A7, I4;
then A8:
I is_halting_on (Initialize s) +* (stop I)
by I4, SCMPDS_6:def 3;
A9:
(IExec (I,s)) . a = s . a
by A1, A3, A6;
now let t be
State of
SCMPDS;
( ( for x being Int_position st x in X holds
t . x = (IExec (I,s)) . x ) & t . a = (IExec (I,s)) . a & t . (DataLoc (((IExec (I,s)) . a),i)) < 0 implies ( (IExec (I,t)) . a = t . a & (IExec (I,t)) . (DataLoc (((IExec (I,s)) . a),i)) > t . (DataLoc (((IExec (I,s)) . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) ) )assume that A10:
for
x being
Int_position st
x in X holds
t . x = (IExec (I,s)) . x
and A11:
(
t . a = (IExec (I,s)) . a &
t . (DataLoc (((IExec (I,s)) . a),i)) < 0 )
;
( (IExec (I,t)) . a = t . a & (IExec (I,t)) . (DataLoc (((IExec (I,s)) . a),i)) > t . (DataLoc (((IExec (I,s)) . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) )hence
(IExec (I,t)) . a = t . a
by A3, A9, A11;
( (IExec (I,t)) . (DataLoc (((IExec (I,s)) . a),i)) > t . (DataLoc (((IExec (I,s)) . a),i)) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) )thus
(IExec (I,t)) . (DataLoc (((IExec (I,s)) . a),i)) > t . (DataLoc (((IExec (I,s)) . a),i))
by A3, A9, A11, A12;
( I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec (I,t)) . x = t . x ) )thus
(
I is_closed_on t &
I is_halting_on t & ( for
x being
Int_position st
x in X holds
(IExec (I,t)) . x = t . x ) )
by A3, A9, A11, A12;
verum end;
then
while<0 (a,i,I) is_halting_on IExec (I,s)
by A2, Th15;
then A14:
ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) halts_on (Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))
by SCMPDS_6:def 3;
set m0 = LifeSpan ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))));
A15:
dom (ProgramPart s) = NAT
by COMPOS_1:34;
A16: dom (ProgramPart s) =
(dom s) /\ NAT
by RELAT_1:90
.=
(({(IC SCMPDS)} \/ SCM-Data-Loc) \/ NAT) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1);
A17:
IC ((Initialize s) +* (stop (while<0 (a,i,I)))) = 0
by SCMPDS_6:21;
A18:
while<0 (a,i,I) = ((a,i) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by SCMPDS_4:51;
A19: Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(0 + 1)) =
Following ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),0)))
by EXTPRO_1:4
.=
Following ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))))
by EXTPRO_1:3
.=
Exec (((a,i) >=0_goto ((card I) + 2)),((Initialize s) +* (stop (while<0 (a,i,I)))))
by A18, I1, SCMPDS_6:22
;
A20: (IExec (I,s)) | NAT =
((Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (ProgramPart s)) | NAT
by SCMPDS_4:def 8
.=
ProgramPart s
by A16, FUNCT_4:24
;
A21:
not DataLoc ((s . a),i) in dom (Initialize (stop (while<0 (a,i,I))))
by SCMPDS_4:31;
not a in dom (Initialize (stop (while<0 (a,i,I))))
by SCMPDS_4:31;
then ((Initialize s) +* (stop (while<0 (a,i,I)))) . (DataLoc ((((Initialize s) +* (stop (while<0 (a,i,I)))) . a),i)) =
((Initialize s) +* (stop (while<0 (a,i,I)))) . (DataLoc ((s . a),i))
by I1, FUNCT_4:12
.=
s . (DataLoc ((s . a),i))
by A21, I1, FUNCT_4:12
;
then A22: IC (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)) =
succ (IC ((Initialize s) +* (stop (while<0 (a,i,I)))))
by A1, A19, SCMPDS_2:69
.=
0 + 1
by A17
;
set mI = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set s5 = Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
set l1 = (card I) + 1;
A23:
DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while<0 (a,i,I))))
by COMPOS_1:138, FUNCT_7:134;
now let a be
Int_position ;
((Initialize s) +* (stop I)) . a = (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)) . athus ((Initialize s) +* (stop I)) . a =
((Initialize s) +* (stop (while<0 (a,i,I)))) . a
by A23, SCMPDS_4:23
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)) . a
by A19, SCMPDS_2:69
;
verum end;
then A24:
DataPart ((Initialize s) +* (stop I)) = DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))
by SCMPDS_4:23;
set m3 = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1;
set s6 = Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1));
(card I) + 1 < (card I) + 2
by XREAL_1:8;
then A25:
(card I) + 1 in dom (while<0 (a,i,I))
by Th7;
set s7 = Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1));
A26:
IExec (I,s) = (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (s | NAT)
by SCMPDS_4:def 8;
( while<0 (a,i,I) c= Initialize (stop (while<0 (a,i,I))) & Initialize (stop (while<0 (a,i,I))) c= (Initialize s) +* (stop (while<0 (a,i,I))) )
by I1, FUNCT_4:26, SCMPDS_6:17;
then A27:
while<0 (a,i,I) c= (Initialize s) +* (stop (while<0 (a,i,I)))
by XBOOLE_1:1;
Shift (I,1) c= while<0 (a,i,I)
by Lm2;
then
Shift (I,1) c= (Initialize s) +* (stop (while<0 (a,i,I)))
by A27, XBOOLE_1:1;
then A28:
Shift (I,1) c= Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)
by AMI_1:81;
I is_closed_on s
by A1, A3, A6;
then A29:
I is_closed_on (Initialize s) +* (stop I)
by SCMPDS_6:38;
then A30:
IC (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = (card I) + 1
by A2, A5, A8, A22, A24, A28, SCMPDS_7:36;
Y:
(ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) = (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))))
by COMPOS_1:38;
ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))
by AMI_1:123;
then A31:
Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)) = Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by EXTPRO_1:5;
then A32: CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) =
(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . ((card I) + 1)
by A2, A5, A8, A29, A22, A24, A28, Y, SCMPDS_7:36
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)) . ((card I) + 1)
by AMI_1:54
.=
((Initialize s) +* (stop (while<0 (a,i,I)))) . ((card I) + 1)
by AMI_1:54
.=
(while<0 (a,i,I)) . ((card I) + 1)
by A25, A27, GRFUNC_1:8
.=
goto (- ((card I) + 1))
by Th8
;
T:
ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))
by AMI_1:123;
A33: Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1)) =
Following ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))))
by EXTPRO_1:4
.=
Exec ((goto (- ((card I) + 1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))))
by A32, T
;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) =
ICplusConst ((Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))),(0 - ((card I) + 1)))
by SCMPDS_2:66
.=
0
by A30, A31, SCMPDS_7:1
;
then A34:
IC ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) = IC (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2)))
by SCMPDS_6:21;
A35:
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = DataPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by A2, A5, A8, A29, A22, A24, A28, SCMPDS_7:36;
now let x be
Int_position ;
(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) . x = ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) . xA36:
not
x in dom (Initialize (stop (while<0 (a,i,I))))
by SCMPDS_4:31;
A37:
not
x in dom (s | NAT)
by A15, SCMPDS_2:53;
(Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),1)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . x =
(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . x
by A35, SCMPDS_4:23
.=
(Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x
by A7, EXTPRO_1:23
.=
(IExec (I,s)) . x
by A26, A37, FUNCT_4:12
;
hence (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) . x =
(IExec (I,s)) . x
by A31, A33, SCMPDS_2:66
.=
((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) . x
by A36, I3, FUNCT_4:12
;
verum end;
then A38:
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1) + 1))) = DataPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))
by SCMPDS_4:23;
TX:
ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2)))
by AMI_1:123;
ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) =
ProgramPart (((Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (ProgramPart s)) +* (Initialize (stop (while<0 (a,i,I)))))
by I3, SCMPDS_4:def 8
.=
(ProgramPart ((Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (ProgramPart s))) +* (ProgramPart (Initialize (stop (while<0 (a,i,I)))))
by FUNCT_4:75
.=
(ProgramPart s) +* (ProgramPart (Initialize (stop (while<0 (a,i,I)))))
by A16, FUNCT_4:24
.=
ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))
by I1, FUNCT_4:75
.=
ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2)))
by AMI_1:123
;
then A39:
Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2)) = (Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))
by A38, A34, SCMPDS_7:7;
then
CurInstr ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2)))) = (a,i) >=0_goto ((card I) + 2)
by A18, TX, I3, SCMPDS_6:22;
then
LifeSpan ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I))))) > (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2
by A4, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A40:
LifeSpan ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I))))) = ((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2) + nn
by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
T:
ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) = ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))
by A39, AMI_1:123;
Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2) + (LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))))) = Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))),(LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))))
by A39, EXTPRO_1:5;
then
CurInstr ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),(Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2) + (LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))))))) = halt SCMPDS
by A14, T, EXTPRO_1:def 14;
then
((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2) + (LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))) >= LifeSpan ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))))
by A4, EXTPRO_1:def 14;
then A41:
LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))) >= nn
by A40, XREAL_1:8;
A42:
Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I))))))) = Comput ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))),nn)
by A39, A40, EXTPRO_1:5;
then
CurInstr ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),(Comput ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))),nn))) = halt SCMPDS
by A4, T, EXTPRO_1:def 14;
then
nn >= LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))
by A14, EXTPRO_1:def 14;
then
nn = LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))
by A41, XXREAL_0:1;
then
Result ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I))))) = Comput ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))),(LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))))
by A4, A42, T, EXTPRO_1:23;
hence IExec ((while<0 (a,i,I)),s) =
(Comput ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))),(LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))))) +* (ProgramPart s)
by SCMPDS_4:def 8
.=
(Result ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))))) +* ((IExec (I,s)) | NAT)
by A14, A20, EXTPRO_1:23
.=
IExec ((while<0 (a,i,I)),(IExec (I,s)))
by SCMPDS_4:def 8
;
verum