let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I be Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
let s be State of SCM+FSA; :: thesis:
set D = Data-Locations ;
given f being Function of (product the Object-Kind of SCM+FSA),NAT such that A1: for k being Element of NAT holds
( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_closed_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . (intloc 0) = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) ; :: thesis:
set s1 = Initialized s;
set P1 = P +* (while>0 (a,I));
A2: (P +* (while>0 (a,I))) +* (while>0 (a,I)) = P +* (while>0 (a,I)) by FUNCT_4:93;
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,P,s,I)) . $1);
A4: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 )

proof

let k be Nat; :: thesis:
k in NAT by ORDINAL1:def 12;
hence ( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A1; :: thesis:

end;

consider m being Nat such that
A5: H₁(m) = 0 and
A6: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(A4);
reconsider m = m as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Element of NAT ] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 (a,P,s,I)) . ($1 + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),k) );
A7: S₁[ 0 ]

proof

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

end;

A8: now

let i be Element of NAT ; :: thesis:
assume i < m ; :: thesis:
then H₁(i) <> 0 by A6;
hence ( I is_closed_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) ) by A1; :: thesis:

end;

A9: now

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

now

set sk = (StepWhile>0 (a,P,s,I)) . k;
set sk1 = (StepWhile>0 (a,P,s,I)) . (k + 1);
assume A11: (k + 1) + 1 <= m ; :: thesis:
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Element of NAT such that
A12: (StepWhile>0 (a,P,s,I)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),n) by A10, A11, XXREAL_0:2;
A13: ((StepWhile>0 (a,P,s,I)) . (k + 1)) . (intloc 0) = 1 by A1;
k + 0 < k + (1 + 1) by XREAL_1:6;
then A14: k < m by A11, XXREAL_0:2;
then A15: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) by A8;
H₁(k) <> 0 by A6, A14;
then A16: ((StepWhile>0 (a,P,s,I)) . k) . a > 0 by A1;
take m = n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . (k + 1))))) + 3); :: thesis:
A17: (P +* (while>0 (a,I))) +* (while>0 (a,I)) = P +* (while>0 (a,I)) by FUNCT_4:93;
A18: (StepWhile>0 (a,P,s,I)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . k)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . k)))) + 3)) by Def1;
I is_closed_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) by A8, A14;
then IC ((StepWhile>0 (a,P,s,I)) . (k + 1)) = 0 by A18, A15, A16, Th19, A17;
then (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . (k + 1))))) + 3))) by A12, A13, Th27;
hence (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),m) ; :: thesis:

end;

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

end;

A19: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A9);

per cases ;

suppose m = 0 ; :: thesis:

then ((StepWhile>0 (a,P,s,I)) . 0) . a <= 0 by A1, A5;
then s . a <= 0 by Def1;
hence ( while>0 (a,I) is_halting_onInit s,P & while>0 (a,I) is_closed_onInit s,P ) by Th16; :: thesis:

end;

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

now

let q be Element of NAT ; :: thesis:

per cases ;

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

A36: (StepWhile>0 (a,P,s,I)) . 0 = s by Def1;
then A37: I is_halting_onInit s,P +* (while>0 (a,I)) by A8, A20;
H₁( 0 ) <> 0 by A6, A20;
then A38: s . a > 0 by A1, A36;
I is_closed_onInit s,P +* (while>0 (a,I)) by A8, A20, A36;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),q)) in dom (while>0 (a,I)) by A35, A38, A37, Th19, A2; :: thesis:

end;

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

A40: now

take k = (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized s))) + 3; :: thesis:
thus ( (StepWhile>0 (a,P,s,I)) . 1 = Comput ((P +* (while>0 (a,I))),(Initialized s),k) & k <= q ) by A39, Th26; :: thesis:

end;

