# 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.
- (2a) and (2b) allow the arguments of
`f`
to be permuted in any way (trivial).
- (2b) is dependent on the remaining three axioms, so it can be removed.

Proof:
`prover9 -f dep-2b.in > dep-2b.out ; ### ( dep-2b.out.xml )`

The remaining three are independent.
- If we permute the arguments in the associativity axiom in the right ways,
we can do without the permutativity axioms. For example, an equivalent
2-basis is
f(x,x,y) = x # label(majority).
f(f(x,w,y),z,w) = f(w,x,f(w,z,y)) # label(associativity2).

We can prove this by deriving (2a) and (2b):
`prover9 -f 2basis.in > 2basis.out ; ### ( 2basis.out.xml )`

## 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.in > dist-both.out ; ### ( dist-both.out.xml )`

Given one of the distributivity properties, prove the other.
Short implies long.

`prover9 -f dist-short-long.in > dist-short-long.out ; ### ( dist-short-long.out.xml )`

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