for I being Instruction of SCM+FSA st I is halting holds
I = halt SCM+FSA by Lm1;