(datatype G)
(function IConst () G)
(let I (IConst))
(function AConst () G)
(let A (AConst))
(function BConst () G)
(let B (BConst))
(function g* (G G) G)
(function inv (G) G)
(birewrite (g* (g* a b) c) (g* a (g* b c))) ; assoc
(rewrite (g* I a) a) ; idl
(rewrite (g* a I) a) ; idr
(rewrite (g* (inv a) a) I) ; invl
(rewrite (g* a (inv a)) I) ; invr

; A is cyclic of period 4
(rewrite (g* A (g* A (g* A A))) I)

(let A2 (g* A A))
(let A4 (g* A2 A2))
(let A8 (g* A4 A4))


(push)
(g* A4 A4)

(run 10000 :until (= (g* A4 A4) (g* (g* A2 A2) (g* A2 A2))))

(check (= (g* A4 A4) (g* (g* A2 A2) (g* A2 A2))))
(pop)

(push)
(g* (g* A2 A2) (g* A2 A2))

(run 10000 :until (= (g* (g* A2 A2) (g* A2 A2))
(g* A2 (g* A2 (g* A2 A2)))))
(check (= (g* (g* A2 A2) (g* A2 A2))
(g* A2 (g* A2 (g* A2 A2)))))
(pop)


(function aConst () G)
(function bConst () G)
(let a (aConst))
(let b (bConst))
(push)

(g* (g* b (g* (inv a) a)) (inv b))

(run 100000 :until (= (g* (g* b (g* (inv a) a)) (inv b)) (g* b (inv b))))

(check (= (g* (g* b (g* (inv a) a)) (inv b)) (g* b (inv b))))

(pop)

(push)
(g* b (inv b))
(run 100000 :until (= (g* b (inv b)) I))
(check (= (g* b (inv b)) I))

(pop)