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