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

A9: now

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

now

set sk1 = (StepWhile>0 (a,I,s)) . (k + 1);
set sk = (StepWhile>0 (a,I,s)) . k;
assume A11: (k + 1) + 1 <= m ; :: thesis:
k + 0 < k + (1 + 1) by XREAL_1:8;
then k < m by A11, XXREAL_0:2;
then A12: ((StepWhile>0 (a,I,s)) . k) . a > 0 by A7;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:8;
then consider n being Element of NAT such that
A13: (StepWhile>0 (a,I,s)) . (k + 1) = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),n) by A10, A11, XXREAL_0:2;
A14: (StepWhile>0 (a,I,s)) . (k + 1) = Comput ((ProgramPart (((StepWhile>0 (a,I,s)) . k) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(((StepWhile>0 (a,I,s)) . k) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((StepWhile>0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA))))),(((StepWhile>0 (a,I,s)) . k) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) by SCMFSA_9:def 5;
take m = n + ((LifeSpan ((ProgramPart (((StepWhile>0 (a,I,s)) . (k + 1)) +* (I +* (Start-At (0,SCM+FSA))))),(((StepWhile>0 (a,I,s)) . (k + 1)) +* (I +* (Start-At (0,SCM+FSA)))))) + 3); :: thesis:
( I is_closed_on (StepWhile>0 (a,I,s)) . k & I is_halting_on (StepWhile>0 (a,I,s)) . k ) by A8, A12, Def4;
then IC ((StepWhile>0 (a,I,s)) . (k + 1)) = 0 by A14, A12, SCMFSA_9:47;
hence (StepWhile>0 (a,I,s)) . ((k + 1) + 1) = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),m) by A13, SCMFSA_9:52; :: thesis:

end;

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

end;

A15: IC SCM+FSA in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
A16: S₂[ 0 ]

proof

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

end;

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

per cases ;

suppose A18: m = 0 ; :: thesis:

A19: DataPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = DataPart s by SCMFSA8A:11
.= DataPart ((StepWhile>0 (a,I,s)) . m) by A18, SCMFSA_9:def 5 ;
then (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a = ((StepWhile>0 (a,I,s)) . m) . a by SCMFSA6A:38;
hence DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . m) by A6, A3, A19, Th35; :: thesis:

end;

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

set sm = (StepWhile>0 (a,I,s)) . m;
set sm1 = ((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)));
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 13;
set si = (StepWhile>0 (a,I,s)) . i;
A22: (StepWhile>0 (a,I,s)) . m = Comput ((ProgramPart (((StepWhile>0 (a,I,s)) . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(((StepWhile>0 (a,I,s)) . i) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (((StepWhile>0 (a,I,s)) . i) +* (I +* (Start-At (0,SCM+FSA))))),(((StepWhile>0 (a,I,s)) . i) +* (I +* (Start-At (0,SCM+FSA)))))) + 3)) by A21, SCMFSA_9:def 5;
m = i + 1 by A21;
then consider n being Element of NAT such that
A23: (StepWhile>0 (a,I,s)) . m = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),n) by A17;
i < m by A21, NAT_1:13;
then A24: ((StepWhile>0 (a,I,s)) . i) . a > 0 by A7;
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 A25: IC ((StepWhile>0 (a,I,s)) . m) = 0 by A22, A24, SCMFSA_9:47;
A26: IC (((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = IC ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by A15, FUNCT_4:14
.= IC ((StepWhile>0 (a,I,s)) . m) by A25, COMPOS_1:142 ;
ProgramPart ((StepWhile>0 (a,I,s)) . m) = ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) by A23, AMI_1:123;
then ( DataPart (((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = DataPart ((StepWhile>0 (a,I,s)) . m) & ProgramPart (((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart ((StepWhile>0 (a,I,s)) . m) ) by FUNCT_4:100, SCMFSA8A:11;
then A27: ((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) = (StepWhile>0 (a,I,s)) . m by A26, SCMFSA_9:29;
while>0 (a,I) is_halting_on (StepWhile>0 (a,I,s)) . m by A6, SCMFSA_9:43;
then ProgramPart (((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) halts_on ((StepWhile>0 (a,I,s)) . m) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA7B:def 8;
then consider j being Element of NAT such that
A28: CurInstr ((ProgramPart ((StepWhile>0 (a,I,s)) . m)),(Comput ((ProgramPart ((StepWhile>0 (a,I,s)) . m)),((StepWhile>0 (a,I,s)) . m),j))) = halt SCM+FSA by A27, EXTPRO_1:30;
S: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),n)) by AMI_1:123;
x: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(n + j)) = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),n)),j) by EXTPRO_1:5;
T: ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart ((StepWhile>0 (a,I,s)) . m) by A23, AMI_1:123;
CurInstr ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(n + j)))) = halt SCM+FSA by A23, A28, x, S;
then A29: Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))))) = Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(n + j)) by EXTPRO_1:24
.= Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((StepWhile>0 (a,I,s)) . m),j) by A23, EXTPRO_1:5
.= Comput ((ProgramPart ((StepWhile>0 (a,I,s)) . m)),((StepWhile>0 (a,I,s)) . m),(LifeSpan ((ProgramPart ((StepWhile>0 (a,I,s)) . m)),((StepWhile>0 (a,I,s)) . m)))) by A28, T, EXTPRO_1:24 ;
(while>0 (a,I)) +* (Start-At (0,SCM+FSA)) c= (StepWhile>0 (a,I,s)) . m by A27, FUNCT_4:26;
hence DataPart (Comput ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(LifeSpan ((ProgramPart (s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))))) = DataPart ((StepWhile>0 (a,I,s)) . m) by A6, A29, Th35; :: thesis:

end;

end;