let p be Instruction-Sequence of SCM+FSA; :: 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:
assume A1: 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 = Initialize s;
set p1 = p +* (while>0 (a,I));
A2: (p +* (while>0 (a,I))) +* (while>0 (a,I)) = p +* (while>0 (a,I)) ;
defpred S₁[ Nat] means ((StepWhile>0 (a,I,p,s)) . $1) . a <= 0 ;
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A3: 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);
A4: for k being Element of NAT holds
( H₁(k + 1) < H₁(k) or S₁[k] ) by A3;
consider m being Element of NAT such that
A5: S₁[m] and
A6: for n being Element of NAT st S₁[n] holds
m <= n from NAT_1:sch 18(A4);
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))),(Initialize s),k) );

A7: now :: thesis:

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

now :: thesis:

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 A9: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A9, XXREAL_0:2;
then A10: ((StepWhile>0 (a,I,p,s)) . k) . a > 0 by A6;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Element of NAT such that
A11: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),n) by A8, A9, XXREAL_0:2;
A12: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p,s)) . k)),((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . k)))) + 3)) by SCMFSA_9:def 5;
take m = n + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . (k + 1))))) + 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 A1, A10;
then IC ((StepWhile>0 (a,I,p,s)) . (k + 1)) = 0 by A12, A10, SCMFSA_9:42;
hence (StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),m) by A11, SCMFSA_9:45; :: thesis:

end;

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

end;

A13: S₂[ 0 ]

proof

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

end;

A14: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A13, A7);

per cases ;

suppose m = 0 ; :: thesis:

then s . a <= 0 by A5, 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:38; :: thesis:

end;

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

set ii = (LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize s))) + 3;
set sm = (StepWhile>0 (a,I,p,s)) . m;
set pm = p +* (while>0 (a,I));
set sm1 = Initialize ((StepWhile>0 (a,I,p,s)) . m);
set pm1 = (p +* (while>0 (a,I))) +* (while>0 (a,I));
consider i being Nat such that
A16: m = i + 1 by A15, NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
set si = (StepWhile>0 (a,I,p,s)) . i;
set psi = p +* (while>0 (a,I));
A17: (StepWhile>0 (a,I,p,s)) . m = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p,s)) . i)),((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . i)))) + 3)) by A16, SCMFSA_9:def 5;
m = i + 1 by A16;
then consider n being Element of NAT such that
A18: (StepWhile>0 (a,I,p,s)) . m = Comput ((p +* (while>0 (a,I))),(Initialize s),n) by A14;
i < m by A16, NAT_1:13;
then A19: ((StepWhile>0 (a,I,p,s)) . i) . a > 0 by A6;
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 A1;
then IC ((StepWhile>0 (a,I,p,s)) . m) = 0 by A17, A19, SCMFSA_9:42;
then Start-At (0,SCM+FSA) c= (StepWhile>0 (a,I,p,s)) . m by MEMSTR_0:30;
then A20: Initialize ((StepWhile>0 (a,I,p,s)) . m) = (StepWhile>0 (a,I,p,s)) . m by FUNCT_4:98;
while>0 (a,I) is_halting_on (StepWhile>0 (a,I,p,s)) . m,p +* (while>0 (a,I)) by A5, SCMFSA_9:38;
then (p +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialize ((StepWhile>0 (a,I,p,s)) . m) by SCMFSA7B:def 7;
then consider j being Element of NAT such that
A21: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j))) = halt SCM+FSA by A20, EXTPRO_1:29;
A22: Comput ((p +* (while>0 (a,I))),(Initialize s),(n + j)) = Comput ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),n)),j) by EXTPRO_1:4;
CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),(n + j)))) = halt SCM+FSA by A18, A21, A22;
then p +* (while>0 (a,I)) halts_on Initialize s by EXTPRO_1:29;
hence while>0 (a,I) is_halting_on s,p by SCMFSA7B:def 7; :: thesis:

now :: thesis:

let q be Element of NAT ; :: thesis:

per cases ;

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

