:: deftheorem Def1 defines parahalting SCMPDS_5:def 2 :
for i being Instruction of SCMPDS holds
( i is parahalting iff Load i is parahalting );