Spickzettel

`A o+ (B o. C) -= (Ao+B)o.(Ao+C)`
`not (Ao+B) -= not A o. not B`
`not AA x [F(x)] -= EE x [ not F(x)]`
`not EE x [F(x)] -= AA x [ not F(x)]`
`AA x EE y AA z EE w F(x,y,z,w) ~= AA x AA z F(x,g(x),z,f(x,g(x),z))`
`G supe N ^^ K` def `AA x [ G(x) larr N(x) ^^ K(x) ]` knf, horn `(G vv not N vv not K)`
`N ^^ K supe G` def `AA x [ N(x) ^^ K(x) larr G(x)]` knf, horn `(N vv not G) ^^ (K vv not G)`
`G supe N vv K` def `AA x [ G(x) larr N(x) vv K(x) ]` knf, horn `(G vv not N) ^^ (G vv not K)`
`N vv K supe G` def `AA x [ N(x) vv K(x) larr G(x)]` knf, not horn `(N vv K vv not G)`
`EE P.C` def `AA x EE y [ P(x,y) ^^ C(y)]` knf `(P(x,f(x))) ^^ (C(f(x)))`
`AA P.C` def `AA x,y [ P(x,y) rarr C(y)]` knf, horn `(C(y) vv not P(x,y))`