let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let I be halt-free shiftable Program of SCMPDS; :: thesis: for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let a be Int_position; :: thesis: for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let i, c be Integer; :: thesis: for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let X, Y be set ; :: thesis: for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let f be Function of (product (the_Values_of SCMPDS)),NAT; :: thesis: ( s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

A1: Initialize s = s by MEMSTR_0:44;

set b = DataLoc ((s . a),i);

set WHL = while>0 (a,i,I);

set pWHL = stop (while>0 (a,i,I));

set P1 = P +* (stop (while>0 (a,i,I)));

set i1 = (a,i) <=0_goto ((card I) + 2);

set i2 = goto (- ((card I) + 1));

assume A2: s . (DataLoc ((s . a),i)) > 0 ; :: thesis: ( ex t being 0 -started State of SCMPDS st

( f . t = 0 & not t . (DataLoc ((s . a),i)) <= 0 ) or ex x being Int_position st

( x in X & not s . x >= c + (s . (DataLoc ((s . a),i))) ) or ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

set s4 = Comput ((P +* (stop (while>0 (a,i,I)))),s,1);

set P4 = P +* (stop (while>0 (a,i,I)));

A3: IC s = 0 by MEMSTR_0:def 11;

A4: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:15;

A5: Comput ((P +* (stop (while>0 (a,i,I)))),s,(0 + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,0))) by EXTPRO_1:3

.= Following ((P +* (stop (while>0 (a,i,I)))),s)

.= Exec (((a,i) <=0_goto ((card I) + 2)),s) by A4, A1, SCMPDS_6:11 ;

set m0 = LifeSpan ((P +* (stop (while>0 (a,i,I)))),s);

set Es = IExec (I,P,s);

set bj = DataLoc (((Initialize (IExec (I,P,s))) . a),i);

set EP = P;

assume A6: for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ; :: thesis: ( ex x being Int_position st

( x in X & not s . x >= c + (s . (DataLoc ((s . a),i))) ) or ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

assume A7: for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis: ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

assume A8: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis: IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

then while>0 (a,i,I) is_halting_on s,P by A6, A7, Th22;

then A9: P +* (stop (while>0 (a,i,I))) halts_on s by A1, SCMPDS_6:def 3;

A10: for x being Int_position st x in Y holds

s . x = s . x ;

A11: DataLoc (((Initialize (IExec (I,P,s))) . a),i) = DataLoc (((IExec (I,P,s)) . a),i) by SCMPDS_5:15

.= DataLoc ((s . a),i) by A2, A7, A8, A10 ;

set PI = P +* (stop I);

set m1 = (LifeSpan ((P +* (stop I)),s)) + 2;

set s2 = Initialize (IExec (I,P,s));

set P2 = P +* (stop (while>0 (a,i,I)));

set m2 = LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))));

A12: stop I c= P +* (stop I) by FUNCT_4:25;

A13: (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by SCMPDS_5:15

.= s . a by A2, A7, A8, A10 ;

(Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)))

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

then A29: P +* (stop (while>0 (a,i,I))) halts_on Initialize (Initialize (IExec (I,P,s))) by SCMPDS_6:def 3;

for a being Int_position holds s . a = (Comput ((P +* (stop (while>0 (a,i,I)))),s,1)) . a by A5, SCMPDS_2:56;

then A30: DataPart s = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),s,1)) by SCMPDS_4:8;

set mI = LifeSpan ((P +* (stop I)),s);

set s5 = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)));

set P5 = P +* (stop (while>0 (a,i,I)));

set l1 = (card I) + 1;

A31: while>0 (a,i,I) c= stop (while>0 (a,i,I)) by AFINSQ_1:74;

stop (while>0 (a,i,I)) c= P +* (stop (while>0 (a,i,I))) by FUNCT_4:25;

then A32: while>0 (a,i,I) c= P +* (stop (while>0 (a,i,I))) by A31, XBOOLE_1:1;

set m3 = (LifeSpan ((P +* (stop I)),s)) + 1;

set s7 = Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1));

set P7 = P +* (stop (while>0 (a,i,I)));

set s6 = Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1));

set P6 = P +* (stop (while>0 (a,i,I)));

(card I) + 1 < (card I) + 2 by XREAL_1:6;

then A33: (card I) + 1 in dom (while>0 (a,i,I)) by Th16;

Shift (I,1) c= while>0 (a,i,I) by Lm4;

then A34: Shift (I,1) c= P +* (stop (while>0 (a,i,I))) by A32, XBOOLE_1:1;

I is_halting_on s,P by A2, A7, A8, A10;

then A35: P +* (stop I) halts_on s by A1, SCMPDS_6:def 3;

(P +* (stop I)) +* (stop I) halts_on s by A35;

then A36: I is_halting_on s,P +* (stop I) by A1, SCMPDS_6:def 3;

A37: IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,1)) = (IC s) + 1 by A2, A5, SCMPDS_2:56

.= 0 + 1 by A3 ;

A38: I is_closed_on s,P +* (stop I) by A2, A7, A8, A10;

then A39: IC (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) = (card I) + 1 by A12, A36, A37, A30, A34, SCMPDS_7:18;

A40: (P +* (stop (while>0 (a,i,I)))) /. (IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (while>0 (a,i,I)))) . (IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;

A41: Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)) = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s))) by EXTPRO_1:4;

then A42: CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (while>0 (a,i,I)))) . ((card I) + 1) by A12, A36, A38, A37, A30, A34, A40, SCMPDS_7:18

.= (while>0 (a,i,I)) . ((card I) + 1) by A33, A32, GRFUNC_1:2

.= goto (- ((card I) + 1)) by Th17 ;

A43: Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by EXTPRO_1:3

.= Exec ((goto (- ((card I) + 1))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by A42 ;

then IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))),(0 - ((card I) + 1))) by SCMPDS_2:54

.= 0 by A39, A41, SCMPDS_7:1 ;

then A44: IC (Initialize (IExec (I,P,s))) = IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2))) by MEMSTR_0:def 11;

A45: DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) by A12, A36, A38, A37, A30, A34, SCMPDS_7:18;

A48: Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2)) = Initialize (IExec (I,P,s)) by A47, A44, MEMSTR_0:78;

then CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2)))) = (a,i) <=0_goto ((card I) + 2) by A4, SCMPDS_6:11;

then LifeSpan ((P +* (stop (while>0 (a,i,I)))),s) > (LifeSpan ((P +* (stop I)),s)) + 2 by A9, EXTPRO_1:36, SCMPDS_6:17;

then consider nn being Nat such that

A49: LifeSpan ((P +* (stop (while>0 (a,i,I)))),s) = ((LifeSpan ((P +* (stop I)),s)) + 2) + nn by NAT_1:10;

reconsider nn = nn as Nat ;

Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))))))) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by A48, EXTPRO_1:4;

then CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))))))))) = halt SCMPDS by A29, EXTPRO_1:def 15;

then ((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))))) >= LifeSpan ((P +* (stop (while>0 (a,i,I)))),s) by A9, EXTPRO_1:def 15;

then A50: LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) >= nn by A49, XREAL_1:6;

A51: Comput ((P +* (stop (while>0 (a,i,I)))),s,(LifeSpan ((P +* (stop (while>0 (a,i,I)))),s))) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),nn) by A48, A49, EXTPRO_1:4;

then CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),nn))) = halt SCMPDS by A9, EXTPRO_1:def 15;

then nn >= LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A29, EXTPRO_1:def 15;

then nn = LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A50, XXREAL_0:1;

then Result ((P +* (stop (while>0 (a,i,I)))),s) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by A9, A51, EXTPRO_1:23;

hence IExec ((while>0 (a,i,I)),P,s) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by SCMPDS_4:def 5

.= Result ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A29, EXTPRO_1:23

.= IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) by SCMPDS_4:def 5 ;

:: thesis: verum

for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let s be 0 -started State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS

for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let I be halt-free shiftable Program of SCMPDS; :: thesis: for a being Int_position

for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let a be Int_position; :: thesis: for i, c being Integer

for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let i, c be Integer; :: thesis: for X, Y being set

for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let X, Y be set ; :: thesis: for f being Function of (product (the_Values_of SCMPDS)),NAT st s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) holds

IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

let f be Function of (product (the_Values_of SCMPDS)),NAT; :: thesis: ( s . (DataLoc ((s . a),i)) > 0 & ( for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ) & ( for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ) & ( for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) implies IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

A1: Initialize s = s by MEMSTR_0:44;

set b = DataLoc ((s . a),i);

set WHL = while>0 (a,i,I);

set pWHL = stop (while>0 (a,i,I));

set P1 = P +* (stop (while>0 (a,i,I)));

set i1 = (a,i) <=0_goto ((card I) + 2);

set i2 = goto (- ((card I) + 1));

assume A2: s . (DataLoc ((s . a),i)) > 0 ; :: thesis: ( ex t being 0 -started State of SCMPDS st

( f . t = 0 & not t . (DataLoc ((s . a),i)) <= 0 ) or ex x being Int_position st

( x in X & not s . x >= c + (s . (DataLoc ((s . a),i))) ) or ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

set s4 = Comput ((P +* (stop (while>0 (a,i,I)))),s,1);

set P4 = P +* (stop (while>0 (a,i,I)));

A3: IC s = 0 by MEMSTR_0:def 11;

A4: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:15;

A5: Comput ((P +* (stop (while>0 (a,i,I)))),s,(0 + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,0))) by EXTPRO_1:3

.= Following ((P +* (stop (while>0 (a,i,I)))),s)

.= Exec (((a,i) <=0_goto ((card I) + 2)),s) by A4, A1, SCMPDS_6:11 ;

set m0 = LifeSpan ((P +* (stop (while>0 (a,i,I)))),s);

set Es = IExec (I,P,s);

set bj = DataLoc (((Initialize (IExec (I,P,s))) . a),i);

set EP = P;

assume A6: for t being 0 -started State of SCMPDS st f . t = 0 holds

t . (DataLoc ((s . a),i)) <= 0 ; :: thesis: ( ex x being Int_position st

( x in X & not s . x >= c + (s . (DataLoc ((s . a),i))) ) or ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

assume A7: for x being Int_position st x in X holds

s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis: ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st

( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 & not ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ) or IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) )

assume A8: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis: IExec ((while>0 (a,i,I)),P,s) = IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s))))

then while>0 (a,i,I) is_halting_on s,P by A6, A7, Th22;

then A9: P +* (stop (while>0 (a,i,I))) halts_on s by A1, SCMPDS_6:def 3;

A10: for x being Int_position st x in Y holds

s . x = s . x ;

A11: DataLoc (((Initialize (IExec (I,P,s))) . a),i) = DataLoc (((IExec (I,P,s)) . a),i) by SCMPDS_5:15

.= DataLoc ((s . a),i) by A2, A7, A8, A10 ;

set PI = P +* (stop I);

set m1 = (LifeSpan ((P +* (stop I)),s)) + 2;

set s2 = Initialize (IExec (I,P,s));

set P2 = P +* (stop (while>0 (a,i,I)));

set m2 = LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))));

A12: stop I c= P +* (stop I) by FUNCT_4:25;

A13: (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by SCMPDS_5:15

.= s . a by A2, A7, A8, A10 ;

A14: now :: thesis: for t being 0 -started State of SCMPDS

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

A22:
for x being Int_position st x in X holds for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 implies ( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) )

assume that

A15: for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) and

A16: for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x and

A17: t . a = (Initialize (IExec (I,P,s))) . a and

