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

proof

assume 0 + 1 <= m ; :: thesis:
take n = (LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3; :: thesis:
thus (StepWhile>0 a,I,s) . (0 + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n by SCMFSA_9:51; :: thesis:

end;

A10: IC SCM+FSA in dom ((while>0 a,I) +* (Start-At (insloc 0 ))) by SF_MASTR:65;

A11: now

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

now

assume A13: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:8;
then A14: k < m by A13, XXREAL_0:2;
A15: (k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
set sk = (StepWhile>0 a,I,s) . k;
set sk1 = (StepWhile>0 a,I,s) . (k + 1);
consider n being Element of NAT such that
A16: (StepWhile>0 a,I,s) . (k + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n by A12, A13, A15, XXREAL_0:2;
A17: (StepWhile>0 a,I,s) . (k + 1) = Computation (((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At (insloc 0 ))))) + 3) by SCMFSA_9:def 5;
A18: ((StepWhile>0 a,I,s) . k) . a > 0 by A6, A14;
then ( I is_closed_on (StepWhile>0 a,I,s) . k & I is_halting_on (StepWhile>0 a,I,s) . k ) by A8, Def4;
then A19: IC ((StepWhile>0 a,I,s) . (k + 1)) = insloc 0 by A17, A18, SCMFSA_9:47;
take m = n + ((LifeSpan (((StepWhile>0 a,I,s) . (k + 1)) +* (I +* (Start-At (insloc 0 ))))) + 3); :: thesis:
thus (StepWhile>0 a,I,s) . ((k + 1) + 1) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),m by A16, A19, SCMFSA_9:52; :: thesis:

end;

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

end;

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

per cases ;

suppose A21: m = 0 ; :: thesis:

A22: DataPart (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = DataPart s by SCMFSA8A:11
.= DataPart ((StepWhile>0 a,I,s) . m) by A21, SCMFSA_9:def 5 ;
then (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . a = ((StepWhile>0 a,I,s) . m) . a by SCMFSA6A:38;
hence DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . m) by A5, A7, A22, Th35; :: thesis:

end;

suppose m <> 0 ; :: thesis:

then consider i being Nat such that
A23: m = i + 1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
set si = (StepWhile>0 a,I,s) . i;
set sm = (StepWhile>0 a,I,s) . m;
set sm1 = ((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 )));
m = i + 1 by A23;
then consider n being Element of NAT such that
A24: (StepWhile>0 a,I,s) . m = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),n by A20;
A25: (StepWhile>0 a,I,s) . m = Computation (((StepWhile>0 a,I,s) . i) +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (((StepWhile>0 a,I,s) . i) +* (I +* (Start-At (insloc 0 ))))) + 3) by A23, SCMFSA_9:def 5;
i < m by A23, NAT_1:13;
then A26: ((StepWhile>0 a,I,s) . i) . a > 0 by A6;
then ( I is_closed_on (StepWhile>0 a,I,s) . i & I is_halting_on (StepWhile>0 a,I,s) . i ) by A8, Def4;
then A27: IC ((StepWhile>0 a,I,s) . m) = insloc 0 by A25, A26, SCMFSA_9:47;
A28: IC (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) . (IC SCM+FSA ) by AMI_1:def 15
.= ((while>0 a,I) +* (Start-At (insloc 0 ))) . (IC SCM+FSA ) by A10, FUNCT_4:14
.= IC ((StepWhile>0 a,I,s) . m) by A27, SF_MASTR:66 ;
A29: DataPart (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) = DataPart ((StepWhile>0 a,I,s) . m) by SCMFSA8A:11;
((StepWhile>0 a,I,s) . m) | NAT = (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))) | NAT by A24, AMI_1:123;
then (((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 )))) | NAT = ((StepWhile>0 a,I,s) . m) | NAT by FUNCT_4:100;
then A30: ((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) = (StepWhile>0 a,I,s) . m by A28, A29, SCMFSA_9:29;
while>0 a,I is_halting_on (StepWhile>0 a,I,s) . m by A5, SCMFSA_9:43;
then ((StepWhile>0 a,I,s) . m) +* ((while>0 a,I) +* (Start-At (insloc 0 ))) is halting by SCMFSA7B:def 8;
then consider j being Element of NAT such that
A31: CurInstr (Computation ((StepWhile>0 a,I,s) . m),j) = halt SCM+FSA by A30, AMI_1:def 20;
A32: CurInstr (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + j)) = halt SCM+FSA by A24, A31, AMI_1:51;
A33: (while>0 a,I) +* (Start-At (insloc 0 )) c= (StepWhile>0 a,I,s) . m by A30, FUNCT_4:26;
Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 ))))) = Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(n + j) by A32, AMI_1:127
.= Computation ((StepWhile>0 a,I,s) . m),j by A24, AMI_1:51
.= Computation ((StepWhile>0 a,I,s) . m),(LifeSpan ((StepWhile>0 a,I,s) . m)) by A31, AMI_1:127 ;
hence DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . m) by A5, A33, Th35; :: thesis:

end;