Пусть Φ Ψ — атомарные формулы логики предикатов

∃x∀yΦ(x,y)→¬∀x¬∀yΦ(x,y)∧∃zΨ(z,y):
подформулы
Φ(x,y),
∀yΦ(x,y),
∃x∀yΦ(x,y),
Ψ(x,y),
∃zΨ(z,y),
∀yΦ(x,y)∧∃zΨ(z,y),
¬∀yΦ(x,y)∧∃zΨ(z,y),
∀x¬∀yΦ(x,y)∧∃zΨ(z,y),
¬∀x¬∀yΦ(x,y)∧∃zΨ(z,y),
∃x∀yΦx,y→¬∀x¬∀yΦx,y∧∃zΨz,y;
переменные
единственным свободным вхождением является последнее вхождение переменной y, все остальные вхождения всех переменных — связанные.