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