for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for sp, cv, result, pp, pD being Nat st s . (intpos sp) > sp & cv < result & s . (intpos pp) = pD & (s . (intpos sp)) + result < pp & pp < pD & pD < s . (intpos pD) holds
( for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_closed_on s,P & for-down ((intpos sp),cv,1,((AddTo ((intpos sp),result,(intpos pD),0)) ';' (AddTo ((intpos pp),0,1)))) is_halting_on s,P )