let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
let s be 0 -started State of SCMPDS; for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
let I be halt-free shiftable Program of ; for a being Int_position
for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
let a be Int_position; for i being Integer
for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
let i be Integer; for n being Nat
for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
let n be Nat; for X being set st s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
let X be set ; ( s . (DataLoc ((s . a),i)) < 0 & not DataLoc ((s . a),i) in X & n > 0 & a <> DataLoc ((s . a),i) & ( for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) implies IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) )
set b = DataLoc ((s . a),i);
set FOR = for-up (a,i,n,I);
set pFOR = stop (for-up (a,i,n,I));
set s1 = s;
set P1 = P +* (stop (for-up (a,i,n,I)));
set i1 = (a,i) >=0_goto ((card I) + 3);
set i2 = AddTo (a,i,n);
set i3 = goto (- ((card I) + 2));
assume A1:
s . (DataLoc ((s . a),i)) < 0
; ( DataLoc ((s . a),i) in X or not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex 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 & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) )
set s4 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,1);
set P4 = P +* (stop (for-up (a,i,n,I)));
A2:
IC s = 0
by MEMSTR_0:def 11;
set m0 = LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s);
set l2 = (card I) + 2;
set sI = s;
set PI = P +* (stop I);
set m1 = (LifeSpan ((P +* (stop I)),s)) + 3;
set J = I ';' (AddTo (a,i,n));
set sJ = s;
set PJ = P +* (stop (I ';' (AddTo (a,i,n))));
set s2 = Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s));
set P2 = P +* (stop (for-up (a,i,n,I)));
set m2 = LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))));
set Es = IExec ((I ';' (AddTo (a,i,n))),P,s);
set bj = DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i);
A3:
stop I c= P +* (stop I)
by FUNCT_4:25;
A4:
for-up (a,i,n,I) = ((a,i) >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2))))
by Th2;
set mI = LifeSpan ((P +* (stop I)),s);
set s5 = Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)));
set P5 = P +* (stop (for-up (a,i,n,I)));
set l1 = (card I) + 1;
set m3 = (LifeSpan ((P +* (stop I)),s)) + 1;
set s6 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1));
set P6 = P +* (stop (for-up (a,i,n,I)));
set s7 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1));
set P7 = P +* (stop (for-up (a,i,n,I)));
A5:
stop (for-up (a,i,n,I)) c= P +* (stop (for-up (a,i,n,I)))
by FUNCT_4:25;
for-up (a,i,n,I) c= stop (for-up (a,i,n,I))
by AFINSQ_1:74;
then A6:
for-up (a,i,n,I) c= P +* (stop (for-up (a,i,n,I)))
by A5, XBOOLE_1:1;
Shift (I,1) c= for-up (a,i,n,I)
by Lm3;
then A7:
Shift (I,1) c= P +* (stop (for-up (a,i,n,I)))
by A6, XBOOLE_1:1;
(card I) + 2 < (card I) + 3
by XREAL_1:6;
then A8:
(card I) + 2 in dom (for-up (a,i,n,I))
by Th31;
set m5 = (((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1;
set s8 = Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1));
(card I) + 1 < (card I) + 3
by XREAL_1:6;
then A9:
(card I) + 1 in dom (for-up (a,i,n,I))
by Th31;
assume A10:
not DataLoc ((s . a),i) in X
; ( not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex 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 & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) )
assume A11:
n > 0
; ( not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex 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 & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) )
assume A12:
a <> DataLoc ((s . a),i)
; ( ex t being State of SCMPDS ex 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 & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) )
A13:
Initialize s = s
by MEMSTR_0:44;
assume A14:
for t being 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 holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )
; IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
then
for-up (a,i,n,I) is_halting_on s,P
by A1, A10, A11, A12, Th37;
then A15:
P +* (stop (for-up (a,i,n,I))) halts_on s
by A13, SCMPDS_6:def 3;
A16:
for x being Int_position st x in X holds
s . x = s . x
;
then A17:
(IExec (I,P,s)) . (DataLoc ((s . a),i)) = s . (DataLoc ((s . a),i))
by A14, A13;
A18:
(IExec (I,P,s)) . a = s . a
by A14, A16, A13;
A19:
DataLoc ((s . a),i) = DataLoc (((IExec (I,P,s)) . a),i)
by A14, A16, A13;
A20:
(IExec (I,P,s)) . a = s . a
by A14, A16, A13;
A21: Comput ((P +* (stop (for-up (a,i,n,I)))),s,(0 + 1)) =
Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,0)))
by EXTPRO_1:3
.=
Exec (((a,i) >=0_goto ((card I) + 3)),s)
by A4, A13, SCMPDS_6:11
;
A22:
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)) = 0 + 1
by A2, A1, A21, SCMPDS_2:57;
for a being Int_position holds s . a = (Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)) . a
by A21, SCMPDS_2:57;
then A23:
DataPart s = DataPart (Comput ((P +* (stop (for-up (a,i,n,I)))),s,1))
by SCMPDS_4:8;
A24:
I is_halting_on s,P
by A14, A16;
then A25:
P +* (stop I) halts_on s
by A13, SCMPDS_6:def 3;
(P +* (stop I)) +* (stop I) halts_on s
by A25;
then A26:
I is_halting_on s,P +* (stop I)
by A13, SCMPDS_6:def 3;
A27:
I is_closed_on s,P
by A14, A16;
then A28: (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc ((s . a),i)) =
(Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . (DataLoc ((s . a),i))
by A24, Th29
.=
((IExec (I,P,s)) . (DataLoc ((s . a),i))) + n
by A18, SCMPDS_2:48
.=
(s . (DataLoc ((s . a),i))) + n
by A14, A16, A13
;
A29:
I is_closed_on s,P +* (stop I)
by A14, A16;
then A30:
IC (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) = (card I) + 1
by A3, A26, A22, A23, A7, Th16;
A31:
(P +* (stop (for-up (a,i,n,I)))) /. (IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (for-up (a,i,n,I)))) . (IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))))
by PBOOLE:143;
A32:
Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))
by EXTPRO_1:4;
then A33: CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) =
(P +* (stop (for-up (a,i,n,I)))) . ((card I) + 1)
by A3, A26, A29, A22, A23, A7, Th16, A31
.=
(for-up (a,i,n,I)) . ((card I) + 1)
by A9, A6, GRFUNC_1:2
.=
AddTo (a,i,n)
by Th32
;
A34:
DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s))))
by A3, A26, A29, A22, A23, A7, Th16;
then A35: (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . a =
(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . a
by SCMPDS_4:8
.=
s . a
by A20, A25, EXTPRO_1:23
;
A36: (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a =
(Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . a
by A27, A24, Th29
.=
s . a
by A12, A18, SCMPDS_2:48
;
now for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),Pper cases
( (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) >= 0 or (IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) < 0 )
;
suppose
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) >= 0
;
for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),Pend; suppose A37:
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) < 0
;
for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),Pnow for t being State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x ) & t . a = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )let t be
State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x ) & t . a = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a holds
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )let Q be
Instruction-Sequence of
SCMPDS;
( ( for x being Int_position st x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x ) & t . a = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a implies ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) )assume that A38:
for
x being
Int_position st
x in X holds
t . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x
and A39:
t . a = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . a
;
( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )A40:
now for x being Int_position st x in X holds
t . x = s . xlet x be
Int_position;
( x in X implies t . x = s . x )assume A41:
x in X
;
t . x = s . xhence t . x =
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . x
by A38
.=
(Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . x
by A27, A24, Th29
.=
(IExec (I,P,s)) . x
by A10, A18, A41, SCMPDS_2:48
.=
s . x
by A14, A16, A41, A13
;
verum end; hence
(IExec (I,Q,(Initialize t))) . a = t . a
by A14, A36, A39;
( (IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )thus
(IExec (I,Q,(Initialize t))) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) = t . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i))
by A14, A36, A39, A40;
( I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )thus
(
I is_closed_on t,
Q &
I is_halting_on t,
Q & ( for
y being
Int_position st
y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) )
by A14, A36, A39, A40;
verum end; hence
for-up (
a,
i,
n,
I)
is_halting_on IExec (
(I ';' (AddTo (a,i,n))),
P,
s),
P
by A10, A11, A12, A36, A37, Th37;
verum end; end; end;
then A42:
P +* (stop (for-up (a,i,n,I))) halts_on Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))
by SCMPDS_6:def 3;
A43: Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)) =
Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))))
by EXTPRO_1:3
.=
Exec ((AddTo (a,i,n)),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))))
by A33
;
then A44: IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) =
(IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) + 1
by SCMPDS_2:48
.=
(card I) + (1 + 1)
by A30, A32
;
then A45: CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)))) =
(P +* (stop (for-up (a,i,n,I)))) . ((card I) + 2)
by PBOOLE:143
.=
(for-up (a,i,n,I)) . ((card I) + 2)
by A6, A8, GRFUNC_1:2
.=
goto (- ((card I) + 2))
by Th32
;
A46: Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1)) =
Following ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))))
by EXTPRO_1:3
.=
Exec ((goto (- ((card I) + 2))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))))
by A45
;
then IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) =
ICplusConst ((Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))),(0 - ((card I) + 2)))
by SCMPDS_2:54
.=
0
by A44, Th1
;
then A47:
IC (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) = IC (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 3)))
by MEMSTR_0:def 11;
A48: (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . (DataLoc ((s . a),i)) =
(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . (DataLoc ((s . a),i))
by A34, SCMPDS_4:8
.=
s . (DataLoc ((s . a),i))
by A17, A25, EXTPRO_1:23
;
A49: (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) =
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . (DataLoc ((s . a),i))
by A46, SCMPDS_2:54
.=
(s . (DataLoc ((s . a),i))) + n
by A35, A48, A32, A43, SCMPDS_2:48
;
now for x being Int_position holds (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . x = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . xlet x be
Int_position;
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . b1 = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . b1A50:
not
x in dom (Start-At (0,SCMPDS))
by SCMPDS_4:18;
then A51:
(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . x = (IExec ((I ';' (AddTo (a,i,n))),P,s)) . x
by FUNCT_4:11;
per cases
( x = DataLoc ((s . a),i) or x <> DataLoc ((s . a),i) )
;
suppose
x = DataLoc (
(s . a),
i)
;
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . b1 = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . b1hence
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . x = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . x
by A49, A28, A50, FUNCT_4:11;
verum end; suppose A52:
x <> DataLoc (
(s . a),
i)
;
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . b1 = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . b1A53:
(Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x =
(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . x
by A34, SCMPDS_4:8
.=
(IExec (I,P,s)) . x
by A25, EXTPRO_1:23
;
A54:
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (Comput ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x
by A35, A32, A43, A52, SCMPDS_2:48;
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . x =
(Exec ((AddTo (a,i,n)),(IExec (I,P,s)))) . x
by A27, A24, Th29
.=
(IExec (I,P,s)) . x
by A19, A52, SCMPDS_2:48
;
hence
(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . x = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . x
by A46, A51, A53, A54, SCMPDS_2:54;
verum end; end; end;
then A55:
DataPart (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) = DataPart (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))
by SCMPDS_4:8;
A56:
Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 3)) = Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))
by A55, A47, MEMSTR_0:78;
then
CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 3)))) = (a,i) >=0_goto ((card I) + 3)
by A4, SCMPDS_6:11;
then
LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s) > (LifeSpan ((P +* (stop I)),s)) + 3
by A15, EXTPRO_1:36;
then consider nn being Nat such that
A57:
LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s) = ((LifeSpan ((P +* (stop I)),s)) + 3) + nn
by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 3) + (LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))))) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),(LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))))
by A56, EXTPRO_1:4;
then
CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 3) + (LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))))))) = halt SCMPDS
by A42, EXTPRO_1:def 15;
then
((LifeSpan ((P +* (stop I)),s)) + 3) + (LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))) >= LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s)
by A15, EXTPRO_1:def 15;
then A58:
LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s)))) >= nn
by A57, XREAL_1:6;
A59:
Comput ((P +* (stop (for-up (a,i,n,I)))),s,(LifeSpan ((P +* (stop (for-up (a,i,n,I)))),s))) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),nn)
by A56, A57, EXTPRO_1:4;
then
CurInstr ((P +* (stop (for-up (a,i,n,I)))),(Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),nn))) = halt SCMPDS
by A15, EXTPRO_1:def 15;
then
nn >= LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
by A42, EXTPRO_1:def 15;
then
nn = LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
by A58, XXREAL_0:1;
then
Result ((P +* (stop (for-up (a,i,n,I)))),s) = Comput ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))),(LifeSpan ((P +* (stop (for-up (a,i,n,I)))),(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))))
by A15, A59, EXTPRO_1:23;
hence
IExec ((for-up (a,i,n,I)),P,s) = IExec ((for-up (a,i,n,I)),P,(Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))))
by A42, EXTPRO_1:23; verum