anchor.diff:  === Summary of Results
   
   
  -==== System~0~
  +==== _System~0~_
   
   This version follows _LoF_ and was the original proof of concept, so not
   much more needs to be said. There is one difference -- theorem *C5* is derived
  
positive.code: 
  *(* {nbsp}{nbsp}{nbsp} *)* {nbsp}{nbsp}{nbsp} *=* {nbsp}{nbsp}{nbsp}
  *|-* {nbsp}{nbsp}{nbsp} *form*
  
  ////
  [none]
  -  *(*
  -  *)*
  -  *=*
  -  *|-*
  -  *form*
  ////
  
  and seven basic axioms -- three to provide a recursive definition of 'form',
  three common notions (so to speak) to power symbol manipulation, and a
  
negative.code: be spelled out case by case in auxiliary theorems. The system as formulated
  is simply unable to prove general statements of commutativity.
  
  === Synopsis
  
  Since my derivation of the Primary Algebra (PA) follows Spencer-Brown rather
  closely, I spend little time on it here. I do provide a full demonstration
  that an alternate basis of *C5* and *C6* is equivalent to PA. I then show
  that *C6* alone is adequate. Finally, I show that *C6* is derivable from the
  Robbins axiom, implying that a Robbins algebra is a Boolean algebra 
  footnote:[To be clear, this is not an alternative to the 1996 computer proof
  that Robbins algebras are Boolean (W. McCune, "Solution of the Robbins Problem", 
  JAR 19(3), 263--276 (1997)). _LoF_ has a natural identity element, the void, 
  and S. Winkler showed in the early 1990's that the existence of such an
  element sufficed to turn a Robbins algebra into a Boolean algebra 
  (S. Winker, "Robbins Algebra: Conditions That Make a Near-Boolean Algebra 
  Boolean", J. Automated Reasoning 6(4), 465--489 (1990) and
  "Absorption and idempotency criteria for a problem in near-Boolean algebras", 
  J. Algebra 153(2), 414--423 (1992)).].
  
  If metamath is installed on your system, you can confirm
  the correctness of the formal derivations in lof.mm by starting the
  