let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P

let I be really-closed Program of SCM+FSA; :: thesis: for J being Program of SCM+FSA
for s being State of SCM+FSA st I is_halting_on s,P holds
((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P

let J be Program of SCM+FSA; :: thesis: for s being State of SCM+FSA st I is_halting_on s,P holds
((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P

let s be State of SCM+FSA; :: thesis: ( I is_halting_on s,P implies ((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P )
set IJ2 = ((I ";" (Goto ((card J) + 1))) ";" J) ";" ();
set s2 = Initialize s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ());
assume I is_halting_on s,P ; :: thesis: ((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P
then P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" ()) halts_on Initialize s by Lm5;
hence ((I ";" (Goto ((card J) + 1))) ";" J) ";" () is_halting_on s,P by SCMFSA7B:def 7; :: thesis: verum