let P be Instruction-Sequence of SCM+FSA; :: thesis:
let I be really-closed MacroInstruction 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 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_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 ) by A1;
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 Nat ;
defpred S₁[ Nat] means ( $1 + 1 <= m implies ex k being 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))) + 2; :: thesis:
thus (StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),n) by Th8; :: thesis:

end;

A7: now :: thesis:

let i be Nat; :: thesis:
assume i < m ; :: thesis:
then H₁(i) <> 0 by A5;
hence 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 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 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))))) + 2); :: 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)))) + 2)) by Def1;
IC ((StepWhile>0 (a,P,s,I)) . (k + 1)) = 0 by A17, A14, A15, Th4, 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))))) + 2))) by A11, A12, Th9;
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 Nat holds S₁[k] from NAT_1:sch 2(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 by SCM_HALT:73; :: thesis:

end;

suppose m <> 0 ; :: thesis:

then consider i being Nat such that
A19: m = i + 1 by NAT_1:6;
reconsider i = i as Nat ;
set si = (StepWhile>0 (a,P,s,I)) . i;
set sm = (StepWhile>0 (a,P,s,I)) . m;
set sm1 = Initialized ((StepWhile>0 (a,P,s,I)) . m);
set sm2 = Initialize ((StepWhile>0 (a,P,s,I)) . m);
A20: i < m by A19, XREAL_1:29;
i < m by A19, NAT_1:13;
then H₁(i) <> 0 by A5;
then A21: ((StepWhile>0 (a,P,s,I)) . i) . a > 0 by A1;
A22: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) by A7, A20;
(StepWhile>0 (a,P,s,I)) . m = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . i)))) + 2)) by A19, Def1;
then IC ((StepWhile>0 (a,P,s,I)) . m) = 0 by A22, A21, Th4, A2;
then A23: Start-At (0,SCM+FSA) c= (StepWhile>0 (a,P,s,I)) . m by MEMSTR_0:30;
((StepWhile>0 (a,P,s,I)) . (i + 1)) . (intloc 0) = 1 by A1;
then A24: Initialized ((StepWhile>0 (a,P,s,I)) . m) = Initialize ((StepWhile>0 (a,P,s,I)) . m) by A19, SCMFSA_M:18;
set p = (LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized s))) + 3;
m = i + 1 by A19;
then consider n being Nat such that
A25: (StepWhile>0 (a,P,s,I)) . m = Comput ((P +* (while>0 (a,I))),(Initialized s),n) by A18;
A26: Initialized ((StepWhile>0 (a,P,s,I)) . m) = (StepWhile>0 (a,P,s,I)) . m by A24, A23, FUNCT_4:98;
((StepWhile>0 (a,P,s,I)) . m) . a <= 0 by A1, A4;
then while>0 (a,I) is_halting_onInit (StepWhile>0 (a,P,s,I)) . m,P +* (while>0 (a,I)) by SCM_HALT:73;
then P +* (while>0 (a,I)) halts_on Initialized ((StepWhile>0 (a,P,s,I)) . m) ;
then consider j being Nat such that
A27: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((StepWhile>0 (a,P,s,I)) . m),j))) = halt SCM+FSA by A26;
A28: Comput ((P +* (while>0 (a,I))),(Initialized s),(j + n)) = Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialized s),n)),j) by EXTPRO_1:4;
P +* (while>0 (a,I)) halts_on Initialized s by A25, A27, A28, EXTPRO_1:29;
hence while>0 (a,I) is_halting_onInit s,P ; :: thesis:

end;