A18: t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 ; :: thesis: ( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

.= t . a by A8, A13, A15, A17, A18, A19 ; :: thesis: ( I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

A21: t . a = (IExec (I,P,s)) . a by A17, SCMPDS_5:15

.= s . a by A2, A7, A8, A10 ;

hence ( I is_closed_on t,Q & I is_halting_on t,Q ) by A8, A15, A17, A18, A19; :: thesis: ( f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus f . (Initialize (IExec (I,Q,t))) < f . t by A8, A15, A17, A18, A19, A21; :: thesis: ( ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) :: thesis: for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x

(IExec (I,Q,t)) . x = t . x by A8, A15, A17, A18, A19, A21; :: thesis: verum

end;t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 implies ( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) )

assume that

A15: for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) and

A16: for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x and

A17: t . a = (Initialize (IExec (I,P,s))) . a and

A18: t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 ; :: thesis: ( (Initialize (IExec (I,Q,t))) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

A19: now :: thesis: for x being Int_position st x in Y holds

t . x = s . x

thus (Initialize (IExec (I,Q,t))) . a =
(IExec (I,Q,t)) . a
by SCMPDS_5:15
t . x = s . x

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

assume A20: x in Y ; :: thesis: t . x = s . x

hence t . x = (Initialize (IExec (I,P,s))) . x by A16

.= (IExec (I,P,s)) . x by SCMPDS_5:15

.= s . x by A2, A7, A8, A10, A20 ;

:: thesis: verum

end;assume A20: x in Y ; :: thesis: t . x = s . x

hence t . x = (Initialize (IExec (I,P,s))) . x by A16

.= (IExec (I,P,s)) . x by SCMPDS_5:15

.= s . x by A2, A7, A8, A10, A20 ;

:: thesis: verum

.= t . a by A8, A13, A15, A17, A18, A19 ; :: thesis: ( I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

A21: t . a = (IExec (I,P,s)) . a by A17, SCMPDS_5:15

.= s . a by A2, A7, A8, A10 ;

hence ( I is_closed_on t,Q & I is_halting_on t,Q ) by A8, A15, A17, A18, A19; :: thesis: ( f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus f . (Initialize (IExec (I,Q,t))) < f . t by A8, A15, A17, A18, A19, A21; :: thesis: ( ( for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus for x being Int_position st x in X holds

(Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) :: thesis: for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x

proof

thus
for x being Int_position st x in Y holds
let x be Int_position; :: thesis: ( x in X implies (Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) )

( (Initialize (IExec (I,Q,t))) . x = (IExec (I,Q,t)) . x & (Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) = (IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) ) by SCMPDS_5:15;

hence ( x in X implies (Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) by A8, A13, A15, A17, A18, A19; :: thesis: verum

end;( (Initialize (IExec (I,Q,t))) . x = (IExec (I,Q,t)) . x & (Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) = (IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) ) by SCMPDS_5:15;

hence ( x in X implies (Initialize (IExec (I,Q,t))) . x >= c + ((Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) by A8, A13, A15, A17, A18, A19; :: thesis: verum

(IExec (I,Q,t)) . x = t . x by A8, A15, A17, A18, A19, A21; :: thesis: verum

(Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)))

proof

for t being 0 -started State of SCMPDS
let x be Int_position; :: thesis: ( x in X implies (Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) )

A23: (Initialize (IExec (I,P,s))) . x = (IExec (I,P,s)) . x by SCMPDS_5:15;

A24: (Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) = (IExec (I,P,s)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) by SCMPDS_5:15;

assume x in X ; :: thesis: (Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)))

hence (Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) by A2, A7, A8, A10, A13, A23, A24; :: thesis: verum

end;A23: (Initialize (IExec (I,P,s))) . x = (IExec (I,P,s)) . x by SCMPDS_5:15;

A24: (Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) = (IExec (I,P,s)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) by SCMPDS_5:15;

assume x in X ; :: thesis: (Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)))

hence (Initialize (IExec (I,P,s))) . x >= c + ((Initialize (IExec (I,P,s))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) by A2, A7, A8, A10, A13, A23, A24; :: thesis: verum

for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

proof

then
while>0 (a,i,I) is_halting_on Initialize (IExec (I,P,s)),P
by A6, A11, Th22, A22;
let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 implies ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) )

assume that

A25: for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) and

A26: for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x and

A27: t . a = (Initialize (IExec (I,P,s))) . a and

A28: t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 ; :: thesis: ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus (IExec (I,Q,t)) . a = (Initialize (IExec (I,Q,t))) . a by SCMPDS_5:15

.= t . a by A14, A25, A26, A27, A28 ; :: thesis: ( I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A14, A25, A26, A27, A28; :: thesis: ( f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus f . (Initialize (IExec (I,Q,t))) < f . t by A14, A25, A26, A27, A28; :: thesis: ( ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) :: thesis: for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x

(IExec (I,Q,t)) . x = t . x by A14, A25, A26, A27, A28; :: thesis: verum

end;t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 holds

( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( ( for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x ) & t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 implies ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) ) )

assume that

A25: for x being Int_position st x in X holds

t . x >= c + (t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) and

A26: for x being Int_position st x in Y holds

t . x = (Initialize (IExec (I,P,s))) . x and

A27: t . a = (Initialize (IExec (I,P,s))) . a and

A28: t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > 0 ; :: thesis: ( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus (IExec (I,Q,t)) . a = (Initialize (IExec (I,Q,t))) . a by SCMPDS_5:15

.= t . a by A14, A25, A26, A27, A28 ; :: thesis: ( I is_closed_on t,Q & I is_halting_on t,Q & f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus ( I is_closed_on t,Q & I is_halting_on t,Q ) by A14, A25, A26, A27, A28; :: thesis: ( f . (Initialize (IExec (I,Q,t))) < f . t & ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus f . (Initialize (IExec (I,Q,t))) < f . t by A14, A25, A26, A27, A28; :: thesis: ( ( for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) & ( for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x ) )

thus for x being Int_position st x in X holds

(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) :: thesis: for x being Int_position st x in Y holds

(IExec (I,Q,t)) . x = t . x

proof

thus
for x being Int_position st x in Y holds
let x be Int_position; :: thesis: ( x in X implies (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) )

( (IExec (I,Q,t)) . x = (Initialize (IExec (I,Q,t))) . x & (IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) = (Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) ) by SCMPDS_5:15;

hence ( x in X implies (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) by A14, A25, A26, A27, A28; :: thesis: verum

end;( (IExec (I,Q,t)) . x = (Initialize (IExec (I,Q,t))) . x & (IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) = (Initialize (IExec (I,Q,t))) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) ) by SCMPDS_5:15;

hence ( x in X implies (IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i))) ) by A14, A25, A26, A27, A28; :: thesis: verum

(IExec (I,Q,t)) . x = t . x by A14, A25, A26, A27, A28; :: thesis: verum

then A29: P +* (stop (while>0 (a,i,I))) halts_on Initialize (Initialize (IExec (I,P,s))) by SCMPDS_6:def 3;

for a being Int_position holds s . a = (Comput ((P +* (stop (while>0 (a,i,I)))),s,1)) . a by A5, SCMPDS_2:56;

then A30: DataPart s = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),s,1)) by SCMPDS_4:8;

