let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ( for k being Nat holds I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
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 ) ) holds
while>0 (a,I) is_halting_on s,P
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA st ( for k being Nat holds I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
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 ) ) holds
while>0 (a,I) is_halting_on s,P
let a be read-write Int-Location; :: thesis: for s being State of SCM+FSA st ( for k being Nat holds I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
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 ) ) holds
while>0 (a,I) is_halting_on s,P
let s be State of SCM+FSA; :: thesis: ( ( for k being Nat holds I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
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 ) ) implies while>0 (a,I) is_halting_on s,P )
set D = Int-Locations \/ FinSeq-Locations;
assume A1: for k being Nat holds I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ; :: thesis: ( for f being Function of (product (the_Values_of SCM+FSA)),NAT holds
not 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 ) ) or while>0 (a,I) is_halting_on s,P )
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)) ;
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A3: 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: while>0 (a,I) is_halting_on s,P
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,P,s)) . $1);
A4: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A3;
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);
defpred S₁[ Nat] means ( $1 + 1 <= m implies ex k being Nat st (StepWhile>0 (a,I,P,s)) . ($1 + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),k) );

A7: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( (k + 1) + 1 <= m implies ex m being Element of NAT st (StepWhile>0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),m) )

set sk1 = (StepWhile>0 (a,I,P,s)) . (k + 1);
set sk = (StepWhile>0 (a,I,P,s)) . k;
assume A9: (k + 1) + 1 <= m ; :: thesis: ex m being Element of NAT st (StepWhile>0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),m)
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A9, XXREAL_0:2;
then H₁(k) <> 0 by A6;
then A10: ((StepWhile>0 (a,I,P,s)) . k) . a > 0 by A3;
A11: 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 Nat such that
A12: (StepWhile>0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),n) by A8, A9, XXREAL_0:2;
take m = n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . (k + 1))))) + 2); :: thesis: (StepWhile>0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),m)
(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)))) + 2)) by Def2;
then IC ((StepWhile>0 (a,I,P,s)) . (k + 1)) = 0 by A11, A10, Th15, A2;
hence (StepWhile>0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),m) by A12, Th18; :: thesis: verum

end;

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

end;

A13: S₁[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis: ex k being Nat st (StepWhile>0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),k)
take n = (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize s))) + 2; :: thesis: (StepWhile>0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),n)
thus (StepWhile>0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),n) by Th17; :: thesis: verum

end;

A14: for k being Nat holds S₁[k] from NAT_1:sch 2(A13, A7);

now :: thesis: while>0 (a,I) is_halting_on s,P

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: while>0 (a,I) is_halting_on s,P

then ((StepWhile>0 (a,I,P,s)) . 0) . a <= 0 by A3, A5;
then s . a <= 0 by Def2;
hence while>0 (a,I) is_halting_on s,P by Th12; :: thesis: verum

end;

suppose A15: m <> 0 ; :: thesis: while>0 (a,I) is_halting_on s,P

set p = (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize s))) + 3;
set sm = (StepWhile>0 (a,I,P,s)) . m;
set sm1 = Initialize ((StepWhile>0 (a,I,P,s)) . m);
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;
consider n being Nat such that
A17: (StepWhile>0 (a,I,P,s)) . m = Comput ((P +* (while>0 (a,I))),(Initialize s),n) by A14, A16;
set si = (StepWhile>0 (a,I,P,s)) . i;
i < m by A16, NAT_1:13;
then H₁(i) <> 0 by A6;
then A18: ((StepWhile>0 (a,I,P,s)) . i) . a > 0 by A3;
A19: I is_halting_on (StepWhile>0 (a,I,P,s)) . i,P +* (while>0 (a,I)) by A1;
(StepWhile>0 (a,I,P,s)) . m = Comput ((P +* (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)))) + 2)) by A16, Def2;
then (StepWhile>0 (a,I,P,s)) . m is 0 -started by A19, A18, Th15, A2;
then Start-At (0,SCM+FSA) c= (StepWhile>0 (a,I,P,s)) . m by MEMSTR_0:29;
then A20: Initialize ((StepWhile>0 (a,I,P,s)) . m) = (StepWhile>0 (a,I,P,s)) . m by FUNCT_4:98;
((StepWhile>0 (a,I,P,s)) . m) . a <= 0 by A3, A5;
then while>0 (a,I) is_halting_on (StepWhile>0 (a,I,P,s)) . m,P +* (while>0 (a,I)) by Th12;
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 P +* (while>0 (a,I)) halts_on Initialize ((StepWhile>0 (a,I,P,s)) . m) ;
then consider j being 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;
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 A17, 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: verum

end;

end;

end;

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