[0,{},{}] in SCM+FSA-Instr by SCMFSA_1:4;
then the haltF of SCM+FSA = [0,{},{}] by FUNCT_7:def 1;
hence the haltF of SCM+FSA is halting by Th103, AMI_3:71; :: according to EXTPRO_1:def 4 :: thesis: verum