netrvrdim to na 100% ale ja som to zrobil takto:
f f b f b b
W(x) ^ W(y) => (pre vsetky x)(x |> y => (existuje y)(y |>x))
a substituovat mozes len volne vyskyty...
takze po:
a) f(x,y) za y:
f f b f
W(x) ^ W(f(x,y)) => (pre vsetky x)(x |> f(x,y) => (existuje y)(y |>x))
nie je substituovatelny
b) f(x,y) za x:
f f
W(f(x,y)) ^ W(y) => (pre vsetky x)(x |> y => (existuje y)(y |>x))
je substituovatelny