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: while=0 (a,I) c= p +* (while=0 (a,I)) by FUNCT_4:26;
A4: (p +* (while=0 (a,I))) +* (while=0 (a,I)) = p +* (while=0 (a,I)) by FUNCT_4:99;
A5: ProgramPart (while=0 (a,I)) = while=0 (a,I) by RELAT_1:209;
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, Def2;
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, Th19;

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 4, A4;
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, Def1;
then IC ((StepWhile=0 (a,I,p,s)) . (k + 1)) = 0 by A17, A15, SCMFSA_9:22;
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:31; :: 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:30; :: 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 4 ;
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, Th22, A3; :: 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 4, A4;
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, Def1;
then A28: IC ((StepWhile=0 (a,I,p,s)) . m) = 0 by A25, A27, SCMFSA_9:22;
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;
A32: (p +* (while=0 (a,I))) +* (while=0 (a,I)) = p +* (while=0 (a,I)) by FUNCT_4:99;
while=0 (a,I) is_halting_on (StepWhile=0 (a,I,p,s)) . m,p +* (while=0 (a,I)) by A9, SCMFSA_9:18;
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, A5;
then consider j being Element of NAT such that
A33: 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, A32;
A34: 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, A33, A34;
then A35: 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 A33, 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, A35, Th22, A3; :: thesis:

end;