let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I be Program of ; :: thesis:
let a be read-write Int-Location; :: thesis:
let s be State of SCM+FSA; :: thesis:
set D = Int-Locations \/ FinSeq-Locations;
assume A1: for k being Nat 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)) ) ; :: 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)) ;
A3: (P +* (while>0 (a,I))) +* (while>0 (a,I)) = P +* (while>0 (a,I)) ;
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A4: for k being Nat holds
( ( f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) ; :: thesis:
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,P,s)) . $1);
A5: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A4;
consider m being Nat such that
A6: H₁(m) = 0 and
A7: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(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))),(Initialize s),k) );

A8: now :: thesis:

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

now :: thesis:

set sk1 = (StepWhile>0 (a,I,P,s)) . (k + 1);
set sk = (StepWhile>0 (a,I,P,s)) . k;
assume A10: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A10, XXREAL_0:2;
then H₁(k) <> 0 by A7;
then A11: ((StepWhile>0 (a,I,P,s)) . k) . a > 0 by A4;
A12: I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) by A1;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Element of NAT such that
A13: (StepWhile>0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),n) by A9, A10, XXREAL_0:2;
take m = n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . (k + 1))))) + 3); :: thesis:
( (StepWhile>0 (a,I,P,s)) . (k + 1) = Comput ((P +* (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)) & I is_closed_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) by A1, Def5;
then IC ((StepWhile>0 (a,I,P,s)) . (k + 1)) = 0 by A12, A11, Th42, A2;
hence (StepWhile>0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),m) by A13, Th45; :: thesis:

end;

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

end;

A14: 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 Th44; :: thesis:

end;

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

now :: thesis:

per cases ;

suppose m = 0 ; :: thesis:

then ((StepWhile>0 (a,I,P,s)) . 0) . a <= 0 by A4, A6;
then s . a <= 0 by Def5;
hence ( while>0 (a,I) is_halting_on s,P & while>0 (a,I) is_closed_on s,P ) by Th38; :: thesis:

end;

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

now :: thesis:

let q be Element of NAT ; :: thesis:
A26: 0 < m by A16;

per cases ;

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

A28: (StepWhile>0 (a,I,P,s)) . 0 = s by Def5;
then A29: ( I is_closed_on s,P +* (while>0 (a,I)) & I is_halting_on s,P +* (while>0 (a,I)) ) by A1;
H₁( 0 ) <> 0 by A7, A26;
then s . a > 0 by A4, A28;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),q)) in dom (while>0 (a,I)) by A27, A29, Th42, A2; :: thesis:

end;

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

A31: 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 A30, Th44; :: 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 ) );
A32: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A26, XREAL_1:6;
then 1 <= m by NAT_1:13;
then A33: ex t being Nat st S₂[t] 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 12;

now :: thesis:

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))),(Initialize s),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 A23, Th38;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
A39: 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 A22, A35, A37, EXTPRO_1:4;
thus IC (Comput ((P +* (while>0 (a,I))),(Initialize s),q)) in dom (while>0 (a,I)) by A38, A39, A3, SCMFSA7B:def 6; :: thesis:

end;

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

set Dt = (StepWhile>0 (a,I,P,s)) . t;
A41: t < m by A34, A40, XXREAL_0:1;
then H₁(t) <> 0 by A7;
then A42: ((StepWhile>0 (a,I,P,s)) . t) . a > 0 by A4;
consider z being Element of NAT such that
A43: (StepWhile>0 (a,I,P,s)) . t = Comput ((P +* (while>0 (a,I))),(Initialize s),z) and
A44: z <= q by A34;
set z2 = z + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . t)))) + 3);
consider w being Nat such that
A45: q = z + w by A44, NAT_1:10;
A46: ( 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;
consider y being Nat such that
A47: t = y + 1 by A34, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 12;
set Dy = (StepWhile>0 (a,I,P,s)) . y;
y + 0 < t by A47, XREAL_1:6;
then y < m by A34, XXREAL_0:2;
then H₁(y) <> 0 by A7;
then A48: ((StepWhile>0 (a,I,P,s)) . y) . a > 0 by A4;
A49: ( 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;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
(StepWhile>0 (a,I,P,s)) . t = Comput ((P +* (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 A47, Def5;
then A50: IC ((StepWhile>0 (a,I,P,s)) . t) = 0 by A49, A48, Th42, A2;

now :: thesis:

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

A52: 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 A43, A50, A51, Th45; :: thesis:

end;

t + 1 <= m by A41, NAT_1:13;
hence contradiction by A34, A52, XREAL_1:29; :: thesis:

end;

then A53: w < (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . t)))) + 3 by A45, XREAL_1:6;
A54: Initialize ((StepWhile>0 (a,I,P,s)) . t) = (StepWhile>0 (a,I,P,s)) . t by A43, A50, Th45;
Comput ((P +* (while>0 (a,I))),(Initialize s),q) = Comput ((P +* (while>0 (a,I))),(Initialize ((StepWhile>0 (a,I,P,s)) . t)),w) by A54, A43, A45, EXTPRO_1:4;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialize s),q)) in dom (while>0 (a,I)) by A53, A46, A42, Th42, A2; :: thesis:

end;

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

end;

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

end;

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