Draft -- October 24, 1996

This page contains the three Robbins algebra lemmas that are used in the solution of the Robbins problem. Lemma 1 uses Lemma 0, Lemma 2 uses Lemma 1, and the solution of the Robbins problem uses Lemma 2. Very orderly. These lemmas were first proved by Steve Winker in the early 1980s.

The EQP proofs use associative-commutative unification, and the Otter proofs use associativity and commutativity as axioms.

**Lemma 0**.
Robbins algebras satisfying *exists C, C+C=C* are Boolean.

**Lemma 1**.
Robbins algebras satisfying *exists C exists D, C+D=C* are Boolean.

**Lemma 2**.
Robbins algebras satisfying *exists C exists D, n(C+D)=n(C)* are Boolean.

You can use Otter to prove some of the easier Robbins lemmas

Automated Deduction Group,

Mathematics and Computer Science Division,

Argonne National Laboratory