anchor.diff:  |===
   ////
   
  -We can now prove the second of the two equations from Basis~0~, *J2*.
  -This completes the proof that Basis~1~ is at least as powerful as Basis~0~.
  +We can now prove the second of the two equations from _Basis~0~_, *J2*.
  +This completes the proof that _Basis~1~_ is at least as powerful as
  +_Basis~0~_.
   
   [cols="<2s,>5e,^1,<4e",grid="none",frame="none",width="50%"]
   |===
  
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: |10 | p p = p |(8,9 *eucr*)
  |===
  
  ==== _System~3~_
  
  Here we derive *C6* from the Robbins equation, demonstrating that a Robbins
  algebra is a Boolean algebra. The more familiar form of the Robbins equation
  is  _\((p q) (p (q))) = p_, but for this exercise I'll be using the
  equivalent form:
  
  