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_Values_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)) ;
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,P,s,I)) . $1);
A3: 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
A4: H₁(m) = 0 and
A5: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(A3);
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) );
A6: 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 Th16; :: thesis:

end;

A7: now :: thesis:

let i be Element of NAT ; :: thesis:
assume i < m ; :: thesis:
then H₁(i) <> 0 by A5;
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;

A8: now :: thesis:

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

now :: thesis:

set sk = (StepWhile>0 (a,P,s,I)) . k;
set sk1 = (StepWhile>0 (a,P,s,I)) . (k + 1);
assume A10: (k + 1) + 1 <= m ; :: thesis:
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Element of NAT such that
A11: (StepWhile>0 (a,P,s,I)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),n) by A9, A10, XXREAL_0:2;
A12: ((StepWhile>0 (a,P,s,I)) . (k + 1)) . (intloc 0) = 1 by A1;
k + 0 < k + (1 + 1) by XREAL_1:6;
then A13: k < m by A10, XXREAL_0:2;
then A14: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) by A7;
H₁(k) <> 0 by A5, A13;
then A15: ((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:
A16: (P +* (while>0 (a,I))) +* (while>0 (a,I)) = P +* (while>0 (a,I)) ;
A17: (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 A7, A13;
then IC ((StepWhile>0 (a,P,s,I)) . (k + 1)) = 0 by A17, A14, A15, Th11, A16;
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 A11, A12, Th17;
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;

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

per cases ;

suppose m = 0 ; :: thesis:

then ((StepWhile>0 (a,P,s,I)) . 0) . a <= 0 by A1, A4;
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 Th8; :: thesis:

end;

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

now :: thesis:

let q be Element of NAT ; :: thesis:

per cases ;

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

A33: (StepWhile>0 (a,P,s,I)) . 0 = s by Def1;
then A34: I is_halting_onInit s,P +* (while>0 (a,I)) by A7, A19;
H₁( 0 ) <> 0 by A5, A19;
then A35: s . a > 0 by A1, A33;
I is_closed_onInit s,P +* (while>0 (a,I)) by A7, A19, A33;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),q)) in dom (while>0 (a,I)) by A32, A35, A34, Th11, A2; :: thesis:

end;

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

A37: now :: thesis:

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 A36, Th16; :: 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 ) );
A38: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A19, XREAL_1:6;
then 1 <= m by NAT_1:13;
then A39: ex t being Nat st S₂[t] by A37;
consider t being Nat such that
A40: ( S₂[t] & ( for i being Nat st S₂[i] holds
i <= t ) ) from NAT_1:sch 6(A38, A39);
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
A41: (StepWhile>0 (a,P,s,I)) . m = Comput ((P +* (while>0 (a,I))),(Initialized s),r) and
A42: r <= q by A40;
consider x being Nat such that
A43: q = r + x by A42, NAT_1:10;
A44: while>0 (a,I) is_closed_onInit (StepWhile>0 (a,P,s,I)) . m,P +* (while>0 (a,I)) by A29, Th8;
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 A28, A41, A43, EXTPRO_1:4;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),q)) in dom (while>0 (a,I)) by A44, A2, SCM_HALT:def 4; :: thesis:

end;

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

set Dt = (StepWhile>0 (a,P,s,I)) . t;
A46: t < m by A40, A45, XXREAL_0:1;
then A47: I is_closed_onInit (StepWhile>0 (a,P,s,I)) . t,P +* (while>0 (a,I)) by A7;
A48: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . t,P +* (while>0 (a,I)) by A7, A46;
consider y being Nat such that
A49: t = y + 1 by A40, NAT_1:6;
reconsider y = y as Element of NAT by ORDINAL1:def 12;
t = y + 1 by A49;
then A50: ((StepWhile>0 (a,P,s,I)) . t) . (intloc 0) = 1 by A1;
H₁(t) <> 0 by A5, A46;
then A51: ((StepWhile>0 (a,P,s,I)) . t) . a > 0 by A1;
consider z being Element of NAT such that
A52: (StepWhile>0 (a,P,s,I)) . t = Comput ((P +* (while>0 (a,I))),(Initialized s),z) and
A53: z <= q by A40;
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
A54: q = z + w by A53, NAT_1:10;
set Dy = (StepWhile>0 (a,P,s,I)) . y;
y + 0 < t by A49, XREAL_1:6;
then A55: y < m by A40, XXREAL_0:2;
then A56: I is_closed_onInit (StepWhile>0 (a,P,s,I)) . y,P +* (while>0 (a,I)) by A7;
H₁(y) <> 0 by A5, A55;
then A57: ((StepWhile>0 (a,P,s,I)) . y) . a > 0 by A1;
A58: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . y,P +* (while>0 (a,I)) by A7, A55;
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 A49, Def1;
then A59: IC ((StepWhile>0 (a,P,s,I)) . t) = 0 by A56, A58, A57, Th11, A2;
A60: (StepWhile>0 (a,P,s,I)) . t = Initialized ((StepWhile>0 (a,P,s,I)) . t) by A50, A52, A59, Th17;

now :: thesis:

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

A62: now :: thesis:

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 A50, A52, A59, Th17; :: thesis:
thus k <= q by A61; :: thesis:

end;

t + 1 <= m by A46, NAT_1:13;
hence contradiction by A40, A62, XREAL_1:29; :: thesis:

end;

then A63: w < (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . t)))) + 3 by A54, 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 A60, A52, A54, EXTPRO_1:4;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),q)) in dom (while>0 (a,I)) by A63, A47, A48, A51, Th11, 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;