twee-0.1: tests/diff.p
cnf(a, axiom, diff(X, diff(Y, X)) = X). cnf(a, axiom, diff(X, diff(X, Y)) = diff(Y, diff(Y, X))). cnf(a, axiom, diff(diff(X, Y), Z) = diff(diff(X, Z), diff(Y, Z))). cnf(a, axiom, diff(diff(a, c), b) != diff(diff(a, b), c)).
cnf(a, axiom, diff(X, diff(Y, X)) = X). cnf(a, axiom, diff(X, diff(X, Y)) = diff(Y, diff(Y, X))). cnf(a, axiom, diff(diff(X, Y), Z) = diff(diff(X, Z), diff(Y, Z))). cnf(a, axiom, diff(diff(a, c), b) != diff(diff(a, b), c)).