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) ";" (Stop SCM+FSA) 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) ";" (Stop SCM+FSA) 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) ";" (Stop SCM+FSA) 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) ";" (Stop SCM+FSA) is_halting_on s,P )
set IJ2 = ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA);
set s2 = Initialize s;
set P2 = P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA));
assume I is_halting_on s,P ; :: thesis: ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P
then P +* (((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA)) halts_on Initialize s by Lm5;
hence ((I ";" (Goto ((card J) + 1))) ";" J) ";" (Stop SCM+FSA) is_halting_on s,P by SCMFSA7B:def 7; :: thesis: verum