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 S₁[ 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 S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[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
(Initialize t) . x = s . x

proof

let x be Int_position; :: thesis: ( x in X implies (Initialize t) . x = s . x )
assume x in X ; :: thesis: (Initialize t) . 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 A11, Th42; :: 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)))),(Initialize t),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)))),(Initialize t),(0 + 1)) = Following ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),0))) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 3)),(Initialize t)) by A15, SCMPDS_6:11 ;
for a being Int_position holds (Initialize t) . a = (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)) . a by A16, SCMPDS_2:56;
then A17: DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)) by SCMPDS_4:8;
A18: (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = (Initialize t) . (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 A8, XREAL_1:20;
then A20: (- n) + (t . (DataLoc ((s . a),i))) <= k by A19, XXREAL_0:2;
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 (Start-At (0,SCMPDS)) by SCMPDS_4:18;
set m2 = LifeSpan ((Q +* (stop I)),(Initialize t));
set t5 = Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))));
set Q5 = Q +* (stop (for-down (a,i,n,I)));
set l1 = (card I) + 1;
A24: IC (Initialize t) = 0 by MEMSTR_0:def 11;
set m3 = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1;
set t6 = Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)),(Initialize t))) + 1) + 1) + 1;
set t8 = Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1));
set Q8 = Q +* (stop (for-down (a,i,n,I)));
set t7 = Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1));
set Q7 = Q +* (stop (for-down (a,i,n,I)));
A26: (IExec (I,Q,(Initialize t))) . a = (Initialize t) . 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 A29, XBOOLE_1:1;
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 A30, XBOOLE_1:1;
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 (Initialize t) by A32;
then A33: I is_halting_on Initialize t,Q +* (stop I) by SCMPDS_6:def 3;
not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
then (Initialize t) . (DataLoc (((Initialize t) . a),i)) = (Initialize t) . (DataLoc ((s . a),i)) by A11, FUNCT_4:11
.= t . (DataLoc ((s . a),i)) by A23, FUNCT_4:11 ;
then A34: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)) = 0 + 1 by A24, A13, A16, SCMPDS_2:56;
then A35: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = (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)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (for-down (a,i,n,I)))) . (IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by PBOOLE:143;
A37: Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)) = Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t)))) by EXTPRO_1:4;
then A38: CurInstr ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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 A25, A30, GRFUNC_1:2
.= AddTo (a,i,(- n)) by Th41 ;
A39: Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)) = Following ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by EXTPRO_1:3
.= Exec ((AddTo (a,i,(- n))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by A38 ;
then A40: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) = (IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) + 1 by SCMPDS_2:48
.= (card I) + (1 + 1) by A35, A37 ;
then A41: CurInstr ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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 A30, A28, GRFUNC_1:2
.= goto (- ((card I) + 2)) by Th41 ;
A42: Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) = Following ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card I) + 2))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by A41 ;
then IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:54
.= 0 by A40, Th1 ;
then A43: Initialize (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by MEMSTR_0:46;
A44: DataPart (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = DataPart (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) 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)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . a by SCMPDS_4:8
.= s . a by A11, A26, A32, EXTPRO_1:23 ;
then DataLoc (((Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a),i) = DataLoc ((s . a),i) by EXTPRO_1:4;
then (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . a = (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a by A4, A39, SCMPDS_2:48
.= s . a by A45, EXTPRO_1:4 ;
then A46: (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . a = s . a by A42, SCMPDS_2:54;

A47: now :: thesis: for x being Int_position st x in X holds
(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x )
assume A48: x in X ; :: thesis: (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x
(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x by A44, SCMPDS_4:8
.= (IExec (I,Q,(Initialize t))) . x by A32, EXTPRO_1:23
.= (Initialize t) . x by A5, A48, A10, A12
.= t . x by SCMPDS_5:15
.= s . x by A9, A48 ;
then (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x by A2, A45, A37, A39, A48, SCMPDS_2:48;
hence (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x by A42, SCMPDS_2:54; :: thesis: verum

end;

A49: (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i)) by A44, SCMPDS_4:8
.= t . (DataLoc ((s . a),i)) by A18, A32, EXTPRO_1:23 ;
A50: (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i)) by A42, SCMPDS_2:54
.= (t . (DataLoc ((s . a),i))) + (- n) by A45, A49, A37, A39, SCMPDS_2:48 ;
then A51: for-down (a,i,n,I) is_closed_on Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)))),(Initialize t),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)))),(Initialize t),b₁)) in dom (stop (for-down (a,i,n,I)))

per cases ( k < (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1 or k >= (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1 ) ;

suppose k < (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),b₁)) in dom (stop (for-down (a,i,n,I)))

then k <= ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 by INT_1:7;
then A52: ( k <= (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 or k = ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 ) by NAT_1:8;

hereby :: thesis: verum

per cases ( k <= LifeSpan ((Q +* (stop I)),(Initialize t)) or k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 or k = ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 ) by A52, NAT_1:8;

suppose A53: k <= LifeSpan ((Q +* (stop I)),(Initialize t)) ; :: thesis: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),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)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I)))

hence IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I))) by A27, A24; :: thesis: verum

end;

suppose k <> 0 ; :: thesis: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),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)),(Initialize t),kn)) as Nat ;
kn < k by A54, XREAL_1:29;
then kn < LifeSpan ((Q +* (stop I)),(Initialize t)) by A53, XXREAL_0:2;
then (IC (Comput ((Q +* (stop I)),(Initialize t),kn))) + 1 = IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),1)),kn)) by A14, A33, A22, A34, A17, A31, Th14;
then A55: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) = lm + 1 by A54, EXTPRO_1:4;
IC (Comput ((Q +* (stop I)),(Initialize t),kn)) in dom (stop I) by A21, SCMPDS_6:def 2;
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 A56, XXREAL_0:2;
then lm + 1 < card (stop (for-down (a,i,n,I))) by Lm4;
hence IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I))) by A55, AFINSQ_1:66; :: thesis: verum

end;

end;

end;

end;

suppose A57: k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I)))

(card I) + 1 in dom (stop (for-down (a,i,n,I))) by A25, COMPOS_1:62;
hence IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),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)),(Initialize t))) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I)))

hence IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I))) by A40, A28, COMPOS_1:62; :: thesis: verum

end;

end;

end;

end;

suppose k >= (((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),b₁)) in dom (stop (for-down (a,i,n,I)))

then consider nn being Nat such that
A58: k = ((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1) + nn by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)))),nn) by A43, A58, EXTPRO_1:4;
hence IC (Comput ((Q +* (stop (for-down (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-down (a,i,n,I))) by A51, SCMPDS_6:def 2; :: 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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by A43, A59, SCMPDS_6:def 3;
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 A1, INT_1:3;
A60: S₁[ 0 ] by Th42;
for k being Nat holds S₁[k] from NAT_1:sch 2(A60, A6);
then A61: S₁[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