Stop SCMPDS = Load (halt SCMPDS ) ;
hence halt SCMPDS is parahalting by Def2; :: thesis: verum