let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: thesis:
let a be Int_position ; :: thesis:
let i, c be Integer; :: thesis:
let X, Y be set ; :: thesis:
let f be Function of (product the Object-Kind of SCMPDS),NAT; :: thesis:
set b = DataLoc ((s . a),i);
set WHL = while>0 (a,i,I);
set pWHL = stop (while>0 (a,i,I));
set pI = stop I;
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume card I > 0 ; :: thesis:
defpred S₁[ Element of NAT ] means for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st f . (Dstate t) <= $1 & ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a holds
( while>0 (a,i,I) is_closed_on t,Q & while>0 (a,i,I) is_halting_on t,Q );
assume A2: for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc ((s . a),i)) <= 0 ; :: thesis:
assume A3: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc ((s . a),i))) ; :: thesis:
assume A4: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) > 0 holds
( (IExec (I,Q,t)) . a = t . a & I is_closed_on t,Q & I is_halting_on t,Q & f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x >= c + ((IExec (I,Q,t)) . (DataLoc ((s . a),i))) ) & ( for x being Int_position st x in Y holds
(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis:
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A6: S₁[k] ; :: thesis:

now

let t be State of SCMPDS; :: thesis:
let Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
assume A7: f . (Dstate t) <= k + 1 ; :: thesis:
assume A8: for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ; :: thesis:
assume A9: for x being Int_position st x in Y holds
t . x = s . x ; :: thesis:
assume A10: t . a = s . a ; :: thesis:

per cases ;

suppose t . (DataLoc ((s . a),i)) <= 0 ; :: thesis:

hence ( while>0 (a,i,I) is_closed_on t,Q & while>0 (a,i,I) is_halting_on t,Q ) by A10, Th20; :: thesis:

end;

suppose A11: t . (DataLoc ((s . a),i)) > 0 ; :: thesis:

A12: dom (ProgramPart t) = NAT by COMPOS_1:34;
A13: not a in dom (t | NAT) by A12, SCMPDS_2:53;
A14: (IExec (I,Q,t)) . a = t . a by A4, A8, A9, A10, A11;
A15: 0 in dom (stop (while>0 (a,i,I))) by COMPOS_1:135;
A16: dom (ProgramPart t) = NAT by COMPOS_1:34;
A17: not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
A18: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
set t2 = Initialize t;
set Q2 = Q +* (stop I);
set t3 = Initialize t;
set Q3 = Q +* (stop (while>0 (a,i,I)));
set t4 = Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),1);
set Q4 = Q +* (stop (while>0 (a,i,I)));
A21: stop I c= Q +* (stop I) by FUNCT_4:26;
B21: Start-At (0,SCMPDS) c= Initialize t by FUNCT_4:26;
A22: Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(0 + 1)) = Following ((Q +* (stop (while>0 (a,i,I)))),(Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),0))) by EXTPRO_1:4
.= Following ((Q +* (stop (while>0 (a,i,I)))),(Initialize t)) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize t)) by A18, SCMPDS_6:22 ;

now

let a be Int_position ; :: thesis:
thus (Initialize t) . a = (Initialize t) . a
.= (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),1)) . a by A22, SCMPDS_2:68 ; :: thesis:

end;

A45: now