defpred S₂[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile>0 (a,P,s,I)) . $1 = Comput ((P +* (while>0 (a,I))),(Initialized s),k) & k <= q ) );
A41: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A20, XREAL_1:6;
then 1 <= m by NAT_1:13;
then A42: ex t being Nat st S₂[t] by A40;
consider t being Nat such that
A43: ( S₂[t] & ( for i being Nat st S₂[i] holds
i <= t ) ) from NAT_1:sch 6(A41, A42);
reconsider t = t as Element of NAT by ORDINAL1:def 12;

now

per cases ;

suppose t = m ; :: thesis:

then consider r being Element of NAT such that
A44: (StepWhile>0 (a,P,s,I)) . m = Comput ((P +* (while>0 (a,I))),(Initialized s),r) and
A45: r <= q by A43;
consider x being Nat such that
A46: q = r + x by A45, NAT_1:10;
A47: while>0 (a,I) is_closed_onInit (StepWhile>0 (a,P,s,I)) . m,P +* (while>0 (a,I)) by A32, Th16;
reconsider x = x as Element of NAT by ORDINAL1:def 12;
Comput ((P +* (while>0 (a,I))),(Initialized s),q) = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . m)),x) by A31, A44, A46, EXTPRO_1:4;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),q)) in dom (while>0 (a,I)) by A47, A2, SCM_HALT:def 4; :: thesis:

end;

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

set Dt = (StepWhile>0 (a,P,s,I)) . t;
A49: t < m by A43, A48, XXREAL_0:1;
then A50: I is_closed_onInit (StepWhile>0 (a,P,s,I)) . t,P +* (while>0 (a,I)) by A8;
A51: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . t,P +* (while>0 (a,I)) by A8, A49;
consider y being Nat such that
A52: t = y + 1 by A43, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 12;
t = y + 1 by A52;
then A53: ((StepWhile>0 (a,P,s,I)) . t) . (intloc 0) = 1 by A1;
H₁(t) <> 0 by A6, A49;
then A54: ((StepWhile>0 (a,P,s,I)) . t) . a > 0 by A1;
consider z being Element of NAT such that
A55: (StepWhile>0 (a,P,s,I)) . t = Comput ((P +* (while>0 (a,I))),(Initialized s),z) and
A56: z <= q by A43;
set z2 = z + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . t)))) + 3);
consider w being Nat such that
A57: q = z + w by A56, NAT_1:10;
set Dy = (StepWhile>0 (a,P,s,I)) . y;
y + 0 < t by A52, XREAL_1:6;
then A58: y < m by A43, XXREAL_0:2;
then A59: I is_closed_onInit (StepWhile>0 (a,P,s,I)) . y,P +* (while>0 (a,I)) by A8;
H₁(y) <> 0 by A6, A58;
then A60: ((StepWhile>0 (a,P,s,I)) . y) . a > 0 by A1;
A61: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . y,P +* (while>0 (a,I)) by A8, A58;
reconsider w = w as Element of NAT by ORDINAL1:def 12;
(StepWhile>0 (a,P,s,I)) . t = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . y)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . y)))) + 3)) by A52, Def1;
then A62: IC ((StepWhile>0 (a,P,s,I)) . t) = 0 by A59, A61, A60, Th19, A2;
A63: (StepWhile>0 (a,P,s,I)) . t = Initialized ((StepWhile>0 (a,P,s,I)) . t) by A53, A55, A62, Th27;

now

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

A65: now

take k = z + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . t)))) + 3); :: thesis:
thus (StepWhile>0 (a,P,s,I)) . (t + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),k) by A53, A55, A62, Th27; :: thesis:
thus k <= q by A64; :: thesis:

end;

t + 1 <= m by A49, NAT_1:13;
hence contradiction by A43, A65, XREAL_1:29; :: thesis:

end;

then A66: w < (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . t)))) + 3 by A57, XREAL_1:6;
Comput ((P +* (while>0 (a,I))),(Initialized s),q) = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . t)),w) by A63, A55, A57, EXTPRO_1:4;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),q)) in dom (while>0 (a,I)) by A66, A50, A51, A54, Th19, A2; :: thesis:

end;

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

end;

hence while>0 (a,I) is_closed_onInit s,P by SCM_HALT:def 4; :: thesis:

end;