reconsider i = halt SCM as Instruction of SCM+FSA by Th38;
InsCode i = 0 by AMI_5:37;
hence halt SCM = halt SCM+FSA by Th122; :: thesis: verum