let s be State of SCMPDS ; :: thesis: for I being parahalting Program of SCMPDS st Initialize (stop I) c= s holds
ProgramPart s halts_on s
let I be parahalting Program of SCMPDS ; :: thesis: ( Initialize (stop I) c= s implies ProgramPart s halts_on s )
assume A1: Initialize (stop I) c= s ; :: thesis: ProgramPart s halts_on s
Initialize (stop I) is halting by Def10;
hence ProgramPart s halts_on s by A1, AMI_1:def 26; :: thesis: verum