for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for md, p0, n being Nat
for f, f1 being FinSequence of INT st s . GBP = 0 & (s . (intpos 4)) - (s . (intpos 2)) > 0 & s . (intpos 2) = md & md >= p0 + 1 & s . (intpos 4) <= p0 + n & p0 >= 7 & f is_FinSequence_on s,p0 & len f = n & f1 is_FinSequence_on IExec (Partition,P,s),p0 & len f1 = n holds
( (IExec (Partition,P,s)) . GBP = 0 & (IExec (Partition,P,s)) . (intpos 1) = s . (intpos 1) & f,f1 are_fiberwise_equipotent & ex m4 being Nat st
( m4 = (IExec (Partition,P,s)) . (intpos 4) & md <= m4 & m4 <= s . (intpos 4) & ( for i being Nat st md <= i & i < m4 holds
(IExec (Partition,P,s)) . (intpos m4) >= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st m4 < i & i <= s . (intpos 4) holds
(IExec (Partition,P,s)) . (intpos m4) <= (IExec (Partition,P,s)) . (intpos i) ) & ( for i being Nat st i >= p0 + 1 & ( i < s . (intpos 2) or i > s . (intpos 4) ) holds
(IExec (Partition,P,s)) . (intpos i) = s . (intpos i) ) ) )