[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 EXTPRO_1:def 4 :: thesis: verum