Deploying to gh-pages from @ e3e94c8 🚀

Author: github-merge-queue[bot]

master/Algebra.Properties.Semiring.Binomial.html

@@ -27,7 +27,7 @@
   <a id="811" class="Keyword">using</a> <a id="817" class="Symbol">(</a><a id="818" href="Data.Fin.Base.html#1132" class="Datatype">Fin</a><a id="821" class="Symbol">;</a> <a id="823" href="Data.Fin.Base.html#1154" class="InductiveConstructor">zero</a><a id="827" class="Symbol">;</a> <a id="829" href="Data.Fin.Base.html#1175" class="InductiveConstructor">suc</a><a id="832" class="Symbol">;</a> <a id="834" href="Data.Fin.Base.html#1240" class="Function">toℕ</a><a id="837" class="Symbol">;</a> <a id="839" href="Data.Fin.Base.html#1825" class="Function">fromℕ</a><a id="844" class="Symbol">;</a> <a id="846" href="Data.Fin.Base.html#3055" class="Function">inject₁</a><a id="853" class="Symbol">)</a>
 <a id="855" class="Keyword">open</a> <a id="860" class="Keyword">import</a> <a id="867" href="Data.Fin.Patterns.html" class="Module">Data.Fin.Patterns</a> <a id="885" class="Keyword">using</a> <a id="891" class="Symbol">(</a><a id="892" href="Data.Fin.Patterns.html#422" class="InductiveConstructor">0F</a><a id="894" class="Symbol">)</a>
 <a id="896" class="Keyword">open</a> <a id="901" class="Keyword">import</a> <a id="908" href="Data.Fin.Properties.html" class="Module">Data.Fin.Properties</a> <a id="928" class="Symbol">as</a> <a id="931" class="Module">Fin</a>
-  <a id="937" class="Keyword">using</a> <a id="943" class="Symbol">(</a><a id="944" href="Data.Fin.Properties.html#6538" class="Function">toℕ&lt;n</a><a id="949" class="Symbol">;</a> <a id="951" href="Data.Fin.Properties.html#7562" class="Function">toℕ-fromℕ</a><a id="960" class="Symbol">;</a> <a id="962" href="Data.Fin.Properties.html#16121" class="Function">toℕ-inject₁</a><a id="973" class="Symbol">)</a>
+  <a id="937" class="Keyword">using</a> <a id="943" class="Symbol">(</a><a id="944" href="Data.Fin.Properties.html#6556" class="Function">toℕ&lt;n</a><a id="949" class="Symbol">;</a> <a id="951" href="Data.Fin.Properties.html#7580" class="Function">toℕ-fromℕ</a><a id="960" class="Symbol">;</a> <a id="962" href="Data.Fin.Properties.html#16139" class="Function">toℕ-inject₁</a><a id="973" class="Symbol">)</a>
 <a id="975" class="Keyword">open</a> <a id="980" class="Keyword">import</a> <a id="987" href="Data.Fin.Relation.Unary.Top.html" class="Module">Data.Fin.Relation.Unary.Top</a>
   <a id="1017" class="Keyword">using</a> <a id="1023" class="Symbol">(</a><a id="1024" href="Data.Fin.Relation.Unary.Top.html#1434" class="Function">view</a><a id="1028" class="Symbol">;</a> <a id="1030" href="Data.Fin.Relation.Unary.Top.html#1270" class="InductiveConstructor">‵fromℕ</a><a id="1036" class="Symbol">;</a> <a id="1038" href="Data.Fin.Relation.Unary.Top.html#1339" class="InductiveConstructor">‵inject₁</a><a id="1046" class="Symbol">;</a> <a id="1048" href="Data.Fin.Relation.Unary.Top.html#2007" class="Function">view-fromℕ</a><a id="1058" class="Symbol">;</a> <a id="1060" href="Data.Fin.Relation.Unary.Top.html#2145" class="Function">view-inject₁</a><a id="1072" class="Symbol">)</a>
 <a id="1074" class="Keyword">open</a> <a id="1079" class="Keyword">import</a> <a id="1086" href="Function.Base.html" class="Module">Function.Base</a> <a id="1100" class="Keyword">using</a> <a id="1106" class="Symbol">(</a><a id="1107" href="Function.Base.html#1134" class="Function Operator">_∘_</a><a id="1110" class="Symbol">)</a>
