1	# bend-mathlib/bool.bend: Bool algebra (not, and, or, xor).
2	import Base
3	
4	# Negating a boolean twice gives it back.
5	law not_not:
6	  for b: Bool
7	  {Bool.not(Bool.not(b)) == b : Bool}
8	
9	def not_not(b):
10	  match b:
11	    case True{}:
12	      {==}
13	    case False{}:
14	      {==}
15	
16	# Boolean and is commutative.
17	law and_comm:
18	  for a: Bool
19	  for b: Bool
20	  {Bool.and(a, b) == Bool.and(b, a) : Bool}
21	
22	def and_comm(a, b):
23	  match a b:
24	    case True{} True{}:
25	      {==}
26	    case True{} False{}:
27	      {==}
28	    case False{} True{}:
29	      {==}
30	    case False{} False{}:
31	      {==}
32	
33	# Boolean or is commutative.
34	law or_comm:
35	  for a: Bool
36	  for b: Bool
37	  {Bool.or(a, b) == Bool.or(b, a) : Bool}
38	
39	def or_comm(a, b):
40	  match a b:
41	    case True{} True{}:
42	      {==}
43	    case True{} False{}:
44	      {==}
45	    case False{} True{}:
46	      {==}
47	    case False{} False{}:
48	      {==}
49	
50	# Boolean and is associative.
51	law and_assoc:
52	  for a: Bool
53	  for -b: Bool
54	  for -c: Bool
55	  {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
56	
57	def and_assoc(a, b, c):
58	  match a:
59	    case True{}:
60	      {==}
61	    case False{}:
62	      {==}
63	
64	# Boolean or is associative.
65	law or_assoc:
66	  for a: Bool
67	  for -b: Bool
68	  for -c: Bool
69	  {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}
70	
71	def or_assoc(a, b, c):
72	  match a:
73	    case True{}:
74	      {==}
75	    case False{}:
76	      {==}
77	
78	# True is a right identity for and: a and true is a.
79	law and_true:
80	  for a: Bool
81	  {Bool.and(a, True{}) == a : Bool}
82	
83	def and_true(a):
84	  match a:
85	    case True{}:
86	      {==}
87	    case False{}:
88	      {==}
89	
90	# True is a left identity for and: true and a is a.
91	law true_and:
92	  for -a: Bool
93	  {Bool.and(True{}, a) == a : Bool}
94	
95	def true_and(a):
96	  {==}
97	
98	# False absorbs and on the right: a and false is false.
99	law and_false:
100	  for a: Bool
101	  {Bool.and(a, False{}) == False{} : Bool}
102	
103	def and_false(a):
104	  match a:
105	    case True{}:
106	      {==}
107	    case False{}:
108	      {==}
109	
110	# False absorbs and on the left: false and a is false.
111	law false_and:
112	  for -a: Bool
113	  {Bool.and(False{}, a) == False{} : Bool}
114	
115	def false_and(a):
116	  {==}
117	
118	# False is a right identity for or: a or false is a.
119	law or_false:
120	  for a: Bool
121	  {Bool.or(a, False{}) == a : Bool}
122	
123	def or_false(a):
124	  match a:
125	    case True{}:
126	      {==}
127	    case False{}:
128	      {==}
129	
130	# False is a left identity for or: false or a is a.
131	law false_or:
132	  for -a: Bool
133	  {Bool.or(False{}, a) == a : Bool}
134	
135	def false_or(a):
136	  {==}
137	
138	# True absorbs or on the right: a or true is true.
139	law or_true:
140	  for a: Bool
141	  {Bool.or(a, True{}) == True{} : Bool}
142	
143	def or_true(a):
144	  match a:
145	    case True{}:
146	      {==}
147	    case False{}:
148	      {==}
149	
150	# True absorbs or on the left: true or a is true.
151	law true_or:
152	  for -a: Bool
153	  {Bool.or(True{}, a) == True{} : Bool}
154	
155	def true_or(a):
156	  {==}
157	
158	# De Morgan: not (a and b) is (not a) or (not b).
159	law de_morgan_and:
160	  for a: Bool
161	  for -b: Bool
162	  {Bool.not(Bool.and(a, b)) == Bool.or(Bool.not(a), Bool.not(b)) : Bool}
163	
164	def de_morgan_and(a, b):
165	  match a:
166	    case True{}:
167	      {==}
168	    case False{}:
169	      {==}
170	
171	# De Morgan: not (a or b) is (not a) and (not b).
172	law de_morgan_or:
173	  for a: Bool
174	  for -b: Bool
175	  {Bool.not(Bool.or(a, b)) == Bool.and(Bool.not(a), Bool.not(b)) : Bool}
176	
177	def de_morgan_or(a, b):
178	  match a:
179	    case True{}:
180	      {==}
181	    case False{}:
182	      {==}
183	
184	def internal_true_ne_false(e: {True{} == False{} : Bool}) -> Empty:
185	  %e : Bool.pick(Type, _, Unit, Empty)
186	  Unit{}
187	
188	# True and False are different booleans.
189	law true_ne_false:
190	  {True{} != False{} : Bool}
191	
192	def true_ne_false():
193	  e => internal_true_ne_false(e)
194	
195	# And with itself: a and a is a.
196	law and_self:
197	  for a: Bool
198	  {Bool.and(a, a) == a : Bool}
199	
200	def and_self(a):
201	  match a:
202	    case True{}:
203	      {==}
204	    case False{}:
205	      {==}
206	
207	# Or with itself: a or a is a.
208	law or_self:
209	  for a: Bool
210	  {Bool.or(a, a) == a : Bool}
211	
212	def or_self(a):
213	  match a:
214	    case True{}:
215	      {==}
216	    case False{}:
217	      {==}
218	
219	# A boolean and its negation are never both true: a and (not a) is false.
220	law and_not_self:
221	  for a: Bool
222	  {Bool.and(a, Bool.not(a)) == False{} : Bool}
223	
224	def and_not_self(a):
225	  match a:
226	    case True{}:
227	      {==}
228	    case False{}:
229	      {==}
230	
231	# A boolean or its negation is always true: a or (not a) is true.
232	law or_not_self:
233	  for a: Bool
234	  {Bool.or(a, Bool.not(a)) == True{} : Bool}
235	
236	def or_not_self(a):
237	  match a:
238	    case True{}:
239	      {==}
240	    case False{}:
241	      {==}
242	
243	# And distributes over or: a and (b or c) is (a and b) or (a and c).
244	law and_or_distrib_left:
245	  for a: Bool
246	  for -b: Bool
247	  for -c: Bool
248	  {Bool.and(a, Bool.or(b, c)) == Bool.or(Bool.and(a, b), Bool.and(a, c)) : Bool}
249	
250	def and_or_distrib_left(a, b, c):
251	  match a:
252	    case True{}:
253	      {==}
254	    case False{}:
255	      {==}
256	
257	# Or distributes over and: a or (b and c) is (a or b) and (a or c).
258	law or_and_distrib_left:
259	  for a: Bool
260	  for -b: Bool
261	  for -c: Bool
262	  {Bool.or(a, Bool.and(b, c)) == Bool.and(Bool.or(a, b), Bool.or(a, c)) : Bool}
263	
264	def or_and_distrib_left(a, b, c):
265	  match a:
266	    case True{}:
267	      {==}
268	    case False{}:
269	      {==}
270	
271	# Absorption: a and (a or b) is a.
272	law and_or_absorb:
273	  for a: Bool
274	  for -b: Bool
275	  {Bool.and(a, Bool.or(a, b)) == a : Bool}
276	
277	def and_or_absorb(a, b):
278	  match a:
279	    case True{}:
280	      {==}
281	    case False{}:
282	      {==}
283	
284	# Absorption: a or (a and b) is a.
285	law or_and_absorb:
286	  for a: Bool
287	  for -b: Bool
288	  {Bool.or(a, Bool.and(a, b)) == a : Bool}
289	
290	def or_and_absorb(a, b):
291	  match a:
292	    case True{}:
293	      {==}
294	    case False{}:
295	      {==}
296	
297	# Exclusive or is commutative.
298	law xor_comm:
299	  for a: Bool
300	  for b: Bool
301	  {Bool.xor(a, b) == Bool.xor(b, a) : Bool}
302	
303	def xor_comm(a, b):
304	  match a b:
305	    case True{} True{}:
306	      {==}
307	    case True{} False{}:
308	      {==}
309	    case False{} True{}:
310	      {==}
311	    case False{} False{}:
312	      {==}
313	
314	# Exclusive or is associative.
315	law xor_assoc:
316	  for a: Bool
317	  for b: Bool
318	  for c: Bool
319	  {Bool.xor(Bool.xor(a, b), c) == Bool.xor(a, Bool.xor(b, c)) : Bool}
320	
321	def xor_assoc(a, b, c):
322	  match a b c:
323	    case True{} True{} True{}:
324	      {==}
325	    case True{} True{} False{}:
326	      {==}
327	    case True{} False{} True{}:
328	      {==}
329	    case True{} False{} False{}:
330	      {==}
331	    case False{} True{} True{}:
332	      {==}
333	    case False{} True{} False{}:
334	      {==}
335	    case False{} False{} True{}:
336	      {==}
337	    case False{} False{} False{}:
338	      {==}
339	
340	# A boolean xor itself is false.
341	law xor_self:
342	  for a: Bool
343	  {Bool.xor(a, a) == False{} : Bool}
344	
345	def xor_self(a):
346	  match a:
347	    case True{}:
348	      {==}
349	    case False{}:
350	      {==}
351	
352	# False is an identity for xor: a xor false is a.
353	law xor_false:
354	  for a: Bool
355	  {Bool.xor(a, False{}) == a : Bool}
356	
357	def xor_false(a):
358	  match a:
359	    case True{}:
360	      {==}
361	    case False{}:
362	      {==}
363	
364	# Xor with true negates: a xor true is not a.
365	law xor_true:
366	  for a: Bool
367	  {Bool.xor(a, True{}) == Bool.not(a) : Bool}
368	
369	def xor_true(a):
370	  match a:
371	    case True{}:
372	      {==}
373	    case False{}:
374	      {==}
375	
376	# Negation is injective: not a = not b implies a = b.
377	law not_inj:
378	  for a: Bool
379	  for b: Bool
380	  for h: {Bool.not(a) == Bool.not(b) : Bool}
381	  {a == b : Bool}
382	
383	def not_inj(a, b, h):
384	  match a b:
385	    case True{} True{}:
386	      {==}
387	    case True{} False{}:
388	      Empty.absurd({True{} == False{} : Bool}, internal_true_ne_false(Equal.sym(Bool, False{}, True{}, h)))
389	    case False{} True{}:
390	      Empty.absurd({False{} == True{} : Bool}, internal_true_ne_false(h))
391	    case False{} False{}:
392	      {==}
393	
394	# A boolean that is not false is true.
395	law eq_true_of_ne_false:
396	  for a: Bool
397	  for h: {a == False{} : Bool} -> Empty
398	  {a == True{} : Bool}
399	
400	def eq_true_of_ne_false(a, h):
401	  match a:
402	    case True{}:
403	      {==}
404	    case False{}:
405	      Empty.absurd({False{} == True{} : Bool}, h({==}))
406	
407	def internal_false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
408	  %e : Bool.pick(Type, _, Empty, Unit)
409	  Unit{}
410	
411	# Comparing a boolean with itself gives EQ.
412	law cmp_refl:
413	  for b: Bool
414	  {Bool.cmp(b, b) == EQ{} : Cmp}
415	
416	def cmp_refl(b):
417	  match b:
418	    case True{}:
419	      {==}
420	    case False{}:
421	      {==}
422	
423	# Two booleans that compare EQ are equal.
424	law eq_of_cmp_eq:
425	  for a: Bool
426	  for b: Bool
427	  for h: {Cmp.is_eq(Bool.cmp(a, b)) == True{} : Bool}
428	  {a == b : Bool}
429	
430	def eq_of_cmp_eq(a, b, h):
431	  match a b:
432	    case True{} True{}:
433	      {==}
434	    case False{} False{}:
435	      {==}
436	    case True{} False{}:
437	      Empty.absurd({True{} == False{} : Bool}, internal_false_ne_true(h))
438	    case False{} True{}:
439	      Empty.absurd({False{} == True{} : Bool}, internal_false_ne_true(h))
440	
441	# False and True are different booleans, the other way round.
442	law false_ne_true:
443	  {False{} != True{} : Bool}
444	
445	def false_ne_true():
446	  e => internal_false_ne_true(e)
447	
448	# If a and b is true then a is true.
449	law eq_true_of_and_left:
450	  for a: Bool
451	  for -b: Bool
452	  for h: {Bool.and(a, b) == True{} : Bool}
453	  {a == True{} : Bool}
454	
455	def eq_true_of_and_left(a, b, h):
456	  match a:
457	    case True{}:
458	      {==}
459	    case False{}:
460	      Empty.absurd({False{} == True{} : Bool}, internal_false_ne_true(h))
461	
462	# If a and b is true then b is true.
463	law eq_true_of_and_right:
464	  for a: Bool
465	  for -b: Bool
466	  for h: {Bool.and(a, b) == True{} : Bool}
467	  {b == True{} : Bool}
468	
469	def eq_true_of_and_right(a, b, h):
470	  match a:
471	    case True{}:
472	      h
473	    case False{}:
474	      Empty.absurd({b == True{} : Bool}, internal_false_ne_true(h))
475	
476	# If a and b are both true then a and b is true.
477	law and_eq_true:
478	  for a: Bool
479	  for -b: Bool
480	  for ha: {a == True{} : Bool}
481	  for hb: {b == True{} : Bool}
482	  {Bool.and(a, b) == True{} : Bool}
483	
484	def and_eq_true(a, b, ha, hb):
485	  match a:
486	    case True{}:
487	      hb
488	    case False{}:
489	      Empty.absurd({Bool.and(False{}, b) == True{} : Bool}, internal_false_ne_true(ha))
490	
491	# If a or b is true and b is false then a is true.
492	law eq_true_of_or_eq_false_right:
493	  for a: Bool
494	  for -b: Bool
495	  for h: {Bool.or(a, b) == True{} : Bool}
496	  for hb: {b == False{} : Bool}
497	  {a == True{} : Bool}
498	
499	def eq_true_of_or_eq_false_right(a, b, h, hb):
500	  match a:
501	    case True{}:
502	      {==}
503	    case False{}:
504	      Empty.absurd({False{} == True{} : Bool}, internal_false_ne_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, hb), h)))
505	
506	# If a or b is true and a is false then b is true.
507	law eq_true_of_or_eq_false_left:
508	  for a: Bool
509	  for -b: Bool
510	  for h: {Bool.or(a, b) == True{} : Bool}
511	  for ha: {a == False{} : Bool}
512	  {b == True{} : Bool}
513	
514	def eq_true_of_or_eq_false_left(a, b, h, ha):
515	  match a:
516	    case True{}:
517	      Empty.absurd({b == True{} : Bool}, internal_true_ne_false(ha))
518	    case False{}:
519	      h
520	
521	# If not b is true then b is false.
522	law eq_false_of_not_eq_true:
523	  for b: Bool
524	  for h: {Bool.not(b) == True{} : Bool}
525	  {b == False{} : Bool}
526	
527	def eq_false_of_not_eq_true(b, h):
528	  match b:
529	    case True{}:
530	      Empty.absurd({True{} == False{} : Bool}, internal_false_ne_true(h))
531	    case False{}:
532	      {==}
533	
534	# --- generated: _sym twins (tools/mathlib/twins.ts), do not edit ---
535	
536	# Negating a boolean twice gives it back, reversed to rewrite toward the simple side.
537	law not_not_sym:
538	  for b: Bool
539	  {b == Bool.not(Bool.not(b)) : Bool}
540	
541	def not_not_sym(b):
542	  Equal.sym(Bool, Bool.not(Bool.not(b)), b, not_not(b))
543	
544	# Boolean and is commutative, reversed to rewrite toward the simple side.
545	law and_comm_sym:
546	  for a: Bool
547	  for b: Bool
548	  {Bool.and(b, a) == Bool.and(a, b) : Bool}
549	
550	def and_comm_sym(a, b):
551	  Equal.sym(Bool, Bool.and(a, b), Bool.and(b, a), and_comm(a, b))
552	
553	# Boolean or is commutative, reversed to rewrite toward the simple side.
554	law or_comm_sym:
555	  for a: Bool
556	  for b: Bool
557	  {Bool.or(b, a) == Bool.or(a, b) : Bool}
558	
559	def or_comm_sym(a, b):
560	  Equal.sym(Bool, Bool.or(a, b), Bool.or(b, a), or_comm(a, b))
561	
562	# Boolean and is associative, reversed to rewrite toward the simple side.
563	law and_assoc_sym:
564	  for a: Bool
565	  for -b: Bool
566	  for -c: Bool
567	  {Bool.and(a, Bool.and(b, c)) == Bool.and(Bool.and(a, b), c) : Bool}
568	
569	def and_assoc_sym(a, b, c):
570	  Equal.sym(Bool, Bool.and(Bool.and(a, b), c), Bool.and(a, Bool.and(b, c)), and_assoc(a, b, c))
571	
572	# Boolean or is associative, reversed to rewrite toward the simple side.
573	law or_assoc_sym:
574	  for a: Bool
575	  for -b: Bool
576	  for -c: Bool
577	  {Bool.or(a, Bool.or(b, c)) == Bool.or(Bool.or(a, b), c) : Bool}
578	
579	def or_assoc_sym(a, b, c):
580	  Equal.sym(Bool, Bool.or(Bool.or(a, b), c), Bool.or(a, Bool.or(b, c)), or_assoc(a, b, c))
581	
582	# True is a right identity for and: a and true is a, reversed to rewrite toward the simple side.
583	law and_true_sym:
584	  for a: Bool
585	  {a == Bool.and(a, True{}) : Bool}
586	
587	def and_true_sym(a):
588	  Equal.sym(Bool, Bool.and(a, True{}), a, and_true(a))
589	
590	# True is a left identity for and: true and a is a, reversed to rewrite toward the simple side.
591	law true_and_sym:
592	  for -a: Bool
593	  {a == Bool.and(True{}, a) : Bool}
594	
595	def true_and_sym(a):
596	  Equal.sym(Bool, Bool.and(True{}, a), a, true_and(a))
597	
598	# False absorbs and on the right: a and false is false, reversed to rewrite toward the simple side.
599	law and_false_sym:
600	  for a: Bool
601	  {False{} == Bool.and(a, False{}) : Bool}
602	
603	def and_false_sym(a):
604	  Equal.sym(Bool, Bool.and(a, False{}), False{}, and_false(a))
605	
606	# False absorbs and on the left: false and a is false, reversed to rewrite toward the simple side.
607	law false_and_sym:
608	  for -a: Bool
609	  {False{} == Bool.and(False{}, a) : Bool}
610	
611	def false_and_sym(a):
612	  Equal.sym(Bool, Bool.and(False{}, a), False{}, false_and(a))
613	
614	# False is a right identity for or: a or false is a, reversed to rewrite toward the simple side.
615	law or_false_sym:
616	  for a: Bool
617	  {a == Bool.or(a, False{}) : Bool}
618	
619	def or_false_sym(a):
620	  Equal.sym(Bool, Bool.or(a, False{}), a, or_false(a))
621	
622	# False is a left identity for or: false or a is a, reversed to rewrite toward the simple side.
623	law false_or_sym:
624	  for -a: Bool
625	  {a == Bool.or(False{}, a) : Bool}
626	
627	def false_or_sym(a):
628	  Equal.sym(Bool, Bool.or(False{}, a), a, false_or(a))
629	
630	# True absorbs or on the right: a or true is true, reversed to rewrite toward the simple side.
631	law or_true_sym:
632	  for a: Bool
633	  {True{} == Bool.or(a, True{}) : Bool}
634	
635	def or_true_sym(a):
636	  Equal.sym(Bool, Bool.or(a, True{}), True{}, or_true(a))
637	
638	# True absorbs or on the left: true or a is true, reversed to rewrite toward the simple side.
639	law true_or_sym:
640	  for -a: Bool
641	  {True{} == Bool.or(True{}, a) : Bool}
642	
643	def true_or_sym(a):
644	  Equal.sym(Bool, Bool.or(True{}, a), True{}, true_or(a))
645	
646	# De Morgan: not (a and b) is (not a) or (not b), reversed to rewrite toward the simple side.
647	law de_morgan_and_sym:
648	  for a: Bool
649	  for -b: Bool
650	  {Bool.or(Bool.not(a), Bool.not(b)) == Bool.not(Bool.and(a, b)) : Bool}
651	
652	def de_morgan_and_sym(a, b):
653	  Equal.sym(Bool, Bool.not(Bool.and(a, b)), Bool.or(Bool.not(a), Bool.not(b)), de_morgan_and(a, b))
654	
655	# De Morgan: not (a or b) is (not a) and (not b), reversed to rewrite toward the simple side.
656	law de_morgan_or_sym:
657	  for a: Bool
658	  for -b: Bool
659	  {Bool.and(Bool.not(a), Bool.not(b)) == Bool.not(Bool.or(a, b)) : Bool}
660	
661	def de_morgan_or_sym(a, b):
662	  Equal.sym(Bool, Bool.not(Bool.or(a, b)), Bool.and(Bool.not(a), Bool.not(b)), de_morgan_or(a, b))
663	
664	# And with itself: a and a is a, reversed to rewrite toward the simple side.
665	law and_self_sym:
666	  for a: Bool
667	  {a == Bool.and(a, a) : Bool}
668	
669	def and_self_sym(a):
670	  Equal.sym(Bool, Bool.and(a, a), a, and_self(a))
671	
672	# Or with itself: a or a is a, reversed to rewrite toward the simple side.
673	law or_self_sym:
674	  for a: Bool
675	  {a == Bool.or(a, a) : Bool}
676	
677	def or_self_sym(a):
678	  Equal.sym(Bool, Bool.or(a, a), a, or_self(a))
679	
680	# A boolean and its negation are never both true: a and (not a) is false, reversed to rewrite toward the simple side.
681	law and_not_self_sym:
682	  for a: Bool
683	  {False{} == Bool.and(a, Bool.not(a)) : Bool}
684	
685	def and_not_self_sym(a):
686	  Equal.sym(Bool, Bool.and(a, Bool.not(a)), False{}, and_not_self(a))
687	
688	# A boolean or its negation is always true: a or (not a) is true, reversed to rewrite toward the simple side.
689	law or_not_self_sym:
690	  for a: Bool
691	  {True{} == Bool.or(a, Bool.not(a)) : Bool}
692	
693	def or_not_self_sym(a):
694	  Equal.sym(Bool, Bool.or(a, Bool.not(a)), True{}, or_not_self(a))
695	
696	# And distributes over or: a and (b or c) is (a and b) or (a and c), reversed to rewrite toward the simple side.
697	law and_or_distrib_left_sym:
698	  for a: Bool
699	  for -b: Bool
700	  for -c: Bool
701	  {Bool.or(Bool.and(a, b), Bool.and(a, c)) == Bool.and(a, Bool.or(b, c)) : Bool}
702	
703	def and_or_distrib_left_sym(a, b, c):
704	  Equal.sym(Bool, Bool.and(a, Bool.or(b, c)), Bool.or(Bool.and(a, b), Bool.and(a, c)), and_or_distrib_left(a, b, c))
705	
706	# Or distributes over and: a or (b and c) is (a or b) and (a or c), reversed to rewrite toward the simple side.
707	law or_and_distrib_left_sym:
708	  for a: Bool
709	  for -b: Bool
710	  for -c: Bool
711	  {Bool.and(Bool.or(a, b), Bool.or(a, c)) == Bool.or(a, Bool.and(b, c)) : Bool}
712	
713	def or_and_distrib_left_sym(a, b, c):
714	  Equal.sym(Bool, Bool.or(a, Bool.and(b, c)), Bool.and(Bool.or(a, b), Bool.or(a, c)), or_and_distrib_left(a, b, c))
715	
716	# Absorption: a and (a or b) is a, reversed to rewrite toward the simple side.
717	law and_or_absorb_sym:
718	  for a: Bool
719	  for -b: Bool
720	  {a == Bool.and(a, Bool.or(a, b)) : Bool}
721	
722	def and_or_absorb_sym(a, b):
723	  Equal.sym(Bool, Bool.and(a, Bool.or(a, b)), a, and_or_absorb(a, b))
724	
725	# Absorption: a or (a and b) is a, reversed to rewrite toward the simple side.
726	law or_and_absorb_sym:
727	  for a: Bool
728	  for -b: Bool
729	  {a == Bool.or(a, Bool.and(a, b)) : Bool}
730	
731	def or_and_absorb_sym(a, b):
732	  Equal.sym(Bool, Bool.or(a, Bool.and(a, b)), a, or_and_absorb(a, b))
733	
734	# Exclusive or is commutative, reversed to rewrite toward the simple side.
735	law xor_comm_sym:
736	  for a: Bool
737	  for b: Bool
738	  {Bool.xor(b, a) == Bool.xor(a, b) : Bool}
739	
740	def xor_comm_sym(a, b):
741	  Equal.sym(Bool, Bool.xor(a, b), Bool.xor(b, a), xor_comm(a, b))
742	
743	# Exclusive or is associative, reversed to rewrite toward the simple side.
744	law xor_assoc_sym:
745	  for a: Bool
746	  for b: Bool
747	  for c: Bool
748	  {Bool.xor(a, Bool.xor(b, c)) == Bool.xor(Bool.xor(a, b), c) : Bool}
749	
750	def xor_assoc_sym(a, b, c):
751	  Equal.sym(Bool, Bool.xor(Bool.xor(a, b), c), Bool.xor(a, Bool.xor(b, c)), xor_assoc(a, b, c))
752	
753	# A boolean xor itself is false, reversed to rewrite toward the simple side.
754	law xor_self_sym:
755	  for a: Bool
756	  {False{} == Bool.xor(a, a) : Bool}
757	
758	def xor_self_sym(a):
759	  Equal.sym(Bool, Bool.xor(a, a), False{}, xor_self(a))
760	
761	# False is an identity for xor: a xor false is a, reversed to rewrite toward the simple side.
762	law xor_false_sym:
763	  for a: Bool
764	  {a == Bool.xor(a, False{}) : Bool}
765	
766	def xor_false_sym(a):
767	  Equal.sym(Bool, Bool.xor(a, False{}), a, xor_false(a))
768	
769	# Xor with true negates: a xor true is not a, reversed to rewrite toward the simple side.
770	law xor_true_sym:
771	  for a: Bool
772	  {Bool.not(a) == Bool.xor(a, True{}) : Bool}
773	
774	def xor_true_sym(a):
775	  Equal.sym(Bool, Bool.xor(a, True{}), Bool.not(a), xor_true(a))
776	
777	# Comparing a boolean with itself gives EQ, reversed to rewrite toward the simple side.
778	law cmp_refl_sym:
779	  for b: Bool
780	  {EQ{} == Bool.cmp(b, b) : Cmp}
781	
782	def cmp_refl_sym(b):
783	  Equal.sym(Cmp, Bool.cmp(b, b), EQ{}, cmp_refl(b))