-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAlgebra.Properties.CommutativeSemigroup.html
124 lines (91 loc) · 71.1 KB
/
Algebra.Properties.CommutativeSemigroup.html
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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Algebra.Properties.CommutativeSemigroup</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Some theory for commutative semigroup</a>
<a id="147" class="Comment">------------------------------------------------------------------------</a>
<a id="221" class="Symbol">{-#</a> <a id="225" class="Keyword">OPTIONS</a> <a id="233" class="Pragma">--without-K</a> <a id="245" class="Pragma">--safe</a> <a id="252" class="Symbol">#-}</a>
<a id="257" class="Keyword">open</a> <a id="262" class="Keyword">import</a> <a id="269" href="Algebra.html" class="Module">Algebra</a> <a id="277" class="Keyword">using</a> <a id="283" class="Symbol">(</a><a id="284" href="Algebra.Bundles.html#2868" class="Record">CommutativeSemigroup</a><a id="304" class="Symbol">)</a>
<a id="307" class="Keyword">module</a> <a id="314" href="Algebra.Properties.CommutativeSemigroup.html" class="Module">Algebra.Properties.CommutativeSemigroup</a>
<a id="356" class="Symbol">{</a><a id="357" href="Algebra.Properties.CommutativeSemigroup.html#357" class="Bound">a</a> <a id="359" href="Algebra.Properties.CommutativeSemigroup.html#359" class="Bound">ℓ</a><a id="360" class="Symbol">}</a> <a id="362" class="Symbol">(</a><a id="363" href="Algebra.Properties.CommutativeSemigroup.html#363" class="Bound">CS</a> <a id="366" class="Symbol">:</a> <a id="368" href="Algebra.Bundles.html#2868" class="Record">CommutativeSemigroup</a> <a id="389" href="Algebra.Properties.CommutativeSemigroup.html#357" class="Bound">a</a> <a id="391" href="Algebra.Properties.CommutativeSemigroup.html#359" class="Bound">ℓ</a><a id="392" class="Symbol">)</a>
<a id="396" class="Keyword">where</a>
<a id="403" class="Keyword">open</a> <a id="408" href="Algebra.Bundles.html#2868" class="Module">CommutativeSemigroup</a> <a id="429" href="Algebra.Properties.CommutativeSemigroup.html#363" class="Bound">CS</a>
<a id="433" class="Keyword">open</a> <a id="438" class="Keyword">import</a> <a id="445" href="Relation.Binary.Reasoning.Setoid.html" class="Module">Relation.Binary.Reasoning.Setoid</a> <a id="478" href="Algebra.Structures.html#1285" class="Function">setoid</a>
<a id="486" class="Comment">------------------------------------------------------------------------------</a>
<a id="565" class="Comment">-- Re-export the contents of semigroup</a>
<a id="605" class="Keyword">open</a> <a id="610" class="Keyword">import</a> <a id="617" href="Algebra.Properties.Semigroup.html" class="Module">Algebra.Properties.Semigroup</a> <a id="646" href="Algebra.Bundles.html#3204" class="Function">semigroup</a> <a id="656" class="Keyword">public</a>
<a id="664" class="Comment">------------------------------------------------------------------------------</a>
<a id="743" class="Comment">-- Permutation laws for _∙_ for three factors.</a>
<a id="791" class="Comment">------------------------------------------------------------------------------</a>
<a id="870" class="Comment">-- Partitions (1,1).</a>
<a id="891" class="Comment">-- There are five nontrivial permutations.</a>
<a id="934" class="Comment">------------------------------------------------------------------------------</a>
<a id="x∙yz≈y∙xz"></a><a id="1014" href="Algebra.Properties.CommutativeSemigroup.html#1014" class="Function">x∙yz≈y∙xz</a> <a id="1024" class="Symbol">:</a> <a id="1027" class="Symbol">∀</a> <a id="1029" href="Algebra.Properties.CommutativeSemigroup.html#1029" class="Bound">x</a> <a id="1031" href="Algebra.Properties.CommutativeSemigroup.html#1031" class="Bound">y</a> <a id="1033" href="Algebra.Properties.CommutativeSemigroup.html#1033" class="Bound">z</a> <a id="1035" class="Symbol">→</a> <a id="1037" href="Algebra.Properties.CommutativeSemigroup.html#1029" class="Bound">x</a> <a id="1039" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1041" class="Symbol">(</a><a id="1042" href="Algebra.Properties.CommutativeSemigroup.html#1031" class="Bound">y</a> <a id="1044" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1046" href="Algebra.Properties.CommutativeSemigroup.html#1033" class="Bound">z</a><a id="1047" class="Symbol">)</a> <a id="1049" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="1051" href="Algebra.Properties.CommutativeSemigroup.html#1031" class="Bound">y</a> <a id="1053" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1055" class="Symbol">(</a><a id="1056" href="Algebra.Properties.CommutativeSemigroup.html#1029" class="Bound">x</a> <a id="1058" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1060" href="Algebra.Properties.CommutativeSemigroup.html#1033" class="Bound">z</a><a id="1061" class="Symbol">)</a>
<a id="1063" href="Algebra.Properties.CommutativeSemigroup.html#1014" class="Function">x∙yz≈y∙xz</a> <a id="1073" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1075" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a> <a id="1077" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a> <a id="1079" class="Symbol">=</a> <a id="1081" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin</a>
<a id="1089" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1091" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1093" class="Symbol">(</a><a id="1094" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a> <a id="1096" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1098" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a><a id="1099" class="Symbol">)</a> <a id="1104" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1107" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="1111" class="Symbol">(</a><a id="1112" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="1118" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1120" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a> <a id="1122" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a><a id="1123" class="Symbol">)</a> <a id="1125" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1129" class="Symbol">(</a><a id="1130" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1132" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1134" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a><a id="1135" class="Symbol">)</a> <a id="1137" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1139" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a> <a id="1144" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1147" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="1155" class="Symbol">(</a><a id="1156" href="Algebra.Structures.html#2188" class="Function">comm</a> <a id="1161" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1163" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a><a id="1164" class="Symbol">)</a> <a id="1166" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1170" class="Symbol">(</a><a id="1171" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a> <a id="1173" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1175" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a><a id="1176" class="Symbol">)</a> <a id="1178" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1180" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a> <a id="1185" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1188" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="1194" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a> <a id="1196" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1198" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a> <a id="1200" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1204" href="Algebra.Properties.CommutativeSemigroup.html#1075" class="Bound">y</a> <a id="1206" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1208" class="Symbol">(</a><a id="1209" href="Algebra.Properties.CommutativeSemigroup.html#1073" class="Bound">x</a> <a id="1211" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1213" href="Algebra.Properties.CommutativeSemigroup.html#1077" class="Bound">z</a><a id="1214" class="Symbol">)</a> <a id="1219" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">∎</a>
<a id="x∙yz≈z∙yx"></a><a id="1222" href="Algebra.Properties.CommutativeSemigroup.html#1222" class="Function">x∙yz≈z∙yx</a> <a id="1232" class="Symbol">:</a> <a id="1235" class="Symbol">∀</a> <a id="1237" href="Algebra.Properties.CommutativeSemigroup.html#1237" class="Bound">x</a> <a id="1239" href="Algebra.Properties.CommutativeSemigroup.html#1239" class="Bound">y</a> <a id="1241" href="Algebra.Properties.CommutativeSemigroup.html#1241" class="Bound">z</a> <a id="1243" class="Symbol">→</a> <a id="1245" href="Algebra.Properties.CommutativeSemigroup.html#1237" class="Bound">x</a> <a id="1247" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1249" class="Symbol">(</a><a id="1250" href="Algebra.Properties.CommutativeSemigroup.html#1239" class="Bound">y</a> <a id="1252" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1254" href="Algebra.Properties.CommutativeSemigroup.html#1241" class="Bound">z</a><a id="1255" class="Symbol">)</a> <a id="1257" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="1259" href="Algebra.Properties.CommutativeSemigroup.html#1241" class="Bound">z</a> <a id="1261" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1263" class="Symbol">(</a><a id="1264" href="Algebra.Properties.CommutativeSemigroup.html#1239" class="Bound">y</a> <a id="1266" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1268" href="Algebra.Properties.CommutativeSemigroup.html#1237" class="Bound">x</a><a id="1269" class="Symbol">)</a>
<a id="1271" href="Algebra.Properties.CommutativeSemigroup.html#1222" class="Function">x∙yz≈z∙yx</a> <a id="1281" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a> <a id="1283" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a> <a id="1285" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a> <a id="1287" class="Symbol">=</a> <a id="1289" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin</a>
<a id="1297" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a> <a id="1299" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1301" class="Symbol">(</a><a id="1302" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a> <a id="1304" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1306" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a><a id="1307" class="Symbol">)</a> <a id="1312" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1315" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="1323" class="Symbol">(</a><a id="1324" href="Algebra.Structures.html#2188" class="Function">comm</a> <a id="1329" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a> <a id="1331" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a><a id="1332" class="Symbol">)</a> <a id="1334" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1338" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a> <a id="1340" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1342" class="Symbol">(</a><a id="1343" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a> <a id="1345" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1347" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a><a id="1348" class="Symbol">)</a> <a id="1353" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1356" href="Algebra.Properties.CommutativeSemigroup.html#1014" class="Function">x∙yz≈y∙xz</a> <a id="1366" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a> <a id="1368" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a> <a id="1370" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a> <a id="1372" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1376" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a> <a id="1378" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1380" class="Symbol">(</a><a id="1381" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a> <a id="1383" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1385" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a><a id="1386" class="Symbol">)</a> <a id="1391" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1394" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="1402" class="Symbol">(</a><a id="1403" href="Algebra.Structures.html#2188" class="Function">comm</a> <a id="1408" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a> <a id="1410" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a><a id="1411" class="Symbol">)</a> <a id="1413" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1417" href="Algebra.Properties.CommutativeSemigroup.html#1285" class="Bound">z</a> <a id="1419" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1421" class="Symbol">(</a><a id="1422" href="Algebra.Properties.CommutativeSemigroup.html#1283" class="Bound">y</a> <a id="1424" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1426" href="Algebra.Properties.CommutativeSemigroup.html#1281" class="Bound">x</a><a id="1427" class="Symbol">)</a> <a id="1432" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">∎</a>
<a id="x∙yz≈x∙zy"></a><a id="1435" href="Algebra.Properties.CommutativeSemigroup.html#1435" class="Function">x∙yz≈x∙zy</a> <a id="1445" class="Symbol">:</a> <a id="1448" class="Symbol">∀</a> <a id="1450" href="Algebra.Properties.CommutativeSemigroup.html#1450" class="Bound">x</a> <a id="1452" href="Algebra.Properties.CommutativeSemigroup.html#1452" class="Bound">y</a> <a id="1454" href="Algebra.Properties.CommutativeSemigroup.html#1454" class="Bound">z</a> <a id="1456" class="Symbol">→</a> <a id="1458" href="Algebra.Properties.CommutativeSemigroup.html#1450" class="Bound">x</a> <a id="1460" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1462" class="Symbol">(</a><a id="1463" href="Algebra.Properties.CommutativeSemigroup.html#1452" class="Bound">y</a> <a id="1465" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1467" href="Algebra.Properties.CommutativeSemigroup.html#1454" class="Bound">z</a><a id="1468" class="Symbol">)</a> <a id="1470" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="1472" href="Algebra.Properties.CommutativeSemigroup.html#1450" class="Bound">x</a> <a id="1474" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1476" class="Symbol">(</a><a id="1477" href="Algebra.Properties.CommutativeSemigroup.html#1454" class="Bound">z</a> <a id="1479" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1481" href="Algebra.Properties.CommutativeSemigroup.html#1452" class="Bound">y</a><a id="1482" class="Symbol">)</a>
<a id="1484" href="Algebra.Properties.CommutativeSemigroup.html#1435" class="Function">x∙yz≈x∙zy</a> <a id="1494" class="Symbol">_</a> <a id="1496" href="Algebra.Properties.CommutativeSemigroup.html#1496" class="Bound">y</a> <a id="1498" href="Algebra.Properties.CommutativeSemigroup.html#1498" class="Bound">z</a> <a id="1500" class="Symbol">=</a> <a id="1503" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="1511" class="Symbol">(</a><a id="1512" href="Algebra.Structures.html#2188" class="Function">comm</a> <a id="1517" href="Algebra.Properties.CommutativeSemigroup.html#1496" class="Bound">y</a> <a id="1519" href="Algebra.Properties.CommutativeSemigroup.html#1498" class="Bound">z</a><a id="1520" class="Symbol">)</a>
<a id="x∙yz≈y∙zx"></a><a id="1523" href="Algebra.Properties.CommutativeSemigroup.html#1523" class="Function">x∙yz≈y∙zx</a> <a id="1533" class="Symbol">:</a> <a id="1536" class="Symbol">∀</a> <a id="1538" href="Algebra.Properties.CommutativeSemigroup.html#1538" class="Bound">x</a> <a id="1540" href="Algebra.Properties.CommutativeSemigroup.html#1540" class="Bound">y</a> <a id="1542" href="Algebra.Properties.CommutativeSemigroup.html#1542" class="Bound">z</a> <a id="1544" class="Symbol">→</a> <a id="1546" href="Algebra.Properties.CommutativeSemigroup.html#1538" class="Bound">x</a> <a id="1548" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1550" class="Symbol">(</a><a id="1551" href="Algebra.Properties.CommutativeSemigroup.html#1540" class="Bound">y</a> <a id="1553" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1555" href="Algebra.Properties.CommutativeSemigroup.html#1542" class="Bound">z</a><a id="1556" class="Symbol">)</a> <a id="1558" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="1560" href="Algebra.Properties.CommutativeSemigroup.html#1540" class="Bound">y</a> <a id="1562" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1564" class="Symbol">(</a><a id="1565" href="Algebra.Properties.CommutativeSemigroup.html#1542" class="Bound">z</a> <a id="1567" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1569" href="Algebra.Properties.CommutativeSemigroup.html#1538" class="Bound">x</a><a id="1570" class="Symbol">)</a>
<a id="1572" href="Algebra.Properties.CommutativeSemigroup.html#1523" class="Function">x∙yz≈y∙zx</a> <a id="1582" href="Algebra.Properties.CommutativeSemigroup.html#1582" class="Bound">x</a> <a id="1584" href="Algebra.Properties.CommutativeSemigroup.html#1584" class="Bound">y</a> <a id="1586" href="Algebra.Properties.CommutativeSemigroup.html#1586" class="Bound">z</a> <a id="1588" class="Symbol">=</a> <a id="1590" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin</a>
<a id="1598" href="Algebra.Properties.CommutativeSemigroup.html#1582" class="Bound">x</a> <a id="1600" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1602" class="Symbol">(</a><a id="1603" href="Algebra.Properties.CommutativeSemigroup.html#1584" class="Bound">y</a> <a id="1605" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1607" href="Algebra.Properties.CommutativeSemigroup.html#1586" class="Bound">z</a><a id="1608" class="Symbol">)</a> <a id="1612" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1615" href="Algebra.Structures.html#2188" class="Function">comm</a> <a id="1620" href="Algebra.Properties.CommutativeSemigroup.html#1582" class="Bound">x</a> <a id="1622" class="Symbol">_</a> <a id="1624" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1628" class="Symbol">(</a><a id="1629" href="Algebra.Properties.CommutativeSemigroup.html#1584" class="Bound">y</a> <a id="1631" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1633" href="Algebra.Properties.CommutativeSemigroup.html#1586" class="Bound">z</a><a id="1634" class="Symbol">)</a> <a id="1636" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1638" href="Algebra.Properties.CommutativeSemigroup.html#1582" class="Bound">x</a> <a id="1642" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1645" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="1651" href="Algebra.Properties.CommutativeSemigroup.html#1584" class="Bound">y</a> <a id="1653" href="Algebra.Properties.CommutativeSemigroup.html#1586" class="Bound">z</a> <a id="1655" href="Algebra.Properties.CommutativeSemigroup.html#1582" class="Bound">x</a> <a id="1657" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1661" href="Algebra.Properties.CommutativeSemigroup.html#1584" class="Bound">y</a> <a id="1663" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1665" class="Symbol">(</a><a id="1666" href="Algebra.Properties.CommutativeSemigroup.html#1586" class="Bound">z</a> <a id="1668" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1670" href="Algebra.Properties.CommutativeSemigroup.html#1582" class="Bound">x</a><a id="1671" class="Symbol">)</a> <a id="1675" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">∎</a>
<a id="x∙yz≈z∙xy"></a><a id="1678" href="Algebra.Properties.CommutativeSemigroup.html#1678" class="Function">x∙yz≈z∙xy</a> <a id="1688" class="Symbol">:</a> <a id="1691" class="Symbol">∀</a> <a id="1693" href="Algebra.Properties.CommutativeSemigroup.html#1693" class="Bound">x</a> <a id="1695" href="Algebra.Properties.CommutativeSemigroup.html#1695" class="Bound">y</a> <a id="1697" href="Algebra.Properties.CommutativeSemigroup.html#1697" class="Bound">z</a> <a id="1699" class="Symbol">→</a> <a id="1701" href="Algebra.Properties.CommutativeSemigroup.html#1693" class="Bound">x</a> <a id="1703" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1705" class="Symbol">(</a><a id="1706" href="Algebra.Properties.CommutativeSemigroup.html#1695" class="Bound">y</a> <a id="1708" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1710" href="Algebra.Properties.CommutativeSemigroup.html#1697" class="Bound">z</a><a id="1711" class="Symbol">)</a> <a id="1713" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="1715" href="Algebra.Properties.CommutativeSemigroup.html#1697" class="Bound">z</a> <a id="1717" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1719" class="Symbol">(</a><a id="1720" href="Algebra.Properties.CommutativeSemigroup.html#1693" class="Bound">x</a> <a id="1722" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1724" href="Algebra.Properties.CommutativeSemigroup.html#1695" class="Bound">y</a><a id="1725" class="Symbol">)</a>
<a id="1727" href="Algebra.Properties.CommutativeSemigroup.html#1678" class="Function">x∙yz≈z∙xy</a> <a id="1737" href="Algebra.Properties.CommutativeSemigroup.html#1737" class="Bound">x</a> <a id="1739" href="Algebra.Properties.CommutativeSemigroup.html#1739" class="Bound">y</a> <a id="1741" href="Algebra.Properties.CommutativeSemigroup.html#1741" class="Bound">z</a> <a id="1743" class="Symbol">=</a> <a id="1745" href="Relation.Binary.Reasoning.Base.Single.html#1916" class="Function Operator">begin</a>
<a id="1753" href="Algebra.Properties.CommutativeSemigroup.html#1737" class="Bound">x</a> <a id="1755" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1757" class="Symbol">(</a><a id="1758" href="Algebra.Properties.CommutativeSemigroup.html#1739" class="Bound">y</a> <a id="1760" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1762" href="Algebra.Properties.CommutativeSemigroup.html#1741" class="Bound">z</a><a id="1763" class="Symbol">)</a> <a id="1767" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1770" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="1774" class="Symbol">(</a><a id="1775" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="1781" href="Algebra.Properties.CommutativeSemigroup.html#1737" class="Bound">x</a> <a id="1783" href="Algebra.Properties.CommutativeSemigroup.html#1739" class="Bound">y</a> <a id="1785" href="Algebra.Properties.CommutativeSemigroup.html#1741" class="Bound">z</a><a id="1786" class="Symbol">)</a> <a id="1788" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1792" class="Symbol">(</a><a id="1793" href="Algebra.Properties.CommutativeSemigroup.html#1737" class="Bound">x</a> <a id="1795" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1797" href="Algebra.Properties.CommutativeSemigroup.html#1739" class="Bound">y</a><a id="1798" class="Symbol">)</a> <a id="1800" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1802" href="Algebra.Properties.CommutativeSemigroup.html#1741" class="Bound">z</a> <a id="1806" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">≈⟨</a> <a id="1809" href="Algebra.Structures.html#2188" class="Function">comm</a> <a id="1814" class="Symbol">_</a> <a id="1816" href="Algebra.Properties.CommutativeSemigroup.html#1741" class="Bound">z</a> <a id="1818" href="Relation.Binary.Reasoning.Setoid.html#1052" class="Function">⟩</a>
<a id="1822" href="Algebra.Properties.CommutativeSemigroup.html#1741" class="Bound">z</a> <a id="1824" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1826" class="Symbol">(</a><a id="1827" href="Algebra.Properties.CommutativeSemigroup.html#1737" class="Bound">x</a> <a id="1829" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="1831" href="Algebra.Properties.CommutativeSemigroup.html#1739" class="Bound">y</a><a id="1832" class="Symbol">)</a> <a id="1836" href="Relation.Binary.Reasoning.Base.Single.html#2555" class="Function Operator">∎</a>
<a id="1839" class="Comment">------------------------------------------------------------------------------</a>
<a id="1918" class="Comment">-- Partitions (1,2).</a>
<a id="1939" class="Comment">-- These permutation laws are proved by composing the proofs for</a>
<a id="2004" class="Comment">-- partitions (1,1) with \p → trans p (sym (assoc _ _ _)).</a>
<a id="2064" class="Comment">------------------------------------------------------------------------------</a>
<a id="x∙yz≈yx∙z"></a><a id="2144" href="Algebra.Properties.CommutativeSemigroup.html#2144" class="Function">x∙yz≈yx∙z</a> <a id="2154" class="Symbol">:</a> <a id="2157" class="Symbol">∀</a> <a id="2159" href="Algebra.Properties.CommutativeSemigroup.html#2159" class="Bound">x</a> <a id="2161" href="Algebra.Properties.CommutativeSemigroup.html#2161" class="Bound">y</a> <a id="2163" href="Algebra.Properties.CommutativeSemigroup.html#2163" class="Bound">z</a> <a id="2165" class="Symbol">→</a> <a id="2167" href="Algebra.Properties.CommutativeSemigroup.html#2159" class="Bound">x</a> <a id="2169" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2171" class="Symbol">(</a><a id="2172" href="Algebra.Properties.CommutativeSemigroup.html#2161" class="Bound">y</a> <a id="2174" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2176" href="Algebra.Properties.CommutativeSemigroup.html#2163" class="Bound">z</a><a id="2177" class="Symbol">)</a> <a id="2179" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="2181" class="Symbol">(</a><a id="2182" href="Algebra.Properties.CommutativeSemigroup.html#2161" class="Bound">y</a> <a id="2184" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2186" href="Algebra.Properties.CommutativeSemigroup.html#2159" class="Bound">x</a><a id="2187" class="Symbol">)</a> <a id="2189" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2191" href="Algebra.Properties.CommutativeSemigroup.html#2163" class="Bound">z</a>
<a id="2193" href="Algebra.Properties.CommutativeSemigroup.html#2144" class="Function">x∙yz≈yx∙z</a> <a id="2203" href="Algebra.Properties.CommutativeSemigroup.html#2203" class="Bound">x</a> <a id="2205" href="Algebra.Properties.CommutativeSemigroup.html#2205" class="Bound">y</a> <a id="2207" href="Algebra.Properties.CommutativeSemigroup.html#2207" class="Bound">z</a> <a id="2209" class="Symbol">=</a> <a id="2212" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="2218" class="Symbol">(</a><a id="2219" href="Algebra.Properties.CommutativeSemigroup.html#1014" class="Function">x∙yz≈y∙xz</a> <a id="2229" href="Algebra.Properties.CommutativeSemigroup.html#2203" class="Bound">x</a> <a id="2231" href="Algebra.Properties.CommutativeSemigroup.html#2205" class="Bound">y</a> <a id="2233" href="Algebra.Properties.CommutativeSemigroup.html#2207" class="Bound">z</a><a id="2234" class="Symbol">)</a> <a id="2236" class="Symbol">(</a><a id="2237" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="2241" class="Symbol">(</a><a id="2242" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="2248" href="Algebra.Properties.CommutativeSemigroup.html#2205" class="Bound">y</a> <a id="2250" href="Algebra.Properties.CommutativeSemigroup.html#2203" class="Bound">x</a> <a id="2252" href="Algebra.Properties.CommutativeSemigroup.html#2207" class="Bound">z</a><a id="2253" class="Symbol">))</a>
<a id="x∙yz≈zy∙x"></a><a id="2257" href="Algebra.Properties.CommutativeSemigroup.html#2257" class="Function">x∙yz≈zy∙x</a> <a id="2267" class="Symbol">:</a> <a id="2270" class="Symbol">∀</a> <a id="2272" href="Algebra.Properties.CommutativeSemigroup.html#2272" class="Bound">x</a> <a id="2274" href="Algebra.Properties.CommutativeSemigroup.html#2274" class="Bound">y</a> <a id="2276" href="Algebra.Properties.CommutativeSemigroup.html#2276" class="Bound">z</a> <a id="2278" class="Symbol">→</a> <a id="2280" href="Algebra.Properties.CommutativeSemigroup.html#2272" class="Bound">x</a> <a id="2282" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2284" class="Symbol">(</a><a id="2285" href="Algebra.Properties.CommutativeSemigroup.html#2274" class="Bound">y</a> <a id="2287" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2289" href="Algebra.Properties.CommutativeSemigroup.html#2276" class="Bound">z</a><a id="2290" class="Symbol">)</a> <a id="2292" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="2294" class="Symbol">(</a><a id="2295" href="Algebra.Properties.CommutativeSemigroup.html#2276" class="Bound">z</a> <a id="2297" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2299" href="Algebra.Properties.CommutativeSemigroup.html#2274" class="Bound">y</a><a id="2300" class="Symbol">)</a> <a id="2302" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2304" href="Algebra.Properties.CommutativeSemigroup.html#2272" class="Bound">x</a>
<a id="2306" href="Algebra.Properties.CommutativeSemigroup.html#2257" class="Function">x∙yz≈zy∙x</a> <a id="2316" href="Algebra.Properties.CommutativeSemigroup.html#2316" class="Bound">x</a> <a id="2318" href="Algebra.Properties.CommutativeSemigroup.html#2318" class="Bound">y</a> <a id="2320" href="Algebra.Properties.CommutativeSemigroup.html#2320" class="Bound">z</a> <a id="2322" class="Symbol">=</a> <a id="2325" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="2331" class="Symbol">(</a><a id="2332" href="Algebra.Properties.CommutativeSemigroup.html#1222" class="Function">x∙yz≈z∙yx</a> <a id="2342" href="Algebra.Properties.CommutativeSemigroup.html#2316" class="Bound">x</a> <a id="2344" href="Algebra.Properties.CommutativeSemigroup.html#2318" class="Bound">y</a> <a id="2346" href="Algebra.Properties.CommutativeSemigroup.html#2320" class="Bound">z</a><a id="2347" class="Symbol">)</a> <a id="2349" class="Symbol">(</a><a id="2350" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="2354" class="Symbol">(</a><a id="2355" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="2361" href="Algebra.Properties.CommutativeSemigroup.html#2320" class="Bound">z</a> <a id="2363" href="Algebra.Properties.CommutativeSemigroup.html#2318" class="Bound">y</a> <a id="2365" href="Algebra.Properties.CommutativeSemigroup.html#2316" class="Bound">x</a><a id="2366" class="Symbol">))</a>
<a id="x∙yz≈xz∙y"></a><a id="2370" href="Algebra.Properties.CommutativeSemigroup.html#2370" class="Function">x∙yz≈xz∙y</a> <a id="2380" class="Symbol">:</a> <a id="2383" class="Symbol">∀</a> <a id="2385" href="Algebra.Properties.CommutativeSemigroup.html#2385" class="Bound">x</a> <a id="2387" href="Algebra.Properties.CommutativeSemigroup.html#2387" class="Bound">y</a> <a id="2389" href="Algebra.Properties.CommutativeSemigroup.html#2389" class="Bound">z</a> <a id="2391" class="Symbol">→</a> <a id="2393" href="Algebra.Properties.CommutativeSemigroup.html#2385" class="Bound">x</a> <a id="2395" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2397" class="Symbol">(</a><a id="2398" href="Algebra.Properties.CommutativeSemigroup.html#2387" class="Bound">y</a> <a id="2400" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2402" href="Algebra.Properties.CommutativeSemigroup.html#2389" class="Bound">z</a><a id="2403" class="Symbol">)</a> <a id="2405" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="2407" class="Symbol">(</a><a id="2408" href="Algebra.Properties.CommutativeSemigroup.html#2385" class="Bound">x</a> <a id="2410" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2412" href="Algebra.Properties.CommutativeSemigroup.html#2389" class="Bound">z</a><a id="2413" class="Symbol">)</a> <a id="2415" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2417" href="Algebra.Properties.CommutativeSemigroup.html#2387" class="Bound">y</a>
<a id="2419" href="Algebra.Properties.CommutativeSemigroup.html#2370" class="Function">x∙yz≈xz∙y</a> <a id="2429" href="Algebra.Properties.CommutativeSemigroup.html#2429" class="Bound">x</a> <a id="2431" href="Algebra.Properties.CommutativeSemigroup.html#2431" class="Bound">y</a> <a id="2433" href="Algebra.Properties.CommutativeSemigroup.html#2433" class="Bound">z</a> <a id="2435" class="Symbol">=</a> <a id="2438" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="2444" class="Symbol">(</a><a id="2445" href="Algebra.Properties.CommutativeSemigroup.html#1435" class="Function">x∙yz≈x∙zy</a> <a id="2455" href="Algebra.Properties.CommutativeSemigroup.html#2429" class="Bound">x</a> <a id="2457" href="Algebra.Properties.CommutativeSemigroup.html#2431" class="Bound">y</a> <a id="2459" href="Algebra.Properties.CommutativeSemigroup.html#2433" class="Bound">z</a><a id="2460" class="Symbol">)</a> <a id="2462" class="Symbol">(</a><a id="2463" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="2467" class="Symbol">(</a><a id="2468" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="2474" href="Algebra.Properties.CommutativeSemigroup.html#2429" class="Bound">x</a> <a id="2476" href="Algebra.Properties.CommutativeSemigroup.html#2433" class="Bound">z</a> <a id="2478" href="Algebra.Properties.CommutativeSemigroup.html#2431" class="Bound">y</a><a id="2479" class="Symbol">))</a>
<a id="x∙yz≈yz∙x"></a><a id="2483" href="Algebra.Properties.CommutativeSemigroup.html#2483" class="Function">x∙yz≈yz∙x</a> <a id="2493" class="Symbol">:</a> <a id="2496" class="Symbol">∀</a> <a id="2498" href="Algebra.Properties.CommutativeSemigroup.html#2498" class="Bound">x</a> <a id="2500" href="Algebra.Properties.CommutativeSemigroup.html#2500" class="Bound">y</a> <a id="2502" href="Algebra.Properties.CommutativeSemigroup.html#2502" class="Bound">z</a> <a id="2504" class="Symbol">→</a> <a id="2506" href="Algebra.Properties.CommutativeSemigroup.html#2498" class="Bound">x</a> <a id="2508" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2510" class="Symbol">(</a><a id="2511" href="Algebra.Properties.CommutativeSemigroup.html#2500" class="Bound">y</a> <a id="2513" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2515" href="Algebra.Properties.CommutativeSemigroup.html#2502" class="Bound">z</a><a id="2516" class="Symbol">)</a> <a id="2518" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="2520" class="Symbol">(</a><a id="2521" href="Algebra.Properties.CommutativeSemigroup.html#2500" class="Bound">y</a> <a id="2523" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2525" href="Algebra.Properties.CommutativeSemigroup.html#2502" class="Bound">z</a><a id="2526" class="Symbol">)</a> <a id="2528" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2530" href="Algebra.Properties.CommutativeSemigroup.html#2498" class="Bound">x</a>
<a id="2532" href="Algebra.Properties.CommutativeSemigroup.html#2483" class="Function">x∙yz≈yz∙x</a> <a id="2542" href="Algebra.Properties.CommutativeSemigroup.html#2542" class="Bound">x</a> <a id="2544" href="Algebra.Properties.CommutativeSemigroup.html#2544" class="Bound">y</a> <a id="2546" href="Algebra.Properties.CommutativeSemigroup.html#2546" class="Bound">z</a> <a id="2548" class="Symbol">=</a> <a id="2551" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="2557" class="Symbol">(</a><a id="2558" href="Algebra.Properties.CommutativeSemigroup.html#1523" class="Function">x∙yz≈y∙zx</a> <a id="2568" class="Symbol">_</a> <a id="2570" class="Symbol">_</a> <a id="2572" class="Symbol">_)</a> <a id="2575" class="Symbol">(</a><a id="2576" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="2580" class="Symbol">(</a><a id="2581" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="2587" href="Algebra.Properties.CommutativeSemigroup.html#2544" class="Bound">y</a> <a id="2589" href="Algebra.Properties.CommutativeSemigroup.html#2546" class="Bound">z</a> <a id="2591" href="Algebra.Properties.CommutativeSemigroup.html#2542" class="Bound">x</a><a id="2592" class="Symbol">))</a>
<a id="x∙yz≈zx∙y"></a><a id="2596" href="Algebra.Properties.CommutativeSemigroup.html#2596" class="Function">x∙yz≈zx∙y</a> <a id="2606" class="Symbol">:</a> <a id="2609" class="Symbol">∀</a> <a id="2611" href="Algebra.Properties.CommutativeSemigroup.html#2611" class="Bound">x</a> <a id="2613" href="Algebra.Properties.CommutativeSemigroup.html#2613" class="Bound">y</a> <a id="2615" href="Algebra.Properties.CommutativeSemigroup.html#2615" class="Bound">z</a> <a id="2617" class="Symbol">→</a> <a id="2619" href="Algebra.Properties.CommutativeSemigroup.html#2611" class="Bound">x</a> <a id="2621" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2623" class="Symbol">(</a><a id="2624" href="Algebra.Properties.CommutativeSemigroup.html#2613" class="Bound">y</a> <a id="2626" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2628" href="Algebra.Properties.CommutativeSemigroup.html#2615" class="Bound">z</a><a id="2629" class="Symbol">)</a> <a id="2631" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="2633" class="Symbol">(</a><a id="2634" href="Algebra.Properties.CommutativeSemigroup.html#2615" class="Bound">z</a> <a id="2636" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2638" href="Algebra.Properties.CommutativeSemigroup.html#2611" class="Bound">x</a><a id="2639" class="Symbol">)</a> <a id="2641" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="2643" href="Algebra.Properties.CommutativeSemigroup.html#2613" class="Bound">y</a>
<a id="2645" href="Algebra.Properties.CommutativeSemigroup.html#2596" class="Function">x∙yz≈zx∙y</a> <a id="2655" href="Algebra.Properties.CommutativeSemigroup.html#2655" class="Bound">x</a> <a id="2657" href="Algebra.Properties.CommutativeSemigroup.html#2657" class="Bound">y</a> <a id="2659" href="Algebra.Properties.CommutativeSemigroup.html#2659" class="Bound">z</a> <a id="2661" class="Symbol">=</a> <a id="2664" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="2670" class="Symbol">(</a><a id="2671" href="Algebra.Properties.CommutativeSemigroup.html#1678" class="Function">x∙yz≈z∙xy</a> <a id="2681" href="Algebra.Properties.CommutativeSemigroup.html#2655" class="Bound">x</a> <a id="2683" href="Algebra.Properties.CommutativeSemigroup.html#2657" class="Bound">y</a> <a id="2685" href="Algebra.Properties.CommutativeSemigroup.html#2659" class="Bound">z</a><a id="2686" class="Symbol">)</a> <a id="2688" class="Symbol">(</a><a id="2689" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="2693" class="Symbol">(</a><a id="2694" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="2700" href="Algebra.Properties.CommutativeSemigroup.html#2659" class="Bound">z</a> <a id="2702" href="Algebra.Properties.CommutativeSemigroup.html#2655" class="Bound">x</a> <a id="2704" href="Algebra.Properties.CommutativeSemigroup.html#2657" class="Bound">y</a><a id="2705" class="Symbol">))</a>
<a id="2710" class="Comment">------------------------------------------------------------------------------</a>
<a id="2789" class="Comment">-- Partitions (2,1).</a>
<a id="2810" class="Comment">-- Their laws are proved by composing proofs for partitions (1,1) with</a>
<a id="2881" class="Comment">-- trans (assoc x y z).</a>
<a id="2905" class="Comment">------------------------------------------------------------------------------</a>
<a id="xy∙z≈y∙xz"></a><a id="2985" href="Algebra.Properties.CommutativeSemigroup.html#2985" class="Function">xy∙z≈y∙xz</a> <a id="2995" class="Symbol">:</a> <a id="2998" class="Symbol">∀</a> <a id="3000" href="Algebra.Properties.CommutativeSemigroup.html#3000" class="Bound">x</a> <a id="3002" href="Algebra.Properties.CommutativeSemigroup.html#3002" class="Bound">y</a> <a id="3004" href="Algebra.Properties.CommutativeSemigroup.html#3004" class="Bound">z</a> <a id="3006" class="Symbol">→</a> <a id="3008" class="Symbol">(</a><a id="3009" href="Algebra.Properties.CommutativeSemigroup.html#3000" class="Bound">x</a> <a id="3011" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3013" href="Algebra.Properties.CommutativeSemigroup.html#3002" class="Bound">y</a><a id="3014" class="Symbol">)</a> <a id="3016" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3018" href="Algebra.Properties.CommutativeSemigroup.html#3004" class="Bound">z</a> <a id="3020" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3022" href="Algebra.Properties.CommutativeSemigroup.html#3002" class="Bound">y</a> <a id="3024" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3026" class="Symbol">(</a><a id="3027" href="Algebra.Properties.CommutativeSemigroup.html#3000" class="Bound">x</a> <a id="3029" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3031" href="Algebra.Properties.CommutativeSemigroup.html#3004" class="Bound">z</a><a id="3032" class="Symbol">)</a>
<a id="3034" href="Algebra.Properties.CommutativeSemigroup.html#2985" class="Function">xy∙z≈y∙xz</a> <a id="3044" href="Algebra.Properties.CommutativeSemigroup.html#3044" class="Bound">x</a> <a id="3046" href="Algebra.Properties.CommutativeSemigroup.html#3046" class="Bound">y</a> <a id="3048" href="Algebra.Properties.CommutativeSemigroup.html#3048" class="Bound">z</a> <a id="3050" class="Symbol">=</a> <a id="3053" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3059" class="Symbol">(</a><a id="3060" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3066" href="Algebra.Properties.CommutativeSemigroup.html#3044" class="Bound">x</a> <a id="3068" href="Algebra.Properties.CommutativeSemigroup.html#3046" class="Bound">y</a> <a id="3070" href="Algebra.Properties.CommutativeSemigroup.html#3048" class="Bound">z</a><a id="3071" class="Symbol">)</a> <a id="3073" class="Symbol">(</a><a id="3074" href="Algebra.Properties.CommutativeSemigroup.html#1014" class="Function">x∙yz≈y∙xz</a> <a id="3084" href="Algebra.Properties.CommutativeSemigroup.html#3044" class="Bound">x</a> <a id="3086" href="Algebra.Properties.CommutativeSemigroup.html#3046" class="Bound">y</a> <a id="3088" href="Algebra.Properties.CommutativeSemigroup.html#3048" class="Bound">z</a><a id="3089" class="Symbol">)</a>
<a id="xy∙z≈z∙yx"></a><a id="3092" href="Algebra.Properties.CommutativeSemigroup.html#3092" class="Function">xy∙z≈z∙yx</a> <a id="3102" class="Symbol">:</a> <a id="3105" class="Symbol">∀</a> <a id="3107" href="Algebra.Properties.CommutativeSemigroup.html#3107" class="Bound">x</a> <a id="3109" href="Algebra.Properties.CommutativeSemigroup.html#3109" class="Bound">y</a> <a id="3111" href="Algebra.Properties.CommutativeSemigroup.html#3111" class="Bound">z</a> <a id="3113" class="Symbol">→</a> <a id="3115" class="Symbol">(</a><a id="3116" href="Algebra.Properties.CommutativeSemigroup.html#3107" class="Bound">x</a> <a id="3118" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3120" href="Algebra.Properties.CommutativeSemigroup.html#3109" class="Bound">y</a><a id="3121" class="Symbol">)</a> <a id="3123" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3125" href="Algebra.Properties.CommutativeSemigroup.html#3111" class="Bound">z</a> <a id="3127" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3129" href="Algebra.Properties.CommutativeSemigroup.html#3111" class="Bound">z</a> <a id="3131" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3133" class="Symbol">(</a><a id="3134" href="Algebra.Properties.CommutativeSemigroup.html#3109" class="Bound">y</a> <a id="3136" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3138" href="Algebra.Properties.CommutativeSemigroup.html#3107" class="Bound">x</a><a id="3139" class="Symbol">)</a>
<a id="3141" href="Algebra.Properties.CommutativeSemigroup.html#3092" class="Function">xy∙z≈z∙yx</a> <a id="3151" href="Algebra.Properties.CommutativeSemigroup.html#3151" class="Bound">x</a> <a id="3153" href="Algebra.Properties.CommutativeSemigroup.html#3153" class="Bound">y</a> <a id="3155" href="Algebra.Properties.CommutativeSemigroup.html#3155" class="Bound">z</a> <a id="3157" class="Symbol">=</a> <a id="3160" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3166" class="Symbol">(</a><a id="3167" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3173" href="Algebra.Properties.CommutativeSemigroup.html#3151" class="Bound">x</a> <a id="3175" href="Algebra.Properties.CommutativeSemigroup.html#3153" class="Bound">y</a> <a id="3177" href="Algebra.Properties.CommutativeSemigroup.html#3155" class="Bound">z</a><a id="3178" class="Symbol">)</a> <a id="3180" class="Symbol">(</a><a id="3181" href="Algebra.Properties.CommutativeSemigroup.html#1222" class="Function">x∙yz≈z∙yx</a> <a id="3191" href="Algebra.Properties.CommutativeSemigroup.html#3151" class="Bound">x</a> <a id="3193" href="Algebra.Properties.CommutativeSemigroup.html#3153" class="Bound">y</a> <a id="3195" href="Algebra.Properties.CommutativeSemigroup.html#3155" class="Bound">z</a><a id="3196" class="Symbol">)</a>
<a id="xy∙z≈x∙zy"></a><a id="3199" href="Algebra.Properties.CommutativeSemigroup.html#3199" class="Function">xy∙z≈x∙zy</a> <a id="3209" class="Symbol">:</a> <a id="3212" class="Symbol">∀</a> <a id="3214" href="Algebra.Properties.CommutativeSemigroup.html#3214" class="Bound">x</a> <a id="3216" href="Algebra.Properties.CommutativeSemigroup.html#3216" class="Bound">y</a> <a id="3218" href="Algebra.Properties.CommutativeSemigroup.html#3218" class="Bound">z</a> <a id="3220" class="Symbol">→</a> <a id="3222" class="Symbol">(</a><a id="3223" href="Algebra.Properties.CommutativeSemigroup.html#3214" class="Bound">x</a> <a id="3225" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3227" href="Algebra.Properties.CommutativeSemigroup.html#3216" class="Bound">y</a><a id="3228" class="Symbol">)</a> <a id="3230" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3232" href="Algebra.Properties.CommutativeSemigroup.html#3218" class="Bound">z</a> <a id="3234" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3236" href="Algebra.Properties.CommutativeSemigroup.html#3214" class="Bound">x</a> <a id="3238" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3240" class="Symbol">(</a><a id="3241" href="Algebra.Properties.CommutativeSemigroup.html#3218" class="Bound">z</a> <a id="3243" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3245" href="Algebra.Properties.CommutativeSemigroup.html#3216" class="Bound">y</a><a id="3246" class="Symbol">)</a>
<a id="3248" href="Algebra.Properties.CommutativeSemigroup.html#3199" class="Function">xy∙z≈x∙zy</a> <a id="3258" href="Algebra.Properties.CommutativeSemigroup.html#3258" class="Bound">x</a> <a id="3260" href="Algebra.Properties.CommutativeSemigroup.html#3260" class="Bound">y</a> <a id="3262" href="Algebra.Properties.CommutativeSemigroup.html#3262" class="Bound">z</a> <a id="3264" class="Symbol">=</a> <a id="3267" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3273" class="Symbol">(</a><a id="3274" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3280" href="Algebra.Properties.CommutativeSemigroup.html#3258" class="Bound">x</a> <a id="3282" href="Algebra.Properties.CommutativeSemigroup.html#3260" class="Bound">y</a> <a id="3284" href="Algebra.Properties.CommutativeSemigroup.html#3262" class="Bound">z</a><a id="3285" class="Symbol">)</a> <a id="3287" class="Symbol">(</a><a id="3288" href="Algebra.Properties.CommutativeSemigroup.html#1435" class="Function">x∙yz≈x∙zy</a> <a id="3298" href="Algebra.Properties.CommutativeSemigroup.html#3258" class="Bound">x</a> <a id="3300" href="Algebra.Properties.CommutativeSemigroup.html#3260" class="Bound">y</a> <a id="3302" href="Algebra.Properties.CommutativeSemigroup.html#3262" class="Bound">z</a><a id="3303" class="Symbol">)</a>
<a id="xy∙z≈y∙zx"></a><a id="3306" href="Algebra.Properties.CommutativeSemigroup.html#3306" class="Function">xy∙z≈y∙zx</a> <a id="3316" class="Symbol">:</a> <a id="3319" class="Symbol">∀</a> <a id="3321" href="Algebra.Properties.CommutativeSemigroup.html#3321" class="Bound">x</a> <a id="3323" href="Algebra.Properties.CommutativeSemigroup.html#3323" class="Bound">y</a> <a id="3325" href="Algebra.Properties.CommutativeSemigroup.html#3325" class="Bound">z</a> <a id="3327" class="Symbol">→</a> <a id="3329" class="Symbol">(</a><a id="3330" href="Algebra.Properties.CommutativeSemigroup.html#3321" class="Bound">x</a> <a id="3332" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3334" href="Algebra.Properties.CommutativeSemigroup.html#3323" class="Bound">y</a><a id="3335" class="Symbol">)</a> <a id="3337" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3339" href="Algebra.Properties.CommutativeSemigroup.html#3325" class="Bound">z</a> <a id="3341" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3343" href="Algebra.Properties.CommutativeSemigroup.html#3323" class="Bound">y</a> <a id="3345" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3347" class="Symbol">(</a><a id="3348" href="Algebra.Properties.CommutativeSemigroup.html#3325" class="Bound">z</a> <a id="3350" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3352" href="Algebra.Properties.CommutativeSemigroup.html#3321" class="Bound">x</a><a id="3353" class="Symbol">)</a>
<a id="3355" href="Algebra.Properties.CommutativeSemigroup.html#3306" class="Function">xy∙z≈y∙zx</a> <a id="3365" href="Algebra.Properties.CommutativeSemigroup.html#3365" class="Bound">x</a> <a id="3367" href="Algebra.Properties.CommutativeSemigroup.html#3367" class="Bound">y</a> <a id="3369" href="Algebra.Properties.CommutativeSemigroup.html#3369" class="Bound">z</a> <a id="3371" class="Symbol">=</a> <a id="3374" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3380" class="Symbol">(</a><a id="3381" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3387" href="Algebra.Properties.CommutativeSemigroup.html#3365" class="Bound">x</a> <a id="3389" href="Algebra.Properties.CommutativeSemigroup.html#3367" class="Bound">y</a> <a id="3391" href="Algebra.Properties.CommutativeSemigroup.html#3369" class="Bound">z</a><a id="3392" class="Symbol">)</a> <a id="3394" class="Symbol">(</a><a id="3395" href="Algebra.Properties.CommutativeSemigroup.html#1523" class="Function">x∙yz≈y∙zx</a> <a id="3405" href="Algebra.Properties.CommutativeSemigroup.html#3365" class="Bound">x</a> <a id="3407" href="Algebra.Properties.CommutativeSemigroup.html#3367" class="Bound">y</a> <a id="3409" href="Algebra.Properties.CommutativeSemigroup.html#3369" class="Bound">z</a><a id="3410" class="Symbol">)</a>
<a id="xy∙z≈z∙xy"></a><a id="3413" href="Algebra.Properties.CommutativeSemigroup.html#3413" class="Function">xy∙z≈z∙xy</a> <a id="3423" class="Symbol">:</a> <a id="3426" class="Symbol">∀</a> <a id="3428" href="Algebra.Properties.CommutativeSemigroup.html#3428" class="Bound">x</a> <a id="3430" href="Algebra.Properties.CommutativeSemigroup.html#3430" class="Bound">y</a> <a id="3432" href="Algebra.Properties.CommutativeSemigroup.html#3432" class="Bound">z</a> <a id="3434" class="Symbol">→</a> <a id="3436" class="Symbol">(</a><a id="3437" href="Algebra.Properties.CommutativeSemigroup.html#3428" class="Bound">x</a> <a id="3439" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3441" href="Algebra.Properties.CommutativeSemigroup.html#3430" class="Bound">y</a><a id="3442" class="Symbol">)</a> <a id="3444" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3446" href="Algebra.Properties.CommutativeSemigroup.html#3432" class="Bound">z</a> <a id="3448" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3450" href="Algebra.Properties.CommutativeSemigroup.html#3432" class="Bound">z</a> <a id="3452" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3454" class="Symbol">(</a><a id="3455" href="Algebra.Properties.CommutativeSemigroup.html#3428" class="Bound">x</a> <a id="3457" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3459" href="Algebra.Properties.CommutativeSemigroup.html#3430" class="Bound">y</a><a id="3460" class="Symbol">)</a>
<a id="3462" href="Algebra.Properties.CommutativeSemigroup.html#3413" class="Function">xy∙z≈z∙xy</a> <a id="3472" href="Algebra.Properties.CommutativeSemigroup.html#3472" class="Bound">x</a> <a id="3474" href="Algebra.Properties.CommutativeSemigroup.html#3474" class="Bound">y</a> <a id="3476" href="Algebra.Properties.CommutativeSemigroup.html#3476" class="Bound">z</a> <a id="3478" class="Symbol">=</a> <a id="3481" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3487" class="Symbol">(</a><a id="3488" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3494" href="Algebra.Properties.CommutativeSemigroup.html#3472" class="Bound">x</a> <a id="3496" href="Algebra.Properties.CommutativeSemigroup.html#3474" class="Bound">y</a> <a id="3498" href="Algebra.Properties.CommutativeSemigroup.html#3476" class="Bound">z</a><a id="3499" class="Symbol">)</a> <a id="3501" class="Symbol">(</a><a id="3502" href="Algebra.Properties.CommutativeSemigroup.html#1678" class="Function">x∙yz≈z∙xy</a> <a id="3512" href="Algebra.Properties.CommutativeSemigroup.html#3472" class="Bound">x</a> <a id="3514" href="Algebra.Properties.CommutativeSemigroup.html#3474" class="Bound">y</a> <a id="3516" href="Algebra.Properties.CommutativeSemigroup.html#3476" class="Bound">z</a><a id="3517" class="Symbol">)</a>
<a id="3520" class="Comment">------------------------------------------------------------------------------</a>
<a id="3599" class="Comment">-- Partitions (2,2).</a>
<a id="3620" class="Comment">-- These proofs are by composing with the proofs for (2,1).</a>
<a id="3680" class="Comment">------------------------------------------------------------------------------</a>
<a id="xy∙z≈yx∙z"></a><a id="3760" href="Algebra.Properties.CommutativeSemigroup.html#3760" class="Function">xy∙z≈yx∙z</a> <a id="3770" class="Symbol">:</a> <a id="3773" class="Symbol">∀</a> <a id="3775" href="Algebra.Properties.CommutativeSemigroup.html#3775" class="Bound">x</a> <a id="3777" href="Algebra.Properties.CommutativeSemigroup.html#3777" class="Bound">y</a> <a id="3779" href="Algebra.Properties.CommutativeSemigroup.html#3779" class="Bound">z</a> <a id="3781" class="Symbol">→</a> <a id="3783" class="Symbol">(</a><a id="3784" href="Algebra.Properties.CommutativeSemigroup.html#3775" class="Bound">x</a> <a id="3786" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3788" href="Algebra.Properties.CommutativeSemigroup.html#3777" class="Bound">y</a><a id="3789" class="Symbol">)</a> <a id="3791" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3793" href="Algebra.Properties.CommutativeSemigroup.html#3779" class="Bound">z</a> <a id="3795" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3797" class="Symbol">(</a><a id="3798" href="Algebra.Properties.CommutativeSemigroup.html#3777" class="Bound">y</a> <a id="3800" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3802" href="Algebra.Properties.CommutativeSemigroup.html#3775" class="Bound">x</a><a id="3803" class="Symbol">)</a> <a id="3805" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3807" href="Algebra.Properties.CommutativeSemigroup.html#3779" class="Bound">z</a>
<a id="3809" href="Algebra.Properties.CommutativeSemigroup.html#3760" class="Function">xy∙z≈yx∙z</a> <a id="3819" href="Algebra.Properties.CommutativeSemigroup.html#3819" class="Bound">x</a> <a id="3821" href="Algebra.Properties.CommutativeSemigroup.html#3821" class="Bound">y</a> <a id="3823" href="Algebra.Properties.CommutativeSemigroup.html#3823" class="Bound">z</a> <a id="3825" class="Symbol">=</a> <a id="3828" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3834" class="Symbol">(</a><a id="3835" href="Algebra.Properties.CommutativeSemigroup.html#2985" class="Function">xy∙z≈y∙xz</a> <a id="3845" class="Symbol">_</a> <a id="3847" class="Symbol">_</a> <a id="3849" class="Symbol">_)</a> <a id="3852" class="Symbol">(</a><a id="3853" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="3857" class="Symbol">(</a><a id="3858" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3864" href="Algebra.Properties.CommutativeSemigroup.html#3821" class="Bound">y</a> <a id="3866" href="Algebra.Properties.CommutativeSemigroup.html#3819" class="Bound">x</a> <a id="3868" href="Algebra.Properties.CommutativeSemigroup.html#3823" class="Bound">z</a><a id="3869" class="Symbol">))</a>
<a id="xy∙z≈zy∙x"></a><a id="3873" href="Algebra.Properties.CommutativeSemigroup.html#3873" class="Function">xy∙z≈zy∙x</a> <a id="3883" class="Symbol">:</a> <a id="3886" class="Symbol">∀</a> <a id="3888" href="Algebra.Properties.CommutativeSemigroup.html#3888" class="Bound">x</a> <a id="3890" href="Algebra.Properties.CommutativeSemigroup.html#3890" class="Bound">y</a> <a id="3892" href="Algebra.Properties.CommutativeSemigroup.html#3892" class="Bound">z</a> <a id="3894" class="Symbol">→</a> <a id="3896" class="Symbol">(</a><a id="3897" href="Algebra.Properties.CommutativeSemigroup.html#3888" class="Bound">x</a> <a id="3899" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3901" href="Algebra.Properties.CommutativeSemigroup.html#3890" class="Bound">y</a><a id="3902" class="Symbol">)</a> <a id="3904" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3906" href="Algebra.Properties.CommutativeSemigroup.html#3892" class="Bound">z</a> <a id="3908" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="3910" class="Symbol">(</a><a id="3911" href="Algebra.Properties.CommutativeSemigroup.html#3892" class="Bound">z</a> <a id="3913" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3915" href="Algebra.Properties.CommutativeSemigroup.html#3890" class="Bound">y</a><a id="3916" class="Symbol">)</a> <a id="3918" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="3920" href="Algebra.Properties.CommutativeSemigroup.html#3888" class="Bound">x</a>
<a id="3922" href="Algebra.Properties.CommutativeSemigroup.html#3873" class="Function">xy∙z≈zy∙x</a> <a id="3932" href="Algebra.Properties.CommutativeSemigroup.html#3932" class="Bound">x</a> <a id="3934" href="Algebra.Properties.CommutativeSemigroup.html#3934" class="Bound">y</a> <a id="3936" href="Algebra.Properties.CommutativeSemigroup.html#3936" class="Bound">z</a> <a id="3938" class="Symbol">=</a> <a id="3941" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="3947" class="Symbol">(</a><a id="3948" href="Algebra.Properties.CommutativeSemigroup.html#3092" class="Function">xy∙z≈z∙yx</a> <a id="3958" href="Algebra.Properties.CommutativeSemigroup.html#3932" class="Bound">x</a> <a id="3960" href="Algebra.Properties.CommutativeSemigroup.html#3934" class="Bound">y</a> <a id="3962" href="Algebra.Properties.CommutativeSemigroup.html#3936" class="Bound">z</a><a id="3963" class="Symbol">)</a> <a id="3965" class="Symbol">(</a><a id="3966" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="3970" class="Symbol">(</a><a id="3971" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="3977" href="Algebra.Properties.CommutativeSemigroup.html#3936" class="Bound">z</a> <a id="3979" href="Algebra.Properties.CommutativeSemigroup.html#3934" class="Bound">y</a> <a id="3981" href="Algebra.Properties.CommutativeSemigroup.html#3932" class="Bound">x</a><a id="3982" class="Symbol">))</a>
<a id="xy∙z≈xz∙y"></a><a id="3986" href="Algebra.Properties.CommutativeSemigroup.html#3986" class="Function">xy∙z≈xz∙y</a> <a id="3996" class="Symbol">:</a> <a id="3999" class="Symbol">∀</a> <a id="4001" href="Algebra.Properties.CommutativeSemigroup.html#4001" class="Bound">x</a> <a id="4003" href="Algebra.Properties.CommutativeSemigroup.html#4003" class="Bound">y</a> <a id="4005" href="Algebra.Properties.CommutativeSemigroup.html#4005" class="Bound">z</a> <a id="4007" class="Symbol">→</a> <a id="4009" class="Symbol">(</a><a id="4010" href="Algebra.Properties.CommutativeSemigroup.html#4001" class="Bound">x</a> <a id="4012" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4014" href="Algebra.Properties.CommutativeSemigroup.html#4003" class="Bound">y</a><a id="4015" class="Symbol">)</a> <a id="4017" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4019" href="Algebra.Properties.CommutativeSemigroup.html#4005" class="Bound">z</a> <a id="4021" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="4023" class="Symbol">(</a><a id="4024" href="Algebra.Properties.CommutativeSemigroup.html#4001" class="Bound">x</a> <a id="4026" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4028" href="Algebra.Properties.CommutativeSemigroup.html#4005" class="Bound">z</a><a id="4029" class="Symbol">)</a> <a id="4031" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4033" href="Algebra.Properties.CommutativeSemigroup.html#4003" class="Bound">y</a>
<a id="4035" href="Algebra.Properties.CommutativeSemigroup.html#3986" class="Function">xy∙z≈xz∙y</a> <a id="4045" href="Algebra.Properties.CommutativeSemigroup.html#4045" class="Bound">x</a> <a id="4047" href="Algebra.Properties.CommutativeSemigroup.html#4047" class="Bound">y</a> <a id="4049" href="Algebra.Properties.CommutativeSemigroup.html#4049" class="Bound">z</a> <a id="4051" class="Symbol">=</a> <a id="4054" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="4060" class="Symbol">(</a><a id="4061" href="Algebra.Properties.CommutativeSemigroup.html#3199" class="Function">xy∙z≈x∙zy</a> <a id="4071" href="Algebra.Properties.CommutativeSemigroup.html#4045" class="Bound">x</a> <a id="4073" href="Algebra.Properties.CommutativeSemigroup.html#4047" class="Bound">y</a> <a id="4075" href="Algebra.Properties.CommutativeSemigroup.html#4049" class="Bound">z</a><a id="4076" class="Symbol">)</a> <a id="4078" class="Symbol">(</a><a id="4079" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="4083" class="Symbol">(</a><a id="4084" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="4090" href="Algebra.Properties.CommutativeSemigroup.html#4045" class="Bound">x</a> <a id="4092" href="Algebra.Properties.CommutativeSemigroup.html#4049" class="Bound">z</a> <a id="4094" href="Algebra.Properties.CommutativeSemigroup.html#4047" class="Bound">y</a><a id="4095" class="Symbol">))</a>
<a id="xy∙z≈yz∙x"></a><a id="4099" href="Algebra.Properties.CommutativeSemigroup.html#4099" class="Function">xy∙z≈yz∙x</a> <a id="4109" class="Symbol">:</a> <a id="4112" class="Symbol">∀</a> <a id="4114" href="Algebra.Properties.CommutativeSemigroup.html#4114" class="Bound">x</a> <a id="4116" href="Algebra.Properties.CommutativeSemigroup.html#4116" class="Bound">y</a> <a id="4118" href="Algebra.Properties.CommutativeSemigroup.html#4118" class="Bound">z</a> <a id="4120" class="Symbol">→</a> <a id="4122" class="Symbol">(</a><a id="4123" href="Algebra.Properties.CommutativeSemigroup.html#4114" class="Bound">x</a> <a id="4125" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4127" href="Algebra.Properties.CommutativeSemigroup.html#4116" class="Bound">y</a><a id="4128" class="Symbol">)</a> <a id="4130" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4132" href="Algebra.Properties.CommutativeSemigroup.html#4118" class="Bound">z</a> <a id="4134" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="4136" class="Symbol">(</a><a id="4137" href="Algebra.Properties.CommutativeSemigroup.html#4116" class="Bound">y</a> <a id="4139" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4141" href="Algebra.Properties.CommutativeSemigroup.html#4118" class="Bound">z</a><a id="4142" class="Symbol">)</a> <a id="4144" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4146" href="Algebra.Properties.CommutativeSemigroup.html#4114" class="Bound">x</a>
<a id="4148" href="Algebra.Properties.CommutativeSemigroup.html#4099" class="Function">xy∙z≈yz∙x</a> <a id="4158" href="Algebra.Properties.CommutativeSemigroup.html#4158" class="Bound">x</a> <a id="4160" href="Algebra.Properties.CommutativeSemigroup.html#4160" class="Bound">y</a> <a id="4162" href="Algebra.Properties.CommutativeSemigroup.html#4162" class="Bound">z</a> <a id="4164" class="Symbol">=</a> <a id="4167" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="4173" class="Symbol">(</a><a id="4174" href="Algebra.Properties.CommutativeSemigroup.html#3306" class="Function">xy∙z≈y∙zx</a> <a id="4184" href="Algebra.Properties.CommutativeSemigroup.html#4158" class="Bound">x</a> <a id="4186" href="Algebra.Properties.CommutativeSemigroup.html#4160" class="Bound">y</a> <a id="4188" href="Algebra.Properties.CommutativeSemigroup.html#4162" class="Bound">z</a><a id="4189" class="Symbol">)</a> <a id="4191" class="Symbol">(</a><a id="4192" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="4196" class="Symbol">(</a><a id="4197" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="4203" href="Algebra.Properties.CommutativeSemigroup.html#4160" class="Bound">y</a> <a id="4205" href="Algebra.Properties.CommutativeSemigroup.html#4162" class="Bound">z</a> <a id="4207" href="Algebra.Properties.CommutativeSemigroup.html#4158" class="Bound">x</a><a id="4208" class="Symbol">))</a>
<a id="xy∙z≈zx∙y"></a><a id="4212" href="Algebra.Properties.CommutativeSemigroup.html#4212" class="Function">xy∙z≈zx∙y</a> <a id="4222" class="Symbol">:</a> <a id="4225" class="Symbol">∀</a> <a id="4227" href="Algebra.Properties.CommutativeSemigroup.html#4227" class="Bound">x</a> <a id="4229" href="Algebra.Properties.CommutativeSemigroup.html#4229" class="Bound">y</a> <a id="4231" href="Algebra.Properties.CommutativeSemigroup.html#4231" class="Bound">z</a> <a id="4233" class="Symbol">→</a> <a id="4235" class="Symbol">(</a><a id="4236" href="Algebra.Properties.CommutativeSemigroup.html#4227" class="Bound">x</a> <a id="4238" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4240" href="Algebra.Properties.CommutativeSemigroup.html#4229" class="Bound">y</a><a id="4241" class="Symbol">)</a> <a id="4243" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4245" href="Algebra.Properties.CommutativeSemigroup.html#4231" class="Bound">z</a> <a id="4247" href="Algebra.Bundles.html#2997" class="Field Operator">≈</a> <a id="4249" class="Symbol">(</a><a id="4250" href="Algebra.Properties.CommutativeSemigroup.html#4231" class="Bound">z</a> <a id="4252" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4254" href="Algebra.Properties.CommutativeSemigroup.html#4227" class="Bound">x</a><a id="4255" class="Symbol">)</a> <a id="4257" href="Algebra.Bundles.html#3041" class="Field Operator">∙</a> <a id="4259" href="Algebra.Properties.CommutativeSemigroup.html#4229" class="Bound">y</a>
<a id="4261" href="Algebra.Properties.CommutativeSemigroup.html#4212" class="Function">xy∙z≈zx∙y</a> <a id="4271" href="Algebra.Properties.CommutativeSemigroup.html#4271" class="Bound">x</a> <a id="4273" href="Algebra.Properties.CommutativeSemigroup.html#4273" class="Bound">y</a> <a id="4275" href="Algebra.Properties.CommutativeSemigroup.html#4275" class="Bound">z</a> <a id="4277" class="Symbol">=</a> <a id="4280" href="Relation.Binary.Structures.html#1620" class="Function">trans</a> <a id="4286" class="Symbol">(</a><a id="4287" href="Algebra.Properties.CommutativeSemigroup.html#3413" class="Function">xy∙z≈z∙xy</a> <a id="4297" href="Algebra.Properties.CommutativeSemigroup.html#4271" class="Bound">x</a> <a id="4299" href="Algebra.Properties.CommutativeSemigroup.html#4273" class="Bound">y</a> <a id="4301" href="Algebra.Properties.CommutativeSemigroup.html#4275" class="Bound">z</a><a id="4302" class="Symbol">)</a> <a id="4304" class="Symbol">(</a><a id="4305" href="Relation.Binary.Structures.html#1594" class="Function">sym</a> <a id="4309" class="Symbol">(</a><a id="4310" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="4316" href="Algebra.Properties.CommutativeSemigroup.html#4275" class="Bound">z</a> <a id="4318" href="Algebra.Properties.CommutativeSemigroup.html#4271" class="Bound">x</a> <a id="4320" href="Algebra.Properties.CommutativeSemigroup.html#4273" class="Bound">y</a><a id="4321" class="Symbol">))</a>
</pre></body></html>