A Sample Otter Proof


Theorem: A Robbins algebra satisfying x+x=x is a Boolean algebra.

Here is Otter's proof in Son of BirdBrain's format:


Searching ...

Success, in 1.28 seconds!

---------------- PROOF ----------------

1        n(n(A)+B)+n(n(A)+n(B))!=A.                 []
2        x=x.                                       []
3        x+y=y+x.                                   []
5,4      (x+y)+z=x+ (y+z).                          []
6        n(n(x+y)+n(x+n(y)))=x.                     []
8        x+x=x.                                     []

10       n(n(A)+n(B))+n(n(A)+B)!=A.                 [para_from,3,1]
13       x+ (x+y)=x+y.                              [para_into,4,8,flip.1]
15       x+ (y+z)=y+ (x+z).                         [para_into,4,3,demod,5]
23,22    x+ (y+x)=x+y.                              [para_into,13,3]
26       n(n(x)+n(x+n(x)))=x.                       [para_into,6,8]
36       n(n(n(x)+x)+n(n(x)))=n(x).                 [para_into,6,8]
42       n(n(x+n(y))+n(x+y))=x.                     [para_into,6,3]
52       x+ (y+z)=x+ (z+y).                         [para_into,15,3,demod,5]
81,80    n(n(x+n(x))+n(x))=x.                       [para_into,26,3]
82       n(n(n(x)+x)+x)=n(x).                       [para_from,26,6,demod,23]
125      n(n(n(x+n(x))+ (n(x)+x))+x)=n(x+n(x))+n(x). [para_into,80,80,demod,5,81]
139      n(n(n(x+n(x))+x)+x)=n(x+n(x)).             [para_from,80,6]
166,165  n(n(x+n(x))+x)=n(x).                       [para_into,82,3]
180,179  n(n(x)+x)=n(x+n(x)).                       [back_demod,139,demod,166]
195      n(n(x+n(x))+n(n(x)))=n(x).                 [back_demod,36,demod,180]
197      n(n(x+ (n(x)+n(x+n(x))))+ (n(x+n(x))+x))=n(x). [para_into,165,165,demod,5,180,5,166]
206,205  n(n(x+ (n(x)+n(x+n(x))))+n(x))=n(x+n(x))+x. [para_from,165,80,demod,166,5,180,5]
223,222  n(n(x+y)+ (y+x))=n(x+ (y+n(x+y))).         [para_into,179,52,demod,5]
231,230  n(n(x+ (n(x)+n(x+n(x))))+x)=n(x+n(x))+n(x). [back_demod,125,demod,223]
564,563  n(x+n(x))+x=x.                             [para_into,195,80,demod,5,223,81,206,81]
582,581  n(x+n(x))+n(x)=n(x).                       [back_demod,197,demod,564,231]
586,585  n(n(x))=x.                                 [back_demod,80,demod,582]
606,605  n(x+n(y))+n(x+y)=n(x).                     [para_into,585,42,flip.1]
621      A!=A.                                      [back_demod,10,demod,606,586]
622      $F.                                        [binary,621,2]

------------ end of proof -------------

These activities are projects of the Mathematics and Computer Science Division of Argonne National Laboratory.