let x be Int_position ; :: thesis:
assume A46: x in Y ; :: thesis:
thus (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = (Comput ((Q +* (stop (while>0 (a,i,I)))),(Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x by A38, A41, SCMPDS_2:66
.= (IExec (I,Q,t)) . x by A44, SCMPDS_3:4
.= t . x by A4, A8, A9, A10, A11, A46
.= s . x by A9, A46 ; :: thesis:

end;

InsCode (goto (- ((card I) + 1))) = 0 by SCMPDS_2:21;
then InsCode (goto (- ((card I) + 1))) in {0,4,5,6} by ENUMSET1:def 2;
then A47: Dstate (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) = Dstate (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) by A41, Th3
.= Dstate (IExec (I,Q,t)) by A44, A38, Th2 ;

A48: now

f . (Dstate (IExec (I,Q,t))) < f . (Dstate t) by A4, A8, A9, A10, A11;
then A49: f . (Dstate (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) < k + 1 by A7, A47, XXREAL_0:2;
assume f . (Dstate (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)))) > k ; :: thesis:
hence contradiction by A49, INT_1:20; :: thesis:

end;

A50: (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),(Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . (DataLoc ((s . a),i)) by A38, A41, SCMPDS_2:66
.= (IExec (I,Q,t)) . (DataLoc ((s . a),i)) by A44, SCMPDS_3:4 ;

A51: now

let x be Int_position ; :: thesis:
assume A52: x in X ; :: thesis:
(Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x = (Comput ((Q +* (stop (while>0 (a,i,I)))),(Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),1)),(LifeSpan ((Q +* (stop I)),(Initialize t))))) . x by A38, A41, SCMPDS_2:66
.= (IExec (I,Q,t)) . x by A44, SCMPDS_3:4 ;
hence (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . x >= c + ((Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . (DataLoc ((s . a),i))) by A4, A8, A9, A10, A11, A50, A52; :: thesis:

end;

A53: (Comput ((Q +* (stop (while>0 (a,i,I)))),(Comput ((Q +* (stop (while>0 (a,i,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 A43, SCMPDS_4:23
.= (Result ((Q +* (stop I)),(Initialize t))) . a by A32, EXTPRO_1:23
.= s . a by A10, A14, A27, A13, FUNCT_4:12 ;
A55: (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1))) . a = (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1))) . a by A41, SCMPDS_2:66
.= s . a by A53, EXTPRO_1:5 ;
then A56: while>0 (a,i,I) is_closed_on Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),(((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1)),Q +* (stop (while>0 (a,i,I))) by A6, A51, A45, A48;

now

let k be Element of NAT ; :: thesis:

per cases ;

suppose k < ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 ; :: thesis:

then A57: k <= (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 by INT_1:20;

hereby :: thesis:

per cases by A57, NAT_1:8;

suppose A58: k <= LifeSpan ((Q +* (stop I)),(Initialize t)) ; :: thesis:

hereby :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

hence IC (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),k)) in dom (stop (while>0 (a,i,I))) by A15, A28, EXTPRO_1:3; :: thesis:

end;

suppose k <> 0 ; :: thesis:

then consider kn being Nat such that
A59: k = kn + 1 by NAT_1:6;
reconsider kn = kn as Element of NAT by ORDINAL1:def 13;
reconsider lm = IC (Comput ((Q +* (stop I)),(Initialize t),kn)) as Element of NAT ;
kn < k by A59, XREAL_1:31;
then kn < LifeSpan ((Q +* (stop I)),(Initialize t)) by A58, XXREAL_0:2;
then (IC (Comput ((Q +* (stop I)),(Initialize t),kn))) + 1 = IC (Comput ((Q +* (stop (while>0 (a,i,I)))),(Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),1)),kn)) by A21, B21, A34, A31, A35, A24, A26, SCMPDS_7:34;
then A61: IC (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),k)) = lm + 1 by A59, EXTPRO_1:5;
IC (Comput ((Q +* (stop I)),(Initialize t),kn)) in dom (stop I) by A30, SCMPDS_6:def 2;
then lm < card (stop I) by AFINSQ_1:70;
then lm < (card I) + 1 by SCMPDS_5:7;
then A62: lm + 1 <= (card I) + 1 by INT_1:20;
(card I) + 1 < (card I) + 3 by XREAL_1:8;
then lm + 1 < (card I) + 3 by A62, XXREAL_0:2;
then lm + 1 < card (stop (while>0 (a,i,I))) by Lm3;
hence IC (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),k)) in dom (stop (while>0 (a,i,I))) by A61, AFINSQ_1:70; :: thesis:

end;

suppose A63: k = (LifeSpan ((Q +* (stop I)),(Initialize t))) + 1 ; :: thesis:

(card I) + 1 in dom (stop (while>0 (a,i,I))) by A29, SCMPDS_6:18;
hence IC (Comput ((Q +* (stop (while>0 (a,i,I)))),(Initialize t),k)) in dom (stop (while>0 (a,i,I))) by A21, B21, A34, A31, A35, A24, A26, A38, A63, SCMPDS_7:36; :: thesis:

end;

suppose k >= ((LifeSpan ((Q +* (stop I)),(Initialize t))) + 1) + 1 ; :: thesis:

end;

end;

hence S₁[k + 1] ; :: thesis:

end;

set n = f . (Dstate s);
A67: for x being Int_position st x in Y holds
s . x = s . x ;
A68: S₁[ 0 ]

proof

let t be State of SCMPDS; :: thesis:
let Q be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
assume f . (Dstate t) <= 0 ; :: thesis:
then f . (Dstate t) = 0 ;
then A69: t . (DataLoc ((s . a),i)) <= 0 by A2;
assume for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((s . a),i))) ; :: thesis:
assume for x being Int_position st x in Y holds
t . x = s . x ; :: thesis:
assume t . a = s . a ; :: thesis:
hence ( while>0 (a,i,I) is_closed_on t,Q & while>0 (a,i,I) is_halting_on t,Q ) by A69, Th20; :: thesis:

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A68, A5);
then S₁[f . (Dstate s)] ;
hence ( while>0 (a,i,I) is_closed_on s,P & while>0 (a,i,I) is_halting_on s,P ) by A3, A67; :: thesis: