let s be State of SCMPDS ; :: according to AMI_1:def 26 :: thesis: ( not Initialize (stop I) c= s or ProgramPart s halts_on s )
assume Initialize (stop I) c= s ; :: thesis: ProgramPart s halts_on s
hence ProgramPart s halts_on s by Th63; :: thesis: verum