set mI = LifeSpan ((P +* (stop I)),s);

set s5 = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)));

set P5 = P +* (stop (while>0 (a,i,I)));

set l1 = (card I) + 1;

A31: while>0 (a,i,I) c= stop (while>0 (a,i,I)) by AFINSQ_1:74;

stop (while>0 (a,i,I)) c= P +* (stop (while>0 (a,i,I))) by FUNCT_4:25;

then A32: while>0 (a,i,I) c= P +* (stop (while>0 (a,i,I))) by A31, XBOOLE_1:1;

set m3 = (LifeSpan ((P +* (stop I)),s)) + 1;

set s7 = Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1));

set P7 = P +* (stop (while>0 (a,i,I)));

set s6 = Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1));

set P6 = P +* (stop (while>0 (a,i,I)));

(card I) + 1 < (card I) + 2 by XREAL_1:6;

then A33: (card I) + 1 in dom (while>0 (a,i,I)) by Th16;

Shift (I,1) c= while>0 (a,i,I) by Lm4;

then A34: Shift (I,1) c= P +* (stop (while>0 (a,i,I))) by A32, XBOOLE_1:1;

I is_halting_on s,P by A2, A7, A8, A10;

then A35: P +* (stop I) halts_on s by A1, SCMPDS_6:def 3;

(P +* (stop I)) +* (stop I) halts_on s by A35;

then A36: I is_halting_on s,P +* (stop I) by A1, SCMPDS_6:def 3;

A37: IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,1)) = (IC s) + 1 by A2, A5, SCMPDS_2:56

.= 0 + 1 by A3 ;

A38: I is_closed_on s,P +* (stop I) by A2, A7, A8, A10;

