[0 ,{} ,<*0 *>] in SCMPDS-Instr by SCMPDS_1:13;
then the haltF of SCMPDS = [0 ,{} ,<*0 *>] by FUNCT_7:def 1
.= goto 0 ;
hence the haltF of SCMPDS is halting by Th75; :: according to AMI_1:def 9 :: thesis: verum