-- vim:ts=4

#include "Eq"

--	The general Monoid Category:
--
MonoidGen: Category == with
{
	--	It seems that we can't use the infix operator "*" for multiplication
	--		here, since "*" is by default left-associative, so the Aldor parser
	--		would re-combine exprs involving "*" in a way we don't want.  So
	--		use "mult" instead:
	--
	mult: (a: %, b: %) -> %;
	I: %;

	-- Monoid axioms:
	--
	leftUnit:  (a: %) -> Eq (%, a, mult(a,I));

	rightUnit: (a: %) -> Eq (%, a, mult(I,a));

	assoc:     (a: %, b: %, c: %) ->
		Eq (%, mult(a, mult (b,c)), mult(mult (a,b), c));
}

MonoidO2: Category == MonoidGen with
{
	order2: (a: %) -> Eq (%, (mult$MonoidGen) (a,a), (I$MonoidGen));
}

comm2  (M2: MonoidO2, a: M2, b: M2):
	Eq (M2, (mult$M2) (b,a),  (mult$M2) (a,b))
==
{
	--
	--	(1) (b*a)*(b*a) = I:
	--
	S01: Eq (M2, (mult$M2) ((mult$M2)(b,a), (mult$M2)(b,a)), (I$M2))
		 ==
		 (order2$M2) ((mult$M2)(b,a));

	--
	--	(2) (b*a)*(b*a) == ((b*a)*b)*a:
	--
	S02: Eq (M2, (mult$M2) ((mult$M2) (b,a),     (mult$M2)(b,a)),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a))
		==
		(assoc$M2) ((mult$M2)(b,a), b, a);

	--
	--	(3) ((b*a)*b)*a == (b*a)*(b*a):
	--
	S03: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a),
				 (mult$M2) ((mult$M2) (b,a), (mult$M2) (b,a)))
		 ==
		 eqSymm (M2,
				 (mult$M2) ((mult$M2) (b,a), (mult$M2)(b,a)),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a),
				 S02);

	--
	--	(4) ((b*a)*b)*a == I:
	--
	S04: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), (I$M2))
		 ==
		 eqTrans (M2,
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a),
				 (mult$M2) ((mult$M2)(b,a), (mult$M2)(b,a)),
				 I$M2,
				 S03, S01);

	--
	--	(5) (((b*a)*b)*a)*a == I*a:
	--
	S05: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a),
			(mult$M2)((I$M2),a))
		 ==
		 eqSubst (M2,
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a),
				 I$M2,
				 S04,
				 M2,
				 (z: M2): M2 +-> (mult$M2) (z,a));

	--
	--	(6) a = I*a:
	--
	S06: Eq (M2, a, (mult$M2)((I$M2),a))
		 ==
		 (rightUnit$M2) (a);

	--
	--	(7) I*a == a:
	--
	S07: Eq (M2, (mult$M2)((I$M2),a), a)
		 ==
		 eqSymm (M2, a, (mult$M2)((I$M2),a), S06);

	--
	--	(8) (((b*a)*b)*a)*a == a:
	--
	S08: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a),
		     a)
		 ==
		 eqTrans (M2,
				 (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a),
				 (mult$M2) ((I$M2),a),
				 a,
				 S05, S07);

	--
	--	(9) ((b*a)*b)*(a*a) == (((b*a)*b)*a)*a:
	--
	S09: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) (b,a), b),  (mult$M2) (a,a)),
				 (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a))
		 ==
		 (assoc$M2)
				((mult$M2) ((mult$M2) (b,a), b),  a, a);

	--
	--	(10) a*a = I:
	--
	S10: Eq (M2, (mult$M2)(a,a), (I$M2))
		 ==
		 (order2$M2) (a);

	--
	--	(11) I = a*a:
	--
	S11: Eq (M2, I$M2, (mult$M2)(a,a))
		 ==
		 eqSymm (M2, (mult$M2)(a,a), I$M2, S10);

	--
	--	(12) (b*a)*b == ((b*a)*b)*I:
	--
	S12: Eq (M2, (mult$M2) ((mult$M2) (b,a), b),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), I$M2) )
		 ==
		 (leftUnit$M2) ((mult$M2) ((mult$M2) (b,a), b));

	--
	--	(13) ((b*a)*b)*I == ((b*a)*b)*(a*a):
	--
	S13: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), I$M2),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b),  (mult$M2) (a,a)))
		 ==
		 eqSubst (M2,
				  I$M2,  (mult$M2)(a,a),  S11, M2,
				  (z: M2): M2 +-> (mult$M2) ((mult$M2) ((mult$M2)(b,a), b), z));

	--
	--	(14) (b*a)*b == ((b*a)*b)*(a*a):
	--
	S14: Eq (M2,  (mult$M2) ((mult$M2) (b,a), b),
				  (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), (mult$M2)(a,a)) )
		 ==
		 eqTrans (M2,
				  (mult$M2) ((mult$M2) (b,a), b),
				  (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), I$M2),
				  (mult$M2) ((mult$M2) ((mult$M2) (b,a), b),  (mult$M2) (a,a)),
				  S12,
				  S13);

	--
	--	(15) (b*a)*b == (((b*a)*b)*a)*a:
	--
	S15: Eq (M2, (mult$M2) ((mult$M2) (b,a), b),
				 (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a) )
		 ==
		 eqTrans (M2,
				 (mult$M2) ((mult$M2) (b,a), b),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), (mult$M2)(a,a)),
				 (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a),
				 S14,
				 S09 );

	--
	--	(16) (b*a)*b == a ... UFF, AT LAST!
	--
	S16: Eq (M2, (mult$M2) ((mult$M2) (b,a), b),  a) 
		 ==
		 eqTrans (M2,
				 (mult$M2) ((mult$M2) (b,a), b),
				 (mult$M2) ((mult$M2) ((mult$M2) ((mult$M2) (b,a), b), a), a),
				 a,
				 S15,
				 S08);

	--
	--	(17) ((b*a)*b)*b == a*b:
	--
	S17: Eq (M2, (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), b),
				 (mult$M2) (a,b))
		 ==
		 eqSubst (M2,
				 (mult$M2) ((mult$M2) (b,a), b),
				 a,
				 S16,
				 M2,
				 (z: M2): M2 +-> (mult$M2) (z, b));

	--
	--	(18) (b*a)*(b*b) == ((b*a)*b)*b:
	--
	S18: Eq (M2, (mult$M2) ((mult$M2) (b,a), (mult$M2) (b,b)),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), b))
		 ==
		 (assoc$M2)  ((mult$M2) (b,a), b, b);

	--
	--	(19) b*b = I:
	--
	S19: Eq (M2, (mult$M2) (b,b), I$M2)
		 ==
		 (order2$M2) (b);

	--
	--	(20) I = b*b:
	--
	S20: Eq (M2, I$M2, (mult$M2) (b,b))
		 ==
		 eqSymm (M2, (mult$M2) (b,b), I$M2, S19);

	--
	--	(21) b*a = (b*a)*I:
	--
	S21: Eq (M2, (mult$M2) (b,a),
				 (mult$M2) ((mult$M2) (b,a), I$M2))
		 ==
		 (leftUnit$M2) ((mult$M2) (b,a));

	--
	--	(22) (b*a)*I = (b*a)*(b*b):
	--
	S22: Eq (M2, (mult$M2) ((mult$M2) (b,a), I$M2),
				 (mult$M2) ((mult$M2) (b,a), (mult$M2) (b,b)) )
		 ==
		 eqSubst (M2,
				 I$M2, (mult$M2) (b,b), S20, M2,
				 (z: M2): M2 +-> (mult$M2) ((mult$M2) (b,a), z) );

	--
	--	(23) b*a = (b*a)*(b*b):
	--
	S23: Eq (M2, (mult$M2) (b,a),
				 (mult$M2) ((mult$M2) (b,a), (mult$M2) (b,b)) )
		 ==
		 eqTrans (M2,
				 (mult$M2) (b,a),
				 (mult$M2) ((mult$M2) (b,a), I$M2),
				 (mult$M2) ((mult$M2) (b,a), (mult$M2) (b,b)),
				 S21,
				 S22);

	--
	--	(24) b*a = ((b*a)*b)*b:
	--
	S24: Eq (M2, (mult$M2) (b,a),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), b) )
		 ==
		 eqTrans (M2,
				 (mult$M2) (b,a),
				 (mult$M2) ((mult$M2) (b,a), (mult$M2) (b,b)),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), b),
				 S23,
				 S18);

	--
	--	(25) AND FINALLY:  b*a = a*b:
	--
	S25: Eq (M2, (mult$M2) (b,a),  (mult$M2) (a,b)) ;
		 ==
		 eqTrans (M2,
				 (mult$M2) (b,a),
				 (mult$M2) ((mult$M2) ((mult$M2) (b,a), b), b),
				 (mult$M2) (a,b),
				 S24,
				 S17);
	--
	--	THE PROOF TERM TO BE RETURNED:
	--
	S25;
}