:: deftheorem defines parahalting SCMPDS_4:def 7 :
for I being Program of holds
( I is parahalting iff for s being 0 -started State of SCMPDS
for P being Instruction-Sequence of SCMPDS st stop I c= P holds
P halts_on s );