let P be Instruction-Sequence of SCM+FSA; :: 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);
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 = Initialize s;
set s2 = Initialize s;
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 Initialize s by A3, Lm5;
A6: LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 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))),(Initialize s),b₁)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))
( k <= LifeSpan ((P +* I),(Initialize s)) or k >= (LifeSpan ((P +* I),(Initialize s))) + 1 ) by NAT_1:13;
then ( k <= LifeSpan ((P +* I),(Initialize s)) or k = (LifeSpan ((P +* I),(Initialize s))) + 1 or k > (LifeSpan ((P +* I),(Initialize s))) + 1 ) by XXREAL_0:1;
then A7: ( k <= LifeSpan ((P +* I),(Initialize s)) or k = (LifeSpan ((P +* I),(Initialize s))) + 1 or k >= ((LifeSpan ((P +* I),(Initialize s))) + 1) + 1 ) by NAT_1:13;
card (Stop SCM+FSA) = 1 by COMPOS_1:4;
then A8: card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) = (card ((I ';' (Goto ((card J) + 1))) ';' J)) + 1 by SCMFSA6A:21
.= ((card (I ';' (Goto ((card J) + 1)))) + (card J)) + 1 by SCMFSA6A:21
.= (((card I) + (card (Goto ((card J) + 1)))) + (card J)) + 1 by SCMFSA6A:21
.= (((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:8;
then A9: (card I) + 0 < card (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A8, XREAL_1:6;

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

suppose A10: k <= LifeSpan ((P +* I),(Initialize s)) ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),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))),(Initialize s),k)) as Element of NAT ;
IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* I),(Initialize s),k)) by A3, A4, A10, Lm5;
then IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) in dom I by A3, SCMFSA7B:def 6;
then n < card I by AFINSQ_1:66;
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))),(Initialize s),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by AFINSQ_1:66; :: thesis: verum

end;

suppose k = (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),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))),(Initialize s),k)) = card I by A3, A4, Lm5;
hence IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A9, AFINSQ_1:66; :: thesis: verum

end;

suppose A11: k >= (LifeSpan ((P +* I),(Initialize s))) + 2 ; :: thesis: IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),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:6;
k >= LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s)) by A3, A4, A11, Lm5;
then IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) = IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),(LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s))))) by A5, EXTPRO_1:25
.= ((card I) + (card J)) + 1 by A3, A4, A6, Lm5 ;
hence IC (Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(Initialize s),k)) in dom (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) by A12, AFINSQ_1:66; :: thesis: verum

end;

end;

end;

hence ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def 6; :: 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 7; :: thesis: verum