let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P )
let I, J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P )
let s be State of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P ) )
set IJ2 = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA);
A1: ProgramPart (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) by RELAT_1:209;
A2: ProgramPart I = I by RELAT_1:209;
assume A3: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or ( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P ) )
set s1 = s +* (Initialize I);
set s2 = s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)));
set P2 = P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA));
assume A4: I is_halting_on s,P ; :: thesis: ( ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P & ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P )
then A5: P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) by A3, Lm5;
A6: LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 2 by A3, A4, Lm5;

now

let k be Element of NAT ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),b₁)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
( k <= LifeSpan ((P +* I),(s +* (Initialize I))) or k >= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ) by NAT_1:13;
then ( k <= LifeSpan ((P +* I),(s +* (Initialize I))) or k = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 or k > (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ) by XXREAL_0:1;
then A7: ( k <= LifeSpan ((P +* I),(s +* (Initialize I))) or k = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 or k >= ((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1) + 1 ) by NAT_1:13;
card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then A8: card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) = (card ((I ';' (Goto ((card J) + 1))) ';' J)) + 1 by SCMFSA6A:61
.= ((card (I ';' (Goto ((card J) + 1)))) + (card J)) + 1 by SCMFSA6A:61
.= (((card I) + (card (Goto ((card J) + 1)))) + (card J)) + 1 by SCMFSA6A:61
.= (((card I) + 1) + (card J)) + 1 by Lm1
.= (card I) + (((card J) + 1) + 1) ;
0 <= (card J) + 1 by NAT_1:2;
then 0 + 0 < ((card J) + 1) + 1 by XREAL_1:10;
then A9: (card I) + 0 < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A8, XREAL_1:8;

per cases ( k <= LifeSpan ((P +* I),(s +* (Initialize I))) or k = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 or k >= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 2 ) by A7;

suppose A10: k <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),b₁)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))

reconsider n = IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) as Element of NAT ;
IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) = IC (Comput ((P +* I),(s +* (Initialize I)),k)) by A3, A4, A10, Lm5;
then IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) in dom I by A3, SCMFSA7B:def 7, A2;
then n < card I by AFINSQ_1:70;
then n < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A9, XXREAL_0:2;
hence IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by AFINSQ_1:70; :: thesis: verum

end;

suppose k = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),b₁)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))

then IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) = card I by A3, A4, Lm5;
hence IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A9, AFINSQ_1:70; :: thesis: verum

end;

suppose A11: k >= (LifeSpan ((P +* I),(s +* (Initialize I)))) + 2 ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),b₁)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))

card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) = (((card I) + (card J)) + 1) + 1 by A8;
then A12: (((card I) + (card J)) + 1) + 0 < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by XREAL_1:8;
k >= LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) by A3, A4, A11, Lm5;
then IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) = IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),(LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))))) by A5, Th5
.= ((card I) + (card J)) + 1 by A3, A4, A6, Lm5 ;
hence IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A12, AFINSQ_1:70; :: thesis: verum

end;

end;

end;

hence ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def 7, A1; :: thesis: ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P
thus ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_halting_on s,P by A5, SCMFSA7B:def 8, A1; :: thesis: verum