1	# bend-mathlib/algebra.bend: abstract associativity/commutativity theorems and their Nat/Bool/List instances.
2	import Base
3	import ./nat.bend as MNat
4	import ./bool.bend as MBool
5	import ./list.bend as MList
6	
7	# Four-way reassociation from associativity alone.
8	law op_assoc4:
9	  for ~A: Data
10	  for ~op: A -> A -> A
11	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
12	  for +a: A
13	  for +b: A
14	  for +c: A
15	  for +d: A
16	  {op(op(op(a, b), c), d) == op(a, op(b, op(c, d))) : A}
17	
18	def op_assoc4(A, op, assoc, a, b, c, d):
19	  %assoc(a, b, op(c, d)) : {op(op(op(a, b), c), d) == _ : A}
20	  assoc(op(a, b), c, d)
21	
22	# Left commutation from associativity and commutativity.
23	law op_left_comm:
24	  for ~A: Data
25	  for ~op: A -> A -> A
26	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
27	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
28	  for +a: A
29	  for +b: A
30	  for +c: A
31	  {op(a, op(b, c)) == op(b, op(a, c)) : A}
32	
33	def op_left_comm(A, op, assoc, comm, a, b, c):
34	  %assoc(a, b, c) : {_ == op(b, op(a, c)) : A}
35	  %Equal.sym(A, op(a, b), op(b, a), comm(a, b)) : {op(_, c) == op(b, op(a, c)) : A}
36	  assoc(b, a, c)
37	
38	# Right commutation from associativity and commutativity.
39	law op_right_comm:
40	  for ~A: Data
41	  for ~op: A -> A -> A
42	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
43	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
44	  for +a: A
45	  for +b: A
46	  for +c: A
47	  {op(op(a, b), c) == op(op(a, c), b) : A}
48	
49	def op_right_comm(A, op, assoc, comm, a, b, c):
50	  %Equal.sym(A, op(op(a, b), c), op(a, op(b, c)), assoc(a, b, c)) : {_ == op(op(a, c), b) : A}
51	  %Equal.sym(A, op(op(a, c), b), op(a, op(c, b)), assoc(a, c, b)) : {op(a, op(b, c)) == _ : A}
52	  %Equal.sym(A, op(c, b), op(b, c), comm(c, b)) : {op(a, op(b, c)) == op(a, _) : A}
53	  {==}
54	
55	# Middle-four interchange from associativity and commutativity.
56	law op_four:
57	  for ~A: Data
58	  for ~op: A -> A -> A
59	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
60	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
61	  for +a: A
62	  for +b: A
63	  for +c: A
64	  for +d: A
65	  {op(op(a, b), op(c, d)) == op(op(a, c), op(b, d)) : A}
66	
67	def op_four(A, op, assoc, comm, a, b, c, d):
68	  %Equal.sym(A, op(op(a, b), op(c, d)), op(a, op(b, op(c, d))), assoc(a, b, op(c, d))) : {_ == op(op(a, c), op(b, d)) : A}
69	  %Equal.sym(A, op(op(a, c), op(b, d)), op(a, op(c, op(b, d))), assoc(a, c, op(b, d))) : {op(a, op(b, op(c, d))) == _ : A}
70	  %op_left_comm(A, op, assoc, comm, b, c, d) : {op(a, op(b, op(c, d))) == op(a, _) : A}
71	  {==}
72	
73	# Three-way commutation from commutativity alone.
74	law op_comm3:
75	  for ~A: Data
76	  for ~op: A -> A -> A
77	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
78	  for +a: A
79	  for +b: A
80	  for +c: A
81	  {op(op(a, b), c) == op(c, op(b, a)) : A}
82	
83	def op_comm3(A, op, comm, a, b, c):
84	  %Equal.sym(A, op(op(a, b), c), op(c, op(a, b)), comm(op(a, b), c)) : {_ == op(c, op(b, a)) : A}
85	  %Equal.sym(A, op(b, a), op(a, b), comm(b, a)) : {op(c, op(a, b)) == op(c, _) : A}
86	  {==}
87	
88	def internal_nat_add_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}:
89	  MNat.add_assoc(x, y, z)
90	
91	def internal_nat_add_comm(x: Nat, y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
92	  MNat.add_comm(x, y)
93	
94	def internal_nat_mul(x: Nat, y: Nat) -> Nat:
95	  Nat.mul(x, y)
96	
97	def internal_nat_mul_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}:
98	  MNat.mul_assoc(x, y, z)
99	
100	def internal_nat_mul_comm(x: Nat, y: Nat) -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}:
101	  MNat.mul_comm(x, y)
102	
103	def internal_bool_and_assoc(x: Bool, y: Bool, z: Bool) -> {Bool.and(Bool.and(x, y), z) == Bool.and(x, Bool.and(y, z)) : Bool}:
104	  MBool.and_assoc(x, y, z)
105	
106	def internal_bool_and_comm(x: Bool, y: Bool) -> {Bool.and(x, y) == Bool.and(y, x) : Bool}:
107	  MBool.and_comm(x, y)
108	
109	def internal_bool_or_assoc(x: Bool, y: Bool, z: Bool) -> {Bool.or(Bool.or(x, y), z) == Bool.or(x, Bool.or(y, z)) : Bool}:
110	  MBool.or_assoc(x, y, z)
111	
112	def internal_bool_or_comm(x: Bool, y: Bool) -> {Bool.or(x, y) == Bool.or(y, x) : Bool}:
113	  MBool.or_comm(x, y)
114	
115	def internal_list_nat_append_assoc(x: List<&2, Nat>, y: List<&2, Nat>, z: List<&2, Nat>) -> {List.append(&2, Nat, List.append(&2, Nat, x, y), z) == List.append(&2, Nat, x, List.append(&2, Nat, y, z)) : List<&2, Nat>}:
116	  MList.append_assoc(&2, Nat, x, y, z)
117	
118	# Nat addition is left-commutative.
119	law nat_add_left_comm:
120	  for +a: Nat
121	  for +b: Nat
122	  for +c: Nat
123	  {Nat.add(a, Nat.add(b, c)) == Nat.add(b, Nat.add(a, c)) : Nat}
124	
125	def nat_add_left_comm(a, b, c):
126	  op_left_comm(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c)
127	
128	# Nat addition is right-commutative.
129	law nat_add_right_comm:
130	  for +a: Nat
131	  for +b: Nat
132	  for +c: Nat
133	  {Nat.add(Nat.add(a, b), c) == Nat.add(Nat.add(a, c), b) : Nat}
134	
135	def nat_add_right_comm(a, b, c):
136	  op_right_comm(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c)
137	
138	# Nat addition's middle-four interchange.
139	law nat_add_four:
140	  for +a: Nat
141	  for +b: Nat
142	  for +c: Nat
143	  for +d: Nat
144	  {Nat.add(Nat.add(a, b), Nat.add(c, d)) == Nat.add(Nat.add(a, c), Nat.add(b, d)) : Nat}
145	
146	def nat_add_four(a, b, c, d):
147	  op_four(~Nat, ~Nat.add, ~internal_nat_add_assoc, ~internal_nat_add_comm, a, b, c, d)
148	
149	# Nat multiplication is left-commutative.
150	law nat_mul_left_comm:
151	  for +a: Nat
152	  for +b: Nat
153	  for +c: Nat
154	  {Nat.mul(a, Nat.mul(b, c)) == Nat.mul(b, Nat.mul(a, c)) : Nat}
155	
156	def nat_mul_left_comm(a, b, c):
157	  op_left_comm(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c)
158	
159	# Nat multiplication is right-commutative.
160	law nat_mul_right_comm:
161	  for +a: Nat
162	  for +b: Nat
163	  for +c: Nat
164	  {Nat.mul(Nat.mul(a, b), c) == Nat.mul(Nat.mul(a, c), b) : Nat}
165	
166	def nat_mul_right_comm(a, b, c):
167	  op_right_comm(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c)
168	
169	# Nat multiplication's middle-four interchange.
170	law nat_mul_four:
171	  for +a: Nat
172	  for +b: Nat
173	  for +c: Nat
174	  for +d: Nat
175	  {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}
176	
177	def nat_mul_four(a, b, c, d):
178	  op_four(~Nat, ~internal_nat_mul, ~internal_nat_mul_assoc, ~internal_nat_mul_comm, a, b, c, d)
179	
180	# Bool and is left-commutative.
181	law bool_and_left_comm:
182	  for +a: Bool
183	  for +b: Bool
184	  for +c: Bool
185	  {Bool.and(a, Bool.and(b, c)) == Bool.and(b, Bool.and(a, c)) : Bool}
186	
187	def bool_and_left_comm(a, b, c):
188	  op_left_comm(~Bool, ~Bool.and, ~internal_bool_and_assoc, ~internal_bool_and_comm, a, b, c)
189	
190	# Bool and is right-commutative.
191	law bool_and_right_comm:
192	  for +a: Bool
193	  for +b: Bool
194	  for +c: Bool
195	  {Bool.and(Bool.and(a, b), c) == Bool.and(Bool.and(a, c), b) : Bool}
196	
197	def bool_and_right_comm(a, b, c):
198	  op_right_comm(~Bool, ~Bool.and, ~internal_bool_and_assoc, ~internal_bool_and_comm, a, b, c)
199	
200	# Bool or is left-commutative.
201	law bool_or_left_comm:
202	  for +a: Bool
203	  for +b: Bool
204	  for +c: Bool
205	  {Bool.or(a, Bool.or(b, c)) == Bool.or(b, Bool.or(a, c)) : Bool}
206	
207	def bool_or_left_comm(a, b, c):
208	  op_left_comm(~Bool, ~Bool.or, ~internal_bool_or_assoc, ~internal_bool_or_comm, a, b, c)
209	
210	# Bool or is right-commutative.
211	law bool_or_right_comm:
212	  for +a: Bool
213	  for +b: Bool
214	  for +c: Bool
215	  {Bool.or(Bool.or(a, b), c) == Bool.or(Bool.or(a, c), b) : Bool}
216	
217	def bool_or_right_comm(a, b, c):
218	  op_right_comm(~Bool, ~Bool.or, ~internal_bool_or_assoc, ~internal_bool_or_comm, a, b, c)
219	
220	# Four-way reassociation for List append over Nat.
221	law list_nat_append_assoc4:
222	  for +a: List<&2, Nat>
223	  for +b: List<&2, Nat>
224	  for +c: List<&2, Nat>
225	  for +d: List<&2, Nat>
226	  {List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) == List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) : List<&2, Nat>}
227	
228	def list_nat_append_assoc4(a, b, c, d):
229	  op_assoc4(~List<&2, Nat>, ~List.append(&2, Nat), ~internal_list_nat_append_assoc, a, b, c, d)
230	
231	# Folding left equals folding right for an associative, commutative operation with a left identity.
232	law foldl_op_eq_foldr_op:
233	  for ~B: Data
234	  for ~op: B -> B -> B
235	  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
236	  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
237	  for ~z: B
238	  for ~id: @x: B -> {op(z, x) == x : B}
239	  for +xs: List<&2, B>
240	  {List.foldl(&2, B, B, op, xs, z) == List.foldr(&2, B, B, op, xs, z) : B}
241	
242	def internal_foldl_foldr(~B: Data, ~op: B -> B -> B, ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}, ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}, ~z: B, ~id: @x: B -> {op(z, x) == x : B}, +xs: List<&2, B>, +acc: B) -> {List.foldl(&2, B, B, op, xs, acc) == op(acc, List.foldr(&2, B, B, op, xs, z)) : B}:
243	  match xs:
244	    case Nil{}:
245	      Equal.sym(B, op(acc, z), acc, Equal.trans(B, op(acc, z), op(z, acc), acc, comm(acc, z), id(acc)))
246	    case +h <> +t:
247	      %Equal.sym(B, List.foldl(&2, B, B, op, t, op(acc, h)), op(op(acc, h), List.foldr(&2, B, B, op, t, z)), internal_foldl_foldr(~B, ~op, ~assoc, ~comm, ~z, ~id, t, op(acc, h))) : {_ == op(acc, op(h, List.foldr(&2, B, B, op, t, z))) : B}
248	      assoc(acc, h, List.foldr(&2, B, B, op, t, z))
249	
250	def foldl_op_eq_foldr_op(B, op, assoc, comm, z, id, xs):
251	  %Equal.sym(B, List.foldl(&2, B, B, op, xs, z), op(z, List.foldr(&2, B, B, op, xs, z)), internal_foldl_foldr(~B, ~op, ~assoc, ~comm, ~z, ~id, xs, z)) : {_ == List.foldr(&2, B, B, op, xs, z) : B}
252	  id(List.foldr(&2, B, B, op, xs, z))
253	
254	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
255	
256	# Four-way reassociation from associativity alone, reversed to rewrite toward the simple side.
257	law op_assoc4_sym:
258	  for ~A: Data
259	  for ~op: A -> A -> A
260	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
261	  for +a: A
262	  for +b: A
263	  for +c: A
264	  for +d: A
265	  {op(a, op(b, op(c, d))) == op(op(op(a, b), c), d) : A}
266	
267	def op_assoc4_sym(A, op, assoc, a, b, c, d):
268	  Equal.sym(A, op(op(op(a, b), c), d), op(a, op(b, op(c, d))), op_assoc4(~A, ~op, ~assoc, a, b, c, d))
269	
270	# Left commutation from associativity and commutativity, reversed to rewrite toward the simple side.
271	law op_left_comm_sym:
272	  for ~A: Data
273	  for ~op: A -> A -> A
274	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
275	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
276	  for +a: A
277	  for +b: A
278	  for +c: A
279	  {op(b, op(a, c)) == op(a, op(b, c)) : A}
280	
281	def op_left_comm_sym(A, op, assoc, comm, a, b, c):
282	  Equal.sym(A, op(a, op(b, c)), op(b, op(a, c)), op_left_comm(~A, ~op, ~assoc, ~comm, a, b, c))
283	
284	# Right commutation from associativity and commutativity, reversed to rewrite toward the simple side.
285	law op_right_comm_sym:
286	  for ~A: Data
287	  for ~op: A -> A -> A
288	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
289	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
290	  for +a: A
291	  for +b: A
292	  for +c: A
293	  {op(op(a, c), b) == op(op(a, b), c) : A}
294	
295	def op_right_comm_sym(A, op, assoc, comm, a, b, c):
296	  Equal.sym(A, op(op(a, b), c), op(op(a, c), b), op_right_comm(~A, ~op, ~assoc, ~comm, a, b, c))
297	
298	# Middle-four interchange from associativity and commutativity, reversed to rewrite toward the simple side.
299	law op_four_sym:
300	  for ~A: Data
301	  for ~op: A -> A -> A
302	  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
303	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
304	  for +a: A
305	  for +b: A
306	  for +c: A
307	  for +d: A
308	  {op(op(a, c), op(b, d)) == op(op(a, b), op(c, d)) : A}
309	
310	def op_four_sym(A, op, assoc, comm, a, b, c, d):
311	  Equal.sym(A, op(op(a, b), op(c, d)), op(op(a, c), op(b, d)), op_four(~A, ~op, ~assoc, ~comm, a, b, c, d))
312	
313	# Three-way commutation from commutativity alone, reversed to rewrite toward the simple side.
314	law op_comm3_sym:
315	  for ~A: Data
316	  for ~op: A -> A -> A
317	  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
318	  for +a: A
319	  for +b: A
320	  for +c: A
321	  {op(c, op(b, a)) == op(op(a, b), c) : A}
322	
323	def op_comm3_sym(A, op, comm, a, b, c):
324	  Equal.sym(A, op(op(a, b), c), op(c, op(b, a)), op_comm3(~A, ~op, ~comm, a, b, c))
325	
326	# Nat addition is left-commutative, reversed to rewrite toward the simple side.
327	law nat_add_left_comm_sym:
328	  for +a: Nat
329	  for +b: Nat
330	  for +c: Nat
331	  {Nat.add(b, Nat.add(a, c)) == Nat.add(a, Nat.add(b, c)) : Nat}
332	
333	def nat_add_left_comm_sym(a, b, c):
334	  Equal.sym(Nat, Nat.add(a, Nat.add(b, c)), Nat.add(b, Nat.add(a, c)), nat_add_left_comm(a, b, c))
335	
336	# Nat addition is right-commutative, reversed to rewrite toward the simple side.
337	law nat_add_right_comm_sym:
338	  for +a: Nat
339	  for +b: Nat
340	  for +c: Nat
341	  {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(a, b), c) : Nat}
342	
343	def nat_add_right_comm_sym(a, b, c):
344	  Equal.sym(Nat, Nat.add(Nat.add(a, b), c), Nat.add(Nat.add(a, c), b), nat_add_right_comm(a, b, c))
345	
346	# Nat addition's middle-four interchange, reversed to rewrite toward the simple side.
347	law nat_add_four_sym:
348	  for +a: Nat
349	  for +b: Nat
350	  for +c: Nat
351	  for +d: Nat
352	  {Nat.add(Nat.add(a, c), Nat.add(b, d)) == Nat.add(Nat.add(a, b), Nat.add(c, d)) : Nat}
353	
354	def nat_add_four_sym(a, b, c, d):
355	  Equal.sym(Nat, Nat.add(Nat.add(a, b), Nat.add(c, d)), Nat.add(Nat.add(a, c), Nat.add(b, d)), nat_add_four(a, b, c, d))
356	
357	# Nat multiplication is left-commutative, reversed to rewrite toward the simple side.
358	law nat_mul_left_comm_sym:
359	  for +a: Nat
360	  for +b: Nat
361	  for +c: Nat
362	  {Nat.mul(b, Nat.mul(a, c)) == Nat.mul(a, Nat.mul(b, c)) : Nat}
363	
364	def nat_mul_left_comm_sym(a, b, c):
365	  Equal.sym(Nat, Nat.mul(a, Nat.mul(b, c)), Nat.mul(b, Nat.mul(a, c)), nat_mul_left_comm(a, b, c))
366	
367	# Nat multiplication is right-commutative, reversed to rewrite toward the simple side.
368	law nat_mul_right_comm_sym:
369	  for +a: Nat
370	  for +b: Nat
371	  for +c: Nat
372	  {Nat.mul(Nat.mul(a, c), b) == Nat.mul(Nat.mul(a, b), c) : Nat}
373	
374	def nat_mul_right_comm_sym(a, b, c):
375	  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), c), Nat.mul(Nat.mul(a, c), b), nat_mul_right_comm(a, b, c))
376	
377	# Nat multiplication's middle-four interchange, reversed to rewrite toward the simple side.
378	law nat_mul_four_sym:
379	  for +a: Nat
380	  for +b: Nat
381	  for +c: Nat
382	  for +d: Nat
383	  {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}
384	
385	def nat_mul_four_sym(a, b, c, d):
386	  Equal.sym(Nat, Nat.mul(Nat.mul(a, b), Nat.mul(c, d)), Nat.mul(Nat.mul(a, c), Nat.mul(b, d)), nat_mul_four(a, b, c, d))
387	
388	# Bool and is left-commutative, reversed to rewrite toward the simple side.
389	law bool_and_left_comm_sym:
390	  for +a: Bool
391	  for +b: Bool
392	  for +c: Bool
393	  {Bool.and(b, Bool.and(a, c)) == Bool.and(a, Bool.and(b, c)) : Bool}
394	
395	def bool_and_left_comm_sym(a, b, c):
396	  Equal.sym(Bool, Bool.and(a, Bool.and(b, c)), Bool.and(b, Bool.and(a, c)), bool_and_left_comm(a, b, c))
397	
398	# Bool and is right-commutative, reversed to rewrite toward the simple side.
399	law bool_and_right_comm_sym:
400	  for +a: Bool
401	  for +b: Bool
402	  for +c: Bool
403	  {Bool.and(Bool.and(a, c), b) == Bool.and(Bool.and(a, b), c) : Bool}
404	
405	def bool_and_right_comm_sym(a, b, c):
406	  Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(Bool.and(a, c), b), bool_and_right_comm(a, b, c))
407	
408	# Bool or is left-commutative, reversed to rewrite toward the simple side.
409	law bool_or_left_comm_sym:
410	  for +a: Bool
411	  for +b: Bool
412	  for +c: Bool
413	  {Bool.or(b, Bool.or(a, c)) == Bool.or(a, Bool.or(b, c)) : Bool}
414	
415	def bool_or_left_comm_sym(a, b, c):
416	  Equal.sym(Bool, Bool.or(a, Bool.or(b, c)), Bool.or(b, Bool.or(a, c)), bool_or_left_comm(a, b, c))
417	
418	# Bool or is right-commutative, reversed to rewrite toward the simple side.
419	law bool_or_right_comm_sym:
420	  for +a: Bool
421	  for +b: Bool
422	  for +c: Bool
423	  {Bool.or(Bool.or(a, c), b) == Bool.or(Bool.or(a, b), c) : Bool}
424	
425	def bool_or_right_comm_sym(a, b, c):
426	  Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(Bool.or(a, c), b), bool_or_right_comm(a, b, c))
427	
428	# Four-way reassociation for List append over Nat, reversed to rewrite toward the simple side.
429	law list_nat_append_assoc4_sym:
430	  for +a: List<&2, Nat>
431	  for +b: List<&2, Nat>
432	  for +c: List<&2, Nat>
433	  for +d: List<&2, Nat>
434	  {List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) == List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) : List<&2, Nat>}
435	
436	def list_nat_append_assoc4_sym(a, b, c, d):
437	  Equal.sym(List<&2, Nat>, List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d), List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))), list_nat_append_assoc4(a, b, c, d))
438	
439	# Folding left equals folding right for an associative, commutative operation with a left identity, reversed to rewrite toward the simple side.
440	law foldl_op_eq_foldr_op_sym:
441	  for ~B: Data
442	  for ~op: B -> B -> B
443	  for ~assoc: @x: B -> @y: B -> @z: B -> {op(op(x, y), z) == op(x, op(y, z)) : B}
444	  for ~comm: @x: B -> @y: B -> {op(x, y) == op(y, x) : B}
445	  for ~z: B
446	  for ~id: @x: B -> {op(z, x) == x : B}
447	  for +xs: List<&2, B>
448	  {List.foldr(&2, B, B, op, xs, z) == List.foldl(&2, B, B, op, xs, z) : B}
449	
450	def foldl_op_eq_foldr_op_sym(B, op, assoc, comm, z, id, xs):
451	  Equal.sym(B, List.foldl(&2, B, B, op, xs, z), List.foldr(&2, B, B, op, xs, z), foldl_op_eq_foldr_op(~B, ~op, ~assoc, ~comm, ~z, ~id, xs))