for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, p0 being Nat st s . GBP = 0 & s . (intpos 2) = md & md >= p0 + 1 & p0 >= 7 holds
( Partition is_closed_on s,P & Partition is_halting_on s,P )