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