The BCSK+ Logic

BSCK+ Axioms

• Start with A1, A2, A4, A5, A8, A9
• Add

      P(i(j(j(x,y),y),j(j(y,x),x)))  % A10 

• Proved

      P(i(j(x,y),i(x,y)))            % T4

  equivalent to A10, avoiding A3, A6, A7

P(i(j(j(x,y),x),x)) % A7

• A7 proved from A1, A2, A4, A5, A8, A9, A10
  avoiding A3 and A6