let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
let I be Program of SCM+FSA; :: thesis:
A1: ProgramPart (while>0 (a,I)) = while>0 (a,I) by RELAT_1:209;
assume A2: for k being Element of NAT st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds
( I is_closed_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) ) ; :: according to SCMFSA9A:def 4 :: thesis:
set s1 = s +* (Initialize (while>0 (a,I)));
set p1 = p +* (while>0 (a,I));
A3: (p +* (while>0 (a,I))) +* (while>0 (a,I)) = p +* (while>0 (a,I)) by FUNCT_4:99;
defpred S₁[ Nat] means ((StepWhile>0 (a,I,p,s)) . $1) . a <= 0 ;
given f being Function of (product the Object-Kind of SCM+FSA),NAT such that A4: for k being Element of NAT holds
( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ) ; :: according to SCMFSA9A:def 5 :: thesis:
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,p,s)) . $1);
A5: for k being Element of NAT holds
( H₁(k + 1) < H₁(k) or S₁[k] ) by A4;
consider m being Element of NAT such that
A6: S₁[m] and
A7: for n being Element of NAT st S₁[n] holds
m <= n from NAT_1:sch 18(A5);
defpred S₂[ Nat] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 (a,I,p,s)) . ($1 + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k) );

A8: now

let k be Element of NAT ; :: thesis:
assume A9: S₂[k] ; :: thesis:

now

set sk1 = (StepWhile>0 (a,I,p,s)) . (k + 1);
set sk = (StepWhile>0 (a,I,p,s)) . k;
set pk = p +* (while>0 (a,I));
assume A10: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:8;
then k < m by A10, XXREAL_0:2;
then A11: ((StepWhile>0 (a,I,p,s)) . k) . a > 0 by A7;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
then consider n being Element of NAT such that
A12: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n) by A9, A10, XXREAL_0:2;
A13: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . k) +* (Initialize (while>0 (a,I)))),((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . k) +* (Initialize I)))) + 3)) by SCMFSA_9:def 5, A3;
take m = n + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . (k + 1)) +* (Initialize I)))) + 3); :: thesis:
( I is_closed_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) ) by A2, A11;
then IC ((StepWhile>0 (a,I,p,s)) . (k + 1)) = 0 by A13, A11, SCMFSA_9:47;
hence (StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),m) by A12, SCMFSA_9:52; :: thesis:

end;

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

end;

A14: IC in dom (Initialize (while>0 (a,I))) by COMPOS_1:141;
A15: S₂[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis:
take n = (LifeSpan (((p +* (while>0 (a,I))) +* I),(s +* (Initialize I)))) + 3; :: thesis:
thus (StepWhile>0 (a,I,p,s)) . (0 + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n) by SCMFSA_9:51; :: thesis:

end;

A16: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A15, A8);

now

per cases ;

suppose m = 0 ; :: thesis:

then s . a <= 0 by A6, SCMFSA_9:def 5;
hence ( while>0 (a,I) is_halting_on s,p & while>0 (a,I) is_closed_on s,p ) by SCMFSA_9:43; :: thesis:

end;

suppose A17: m <> 0 ; :: thesis:

set ii = (LifeSpan (((p +* (while>0 (a,I))) +* I),(s +* (Initialize I)))) + 3;
set sm = (StepWhile>0 (a,I,p,s)) . m;
set pm = p +* (while>0 (a,I));
set sm1 = ((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)));
set pm1 = (p +* (while>0 (a,I))) +* (while>0 (a,I));
consider i being Nat such that
A18: m = i + 1 by A17, NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set si = (StepWhile>0 (a,I,p,s)) . i;
set psi = p +* (while>0 (a,I));
A19: (StepWhile>0 (a,I,p,s)) . m = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . i) +* (Initialize (while>0 (a,I)))),((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . i) +* (Initialize I)))) + 3)) by A18, SCMFSA_9:def 5, A3;
m = i + 1 by A18;
then consider n being Element of NAT such that
A20: (StepWhile>0 (a,I,p,s)) . m = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n) by A16;
i < m by A18, NAT_1:13;
then A21: ((StepWhile>0 (a,I,p,s)) . i) . a > 0 by A7;
then ( I is_closed_on (StepWhile>0 (a,I,p,s)) . i,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . i,p +* (while>0 (a,I)) ) by A2;
then A22: IC ((StepWhile>0 (a,I,p,s)) . m) = 0 by A19, A21, SCMFSA_9:47;
ProgramPart ((StepWhile>0 (a,I,p,s)) . m) = ProgramPart (s +* (Initialize (while>0 (a,I)))) by A20, AMI_1:123;
then A23: ( DataPart (((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) & ProgramPart (((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))) = ProgramPart ((StepWhile>0 (a,I,p,s)) . m) ) by FUNCT_4:100, SCMFSA8A:11;
IC (((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))) = IC (Initialize (while>0 (a,I))) by A14, FUNCT_4:14
.= IC ((StepWhile>0 (a,I,p,s)) . m) by A22, COMPOS_1:142 ;
then A24: ((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I))) = (StepWhile>0 (a,I,p,s)) . m by A23, SCMFSA_9:29;
while>0 (a,I) is_halting_on (StepWhile>0 (a,I,p,s)) . m,p +* (while>0 (a,I)) by A6, SCMFSA_9:43;
then (p +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on ((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I))) by SCMFSA7B:def 8, A1;
then consider j being Element of NAT such that
A25: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j))) = halt SCM+FSA by A24, EXTPRO_1:30, A3;
A26: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(n + j)) = Comput ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n)),j) by EXTPRO_1:5;
CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(n + j)))) = halt SCM+FSA by A20, A25, A26;
then p +* (while>0 (a,I)) halts_on s +* (Initialize (while>0 (a,I))) by EXTPRO_1:30;
hence while>0 (a,I) is_halting_on s,p by SCMFSA7B:def 8, A1; :: thesis:

