Решение
{
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
).
Назад