for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st s . GBP = 0 holds
( for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_closed_on s,P & for-down (GBP,2,1,(Load (AddTo (GBP,3,1)))) is_halting_on s,P )