let P be Instruction-Sequence of SCMPDS; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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) ; :: thesis: ( 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 ) ) ; :: thesis: 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 ;

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 ;

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; :: thesis: verum

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; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: ( 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) ; :: thesis: ( 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 ) ) ; :: thesis: 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 :: thesis: for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),Pend;

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;per 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 )
;

end;

suppose
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) >= 0
; :: thesis: for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),P

hence
for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),P
by Th33; :: thesis: verum

end;suppose A37:
(IExec ((I ';' (AddTo (a,i,n))),P,s)) . (DataLoc (((IExec ((I ';' (AddTo (a,i,n))),P,s)) . a),i)) < 0
; :: thesis: for-up (a,i,n,I) is_halting_on IExec ((I ';' (AddTo (a,i,n))),P,s),P

end;

now :: thesis: 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 ) )

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; :: thesis: verumfor 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: ( (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 ) )

(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; :: thesis: ( 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; :: thesis: verum

end;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; :: thesis: ( ( 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 ; :: thesis: ( (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 :: thesis: for x being Int_position st x in X holds

t . x = s . x

hence
(IExec (I,Q,(Initialize t))) . a = t . a
by A14, A36, A39; :: thesis: ( (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 t . x = s . x

let x be Int_position; :: thesis: ( x in X implies t . x = s . x )

assume A41: x in X ; :: thesis: t . x = s . x

hence 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 ;

:: thesis: verum

end;assume A41: x in X ; :: thesis: t . x = s . x

hence 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 ;

:: thesis: verum

(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; :: thesis: ( 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; :: thesis: verum

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 :: thesis: 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))) . x

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;let x be Int_position; :: thesis: (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . b_{1} = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . b_{1}

A50: 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;

end;A50: 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) )
;

end;

suppose
x = DataLoc ((s . a),i)
; :: thesis: (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . b_{1} = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . b_{1}

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 A49, A28, A50, FUNCT_4:11; :: thesis: verum

end;suppose A52:
x <> DataLoc ((s . a),i)
; :: thesis: (Comput ((P +* (stop (for-up (a,i,n,I)))),s,((((LifeSpan ((P +* (stop I)),s)) + 1) + 1) + 1))) . b_{1} = (Initialize (IExec ((I ';' (AddTo (a,i,n))),P,s))) . b_{1}

A53: (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; :: thesis: verum

end;.= (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; :: thesis: verum

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; :: thesis: verum