twee-2.3.1: tests/gmv2.p

cnf('Associativity-∧', axiom,
    (X ∧ Y) ∧ Z = X ∧ (Y ∧ Z)).   
cnf('Associativity-∨', axiom,
    (X ∨ Y) ∨ Z = X ∨ (Y ∨ Z)).
cnf('Idempotence-∧', axiom,
    X ∧ X = X).
cnf('Idempotence-∨', axiom,
    X ∨ X = X).
cnf('Commutativity-∧', axiom,
    X ∧ Y = Y ∧ X).
cnf('Commutativity-∨', axiom,
    X ∨ Y = Y ∨ X).
cnf('Absorption a', axiom,
    (X ∧ Y) ∨ X = X).
cnf('Absorption b', axiom,
    (X ∨ Y) ∧ X = X).

cnf('Residual a', axiom,
    (X * ((X \ Z) ∧ Y)) ∨ Z = Z).
cnf('Residual b', axiom,
    ((Y ∧ (Z / X)) * X) ∨ Z = Z).
cnf('Residual c', axiom,
    (X \ ((X * Y) ∨ Z)) ∧ Y = Y).
cnf('Residual d', axiom,
    (((Y * X) ∨ Z) / X) ∧ Y = Y).

cnf('Associativity-* (fusion)', axiom,
    (X * Y) * Z = X * (Y * Z)).
cnf('Left monoid unit', axiom,
    '1' * X = X).
cnf('Right monoid unit', axiom,
    X * '1' = X).

cnf('GMV a', axiom,
    X ∨ Y = X / ((X ∨ Y) \ X)).
cnf('GMV b', axiom,
    X ∨ Y = (X / (X ∨ Y)) \ X).

cnf('Definition-@', axiom,
    X @ Y = (X * (X \ '1')) * ((Y \ '1') \ '1')).

cnf('Goal 2', conjecture,
    (x @ y) @ z = x @ z).