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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) holds
( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) implies ( 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 i2 = AddTo (a,i,n);
set i3 = goto (- ((card I) + 2));
assume A1: s . (DataLoc ((s . a),i)) < 0 ; :: thesis: ( DataLoc ((s . a),i) in X or not n > 0 or not a <> DataLoc ((s . a),i) or ex t being State of SCMPDS ex Q being Instruction-Sequence of SCMPDS st
( ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & not ( (IExec (I,Q,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ) or ( 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,(Initialize t))) . a = t . a & (IExec (I,Q,(Initialize t))) . (DataLoc ((s . a),i)) = t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for y being Int_position st y in X holds
(IExec (I,Q,(Initialize t))) . y = t . y ) ) ; :: thesis: ( 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 A10, Th33; :: 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)))),(Initialize t),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)))),(Initialize t),(0 + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),0))) by EXTPRO_1:3
.= Exec (((a,i) >=0_goto ((card I) + 3)),(Initialize t)) by A13, SCMPDS_6:11 ;
for a being Int_position holds (Initialize t) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) . a by A14, SCMPDS_2:57;
then A15: DataPart (Initialize t) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) by SCMPDS_4:8;
A16: (IExec (I,Q,(Initialize t))) . (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 A8, XREAL_1:20;
then A18: (- n) - (t . (DataLoc ((s . a),i))) <= k by A17, XXREAL_0:2;
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 (Start-At (0,SCMPDS)) by SCMPDS_4:18;
set m2 = LifeSpan ((Q +* (stop I)),(Initialize t));
set t5 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))));
set Q5 = Q +* (stop (for-up (a,i,n,I)));
set l1 = (card I) + 1;
A22: IC (Initialize t) = 0 by MEMSTR_0:def 11;
set m3 = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1;
set t6 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)),(Initialize t))) + 1) + 1) + 1;
set t8 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1));
set Q8 = Q +* (stop (for-up (a,i,n,I)));
set t7 = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1));
set Q7 = Q +* (stop (for-up (a,i,n,I)));
A24: (IExec (I,Q,(Initialize t))) . 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 A27, XBOOLE_1:1;
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 A28, XBOOLE_1:1;
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 (Initialize t) by A30;
then A31: 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 A10, FUNCT_4:11
.= t . (DataLoc ((s . a),i)) by A21, FUNCT_4:11 ;
then A32: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)) = 0 + 1 by A22, A11, A14, SCMPDS_2:57;
then A33: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = (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)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) = (Q +* (stop (for-up (a,i,n,I)))) . (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by PBOOLE:143;
A35: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t)))) by EXTPRO_1:4;
then A36: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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 A23, A28, GRFUNC_1:2
.= AddTo (a,i,n) by Th32 ;
A37: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (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-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) by A36 ;
then A38: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) = (IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1)))) + 1 by SCMPDS_2:48
.= (card I) + (1 + 1) by A33, A35 ;
then A39: CurInstr ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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 A28, A26, GRFUNC_1:2
.= goto (- ((card I) + 2)) by Th32 ;
A40: Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) = Following ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (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-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) by A39 ;
then IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = ICplusConst ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))),(0 - ((card I) + 2))) by SCMPDS_2:54
.= 0 by A38, Th1 ;
then A41: Initialize (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) = Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by MEMSTR_0:46;
A42: DataPart (Comput ((Q +* (stop I)),(Initialize t),(LifeSpan ((Q +* (stop I)),(Initialize t))))) = DataPart (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) 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)))),(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 A10, A24, A30, EXTPRO_1:23 ;
then DataLoc (((Comput ((Q +* (stop (for-up (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-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . a = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a by A4, A37, SCMPDS_2:48
.= s . a by A43, EXTPRO_1:4 ;
then A44: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . a = s . a by A40, SCMPDS_2:54;
A45: now :: thesis: for x being Int_position st x in X holds
(Comput ((Q +* (stop (for-up (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-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x )
assume A46: x in X ; :: thesis: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x
(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (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 A42, SCMPDS_4:8
.= (IExec (I,Q,(Initialize t))) . x by A30, EXTPRO_1:23
.= t . x by A5, A9, A10, A46
.= s . x by A9, A46 ;
then (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = s . x by A2, A43, A35, A37, A46, SCMPDS_2:48;
hence (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . x = s . x by A40, SCMPDS_2:54; :: thesis: verum
end;
A47: (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (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 A42, SCMPDS_4:8
.= t . (DataLoc ((s . a),i)) by A16, A30, EXTPRO_1:23 ;
(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i)) by A40, SCMPDS_2:54
.= (t . (DataLoc ((s . a),i))) + n by A43, A47, A35, A37, SCMPDS_2:48 ;
then A48: - ((Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)))),(Initialize t),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)))),(Initialize t),b1)) in dom (stop (for-up (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-up (a,i,n,I)))),(Initialize t),b1)) in dom (stop (for-up (a,i,n,I)))
then k <= ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 by INT_1:7;
then A50: ( 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 A50, NAT_1:8;
suppose A51: k <= LifeSpan ((Q +* (stop I)),(Initialize t)) ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),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)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A25, A22; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),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)),(Initialize t),kn)) as Nat ;
kn < k by A52, XREAL_1:29;
then kn < LifeSpan ((Q +* (stop I)),(Initialize t)) by A51, XXREAL_0:2;
then (IC (Comput ((Q +* (stop I)),(Initialize t),kn))) + 1 = IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),1)),kn)) by A12, A31, A20, A32, A15, A29, Th14;
then A53: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) = lm + 1 by A52, EXTPRO_1:4;
IC (Comput ((Q +* (stop I)),(Initialize t),kn)) in dom (stop I) by A19, SCMPDS_6:def 2;
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 A54, XXREAL_0:2;
then lm + 1 < card (stop (for-up (a,i,n,I))) by Lm2;
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A53, AFINSQ_1:66; :: thesis: verum
end;
end;
end;
end;
suppose A55: k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))
(card I) + 1 in dom (stop (for-up (a,i,n,I))) by A23, COMPOS_1:62;
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),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)),(Initialize t))) + 1) + 1 ; :: thesis: IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I)))
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A38, A26, 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-up (a,i,n,I)))),(Initialize t),b1)) in dom (stop (for-up (a,i,n,I)))
then consider nn being Nat such that
A56: k = ((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1) + nn by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)))),nn) by A41, A56, EXTPRO_1:4;
hence IC (Comput ((Q +* (stop (for-up (a,i,n,I)))),(Initialize t),k)) in dom (stop (for-up (a,i,n,I))) by A49, SCMPDS_6:def 2; :: 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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 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)))),(Initialize t),((((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1) + 1)) by A41, A57, SCMPDS_6:def 3;
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 A1, INT_1:3;
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 A59, Th33; :: 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