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 = Int-Locations \/ FinSeq-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,s,I) . k) <> 0 implies ( f . ((StepWhile>0 a,s,I) . (k + 1)) < f . ((StepWhile>0 a,s,I) . k) & I is_closed_onInit (StepWhile>0 a,s,I) . k & I is_halting_onInit (StepWhile>0 a,s,I) . k ) ) & ((StepWhile>0 a,s,I) . (k + 1)) . (intloc 0 ) = 1 & ( f . ((StepWhile>0 a,s,I) . k) = 0 implies ((StepWhile>0 a,s,I) . k) . a <= 0 ) & ( ((StepWhile>0 a,s,I) . k) . a <= 0 implies f . ((StepWhile>0 a,s,I) . k) = 0 ) ) ; :: thesis:
set IniI = Initialized I;
set Iwhile = Initialized (while>0 a,I);
set s1 = s +* (Initialized (while>0 a,I));
A2: IC SCM+FSA in dom (Initialized (while>0 a,I)) by SCMFSA6A:24;
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 a,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 13;
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 13;
defpred S₁[ Element of NAT ] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 a,s,I) . ($1 + 1) = Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),k );
A6: S₁[ 0 ]

proof

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

end;

A7: now

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,s,I) . i & I is_halting_onInit (StepWhile>0 a,s,I) . i ) by A1; :: thesis:

end;

A8: now

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

now

end;

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

end;

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

now

per cases ;

suppose m = 0 ; :: thesis:

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

end;

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

now

let q be Element of NAT ; :: thesis:

per cases ;

suppose A32: q <= (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 ; :: thesis:

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

end;

suppose A36: q > (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 3 ; :: thesis:

A37: now

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

end;

defpred S₂[ Nat] means ( $1 <= m & $1 <> 0 & ex k being Element of NAT st
( (StepWhile>0 a,s,I) . $1 = Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),k & k <= q ) );
A38: for i being Nat st S₂[i] holds
i <= m ;
0 + 1 < m + 1 by A18, XREAL_1:8;
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 13;

now

per cases ;

suppose t = m ; :: thesis:

end;

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

now

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

A61: now

take k = z + ((LifeSpan (ProgramPart (((StepWhile>0 a,s,I) . t) +* (Initialized I))),(((StepWhile>0 a,s,I) . t) +* (Initialized I))) + 3); :: thesis:
thus ( (StepWhile>0 a,s,I) . (t + 1) = Comput (ProgramPart (s +* (Initialized (while>0 a,I)))),(s +* (Initialized (while>0 a,I))),k & k <= q ) by A50, A52, A59, A60, Th27; :: thesis:

end;

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

end;

end;

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

end;

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

end;

hence ( while>0 a,I is_halting_onInit s & while>0 a,I is_closed_onInit s ) ; :: thesis: