- 217
- 35
∀ CM ∀ t ∀ j:
SM(t) = SM0 ∧
PM(t) = j ∧
{ CM(t, j) … CM(t, j + |v| - 1)} = v ⇒
∃ v' ∃ j' ∃ t' ∃ t":
t < t" < t' ∧
{j' … j' +|v'|} ∩ {j … j + |v|} = ∅ ∧
{ CM(t', j') … CM(t', j' + |v'| - 1)} = v' ∧
PM(t") ∈ { j' … j' + |v'| - 1 }
SM(t) = SM0 ∧
PM(t) = j ∧
{ CM(t, j) … CM(t, j + |v| - 1)} = v ⇒
∃ v' ∃ j' ∃ t' ∃ t":
t < t" < t' ∧
{j' … j' +|v'|} ∩ {j … j + |v|} = ∅ ∧
{ CM(t', j') … CM(t', j' + |v'| - 1)} = v' ∧
PM(t") ∈ { j' … j' + |v'| - 1 }