A24: (StepWhile>0 (a,I,p,s)) . 0 = s by SCMFSA_9:def 5;
then A25: s . a > 0 by A6, A15;
then ( I is_closed_on s,p +* (while>0 (a,I)) & I is_halting_on s,p +* (while>0 (a,I)) ) by A1, A24;
hence IC (Comput ((p +* (while>0 (a,I))),(Initialize s),q)) in dom (while>0 (a,I)) by A23, A25, A2, SCMFSA_9:42; :: thesis:

end;

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

A27: now :: thesis:

take k = (LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize s))) + 3; :: thesis:
thus ( (StepWhile>0 (a,I,p,s)) . 1 = Comput ((p +* (while>0 (a,I))),(Initialize s),k) & k <= q ) by A26, SCMFSA_9:44; :: 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))),(Initialize s),k) & k <= q ) );
A28: for i being Nat st S₃[i] holds
i <= m ;
0 + 1 < m + 1 by A15, XREAL_1:6;
then 1 <= m by NAT_1:13;
then A29: ex k being Nat st S₃[k] by A27;
consider t being Nat such that
A30: ( S₃[t] & ( for i being Nat st S₃[i] holds
i <= t ) ) from NAT_1:sch 6(A28, A29);
reconsider t = t as Element of NAT by ORDINAL1:def 12;

per cases ;

suppose t = m ; :: thesis:

then consider r being Element of NAT such that
A31: (StepWhile>0 (a,I,p,s)) . m = Comput ((p +* (while>0 (a,I))),(Initialize s),r) and
A32: r <= q by A30;
consider x being Nat such that
A33: q = r + x by A32, NAT_1:10;
A34: while>0 (a,I) is_closed_on (StepWhile>0 (a,I,p,s)) . m,p +* (while>0 (a,I)) by A5, SCMFSA_9:38;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
Comput ((p +* (while>0 (a,I))),(Initialize s),q) = Comput ((p +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p,s)) . m)),x) by A20, A31, A33, EXTPRO_1:4;
hence IC (Comput ((p +* (while>0 (a,I))),(Initialize s),q)) in dom (while>0 (a,I)) by A34, A2, SCMFSA7B:def 6; :: thesis:

end;

suppose A35: 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
A36: t = y + 1 by A30, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 12;
set Dy = (StepWhile>0 (a,I,p,s)) . y;
set py = p +* (while>0 (a,I));
A37: (StepWhile>0 (a,I,p,s)) . t = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p,s)) . y)),((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . y)))) + 3)) by A36, SCMFSA_9:def 5;
y + 0 < t by A36, XREAL_1:6;
then y < m by A30, XXREAL_0:2;
then A38: ((StepWhile>0 (a,I,p,s)) . y) . a > 0 by A6;
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 A1;
then A39: IC ((StepWhile>0 (a,I,p,s)) . t) = 0 by A37, A38, SCMFSA_9:42;
consider z being Element of NAT such that
A40: (StepWhile>0 (a,I,p,s)) . t = Comput ((p +* (while>0 (a,I))),(Initialize s),z) and
A41: z <= q by A30;
consider w being Nat such that
A42: q = z + w by A41, NAT_1:10;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
A43: (StepWhile>0 (a,I,p,s)) . t = Initialize ((StepWhile>0 (a,I,p,s)) . t) by A40, A39, SCMFSA_9:45;
A44: Comput ((p +* (while>0 (a,I))),(Initialize s),q) = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,p,s)) . t)),w) by A43, A40, A42, EXTPRO_1:4;
set z2 = z + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . t)))) + 3);
A45: t < m by A30, A35, XXREAL_0:1;

now :: thesis:

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

A47: now :: thesis:

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

end;

t + 1 <= m by A45, NAT_1:13;
hence contradiction by A30, A47, XREAL_1:29; :: thesis:

end;

then A48: w < (LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . t)))) + 3 by A42, XREAL_1:6;
A49: ((StepWhile>0 (a,I,p,s)) . t) . a > 0 by A6, A45;
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 A1;
hence IC (Comput ((p +* (while>0 (a,I))),(Initialize s),q)) in dom (while>0 (a,I)) by A48, A44, A49, SCMFSA_9:42; :: thesis:

end;

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

end;