[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 AMI_1:def 9 :: thesis: verum