let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis:
let s be State of SCM+FSA; :: thesis:
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis:
let a be read-write Int-Location ; :: thesis:
assume A1: I is_closed_on s,P ; :: thesis:
set sI = s +* (Initialize I);
set PI = P +* I;
set s1 = s +* (Initialize (while>0 (a,I)));
set P1 = P +* (while>0 (a,I));
A2: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:26;
A3: ProgramPart I = I by RELAT_1:209;
defpred S₁[ Nat] means ( $1 <= LifeSpan ((P +* I),(s +* (Initialize I))) implies ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + $1))) = (IC (Comput ((P +* I),(s +* (Initialize I)),$1))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + $1))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),$1)) ) );
assume A4: I is_halting_on s,P ; :: thesis:

A5: now

let k be Element of NAT ; :: thesis:
assume A6: S₁[k] ; :: thesis:

now

A7: k + 0 < k + 1 by XREAL_1:8;
assume k + 1 <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis:
then k < LifeSpan ((P +* I),(s +* (Initialize I))) by A7, XXREAL_0:2;
hence ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + k) + 1))) = (IC (Comput ((P +* I),(s +* (Initialize I)),(k + 1)))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(k + 1))) ) by A1, A4, A6, Th44; :: thesis:

end;

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

end;

reconsider l = LifeSpan ((P +* I),(s +* (Initialize I))) as Element of NAT ;
set loc4 = (card I) + 4;
set i = a >0_goto 4;
set s2 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1);
A8: IC in dom (Initialize (while>0 (a,I))) by COMPOS_1:141;
A9: IC (s +* (Initialize (while>0 (a,I)))) = IC (Initialize (while>0 (a,I))) by A8, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
not a in dom (Initialize (while>0 (a,I))) by SCMFSA6B:12;
then A10: (s +* (Initialize (while>0 (a,I)))) . a = s . a by FUNCT_4:12;
assume A11: s . a > 0 ; :: thesis:
A12: 0 in dom (while>0 (a,I)) by Th10;
A13: (P +* (while>0 (a,I))) /. (IC (s +* (Initialize (while>0 (a,I))))) = (P +* (while>0 (a,I))) . (IC (s +* (Initialize (while>0 (a,I))))) by PBOOLE:158;
(P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by A12, FUNCT_4:14
.= (while>0 (a,I)) . 0
.= a >0_goto 4 by Th11 ;
then A14: CurInstr ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))) = a >0_goto 4 by A9, A13;
A15: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),0))) by EXTPRO_1:4
.= Following ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I))))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),(s +* (Initialize (while>0 (a,I))))) by A14 ;
then ( ( for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . c = (s +* (Initialize (while>0 (a,I)))) . c ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . f = (s +* (Initialize (while>0 (a,I)))) . f ) ) by SCMFSA_2:97;
then A16: DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) = DataPart (s +* (Initialize (while>0 (a,I)))) by SCMFSA6A:38
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* (Initialize I)) by SCMFSA8A:11 ;
A17: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),1)) . (IC )
.= 4 by A11, A15, A10, SCMFSA_2:97 ;
A18: S₁[ 0 ]

proof

assume 0 <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis:
A19: IC in dom (Initialize I) by COMPOS_1:141;
IC (Comput ((P +* I),(s +* (Initialize I)),0)) = IC (s +* (Initialize I)) by EXTPRO_1:3
.= IC (Initialize I) by A19, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
hence ( IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + 0))) = (IC (Comput ((P +* I),(s +* (Initialize I)),0))) + 4 & DataPart (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + 0))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),0)) ) by A17, A16, EXTPRO_1:3; :: thesis:

end;

A20: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A18, A5);
set s4 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1) + 1));
set s3 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1));
A21: (card I) + 4 in dom (while>0 (a,I)) by Th38;
set s2 = Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialize I))))));
S₁[l] by A20;
then A22: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialize I)))))))) = goto ((card I) + 4) by A1, A4, Th45;
A23: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialize I)))))))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + (LifeSpan ((P +* I),(s +* (Initialize I)))))))) by A22 ;
A24: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1))) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1))) . (IC )
.= (card I) + 4 by A23, SCMFSA_2:95 ;
A25: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1)))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1)))) by PBOOLE:158;
(P +* (while>0 (a,I))) . ((card I) + 4) = (P +* (while>0 (a,I))) . ((card I) + 4)
.= (while>0 (a,I)) . ((card I) + 4) by A21, A2, GRFUNC_1:8
.= goto 0 by Th46 ;
then A26: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1)))) = goto 0 by A24, A25;
A27: Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1) + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1)))) by EXTPRO_1:4
.= Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1)))) by A26 ;
A28: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1) + 1))) = (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(((1 + (LifeSpan ((P +* I),(s +* (Initialize I))))) + 1) + 1))) . (IC )
.= 0 by A27, SCMFSA_2:95 ;
hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 3))) = 0 ; :: thesis:
A29: (((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + 1) + 1 = (LifeSpan ((P +* I),(s +* (Initialize I)))) + (2 + 1) ;

A30: now

let k be Element of NAT ; :: thesis:
assume A31: k <= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 3 ; :: thesis:
assume k <> 0 ; :: thesis:
then consider n being Nat such that
A32: k = n + 1 by NAT_1:6;
( k <= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 or k >= ((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + 1 ) by NAT_1:13;
then A33: ( k <= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 or k = ((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + 1 or k > ((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + 1 ) by XXREAL_0:1;
reconsider n = n as Element of NAT by ORDINAL1:def 13;

per cases by A29, A33, NAT_1:13;

suppose k <= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ; :: thesis:

then n <= LifeSpan ((P +* I),(s +* (Initialize I))) by A32, XREAL_1:8;
then A34: IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),(1 + n))) = (IC (Comput ((P +* I),(s +* (Initialize I)),n))) + 4 by A20;
reconsider m = IC (Comput ((P +* I),(s +* (Initialize I)),n)) as Element of NAT ;
m in dom I by A1, SCMFSA7B:def 7, A3;
then m < card I by AFINSQ_1:70;
then A35: m + 4 < (card I) + 6 by XREAL_1:10;
card (while>0 (a,I)) = (card I) + 6 by Th5;
hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A32, A34, A35, AFINSQ_1:70; :: thesis:

end;

suppose k = ((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + 1 ; :: thesis:

hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A24, Th38; :: thesis:

end;

suppose k >= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 3 ; :: thesis:

then k = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 3 by A31, XXREAL_0:1;
hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A28, Th10; :: thesis:

end;

now

let k be Element of NAT ; :: thesis:
assume A36: k <= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 3 ; :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A12, A9, EXTPRO_1:3; :: thesis:

end;

suppose k <> 0 ; :: thesis:

hence IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) by A30, A36; :: thesis:

end;

hence for k being Element of NAT st k <= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 3 holds
IC (Comput ((P +* (while>0 (a,I))),(s +* (Initialize (while>0 (a,I)))),k)) in dom (while>0 (a,I)) ; :: thesis: