Prover9 Examples: Distributivity in Median Algebras

For more detail on this, see Bob Veroff's median algebra page.

Median Algebras

A median algebra has a ternary operation satisfying the following axioms.
   f(x,x,y) = x                       # label(majority).
   f(x,y,z) = f(z,x,y)                # label(2a).
   f(x,y,z) = f(x,z,y)                # label(2b).
   f(f(x,w,y),w,z) = f(x,w,f(y,w,z))  # label(associativity).
Notes about the axioms.

Ternary Distributivity Properties

The following two distributrivity properties hold for median algebras.
   f(f(x,y,z),u,w) = f(x,       f(y,u,w),f(z,u,w))    # label(dist_short).
   f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w))    # label(dist_long).
A higher-order proof was given by M. Kolibiar and T. Marcisova in 1974.

The first equational proof we know of was found by Bob Veroff and Otter.

A proof by Prover9:

prover9 -f > dist-both.out ; ### ( dist-both.out.xml )
Given one of the distributivity properties, prove the other.

Short implies long.

prover9 -f > dist-short-long.out ; ### ( dist-short-long.out.xml )
Long implies short.
prover9 -f > dist-long-short.out ; ### ( dist-long-short.out.xml )