set S = s +* (Initialize (while>0 (a,I)));
set P = p +* (while>0 (a,I));
set SW = StepWhile>0 (a,I,p,s);
set PW = p +* (while>0 (a,I));
A3: ProgramPart (while>0 (a,I)) = while>0 (a,I) by RELAT_1:209;
A4: while>0 (a,I) c= p +* (while>0 (a,I)) by FUNCT_4:26;
A5: (p +* (while>0 (a,I))) +* (while>0 (a,I)) = p +* (while>0 (a,I)) by FUNCT_4:99;
defpred S₁[ Nat] means ((StepWhile>0 (a,I,p,s)) . $1) . a <= 0 ;
A6: Initialize (while>0 (a,I)) c= s +* (Initialize (while>0 (a,I))) by FUNCT_4:26;
consider f being Function of (product the Object-Kind of SCM+FSA),NAT such that
A7: for k being Element of NAT holds
( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or S₁[k] ) by A2, Def5;
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,p,s)) . $1);
A8: for k being Element of NAT holds
( H₁(k + 1) < H₁(k) or S₁[k] ) by A7;
consider m being Element of NAT such that
A9: S₁[m] and
A10: for n being Element of NAT st S₁[n] holds
m <= n from NAT_1:sch 18(A8);
take m ; :: thesis:
take m ; :: thesis:
thus m = m ; :: thesis:
thus ((StepWhile>0 (a,I,p,s)) . m) . a <= 0 by A9; :: thesis:
thus for n being Element of NAT st ((StepWhile>0 (a,I,p,s)) . n) . a <= 0 holds
m <= n by A10; :: thesis:
defpred S₂[ Nat] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 (a,I,p,s)) . ($1 + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k) );
A11: ProperBodyWhile>0 a,I,s,p by A1, Th32;

A12: now

let k be Element of NAT ; :: thesis:
assume A13: S₂[k] ; :: thesis:

now

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 A14: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:8;
then k < m by A14, XXREAL_0:2;
then A15: ((StepWhile>0 (a,I,p,s)) . k) . a > 0 by A10;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
then consider n being Element of NAT such that
A16: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n) by A13, A14, XXREAL_0:2;
A17: (StepWhile>0 (a,I,p,s)) . (k + 1) = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . k) +* (Initialize (while>0 (a,I)))),((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . k) +* (Initialize I)))) + 3)) by SCMFSA_9:def 5, A5;
take m = n + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . (k + 1)) +* (Initialize I)))) + 3); :: thesis:
( I is_closed_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) ) by A11, A15, Def4;
then IC ((StepWhile>0 (a,I,p,s)) . (k + 1)) = 0 by A17, A15, SCMFSA_9:47;
hence (StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),m) by A16, SCMFSA_9:52; :: thesis:

end;

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

end;

A18: IC in dom (Initialize (while>0 (a,I))) by COMPOS_1:141;
A19: S₂[ 0 ]

proof

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

end;

A20: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A19, A12);

per cases ;

suppose A21: m = 0 ; :: thesis:

A22: DataPart (s +* (Initialize (while>0 (a,I)))) = DataPart s by SCMFSA8A:11
.= DataPart ((StepWhile>0 (a,I,p,s)) . m) by A21, SCMFSA_9:def 5 ;
then (s +* (Initialize (while>0 (a,I)))) . a = ((StepWhile>0 (a,I,p,s)) . m) . a by SCMFSA6A:38;
hence DataPart (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) by A9, A6, A22, Th35, A4; :: thesis:

end;

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

set sm = (StepWhile>0 (a,I,p,s)) . m;
set pm = p +* (while>0 (a,I));
set sm1 = ((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)));
set pm1 = (p +* (while>0 (a,I))) +* (while>0 (a,I));
consider i being Nat such that
A24: m = i + 1 by A23, NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set si = (StepWhile>0 (a,I,p,s)) . i;
set psi = p +* (while>0 (a,I));
A25: (StepWhile>0 (a,I,p,s)) . m = Comput (((p +* (while>0 (a,I))) +* (while>0 (a,I))),(((StepWhile>0 (a,I,p,s)) . i) +* (Initialize (while>0 (a,I)))),((LifeSpan (((p +* (while>0 (a,I))) +* I),(((StepWhile>0 (a,I,p,s)) . i) +* (Initialize I)))) + 3)) by A24, SCMFSA_9:def 5, A5;
m = i + 1 by A24;
then consider n being Element of NAT such that
A26: (StepWhile>0 (a,I,p,s)) . m = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n) by A20;
i < m by A24, NAT_1:13;
then A27: ((StepWhile>0 (a,I,p,s)) . i) . a > 0 by A10;
then ( I is_closed_on (StepWhile>0 (a,I,p,s)) . i,p +* (while>0 (a,I)) & I is_halting_on (StepWhile>0 (a,I,p,s)) . i,p +* (while>0 (a,I)) ) by A11, Def4;
then A28: IC ((StepWhile>0 (a,I,p,s)) . m) = 0 by A25, A27, SCMFSA_9:47;
A29: IC (((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))) = IC (Initialize (while>0 (a,I))) by A18, FUNCT_4:14
.= IC ((StepWhile>0 (a,I,p,s)) . m) by A28, COMPOS_1:142 ;
A30: ProgramPart ((StepWhile>0 (a,I,p,s)) . m) = ProgramPart (s +* (Initialize (while>0 (a,I)))) by A26, AMI_1:123
.= ProgramPart ((s +* (Initialize (while>0 (a,I)))) +* (Initialize (while>0 (a,I)))) by FUNCT_4:99
.= (ProgramPart (s +* (Initialize (while>0 (a,I))))) +* (ProgramPart (Initialize (while>0 (a,I)))) by FUNCT_4:75
.= (ProgramPart ((StepWhile>0 (a,I,p,s)) . m)) +* (ProgramPart (Initialize (while>0 (a,I)))) by A26, AMI_1:123
.= ProgramPart (((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))) by FUNCT_4:75 ;
DataPart (((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I)))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) by SCMFSA8A:11;
then A31: ((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I))) = (StepWhile>0 (a,I,p,s)) . m by A29, SCMFSA_9:29, A30;
while>0 (a,I) is_halting_on (StepWhile>0 (a,I,p,s)) . m,p +* (while>0 (a,I)) by A9, SCMFSA_9:43;
then (p +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on ((StepWhile>0 (a,I,p,s)) . m) +* (Initialize (while>0 (a,I))) by SCMFSA7B:def 8, A3;
then consider j being Element of NAT such that
A32: CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j))) = halt SCM+FSA by A31, EXTPRO_1:30, A5;
A33: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(n + j)) = Comput ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),n)),j) by EXTPRO_1:5;
CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(n + j)))) = halt SCM+FSA by A26, A32, A33;
then A34: Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))))) = Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(n + j)) by EXTPRO_1:24
.= Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j) by A26, EXTPRO_1:5
.= 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 A32, EXTPRO_1:24 ;
Initialize (while>0 (a,I)) c= (StepWhile>0 (a,I,p,s)) . m by A31, FUNCT_4:26;
hence DataPart (Comput ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(LifeSpan ((p +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) by A9, A34, Th35, A4; :: thesis:

end;