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

set b = DataLoc ((s . a),i);
set FOR = for-down (a,i,n,I);
set pFOR = stop (for-down (a,i,n,I));
set pI = stop 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 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 = s . x ) & t . a = s . a & not ( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,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,t)) . y = t . y ) ) ) or ( for-down (a,i,n,I) is_closed_on s,P & for-down (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-down (a,i,n,I) is_closed_on t,Q & for-down (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 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 = s . x ) & t . a = s . a & not ( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,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,t)) . y = t . y ) ) ) or ( for-down (a,i,n,I) is_closed_on s,P & for-down (a,i,n,I) is_halting_on s,P ) )

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

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

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