set S = Initialize s;
set P = p +* (while>0 (a,I));
set SW = StepWhile>0 (a,I,p,s);
set PW = p +* (while>0 (a,I));
A3: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:25;
defpred S₁[ Nat] means ((StepWhile>0 (a,I,p,s)) . $1) . a <= 0 ;
consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that
A4: for k being Nat holds
( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or S₁[k] ) by A2;
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,p,s)) . $1);
A5: for k being Nat holds
( H₁(k + 1) < H₁(k) or S₁[k] ) by A4;
consider m being Nat such that
A6: S₁[m] and
A7: for n being Nat st S₁[n] holds
m <= n from NAT_1:sch 18(A5);
take m ; :: thesis:
take m ; :: thesis:
thus m = m ; :: thesis:
thus ((StepWhile>0 (a,I,p,s)) . m) . a <= 0 by A6; :: thesis:
thus for n being Nat st ((StepWhile>0 (a,I,p,s)) . n) . a <= 0 holds
m <= n by A7; :: thesis:
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) );
A8: ProperBodyWhile>0 a,I,s,p by A1, Th26;

A9: now :: thesis:

let k be Nat; :: thesis:
assume A10: 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 A11: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A11, XXREAL_0:2;
then A12: ((StepWhile>0 (a,I,p,s)) . k) . a > 0 by A7;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Nat such that
A13: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),n) by A10, A11, XXREAL_0:2;
A14: (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))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . k)))) + 2)) by SCMFSA_9:def 5;
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 A8, A12;
then IC ((StepWhile>0 (a,I,p,s)) . (k + 1)) = 0 by A14, A12, SCMFSA_9:42;
hence (StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),m) by A13, SCMFSA_9:45; :: thesis:

end;

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

end;

A15: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
A16: 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:44; :: thesis:

end;

A17: for k being Nat holds S₂[k] from NAT_1:sch 2(A16, A9);

per cases ;

suppose A18: m = 0 ; :: thesis:

A19: DataPart (Initialize s) = DataPart s by MEMSTR_0:79
.= DataPart ((StepWhile>0 (a,I,p,s)) . m) by A18, SCMFSA_9:def 5 ;
then (Initialize s) . a = ((StepWhile>0 (a,I,p,s)) . m) . a by SCMFSA_M:2;
hence DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) by A6, A19, Th29, A3; :: thesis:

end;

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

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
A21: m = i + 1 by A20, 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));
A22: (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 A21, SCMFSA_9:def 5;
m = i + 1 by A21;
then consider n being Nat such that
A23: (StepWhile>0 (a,I,p,s)) . m = Comput ((p +* (while>0 (a,I))),(Initialize s),n) by A17;
i < m by A21, NAT_1:13;
then A24: ((StepWhile>0 (a,I,p,s)) . i) . a > 0 by A7;
then I is_halting_on (StepWhile>0 (a,I,p,s)) . i,p +* (while>0 (a,I)) by A8;
then A25: IC ((StepWhile>0 (a,I,p,s)) . m) = 0 by A22, A24, SCMFSA_9:42;
A26: IC (Initialize ((StepWhile>0 (a,I,p,s)) . m)) = IC (Start-At (0,SCM+FSA)) by A15, FUNCT_4:13
.= IC ((StepWhile>0 (a,I,p,s)) . m) by A25, FUNCOP_1:72 ;
DataPart (Initialize ((StepWhile>0 (a,I,p,s)) . m)) = DataPart ((StepWhile>0 (a,I,p,s)) . m) by MEMSTR_0:79;
then A27: Initialize ((StepWhile>0 (a,I,p,s)) . m) = (StepWhile>0 (a,I,p,s)) . m by A26, MEMSTR_0:78;
while>0 (a,I) is_halting_on (StepWhile>0 (a,I,p,s)) . m,p +* (while>0 (a,I)) by A6, SCMFSA_9:38;
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
A28: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j))) = halt SCM+FSA by A27;
A29: 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 A23, A28, A29;
then A30: Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s)))) = Comput ((p +* (while>0 (a,I))),(Initialize s),(n + j)) by EXTPRO_1:24
.= Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j) by A23, EXTPRO_1:4
.= Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),(LifeSpan ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m)))) by A28, EXTPRO_1:24 ;
Start-At (0,SCM+FSA) c= (StepWhile>0 (a,I,p,s)) . m by A27, FUNCT_4:25;
then (StepWhile>0 (a,I,p,s)) . m is 0 -started by MEMSTR_0:29;
hence DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) by A6, A30, Th29, A3; :: thesis:

end;