@@ -147,10 +147,10 @@
     <a id="5329" href="Algebra.Properties.Semiring.Binomial.html#5329" class="Function">nC[j+1]</a>     <a id="5341" class="Symbol">=</a> <a id="5343" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5345" href="Data.Nat.Combinatorics.Base.html#1622" class="Function Operator">C</a> <a id="5347" href="Algebra.Properties.Semiring.Binomial.html#5191" class="Function">[j+1]</a>
 
     <a id="5358" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a> <a id="5362" class="Symbol">:</a> <a id="5364" href="Algebra.Properties.Semiring.Binomial.html#5141" class="Function">k</a> <a id="5366" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="5368" href="Data.Fin.Base.html#1240" class="Function">toℕ</a> <a id="5372" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a>
-    <a id="5378" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a> <a id="5382" class="Symbol">=</a> <a id="5384" href="Data.Fin.Properties.html#16121" class="Function">toℕ-inject₁</a> <a id="5396" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a>
+    <a id="5378" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a> <a id="5382" class="Symbol">=</a> <a id="5384" href="Data.Fin.Properties.html#16139" class="Function">toℕ-inject₁</a> <a id="5396" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a>
 
     <a id="5403" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5415" class="Symbol">:</a> <a id="5417" href="Algebra.Properties.Semiring.Binomial.html#5221" class="Function">[n-k]</a> <a id="5423" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="5425" href="Algebra.Properties.Semiring.Binomial.html#5297" class="Function">[n-j]</a>
-    <a id="5435" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5447" class="Symbol">=</a> <a id="5449" href="Relation.Binary.PropositionalEquality.Core.html#2080" class="Function">≡.trans</a> <a id="5457" class="Symbol">(</a><a id="5458" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="5463" class="Symbol">(</a><a id="5464" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5466" href="Data.Nat.Base.html#4462" class="Primitive Operator">∸_</a><a id="5468" class="Symbol">)</a> <a id="5470" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a><a id="5473" class="Symbol">)</a> <a id="5475" class="Symbol">(</a><a id="5476" href="Data.Nat.Properties.html#47511" class="Function">∸-suc</a> <a id="5482" class="Symbol">(</a><a id="5483" href="Data.Fin.Properties.html#6538" class="Function">toℕ&lt;n</a> <a id="5489" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a><a id="5490" class="Symbol">))</a>
+    <a id="5435" href="Algebra.Properties.Semiring.Binomial.html#5403" class="Function">[n-k]≡[n-j]</a> <a id="5447" class="Symbol">=</a> <a id="5449" href="Relation.Binary.PropositionalEquality.Core.html#2080" class="Function">≡.trans</a> <a id="5457" class="Symbol">(</a><a id="5458" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="5463" class="Symbol">(</a><a id="5464" href="Algebra.Properties.Semiring.Binomial.html#4566" class="Bound">n</a> <a id="5466" href="Data.Nat.Base.html#4462" class="Primitive Operator">∸_</a><a id="5468" class="Symbol">)</a> <a id="5470" href="Algebra.Properties.Semiring.Binomial.html#5358" class="Function">k≡j</a><a id="5473" class="Symbol">)</a> <a id="5475" class="Symbol">(</a><a id="5476" href="Data.Nat.Properties.html#47511" class="Function">∸-suc</a> <a id="5482" class="Symbol">(</a><a id="5483" href="Data.Fin.Properties.html#6556" class="Function">toℕ&lt;n</a> <a id="5489" href="Algebra.Properties.Semiring.Binomial.html#4569" class="Bound">j</a><a id="5490" class="Symbol">))</a>
 
 <a id="5494" class="Comment">------------------------------------------------------------------------</a>
 <a id="5567" class="Comment">-- Now, a lemma characterising the sum of the term₁ and term₂ expressions</a>