now

let q be Element of NAT ; :: thesis:

per cases ;

suppose A27: q <= (LifeSpan (((p +* (while>0 (a,I))) +* I),(s +* (Initialize I)))) + 3 ; :: thesis:

A28: (StepWhile>0 (a,I,p,s)) . 0 = s by SCMFSA_9:def 5;
then A29: s . a > 0 by A7, A17;
then ( I is_closed_on s,p +* (while>0 (a,I)) & I is_halting_on s,p +* (while>0 (a,I)) ) by A2, A28;
hence IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),q)) in dom (while>0 (a,I)) by A27, A29, SCMFSA_9:47, A3; :: thesis:

end;

suppose A30: q > (LifeSpan (((p +* (while>0 (a,I))) +* I),(s +* (Initialize I)))) + 3 ; :: thesis:

A31: now

take k = (LifeSpan (((p +* (while>0 (a,I))) +* I),(s +* (Initialize I)))) + 3; :: thesis:
thus ( (StepWhile>0 (a,I,p,s)) . 1 = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k) & k <= q ) by A30, SCMFSA_9:51; :: thesis:

end;

defpred S₃[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile>0 (a,I,p,s)) . $1 = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k) & k <= q ) );
A32: for i being Nat st S₃[i] holds
i <= m ;
0 + 1 < m + 1 by A17, XREAL_1:8;
then 1 <= m by NAT_1:13;
then A33: ex k being Nat st S₃[k] by A31;
consider t being Nat such that
A34: ( S₃[t] & ( for i being Nat st S₃[i] holds
i <= t ) ) from NAT_1:sch 6(A32, A33);
reconsider t = t as Element of NAT by ORDINAL1:def 13;

now

per cases ;

suppose t = m ; :: thesis:

then consider r being Element of NAT such that
A35: (StepWhile>0 (a,I,p,s)) . m = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),r) and
A36: r <= q by A34;
consider x being Nat such that
A37: q = r + x by A36, NAT_1:10;
A38: while>0 (a,I) is_closed_on (StepWhile>0 (a,I,p,s)) . m,p +* (while>0 (a,I)) by A6, SCMFSA_9:43;
reconsider x = x as Element of NAT by ORDINAL1:def 13;
Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),q) = Comput ((p +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))),x) by A24, A35, A37, EXTPRO_1:5;
hence IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),q)) in dom (while>0 (a,I)) by A38, SCMFSA7B:def 7, A1, A3; :: thesis:

end;

suppose A39: t <> m ; :: thesis:

set Dt = (StepWhile>0 (a,I,p,s)) . t;
set pt = p +* (while>0 (a,I));
consider y being Nat such that
A40: t = y + 1 by A34, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 13;
set Dy = (StepWhile>0 (a,I,p,s)) . y;
set py = p +* (while>0 (a,I));
A41: (StepWhile>0 (a,I,p,s)) . t = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . y) +* (Initialize (while>0 (a,I)))),((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . y) +* (Initialize I)))) + 3)) by A40, SCMFSA_9:def 5, A3;
y + 0 < t by A40, XREAL_1:8;
then y < m by A34, XXREAL_0:2;
then A42: ((StepWhile>0 (a,I,p,s)) . y) . a > 0 by A7;
then ( I is_closed_on (StepWhile>0 (a,I,p,s)) . y,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . y,p +* (while>0 (a,I)) ) by A2;
then A43: IC ((StepWhile>0 (a,I,p,s)) . t) = 0 by A41, A42, SCMFSA_9:47;
consider z being Element of NAT such that
A44: (StepWhile>0 (a,I,p,s)) . t = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),z) and
A45: z <= q by A34;
consider w being Nat such that
A46: q = z + w by A45, NAT_1:10;
reconsider w = w as Element of NAT by ORDINAL1:def 13;
A47: (StepWhile>0 (a,I,p,s)) . t = ((StepWhile>0 (a,I,p,s)) . t) +* (Initialize (while>0 (a,I))) by A44, A43, SCMFSA_9:52;
A48: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),q) = Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . t),w) by A44, A46, EXTPRO_1:5
.= Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . t) +* (Initialize (while>0 (a,I)))),w) by A47, A3 ;
set z2 = z + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . t) +* (Initialize I)))) + 3);
A49: t < m by A34, A39, XXREAL_0:1;

now

assume A50: z + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . t) +* (Initialize I)))) + 3) <= q ; :: thesis:

A51: now

take k = z + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . t) +* (Initialize I)))) + 3); :: thesis:
thus ( (StepWhile>0 (a,I,p,s)) . (t + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k) & k <= q ) by A44, A43, A50, SCMFSA_9:52; :: thesis:

end;

t + 1 <= m by A49, NAT_1:13;
hence contradiction by A34, A51, XREAL_1:31; :: thesis:

end;

then A52: w < (LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . t) +* (Initialize I)))) + 3 by A46, XREAL_1:8;
A53: ((StepWhile>0 (a,I,p,s)) . t) . a > 0 by A7, A49;
then ( I is_closed_on (StepWhile>0 (a,I,p,s)) . t,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . t,p +* (while>0 (a,I)) ) by A2;
hence IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),q)) in dom (while>0 (a,I)) by A52, A48, A53, SCMFSA_9:47; :: thesis:

end;

hence IC (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),q)) in dom (while>0 (a,I)) ; :: thesis:

end;

hence while>0 (a,I) is_closed_on s,p by SCMFSA7B:def 7, A1; :: thesis:

end;

hence ( while>0 (a,I) is_halting_on s,p & while>0 (a,I) is_closed_on s,p ) ; :: thesis: