let p be Instruction-Sequence of SCM+FSA; :: thesis:
let s be State of SCM+FSA; :: thesis:
let a be read-write Int-Location; :: thesis:
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis:
assume A1: for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds
I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) ; :: according to SCMFSA9A:def 1 :: thesis:
set s1 = Initialize s;
set p1 = p +* (while=0 (a,I));
defpred S₁[ Nat] means ((StepWhile=0 (a,I,p,s)) . $1) . a <> 0 ;
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A2: for k being Nat holds
( f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 ) ; :: according to SCMFSA9A:def 2 :: thesis:
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile=0 (a,I,p,s)) . $1);
A3: for k being Nat holds
( H₁(k + 1) < H₁(k) or S₁[k] ) by A2;
consider m being Nat such that
A4: S₁[m] and
A5: for n being Nat st S₁[n] holds
m <= n from NAT_1:sch 18(A3);
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) );

A6: now :: thesis:

let k be Nat; :: thesis:
assume A7: S₂[k] ; :: thesis:

now :: thesis:

set sk1 = (StepWhile=0 (a,I,p,s)) . (k + 1);
set sk = (StepWhile=0 (a,I,p,s)) . k;
set pk = p +* (while=0 (a,I));
assume A8: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A8, XXREAL_0:2;
then A9: ((StepWhile=0 (a,I,p,s)) . k) . a = 0 by A5;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Nat such that
A10: (StepWhile=0 (a,I,p,s)) . (k + 1) = Comput ((p +* (while=0 (a,I))),(Initialize s),n) by A7, A8, XXREAL_0:2;
A11: (StepWhile=0 (a,I,p,s)) . (k + 1) = Comput (((p +* (while=0 (a,I))) +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,p,s)) . k)),((LifeSpan ((((p +* (while=0 (a,I))) +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . k)))) + 2)) by SCMFSA_9:def 4;
take m = n + ((LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . (k + 1))))) + 2); :: thesis:
I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) by A1, A9;
then IC ((StepWhile=0 (a,I,p,s)) . (k + 1)) = 0 by A11, A9, SCMFSA_9:22;
then (StepWhile=0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while=0 (a,I))),(Initialize s),(n + ((LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,p,s)) . (k + 1))))) + 2))) by A10, SCMFSA_9:26;
hence (StepWhile=0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while=0 (a,I))),(Initialize s),m) ; :: thesis:

end;

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

end;

A12: S₂[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis:
take n = (LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize s))) + 2; :: thesis:
thus (StepWhile=0 (a,I,p,s)) . (0 + 1) = Comput ((p +* (while=0 (a,I))),(Initialize s),n) by SCMFSA_9:25; :: thesis:

end;

A13: for k being Nat holds S₂[k] from NAT_1:sch 2(A12, A6);

per cases ;

suppose m = 0 ; :: thesis:

then s . a <> 0 by A4, SCMFSA_9:def 4;
hence while=0 (a,I) is_halting_on s,p by SCMFSA_9:18; :: thesis:

end;

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

set ii = (LifeSpan (((p +* (while=0 (a,I))) +* I),(Initialize s))) + 2;
set sm = (StepWhile=0 (a,I,p,s)) . m;
set pm = p +* (while=0 (a,I));
set sm1 = Initialize ((StepWhile=0 (a,I,p,s)) . m);
set pm1 = (p +* (while=0 (a,I))) +* (while=0 (a,I));
consider i being Nat such that
A15: m = i + 1 by A14, NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
set si = (StepWhile=0 (a,I,p,s)) . i;
set psi = p +* (while=0 (a,I));
A16: (StepWhile=0 (a,I,p,s)) . m = Comput (((p +* (while=0 (a,I))) +* (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 A15, SCMFSA_9:def 4;
m = i + 1 by A15;
then consider n being Nat such that
A17: (StepWhile=0 (a,I,p,s)) . m = Comput ((p +* (while=0 (a,I))),(Initialize s),n) by A13;
i < m by A15, NAT_1:13;
then A18: ((StepWhile=0 (a,I,p,s)) . i) . a = 0 by A5;
then I is_halting_on (StepWhile=0 (a,I,p,s)) . i,p +* (while=0 (a,I)) by A1;
then IC ((StepWhile=0 (a,I,p,s)) . m) = 0 by A16, A18, SCMFSA_9:22;
then Start-At (0,SCM+FSA) c= (StepWhile=0 (a,I,p,s)) . m by MEMSTR_0:30;
then A19: Initialize ((StepWhile=0 (a,I,p,s)) . m) = (StepWhile=0 (a,I,p,s)) . m by FUNCT_4:98;
while=0 (a,I) is_halting_on (StepWhile=0 (a,I,p,s)) . m,p +* (while=0 (a,I)) by A4, SCMFSA_9:18;
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 consider j being Nat such that
A20: CurInstr ((p +* (while=0 (a,I))),(Comput ((p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . m),j))) = halt SCM+FSA by A19;
A21: 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, A20, A21;
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:

end;