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 Lm1;
hence I = halt SCM+FSA by Lm1; :: thesis: verum