1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
(datatype G)
(constructor IConst () G)
(let $I (IConst))
(constructor AConst () G)
(let $A (AConst))
(constructor BConst () G)
(let $B (BConst))
(constructor g* (G G) G)
(constructor 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)
(constructor aConst () G)
(constructor 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)