for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds not P +* ((IC s),(goto (IC s))) halts_on s by Lm1;