axioms.txt

commutativity+		(A+B)=(B+A)
commutativity*		(A*B)=(B*A)
associativity+		(A+(B+C))=((A+B)+C)
associativity*		(A*(B*C))=((A*B)*C)
left_distributivity	(A*(B+C))=((A*B)+(A*C))
right_distributivity	((A+B)*C)=((A*C)+(B*C))
left_unit+		(0+A)=A
right_unit+		(A+0)=A
left_unit*		(1*A)=A
right_unit*		(A*1)=A
right_cycling+		(A+(B+C))=(C+(A+B))
left_cycling+		((A+B)+C)=((C+A)+B)
right_cycling*		(A*(B*C))=(C*(A*B))
left_cycling*		((A*B)*C)=((C*A)*B)
contradiction		A=B
idempotent*		(A*A)=A

order2*			(A*A)=1
order3*			((A*A)*A)=1
order4*			(((A*A)*A)*A)=1

3to1_1*			(A*(A*B))=A
3to1_2*			((B*A)*A)=A
3to1_3*			((A*A)*B)=A
3to1_4*			(B*(A*A))=A
3to1_5*			(A*(A*B))=B
3to1_6*			((B*A)*A)=B
3to1_7*			((A*A)*B)=B
3to1_8*			(B*(A*A))=B
3to1_9*			(A*(B*A))=A
3to1_10*		((A*B)*A)=A
3to1_11*		(A*(B*A))=B
3to1_12*		((A*B)*A)=B
3to1_12*		(A*(A*A))=A
3to1_13*		((A*A)*A)=A

3to2_1*			((A*B)*A)=(A*B)
3to2_2*			((A*A)*A)=(A*A)
3to2_3*			(A*(A*A))=(A*A)

associativity1*		((A*B)*B)=(A*(A*B))
associativity2*		((A*A)*B)=(A*(A*B))
associativity3*		((B*A)*A)=(B*(A*A))



% Delete these when possible
nameless1		(A+(A+B)) = A
nameless2		((B+A)+A) = A
nameless3		(a*c) = b
nameless4		(b*d) = a