[0,{},{}] in SCM-Instr by AMI_2:1;
then the haltF of SCM = [0,{},{}] by FUNCT_7:def 1;
hence the haltF of SCM is halting by Lm4; :: according to EXTPRO_1:def 4 :: thesis: verum