# Yet Another Single Law for Lattices

TEMPORARY: for the authors and the journal.
The final version for publication in Algebra Universalis:

William McCune, R. Padmanabhan, Robert Veroff

April 24, 2002

This page is associated with a paper (submitted for publication) of the same name.

A preprint (the submitted version) is available: DVI, PS, PDF.

# Lattice Theory Bases

The two new single axioms are (length 29, 8 variables)
```(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (w v ((v6 v x) ^ (x v v7))) = x.  % A1
(((y v x) ^ x) v (((z ^ (x v x)) v (u ^ x)) ^ v)) ^ (((w v x) ^ (v6 v x)) v v7) = x.  % A2
```
The McKenzie 4-basis is
```x v (y ^ (x ^ z)) = x.
x ^ (y v (x v z)) = x.
((y ^ x) v (x ^ z)) v x = x.
((y v x) ^ (x v z)) ^ x = x.
```

# Proofs

The short proof in the paper: A1 -> McKenzie-4-basis.
This uses the hints list to lead Otter to a specific short proof.
(The steps in proof in the paper were renumbered for better presentation.)

An "automatic" proof of A1 -> McKenzie-4-basis.

An "automatic" proof of A2 -> McKenzie-4-basis.

# Previously Known Axioms

The length-79 axiom (7 variables) from [McCune-Padmanabhan:1996]:
```(((x ^ y) v (y ^ (x v y))) ^ z) v (((x ^ (((x1 ^ y) v (y ^ x2)) v y)) v (((y ^
(((x1 v (y v x2)) ^ (x3 v y)) ^ y)) v (u ^ (y v (((x1 v (y v x2)) ^
(x3 v y)) ^ y)))) ^ (x v (((x1 ^ y) v (y ^ x2)) v y)))) ^ (((x ^ y) v (y ^
(x v y))) v z)) = y.
```
The length-77 axiom (8 variables) from [Veroff:2001]:
```(((x ^ y) v (y ^ (x v y))) ^ z) v (((x ^ (((x1 ^ y) v (y ^ x2)) v y)) v (((y ^
(((x1 v (y v x2)) ^ (x3 v y)) ^ y)) v (u ^ (y v (((y v xnew) ^
(x3 v y)) ^ y)))) ^ (x v (((x1 ^ y) v (y ^ x2)) v y)))) ^ (((x ^ y) v (y ^
(x v y))) v z)) = y.

```