@@ -175,7 +175,7 @@
 <a id="6336" href="Algebra.Properties.Semiring.Binomial.html#5756" class="Function">term₁+term₂≈term</a> <a id="6353" href="Algebra.Properties.Semiring.Binomial.html#6353" class="Bound">x*y≈y*x</a> <a id="6361" href="Algebra.Properties.Semiring.Binomial.html#6361" class="Bound">n</a> <a id="6363" class="Symbol">(</a><a id="6364" href="Data.Fin.Base.html#1175" class="InductiveConstructor">suc</a> <a id="6368" href="Algebra.Properties.Semiring.Binomial.html#6368" class="Bound">i</a><a id="6369" class="Symbol">)</a> <a id="6371" class="Keyword">with</a> <a id="6376" href="Data.Fin.Relation.Unary.Top.html#1434" class="Function">view</a> <a id="6381" href="Algebra.Properties.Semiring.Binomial.html#6368" class="Bound">i</a>
 <a id="6383" class="Symbol">...</a> <a id="6387" class="Symbol">|</a> <a id="6389" href="Data.Fin.Relation.Unary.Top.html#1270" class="InductiveConstructor">‵fromℕ</a> <a id="6396" class="Symbol">{</a><a id="6397" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a><a id="6398" class="Symbol">}</a>
 <a id="6400" class="Comment">{- remembering that i = fromℕ n, definitionally -}</a>
-  <a id="6453" class="Keyword">rewrite</a> <a id="6461" href="Data.Fin.Properties.html#7562" class="Function">toℕ-fromℕ</a> <a id="6471" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
+  <a id="6453" class="Keyword">rewrite</a> <a id="6461" href="Data.Fin.Properties.html#7580" class="Function">toℕ-fromℕ</a> <a id="6471" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6477" class="Symbol">|</a> <a id="6479" href="Data.Nat.Combinatorics.html#2974" class="Function">nCn≡1</a> <a id="6485" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6491" class="Symbol">|</a> <a id="6493" href="Data.Nat.Properties.html#46995" class="Function">n∸n≡0</a> <a id="6499" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
     <a id="6505" class="Symbol">|</a> <a id="6507" href="Algebra.Properties.Semiring.Binomial.html#5652" class="Function">n&lt;ᵇ1+n</a> <a id="6514" href="Algebra.Properties.Semiring.Binomial.html#6397" class="Bound">n</a>
@@ -210,7 +210,7 @@
     <a id="7539" href="Algebra.Properties.Semiring.Binomial.html#7539" class="Function">[x^k+1]*[y^n-k]</a> <a id="7555" class="Symbol">=</a> <a id="7557" href="Algebra.Properties.Semiring.Binomial.html#1629" class="Function">binomial</a> <a id="7566" class="Symbol">(</a><a id="7567" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="7571" class="Bound">n</a><a id="7572" class="Symbol">)</a> <a id="7574" class="Symbol">(</a><a id="7575" href="Data.Fin.Base.html#1175" class="InductiveConstructor">suc</a> <a id="7579" class="Bound">i</a><a id="7580" class="Symbol">)</a>
 
     <a id="7587" href="Algebra.Properties.Semiring.Binomial.html#7587" class="Function">nC[k+1]≡nC[j+1]</a> <a id="7603" class="Symbol">:</a> <a id="7605" href="Algebra.Properties.Semiring.Binomial.html#7475" class="Function">nC[k+1]</a> <a id="7613" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="7615" href="Algebra.Properties.Semiring.Binomial.html#7507" class="Function">nC[j+1]</a>
-    <a id="7627" href="Algebra.Properties.Semiring.Binomial.html#7587" class="Function">nC[k+1]≡nC[j+1]</a> <a id="7643" class="Symbol">=</a> <a id="7645" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="7650" class="Symbol">((</a><a id="7652" class="Bound">n</a> <a id="7654" href="Data.Nat.Combinatorics.Base.html#1622" class="Function Operator">C_</a><a id="7656" class="Symbol">)</a> <a id="7658" href="Function.Base.html#1134" class="Function Operator">∘</a> <a id="7660" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a><a id="7663" class="Symbol">)</a> <a id="7665" class="Symbol">(</a><a id="7666" href="Data.Fin.Properties.html#16121" class="Function">toℕ-inject₁</a> <a id="7678" href="Algebra.Properties.Semiring.Binomial.html#6787" class="Bound">j</a><a id="7679" class="Symbol">)</a>
+    <a id="7627" href="Algebra.Properties.Semiring.Binomial.html#7587" class="Function">nC[k+1]≡nC[j+1]</a> <a id="7643" class="Symbol">=</a> <a id="7645" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="7650" class="Symbol">((</a><a id="7652" class="Bound">n</a> <a id="7654" href="Data.Nat.Combinatorics.Base.html#1622" class="Function Operator">C_</a><a id="7656" class="Symbol">)</a> <a id="7658" href="Function.Base.html#1134" class="Function Operator">∘</a> <a id="7660" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a><a id="7663" class="Symbol">)</a> <a id="7665" class="Symbol">(</a><a id="7666" href="Data.Fin.Properties.html#16139" class="Function">toℕ-inject₁</a> <a id="7678" href="Algebra.Properties.Semiring.Binomial.html#6787" class="Bound">j</a><a id="7679" class="Symbol">)</a>
 
 <a id="7682" class="Comment">------------------------------------------------------------------------</a>
 <a id="7755" class="Comment">-- Finally, the main result</a>

