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 A1: 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 A2: 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 A3: P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by A1, Lm5;
A4: LifeSpan ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s)) = (LifeSpan ((P +* I),(Initialize s))) + 2 by A1, A2, Lm5;

now :: thesis: for k being Element of NAT holds 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))

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 A5: ( 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 A6: 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 A7: (card I) + 0 < card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by A6, 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 A5;

suppose A8: 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 A1, A2, A8, Lm5;
then IC (Comput ((P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA))),(Initialize s),k)) in dom I by A1, SCMFSA7B:def 6;
then n < card I by AFINSQ_1:66;
then n < card (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) by A7, 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 A1, A2, 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 A7, AFINSQ_1:66; :: thesis: verum

end;

suppose A9: 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 A6;
then A10: (((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 A1, A2, A9, 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 A3, EXTPRO_1:25
.= ((card I) + (card J)) + 1 by A1, A2, 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 A10, 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 A3, SCMFSA7B:def 7; :: thesis: verum