; A simple group
(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

; 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))

; non terminating rule
(relation allgs (G))
(rule ((allgs x)) ((allgs (g* B x))))
(allgs A)

; if you remove :until, this will take a very long time
(run 10000 :until (= A8 I))
(check (= A8 I))
(check (!= B A))
(check (!= I A))
; If you need multiple stop conditions, consider using a (relation relation stop (unit))
; With rules filling it in with different stop conditions of interest.