master/Algebra.Solver.Monoid.Normal.html

@@ -55,7 +55,7 @@
 
 <a id="_≟_"></a><a id="1478" href="Algebra.Solver.Monoid.Normal.html#1478" class="Function Operator">_≟_</a> <a id="1482" class="Symbol">:</a> <a id="1484" href="Relation.Binary.Definitions.html#7028" class="Function">DecidableEquality</a> <a id="1502" class="Symbol">(</a><a id="1503" href="Algebra.Solver.Monoid.Normal.html#1228" class="Function">Normal</a> <a id="1510" href="Algebra.Solver.Monoid.Normal.html#929" class="Generalizable">n</a><a id="1511" class="Symbol">)</a>
 <a id="1513" href="Algebra.Solver.Monoid.Normal.html#1513" class="Bound">nf₁</a> <a id="1517" href="Algebra.Solver.Monoid.Normal.html#1478" class="Function Operator">≟</a> <a id="1519" href="Algebra.Solver.Monoid.Normal.html#1519" class="Bound">nf₂</a> <a id="1523" class="Symbol">=</a> <a id="1525" href="Relation.Nullary.Decidable.Core.html#6315" class="Function">Dec.map′</a> <a id="1534" href="Data.List.Relation.Binary.Equality.Propositional.html#1062" class="Function">≋⇒≡</a> <a id="1538" href="Data.List.Relation.Binary.Equality.Propositional.html#1150" class="Function">≡⇒≋</a> <a id="1542" class="Symbol">(</a><a id="1543" href="Algebra.Solver.Monoid.Normal.html#1513" class="Bound">nf₁</a> <a id="1547" href="Data.List.Relation.Binary.Equality.DecSetoid.html#863" class="Function Operator">≋?</a> <a id="1550" href="Algebra.Solver.Monoid.Normal.html#1519" class="Bound">nf₂</a><a id="1553" class="Symbol">)</a>
-  <a id="1557" class="Keyword">where</a> <a id="1563" class="Keyword">open</a> <a id="1568" href="Data.List.Relation.Binary.Equality.DecPropositional.html" class="Module">≋</a> <a id="1570" href="Data.Fin.Properties.html#3895" class="Function Operator">Fin._≟_</a> <a id="1578" class="Keyword">using</a> <a id="1584" class="Symbol">(</a><a id="1585" href="Data.List.Relation.Binary.Equality.DecSetoid.html#863" class="Function Operator">_≋?_</a><a id="1589" class="Symbol">;</a> <a id="1591" href="Data.List.Relation.Binary.Equality.Propositional.html#1062" class="Function">≋⇒≡</a><a id="1594" class="Symbol">;</a> <a id="1596" href="Data.List.Relation.Binary.Equality.Propositional.html#1150" class="Function">≡⇒≋</a><a id="1599" class="Symbol">)</a>
+  <a id="1557" class="Keyword">where</a> <a id="1563" class="Keyword">open</a> <a id="1568" href="Data.List.Relation.Binary.Equality.DecPropositional.html" class="Module">≋</a> <a id="1570" href="Data.Fin.Properties.html#3913" class="Function Operator">Fin._≟_</a> <a id="1578" class="Keyword">using</a> <a id="1584" class="Symbol">(</a><a id="1585" href="Data.List.Relation.Binary.Equality.DecSetoid.html#863" class="Function Operator">_≋?_</a><a id="1589" class="Symbol">;</a> <a id="1591" href="Data.List.Relation.Binary.Equality.Propositional.html#1062" class="Function">≋⇒≡</a><a id="1594" class="Symbol">;</a> <a id="1596" href="Data.List.Relation.Binary.Equality.Propositional.html#1150" class="Function">≡⇒≋</a><a id="1599" class="Symbol">)</a>
 
 <a id="1602" class="Comment">-- A normaliser.</a>