then A39: IC (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) = (card I) + 1 by A12, A36, A37, A30, A34, SCMPDS_7:18;

A40: (P +* (stop (while>0 (a,i,I)))) /. (IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (while>0 (a,i,I)))) . (IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;

A41: Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)) = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s))) by EXTPRO_1:4;

then A42: CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (while>0 (a,i,I)))) . ((card I) + 1) by A12, A36, A38, A37, A30, A34, A40, SCMPDS_7:18

.= (while>0 (a,i,I)) . ((card I) + 1) by A33, A32, GRFUNC_1:2

.= goto (- ((card I) + 1)) by Th17 ;

A43: Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by EXTPRO_1:3

.= Exec ((goto (- ((card I) + 1))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by A42 ;

then IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))),(0 - ((card I) + 1))) by SCMPDS_2:54

.= 0 by A39, A41, SCMPDS_7:1 ;

then A44: IC (Initialize (IExec (I,P,s))) = IC (Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2))) by MEMSTR_0:def 11;

A45: DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) by A12, A36, A38, A37, A30, A34, SCMPDS_7:18;

now :: thesis: for x being Int_position holds (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (Initialize (IExec (I,P,s))) . x

then A47:
DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) = DataPart (Initialize (IExec (I,P,s)))
by SCMPDS_4:8;let x be Int_position; :: thesis: (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (Initialize (IExec (I,P,s))) . x

A46: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

(Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x = (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . x by A45, SCMPDS_4:8

.= (Result ((P +* (stop I)),s)) . x by A35, EXTPRO_1:23

.= (IExec (I,P,s)) . x by SCMPDS_4:def 5 ;

hence (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (IExec (I,P,s)) . x by A41, A43, SCMPDS_2:54

.= (Initialize (IExec (I,P,s))) . x by A46, FUNCT_4:11 ;

:: thesis: verum

end;A46: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;

(Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x = (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . x by A45, SCMPDS_4:8

.= (Result ((P +* (stop I)),s)) . x by A35, EXTPRO_1:23

.= (IExec (I,P,s)) . x by SCMPDS_4:def 5 ;

hence (Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (IExec (I,P,s)) . x by A41, A43, SCMPDS_2:54

.= (Initialize (IExec (I,P,s))) . x by A46, FUNCT_4:11 ;

:: thesis: verum

A48: Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2)) = Initialize (IExec (I,P,s)) by A47, A44, MEMSTR_0:78;

then CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2)))) = (a,i) <=0_goto ((card I) + 2) by A4, SCMPDS_6:11;

then LifeSpan ((P +* (stop (while>0 (a,i,I)))),s) > (LifeSpan ((P +* (stop I)),s)) + 2 by A9, EXTPRO_1:36, SCMPDS_6:17;

then consider nn being Nat such that

A49: LifeSpan ((P +* (stop (while>0 (a,i,I)))),s) = ((LifeSpan ((P +* (stop I)),s)) + 2) + nn by NAT_1:10;

reconsider nn = nn as Nat ;

Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))))))) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by A48, EXTPRO_1:4;

then CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))))))))) = halt SCMPDS by A29, EXTPRO_1:def 15;

then ((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))))) >= LifeSpan ((P +* (stop (while>0 (a,i,I)))),s) by A9, EXTPRO_1:def 15;

then A50: LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) >= nn by A49, XREAL_1:6;

A51: Comput ((P +* (stop (while>0 (a,i,I)))),s,(LifeSpan ((P +* (stop (while>0 (a,i,I)))),s))) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),nn) by A48, A49, EXTPRO_1:4;

then CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),nn))) = halt SCMPDS by A9, EXTPRO_1:def 15;

then nn >= LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A29, EXTPRO_1:def 15;

then nn = LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A50, XXREAL_0:1;

then Result ((P +* (stop (while>0 (a,i,I)))),s) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by A9, A51, EXTPRO_1:23;

hence IExec ((while>0 (a,i,I)),P,s) = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by SCMPDS_4:def 5

.= Result ((P +* (stop (while>0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A29, EXTPRO_1:23

.= IExec ((while>0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) by SCMPDS_4:def 5 ;

:: thesis: verum