9.3. Лемма

У состояний из ВС vs⚪ множества их прообразов в её ВС-прообразе vs◎ не пересекаются.

Если бы это было не так, то имелось бы некое состояние s◎ в vs◎, имеющее проекцией как минимум пару состояний s1⚪ и s2⚪ из vs⚪.

Но эти состояния находятся в отношении ЛИБО, то есть их формирует в том числе хотя бы одна переменная v, которая имеет для них разные значения.

Эта же переменная должна формировать и s◎, но её значения оказывается противоречивым, что доказывает ложность исходного предположения о наличии в vs◎ указанного состояния s◎.

Назад Вперёд