Решение

	{x = y} |– x = y Ж |– f(x, x) = f(x, x) (УП) {x = y} |– f(x, x) = f(x, x)
(З=)
	{x = y} |– f(x, y) = f(y, x) (ВЙ) Ж |– x = y Й f(x, y) = f(y, x)

Здесь мы применили первое правило замены. В нём в качестве формулы F(v) можно взять формулу f(x, v) = f(v, x). Тогда F(x) принимает вид f(x, x) = f(x, x), а F(y) – f(x, y) = f(y, x).

---

Назад