let I be Instruction of SCM+FSA; :: thesis: ( I is halting implies I = halt SCM+FSA )
assume I is halting ; :: thesis: I = halt SCM+FSA
then I = [0,{},{}] by Lm4;
hence I = halt SCM+FSA by Lm4; :: thesis: verum