let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

let s be 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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) holds
( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )

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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) implies ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

set b = DataLoc ((s . a),i);
set FOR = for-up (a,i,n,I);
set pFOR = stop (for-up (a,i,n,I));
set pI = stop I;
set i1 = (a,i) >=0_goto ((card I) + 3);
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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

defpred S1[ Nat] means for t being State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= \$1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q );
assume A2: 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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A3: 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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A4: 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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ) or ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) )

assume A5: 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,())) . a = t . a & (IExec (I,Q,())) . (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,())) . y = t . y ) ) ; :: thesis: ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P )
A6: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: S1[k] ; :: thesis: S1[k + 1]
let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( - (t . (DataLoc ((s . a),i))) <= k + 1 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A8: - (t . (DataLoc ((s . a),i))) <= k + 1 ; :: thesis: ( ex x being Int_position st
( x in X & not t . x = s . x ) or not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume A9: for x being Int_position st x in X holds
t . x = s . x ; :: thesis: ( not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )
assume A10: t . a = s . a ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )
per cases ( t . (DataLoc ((s . a),i)) >= 0 or t . (DataLoc ((s . a),i)) < 0 ) ;
suppose t . (DataLoc ((s . a),i)) >= 0 ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )
hence ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) by ; :: thesis: verum
end;
suppose A11: t . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )
set t2 = Initialize t;
set t3 = Initialize t;
set Q2 = Q +* (stop I);
set Q3 = Q +* (stop (for-up (a,i,n,I)));
set t4 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1);
set Q4 = Q +* (stop (for-up (a,i,n,I)));
A12: stop I c= Q +* (stop I) by FUNCT_4:25;
A13: for-up (a,i,n,I) = ((a,i) >=0_goto ((card I) + 3)) ';' ((I ';' (AddTo (a,i,n))) ';' (goto (- ((card I) + 2)))) by Th2;
A14: Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(0 + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),0))) by EXTPRO_1:3
.= Exec (((a,i) >=0_goto ((card I) + 3)),()) by ;
for a being Int_position holds () . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)) . a by ;
then A15: DataPart () = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)) by SCMPDS_4:8;
A16: (IExec (I,Q,())) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) by A5, A9, A10;
- (- n) > 0 by A3;
then - n < 0 ;
then - n <= - 1 by INT_1:8;
then A17: (- n) - (t . (DataLoc ((s . a),i))) <= (- 1) - (t . (DataLoc ((s . a),i))) by XREAL_1:9;
(- (t . (DataLoc ((s . a),i)))) - 1 <= k by ;
then A18: (- n) - (t . (DataLoc ((s . a),i))) <= k by ;
A19: I is_closed_on t,Q by A5, A9, A10;
then A20: I is_closed_on Initialize t,Q +* (stop I) by SCMPDS_6:24;
A21: not DataLoc ((s . a),i) in dom () by SCMPDS_4:18;
set m2 = LifeSpan ((Q +* (stop I)),());
set t5 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),())));
set Q5 = Q +* (stop (for-up (a,i,n,I)));
set l1 = (card I) + 1;
A22: IC () = 0 by MEMSTR_0:def 11;
set m3 = (LifeSpan ((Q +* (stop I)),())) + 1;
set t6 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1));
set Q6 = Q +* (stop (for-up (a,i,n,I)));
(card I) + 1 < (card I) + 3 by XREAL_1:6;
then A23: (card I) + 1 in dom (for-up (a,i,n,I)) by Th31;
set m5 = (((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1;
set t8 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1));
set Q8 = Q +* (stop (for-up (a,i,n,I)));
set t7 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1));
set Q7 = Q +* (stop (for-up (a,i,n,I)));
A24: (IExec (I,Q,())) . a = t . a by A5, A9, A10;
set l2 = (card I) + 2;
A25: 0 in dom (stop (for-up (a,i,n,I))) by COMPOS_1:36;
(card I) + 2 < (card I) + 3 by XREAL_1:6;
then A26: (card I) + 2 in dom (for-up (a,i,n,I)) by Th31;
A27: stop (for-up (a,i,n,I)) c= Q +* (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 A28: for-up (a,i,n,I) c= Q +* (stop (for-up (a,i,n,I))) by ;
Shift (I,1) c= for-up (a,i,n,I) by Lm3;
then A29: Shift (I,1) c= Q +* (stop (for-up (a,i,n,I))) by ;
I is_halting_on t,Q by A5, A9, A10;
then A30: Q +* (stop I) halts_on Initialize t by SCMPDS_6:def 3;
(Q +* (stop I)) +* (stop I) halts_on Initialize () by A30;
then A31: I is_halting_on Initialize t,Q +* (stop I) by SCMPDS_6:def 3;
not a in dom () by SCMPDS_4:18;
then () . (DataLoc ((() . a),i)) = () . (DataLoc ((s . a),i)) by
.= t . (DataLoc ((s . a),i)) by ;
then A32: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)) = 0 + 1 by ;
then A33: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),())))) = (card I) + 1 by A12, A31, A20, A15, A29, Th16;
A34: (Q +* (stop (for-up (a,i,n,I)))) /. (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)))) by PBOOLE:143;
A35: Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),()))) by EXTPRO_1:4;
then A36: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . ((card I) + 1) by A12, A31, A20, A32, A15, A29, Th16, A34
.= (for-up (a,i,n,I)) . ((card I) + 1) by
.= AddTo (a,i,n) by Th32 ;
A37: Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)))) by EXTPRO_1:3
.= Exec ((AddTo (a,i,n)),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)))) by A36 ;
then A38: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1))) = (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1)))) + 1 by SCMPDS_2:48
.= (card I) + (1 + 1) by ;
then A39: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . ((card I) + 2) by PBOOLE:143
.= (for-up (a,i,n,I)) . ((card I) + 2) by
.= goto (- ((card I) + 2)) by Th32 ;
A40: Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card I) + 2))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1)))) by A39 ;
then IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:54
.= 0 by ;
then A41: Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1)) by MEMSTR_0:46;
A42: DataPart (Comput ((Q +* (stop I)),(),(LifeSpan ((Q +* (stop I)),())))) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),())))) by A12, A31, A20, A32, A15, A29, Th16;
then A43: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),())))) . a = (Comput ((Q +* (stop I)),(),(LifeSpan ((Q +* (stop I)),())))) . a by SCMPDS_4:8
.= s . a by ;
then DataLoc (((Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1))) . a),i) = DataLoc ((s . a),i) by EXTPRO_1:4;
then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1))) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((LifeSpan ((Q +* (stop I)),())) + 1))) . a by
.= s . a by ;
then A44: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . a = s . a by ;
A45: now :: thesis: for x being Int_position st x in X holds
(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . x = s . x
let x be Int_position; :: thesis: ( x in X implies (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . x = s . x )
assume A46: x in X ; :: thesis: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . x = s . x
(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),())))) . x = (Comput ((Q +* (stop I)),(),(LifeSpan ((Q +* (stop I)),())))) . x by
.= (IExec (I,Q,())) . x by
.= t . x by A5, A9, A10, A46
.= s . x by ;
then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1))) . x = s . x by ;
hence (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . x = s . x by ; :: thesis: verum
end;
A47: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),(LifeSpan ((Q +* (stop I)),())))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop I)),(),(LifeSpan ((Q +* (stop I)),())))) . (DataLoc ((s . a),i)) by
.= t . (DataLoc ((s . a),i)) by ;
(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),(((LifeSpan ((Q +* (stop I)),())) + 1) + 1))) . (DataLoc ((s . a),i)) by
.= (t . (DataLoc ((s . a),i))) + n by ;
then A48: - ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1))) . (DataLoc ((s . a),i))) = (- n) - (t . (DataLoc ((s . a),i))) ;
then A49: for-up (a,i,n,I) is_closed_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1)),Q +* (stop (for-up (a,i,n,I))) by A7, A44, A45, A18;
now :: thesis: for k being Nat holds IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I)))
let k be Nat; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),b1)) in dom (stop (for-up (a,i,n,I)))
per cases ( k < (((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1 or k >= (((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1 ) ;
suppose k < (((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),b1)) in dom (stop (for-up (a,i,n,I)))
then k <= ((LifeSpan ((Q +* (stop I)),())) + 1) + 1 by INT_1:7;
then A50: ( k <= (LifeSpan ((Q +* (stop I)),())) + 1 or k = ((LifeSpan ((Q +* (stop I)),())) + 1) + 1 ) by NAT_1:8;
hereby :: thesis: verum
per cases ( k <= LifeSpan ((Q +* (stop I)),()) or k = (LifeSpan ((Q +* (stop I)),())) + 1 or k = ((LifeSpan ((Q +* (stop I)),())) + 1) + 1 ) by ;
suppose A51: k <= LifeSpan ((Q +* (stop I)),()) ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I)))
hereby :: thesis: verum
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I)))
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I))) by ; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I)))
then consider kn being Nat such that
A52: k = kn + 1 by NAT_1:6;
reconsider kn = kn as Nat ;
reconsider lm = IC (Comput ((Q +* (stop I)),(),kn)) as Nat ;
kn < k by ;
then kn < LifeSpan ((Q +* (stop I)),()) by ;
then (IC (Comput ((Q +* (stop I)),(),kn))) + 1 = IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(),1)),kn)) by A12, A31, A20, A32, A15, A29, Th14;
then A53: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) = lm + 1 by ;
IC (Comput ((Q +* (stop I)),(),kn)) in dom (stop I) by ;
then lm < card (stop I) by AFINSQ_1:66;
then lm < (card I) + 1 by COMPOS_1:55;
then A54: lm + 1 <= (card I) + 1 by INT_1:7;
(card I) + 1 < (card I) + 4 by XREAL_1:6;
then lm + 1 < (card I) + 4 by ;
then lm + 1 < card (stop (for-up (a,i,n,I))) by Lm2;
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I))) by ; :: thesis: verum
end;
end;
end;
end;
suppose A55: k = (LifeSpan ((Q +* (stop I)),())) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I)))
(card I) + 1 in dom (stop (for-up (a,i,n,I))) by ;
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I))) by A12, A31, A20, A32, A15, A29, A35, A55, Th16; :: thesis: verum
end;
suppose k = ((LifeSpan ((Q +* (stop I)),())) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I)))
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I))) by ; :: thesis: verum
end;
end;
end;
end;
suppose k >= (((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),b1)) in dom (stop (for-up (a,i,n,I)))
then consider nn being Nat such that
A56: k = ((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1) + nn by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k) = Comput (((Q +* (stop (for-up (a,i,n,I)))) +* (stop (for-up (a,i,n,I)))),(Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1)))),nn) by ;
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(),k)) in dom (stop (for-up (a,i,n,I))) by ; :: thesis: verum
end;
end;
end;
hence for-up (a,i,n,I) is_closed_on t,Q by SCMPDS_6:def 2; :: thesis: for-up (a,i,n,I) is_halting_on t,Q
A57: (Q +* (stop (for-up (a,i,n,I)))) +* (stop (for-up (a,i,n,I))) = Q +* (stop (for-up (a,i,n,I))) ;
for-up (a,i,n,I) is_halting_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1)),Q +* (stop (for-up (a,i,n,I))) by A7, A44, A45, A18, A48;
then Q +* (stop (for-up (a,i,n,I))) halts_on Comput ((Q +* (stop (for-up (a,i,n,I)))),(),((((LifeSpan ((Q +* (stop I)),())) + 1) + 1) + 1)) by ;
then Q +* (stop (for-up (a,i,n,I))) halts_on Initialize t by EXTPRO_1:22;
hence for-up (a,i,n,I) is_halting_on t,Q by SCMPDS_6:def 3; :: thesis: verum
end;
end;
end;
reconsider nn = - (s . (DataLoc ((s . a),i))) as Element of NAT by ;
A58: S1[ 0 ]
proof
let t be State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS st - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a holds
( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )

let Q be Instruction-Sequence of SCMPDS; :: thesis: ( - (t . (DataLoc ((s . a),i))) <= 0 & ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a implies ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

assume - (t . (DataLoc ((s . a),i))) <= 0 ; :: thesis: ( ex x being Int_position st
( x in X & not t . x = s . x ) or not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )

then - (t . (DataLoc ((s . a),i))) <= - 0 ;
then A59: t . (DataLoc ((s . a),i)) >= 0 by XREAL_1:24;
assume for x being Int_position st x in X holds
t . x = s . x ; :: thesis: ( not t . a = s . a or ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) )
assume t . a = s . a ; :: thesis: ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q )
hence ( for-up (a,i,n,I) is_closed_on t,Q & for-up (a,i,n,I) is_halting_on t,Q ) by ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A58, A6);
then A60: S1[nn] ;
for x being Int_position st x in X holds
s . x = s . x ;
hence ( for-up (a,i,n,I) is_closed_on s,P & for-up (a,i,n,I) is_halting_on s,P ) by A60; :: thesis: verum