1	import Base
2	
3	law append_assoc:
4	  for -A: Data
5	  for xs: List<&2, A>
6	  for ys: List<&2, A>
7	  for zs: List<&2, A>
8	  {List.append(&2, A, List.append(&2, A, xs, ys), zs)
9	    == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}
10	
11	def append_assoc(A, xs, ys, zs):
12	  match xs:
13	    case Nil{}:
14	      {==}
15	    case h <> t:
16	      %append_assoc(A, t, ys, zs) :
17	        {h <> List.append(&2, A, List.append(&2, A, t, ys), zs) == h <> _ : List<&2, A>}
18	      {==}
19	
20	law reverse_twice:
21	  for -A: Data
22	  for xs: List<&2, A>
23	  for acc: List<&2, A>
24	  for ys: List<&2, A>
25	  {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), ys)
26	    == List.reverse.go(&2, A, acc, List.append(&2, A, xs, ys)) : List<&2, A>}
27	
28	def reverse_twice(A, xs, acc, ys):
29	  match xs:
30	    case Nil{}:
31	      {==}
32	    case h <> t:
33	      reverse_twice(A, t, h <> acc, ys)
34	
35	law reverse_append:
36	  for -A: Data
37	  for xs: List<&2, A>
38	  for ys: List<&2, A>
39	  {List.reverse.go(&2, A, List.reverse(&2, A, xs), ys)
40	    == List.append(&2, A, xs, ys) : List<&2, A>}
41	
42	def reverse_append(A, xs, ys):
43	  reverse_twice(A, xs, Nil{}, ys)
44	
45	law add_succ:
46	  for n: Nat
47	  for m: Nat
48	  {Nat.add(n, 1n+m) == 1n+Nat.add(n, m) : Nat}
49	
50	def add_succ(n, m):
51	  match n:
52	    case 0n:
53	      {==}
54	    case 1n+p:
55	      %add_succ(p, m) : {1n+Nat.add(p, 1n+m) == 1n+_ : Nat}
56	      {==}
57	
58	law add_zero:
59	  for n: Nat
60	  {Nat.add(n, 0n) == n : Nat}
61	
62	def add_zero(n):
63	  match n:
64	    case 0n:
65	      {==}
66	    case 1n+p:
67	      %add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
68	      {==}
69	
70	law append_assoc_reverse:
71	  for -A: Data
72	  for +xs: List<&2, A>
73	  for +ys: List<&2, A>
74	  for +zs: List<&2, A>
75	  {List.append(&2, A, xs, List.append(&2, A, ys, zs))
76	    == List.append(&2, A, List.append(&2, A, xs, ys), zs) : List<&2, A>}
77	
78	def append_assoc_reverse(A, xs, ys, zs):
79	  Equal.sym(List<&2, A>, List.append(&2, A, List.append(&2, A, xs, ys), zs),
80	    List.append(&2, A, xs, List.append(&2, A, ys, zs)), append_assoc(A, xs, ys, zs))
81	
82	law add_swap:
83	  for +n: Nat
84	  for +k: Nat
85	  for +m: Nat
86	  {Nat.add(n, Nat.add(k, m)) == Nat.add(k, Nat.add(n, m)) : Nat}
87	
88	def add_swap(n, k, m):
89	  match k:
90	    case 0n:
91	      {==}
92	    case 1n+p:
93	      Equal.trans(Nat, Nat.add(n, 1n+Nat.add(p, m)),
94	        1n+Nat.add(n, Nat.add(p, m)), 1n+Nat.add(p, Nat.add(n, m)),
95	        add_succ(n, Nat.add(p, m)),
96	        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(n, Nat.add(p, m)),
97	          Nat.add(p, Nat.add(n, m)), add_swap(n, p, m)))