agda-stdlib-doc 0.14-1 / usr / share / doc / agda-stdlib-doc / html / Data.Fin.Dec.html

This file is indexed.

/usr/share/doc/agda-stdlib-doc/html/Data.Fin.Dec.html is in agda-stdlib-doc 0.14-1.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below. 

  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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Data.Fin.Dec</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Decision procedures for finite sets and subsets of finite sets</a>
<a id="172" class="Comment">------------------------------------------------------------------------</a>

<a id="246" class="Keyword">module</a> <a id="253" href="Data.Fin.Dec.html" class="Module">Data.Fin.Dec</a> <a id="266" class="Keyword">where</a>

<a id="273" class="Keyword">open</a> <a id="278" class="Keyword">import</a> <a id="285" href="Function.html" class="Module">Function</a>
<a id="294" class="Keyword">import</a> <a id="301" href="Data.Bool.html" class="Module">Data.Bool</a> <a id="311" class="Symbol">as</a> <a id="314" class="Module">Bool</a>
<a id="319" class="Keyword">open</a> <a id="324" class="Keyword">import</a> <a id="331" href="Data.Nat.Base.html" class="Module">Data.Nat.Base</a> <a id="345" class="Keyword">hiding</a> <a id="352" class="Symbol">(</a><a id="353" href="Data.Nat.Base.html#_%3C_" class="Function Operator">_&lt;_</a><a id="356" class="Symbol">)</a>
<a id="358" class="Keyword">open</a> <a id="363" class="Keyword">import</a> <a id="370" href="Data.Vec.html" class="Module">Data.Vec</a> <a id="379" class="Keyword">hiding</a> <a id="386" class="Symbol">(</a><a id="387" href="Data.Vec.html#_%E2%88%88_" class="Datatype Operator">_∈_</a><a id="390" class="Symbol">)</a>
<a id="392" class="Keyword">open</a> <a id="397" class="Keyword">import</a> <a id="404" href="Data.Vec.Equality.html" class="Module">Data.Vec.Equality</a> <a id="422" class="Symbol">as</a> <a id="425" class="Module">VecEq</a>
  <a id="433" class="Keyword">using</a> <a id="439" class="Symbol">()</a> <a id="442" class="Keyword">renaming</a> <a id="451" class="Symbol">(</a><a id="452" class="Keyword">module</a> <a id="459" href="Data.Vec.Equality.html#PropositionalEquality" class="Module">PropositionalEquality</a> <a id="481" class="Symbol">to</a> <a id="484" href="Data.Vec.Equality.html#PropositionalEquality" class="Module">PropVecEq</a><a id="493" class="Symbol">)</a>
<a id="495" class="Keyword">open</a> <a id="500" class="Keyword">import</a> <a id="507" href="Data.Fin.html" class="Module">Data.Fin</a>
<a id="516" class="Keyword">open</a> <a id="521" class="Keyword">import</a> <a id="528" href="Data.Fin.Subset.html" class="Module">Data.Fin.Subset</a>
<a id="544" class="Keyword">open</a> <a id="549" class="Keyword">import</a> <a id="556" href="Data.Fin.Subset.Properties.html" class="Module">Data.Fin.Subset.Properties</a>
<a id="583" class="Keyword">open</a> <a id="588" class="Keyword">import</a> <a id="595" href="Data.Product.html" class="Module">Data.Product</a> <a id="608" class="Symbol">as</a> <a id="611" class="Module">Prod</a>
<a id="616" class="Keyword">open</a> <a id="621" class="Keyword">import</a> <a id="628" href="Data.Empty.html" class="Module">Data.Empty</a>
<a id="639" class="Keyword">open</a> <a id="644" class="Keyword">import</a> <a id="651" href="Function.html" class="Module">Function</a>
<a id="660" class="Keyword">import</a> <a id="667" href="Function.Equivalence.html" class="Module">Function.Equivalence</a> <a id="688" class="Symbol">as</a> <a id="691" class="Module">Eq</a>
<a id="694" class="Keyword">open</a> <a id="699" class="Keyword">import</a> <a id="706" href="Relation.Binary.html" class="Module">Relation.Binary</a> <a id="722" class="Symbol">as</a> <a id="725" class="Module">B</a>
<a id="727" class="Keyword">import</a> <a id="734" href="Relation.Binary.HeterogeneousEquality.html" class="Module">Relation.Binary.HeterogeneousEquality</a> <a id="772" class="Symbol">as</a> <a id="775" class="Module">H</a>
<a id="777" class="Keyword">open</a> <a id="782" class="Keyword">import</a> <a id="789" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
<a id="806" class="Keyword">import</a> <a id="813" href="Relation.Nullary.Decidable.html" class="Module">Relation.Nullary.Decidable</a> <a id="840" class="Symbol">as</a> <a id="843" class="Module">Dec</a>
<a id="847" class="Keyword">open</a> <a id="852" class="Keyword">import</a> <a id="859" href="Relation.Unary.html" class="Module">Relation.Unary</a> <a id="874" class="Symbol">as</a> <a id="877" class="Module">U</a> <a id="879" class="Keyword">using</a> <a id="885" class="Symbol">(</a><a id="886" href="Relation.Unary.html#Pred" class="Function">Pred</a><a id="890" class="Symbol">)</a>

<a id="893" class="Keyword">infix</a> <a id="899" class="Number">4</a> <a id="901" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">_∈?_</a>

<a id="_∈?_" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">_∈?_</a> <a id="912" class="Symbol">:</a> <a id="914" class="Symbol">∀</a> <a id="916" class="Symbol">{</a><a id="917" href="Data.Fin.Dec.html#917" class="Bound">n</a><a id="918" class="Symbol">}</a> <a id="920" href="Data.Fin.Dec.html#920" class="Bound">x</a> <a id="922" class="Symbol">(</a><a id="923" href="Data.Fin.Dec.html#923" class="Bound">p</a> <a id="925" class="Symbol">:</a> <a id="927" href="Data.Fin.Subset.html#Subset" class="Function">Subset</a> <a id="934" href="Data.Fin.Dec.html#917" class="Bound">n</a><a id="935" class="Symbol">)</a> <a id="937" class="Symbol">→</a> <a id="939" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="943" class="Symbol">(</a><a id="944" href="Data.Fin.Dec.html#920" class="Bound">x</a> <a id="946" href="Data.Fin.Subset.html#_%E2%88%88_" class="Function Operator">∈</a> <a id="948" href="Data.Fin.Dec.html#923" class="Bound">p</a><a id="949" class="Symbol">)</a>
<a id="951" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>  <a id="957" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">∈?</a> <a id="960" href="Agda.Builtin.Bool.html#Bool.inside" class="InductiveConstructor">inside</a>  <a id="968" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="970" href="Data.Fin.Dec.html#970" class="Bound">p</a> <a id="972" class="Symbol">=</a> <a id="974" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="978" href="Data.Vec.html#_%5B_%5D%3D_.here" class="InductiveConstructor">here</a>
<a id="983" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>  <a id="989" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">∈?</a> <a id="992" href="Agda.Builtin.Bool.html#Bool.outside" class="InductiveConstructor">outside</a> <a id="1000" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="1002" href="Data.Fin.Dec.html#1002" class="Bound">p</a> <a id="1004" class="Symbol">=</a> <a id="1006" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a>  <a id="1010" class="Symbol">λ()</a>
<a id="1014" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="1018" href="Data.Fin.Dec.html#1018" class="Bound">n</a> <a id="1020" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">∈?</a> <a id="1023" href="Data.Fin.Dec.html#1023" class="Bound">s</a> <a id="1025" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="1027" href="Data.Fin.Dec.html#1027" class="Bound">p</a>       <a id="1035" class="Keyword">with</a> <a id="1040" href="Data.Fin.Dec.html#1018" class="Bound">n</a> <a id="1042" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">∈?</a> <a id="1045" href="Data.Fin.Dec.html#1027" class="Bound">p</a>
<a id="1047" class="Symbol">...</a>                  <a id="1068" class="Symbol">|</a> <a id="1070" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="1074" href="Data.Fin.Dec.html#1074" class="Bound">n∈p</a> <a id="1078" class="Symbol">=</a> <a id="1080" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="1084" class="Symbol">(</a><a id="1085" href="Data.Vec.html#_%5B_%5D%3D_.there" class="InductiveConstructor">there</a> <a id="1091" href="Data.Fin.Dec.html#1074" class="Bound">n∈p</a><a id="1094" class="Symbol">)</a>
<a id="1096" class="Symbol">...</a>                  <a id="1117" class="Symbol">|</a> <a id="1119" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a>  <a id="1123" href="Data.Fin.Dec.html#1123" class="Bound">n∉p</a> <a id="1127" class="Symbol">=</a> <a id="1129" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a>  <a id="1133" class="Symbol">(</a><a id="1134" href="Data.Fin.Dec.html#1123" class="Bound">n∉p</a> <a id="1138" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="1140" href="Data.Fin.Subset.Properties.html#drop-there" class="Function">drop-there</a><a id="1150" class="Symbol">)</a>

<a id="1153" class="Keyword">private</a>

  <a id="restrictP" href="Data.Fin.Dec.html#restrictP" class="Function">restrictP</a> <a id="1174" class="Symbol">:</a> <a id="1176" class="Symbol">∀</a> <a id="1178" class="Symbol">{</a><a id="1179" href="Data.Fin.Dec.html#1179" class="Bound">p</a> <a id="1181" href="Data.Fin.Dec.html#1181" class="Bound">n</a><a id="1182" class="Symbol">}</a> <a id="1184" class="Symbol">→</a> <a id="1186" class="Symbol">(</a><a id="1187" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1191" class="Symbol">(</a><a id="1192" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1196" href="Data.Fin.Dec.html#1181" class="Bound">n</a><a id="1197" class="Symbol">)</a> <a id="1199" class="Symbol">→</a> <a id="1201" class="PrimitiveType">Set</a> <a id="1205" href="Data.Fin.Dec.html#1179" class="Bound">p</a><a id="1206" class="Symbol">)</a> <a id="1208" class="Symbol">→</a> <a id="1210" class="Symbol">(</a><a id="1211" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1215" href="Data.Fin.Dec.html#1181" class="Bound">n</a> <a id="1217" class="Symbol">→</a> <a id="1219" class="PrimitiveType">Set</a> <a id="1223" href="Data.Fin.Dec.html#1179" class="Bound">p</a><a id="1224" class="Symbol">)</a>
  <a id="1228" href="Data.Fin.Dec.html#restrictP" class="Function">restrictP</a> <a id="1238" href="Data.Fin.Dec.html#1238" class="Bound">P</a> <a id="1240" href="Data.Fin.Dec.html#1240" class="Bound">f</a> <a id="1242" class="Symbol">=</a> <a id="1244" href="Data.Fin.Dec.html#1238" class="Bound">P</a> <a id="1246" class="Symbol">(</a><a id="1247" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="1251" href="Data.Fin.Dec.html#1240" class="Bound">f</a><a id="1252" class="Symbol">)</a>

  <a id="restrict" href="Data.Fin.Dec.html#restrict" class="Function">restrict</a> <a id="1266" class="Symbol">:</a> <a id="1268" class="Symbol">∀</a> <a id="1270" class="Symbol">{</a><a id="1271" href="Data.Fin.Dec.html#1271" class="Bound">p</a> <a id="1273" href="Data.Fin.Dec.html#1273" class="Bound">n</a><a id="1274" class="Symbol">}</a> <a id="1276" class="Symbol">{</a><a id="1277" href="Data.Fin.Dec.html#1277" class="Bound">P</a> <a id="1279" class="Symbol">:</a> <a id="1281" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1285" class="Symbol">(</a><a id="1286" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1290" href="Data.Fin.Dec.html#1273" class="Bound">n</a><a id="1291" class="Symbol">)</a> <a id="1293" class="Symbol">→</a> <a id="1295" class="PrimitiveType">Set</a> <a id="1299" href="Data.Fin.Dec.html#1271" class="Bound">p</a><a id="1300" class="Symbol">}</a> <a id="1302" class="Symbol">→</a>
             <a id="1317" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="1329" href="Data.Fin.Dec.html#1277" class="Bound">P</a> <a id="1331" class="Symbol">→</a> <a id="1333" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="1345" class="Symbol">(</a><a id="1346" href="Data.Fin.Dec.html#restrictP" class="Function">restrictP</a> <a id="1356" href="Data.Fin.Dec.html#1277" class="Bound">P</a><a id="1357" class="Symbol">)</a>
  <a id="1361" href="Data.Fin.Dec.html#restrict" class="Function">restrict</a> <a id="1370" href="Data.Fin.Dec.html#1370" class="Bound">dec</a> <a id="1374" href="Data.Fin.Dec.html#1374" class="Bound">f</a> <a id="1376" class="Symbol">=</a> <a id="1378" href="Data.Fin.Dec.html#1370" class="Bound">dec</a> <a id="1382" class="Symbol">(</a><a id="1383" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="1387" href="Data.Fin.Dec.html#1374" class="Bound">f</a><a id="1388" class="Symbol">)</a>

<a id="any?" href="Data.Fin.Dec.html#any%3F" class="Function">any?</a> <a id="1396" class="Symbol">:</a> <a id="1398" class="Symbol">∀</a> <a id="1400" class="Symbol">{</a><a id="1401" href="Data.Fin.Dec.html#1401" class="Bound">n</a><a id="1402" class="Symbol">}</a> <a id="1404" class="Symbol">{</a><a id="1405" href="Data.Fin.Dec.html#1405" class="Bound">P</a> <a id="1407" class="Symbol">:</a> <a id="1409" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1413" href="Data.Fin.Dec.html#1401" class="Bound">n</a> <a id="1415" class="Symbol">→</a> <a id="1417" class="PrimitiveType">Set</a><a id="1420" class="Symbol">}</a> <a id="1422" class="Symbol">→</a>
       <a id="1431" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="1443" href="Data.Fin.Dec.html#1405" class="Bound">P</a> <a id="1445" class="Symbol">→</a> <a id="1447" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="1451" class="Symbol">(</a><a id="1452" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="1454" href="Data.Fin.Dec.html#1405" class="Bound">P</a><a id="1455" class="Symbol">)</a>
<a id="1457" href="Data.Fin.Dec.html#any%3F" class="Function">any?</a> <a id="1462" class="Symbol">{</a><a id="1463" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a><a id="1467" class="Symbol">}</a>      <a id="1474" href="Data.Fin.Dec.html#1474" class="Bound">dec</a> <a id="1478" class="Symbol">=</a> <a id="1480" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="1483" class="Symbol">λ</a> <a id="1485" class="Symbol">{</a> <a id="1487" class="Symbol">(()</a> <a id="1491" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1493" class="Symbol">_)</a> <a id="1496" class="Symbol">}</a>
<a id="1498" href="Data.Fin.Dec.html#any%3F" class="Function">any?</a> <a id="1503" class="Symbol">{</a><a id="1504" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1508" href="Data.Fin.Dec.html#1508" class="Bound">n</a><a id="1509" class="Symbol">}</a> <a id="1511" class="Symbol">{</a><a id="1512" href="Data.Fin.Dec.html#1512" class="Bound">P</a><a id="1513" class="Symbol">}</a> <a id="1515" href="Data.Fin.Dec.html#1515" class="Bound">dec</a> <a id="1519" class="Keyword">with</a> <a id="1524" href="Data.Fin.Dec.html#1515" class="Bound">dec</a> <a id="1528" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a> <a id="1533" class="Symbol">|</a> <a id="1535" href="Data.Fin.Dec.html#any%3F" class="Function">any?</a> <a id="1540" class="Symbol">(</a><a id="1541" href="Data.Fin.Dec.html#restrict" class="Function">restrict</a> <a id="1550" href="Data.Fin.Dec.html#1515" class="Bound">dec</a><a id="1553" class="Symbol">)</a>
<a id="1555" class="Symbol">...</a>                  <a id="1576" class="Symbol">|</a> <a id="1578" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="1582" href="Data.Fin.Dec.html#1582" class="Bound">p</a> <a id="1584" class="Symbol">|</a> <a id="1586" class="Symbol">_</a>            <a id="1599" class="Symbol">=</a> <a id="1601" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="1605" class="Symbol">(_</a> <a id="1608" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1610" href="Data.Fin.Dec.html#1582" class="Bound">p</a><a id="1611" class="Symbol">)</a>
<a id="1613" class="CatchallClause Symbol">...</a><a id="1616" class="CatchallClause">                  </a><a id="1634" class="CatchallClause Symbol">|</a><a id="1635" class="CatchallClause"> </a><a id="1636" class="CatchallClause Symbol">_</a><a id="1637" class="CatchallClause">     </a><a id="1642" class="CatchallClause Symbol">|</a><a id="1643" class="CatchallClause"> </a><a id="1644" href="Relation.Nullary.html#Dec.yes" class="CatchallClause InductiveConstructor">yes</a><a id="1647" class="CatchallClause"> </a><a id="1648" class="CatchallClause Symbol">(_</a><a id="1650" class="CatchallClause"> </a><a id="1651" href="Data.Product.html#%CE%A3._%2C_" class="CatchallClause InductiveConstructor Operator">,</a><a id="1652" class="CatchallClause"> </a><a id="1653" href="Data.Fin.Dec.html#1653" class="CatchallClause Bound">p&#39;</a><a id="1655" class="CatchallClause Symbol">)</a> <a id="1657" class="Symbol">=</a> <a id="1659" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="1663" class="Symbol">(_</a> <a id="1666" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1668" href="Data.Fin.Dec.html#1653" class="Bound">p&#39;</a><a id="1670" class="Symbol">)</a>
<a id="1672" class="Symbol">...</a>                  <a id="1693" class="Symbol">|</a> <a id="1695" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="1698" href="Data.Fin.Dec.html#1698" class="Bound">¬p</a> <a id="1701" class="Symbol">|</a> <a id="1703" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="1706" href="Data.Fin.Dec.html#1706" class="Bound">¬p&#39;</a>       <a id="1716" class="Symbol">=</a> <a id="1718" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="1721" href="Data.Fin.Dec.html#1738" class="Function">helper</a>
  <a id="1730" class="Keyword">where</a>
  <a id="1738" href="Data.Fin.Dec.html#1738" class="Function">helper</a> <a id="1745" class="Symbol">:</a> <a id="1747" href="Data.Product.html#%E2%88%84" class="Function">∄</a> <a id="1749" class="Bound">P</a>
  <a id="1753" href="Data.Fin.Dec.html#1738" class="Function">helper</a> <a id="1760" class="Symbol">(</a><a id="1761" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>  <a id="1767" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1769" href="Data.Fin.Dec.html#1769" class="Bound">p</a><a id="1770" class="Symbol">)</a>  <a id="1773" class="Symbol">=</a> <a id="1775" href="Data.Fin.Dec.html#1698" class="Bound">¬p</a> <a id="1778" href="Data.Fin.Dec.html#1769" class="Bound">p</a>
  <a id="1782" href="Data.Fin.Dec.html#1738" class="Function">helper</a> <a id="1789" class="Symbol">(</a><a id="1790" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="1794" href="Data.Fin.Dec.html#1794" class="Bound">f</a> <a id="1796" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1798" href="Data.Fin.Dec.html#1798" class="Bound">p&#39;</a><a id="1800" class="Symbol">)</a> <a id="1802" class="Symbol">=</a> <a id="1804" href="Data.Fin.Dec.html#1706" class="Bound">¬p&#39;</a> <a id="1808" class="Symbol">(_</a> <a id="1811" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1813" href="Data.Fin.Dec.html#1798" class="Bound">p&#39;</a><a id="1815" class="Symbol">)</a>

<a id="nonempty?" href="Data.Fin.Dec.html#nonempty%3F" class="Function">nonempty?</a> <a id="1828" class="Symbol">:</a> <a id="1830" class="Symbol">∀</a> <a id="1832" class="Symbol">{</a><a id="1833" href="Data.Fin.Dec.html#1833" class="Bound">n</a><a id="1834" class="Symbol">}</a> <a id="1836" class="Symbol">(</a><a id="1837" href="Data.Fin.Dec.html#1837" class="Bound">p</a> <a id="1839" class="Symbol">:</a> <a id="1841" href="Data.Fin.Subset.html#Subset" class="Function">Subset</a> <a id="1848" href="Data.Fin.Dec.html#1833" class="Bound">n</a><a id="1849" class="Symbol">)</a> <a id="1851" class="Symbol">→</a> <a id="1853" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="1857" class="Symbol">(</a><a id="1858" href="Data.Fin.Subset.html#Nonempty" class="Function">Nonempty</a> <a id="1867" href="Data.Fin.Dec.html#1837" class="Bound">p</a><a id="1868" class="Symbol">)</a>
<a id="1870" href="Data.Fin.Dec.html#nonempty%3F" class="Function">nonempty?</a> <a id="1880" href="Data.Fin.Dec.html#1880" class="Bound">p</a> <a id="1882" class="Symbol">=</a> <a id="1884" href="Data.Fin.Dec.html#any%3F" class="Function">any?</a> <a id="1889" class="Symbol">(λ</a> <a id="1892" href="Data.Fin.Dec.html#1892" class="Bound">x</a> <a id="1894" class="Symbol">→</a> <a id="1896" href="Data.Fin.Dec.html#1892" class="Bound">x</a> <a id="1898" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">∈?</a> <a id="1901" href="Data.Fin.Dec.html#1880" class="Bound">p</a><a id="1902" class="Symbol">)</a>

<a id="1905" class="Keyword">private</a>

  <a id="restrict∈" href="Data.Fin.Dec.html#restrict%E2%88%88" class="Function">restrict∈</a> <a id="1926" class="Symbol">:</a> <a id="1928" class="Symbol">∀</a> <a id="1930" class="Symbol">{</a><a id="1931" href="Data.Fin.Dec.html#1931" class="Bound">p</a> <a id="1933" href="Data.Fin.Dec.html#1933" class="Bound">q</a> <a id="1935" href="Data.Fin.Dec.html#1935" class="Bound">n</a><a id="1936" class="Symbol">}</a>
              <a id="1952" class="Symbol">(</a><a id="1953" href="Data.Fin.Dec.html#1953" class="Bound">P</a> <a id="1955" class="Symbol">:</a> <a id="1957" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1961" class="Symbol">(</a><a id="1962" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1966" href="Data.Fin.Dec.html#1935" class="Bound">n</a><a id="1967" class="Symbol">)</a> <a id="1969" class="Symbol">→</a> <a id="1971" class="PrimitiveType">Set</a> <a id="1975" href="Data.Fin.Dec.html#1931" class="Bound">p</a><a id="1976" class="Symbol">)</a> <a id="1978" class="Symbol">{</a><a id="1979" href="Data.Fin.Dec.html#1979" class="Bound">Q</a> <a id="1981" class="Symbol">:</a> <a id="1983" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="1987" class="Symbol">(</a><a id="1988" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="1992" href="Data.Fin.Dec.html#1935" class="Bound">n</a><a id="1993" class="Symbol">)</a> <a id="1995" class="Symbol">→</a> <a id="1997" class="PrimitiveType">Set</a> <a id="2001" href="Data.Fin.Dec.html#1933" class="Bound">q</a><a id="2002" class="Symbol">}</a> <a id="2004" class="Symbol">→</a>
              <a id="2020" class="Symbol">(∀</a> <a id="2023" class="Symbol">{</a><a id="2024" href="Data.Fin.Dec.html#2024" class="Bound">f</a><a id="2025" class="Symbol">}</a> <a id="2027" class="Symbol">→</a> <a id="2029" href="Data.Fin.Dec.html#1979" class="Bound">Q</a> <a id="2031" href="Data.Fin.Dec.html#2024" class="Bound">f</a> <a id="2033" class="Symbol">→</a> <a id="2035" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="2039" class="Symbol">(</a><a id="2040" href="Data.Fin.Dec.html#1953" class="Bound">P</a> <a id="2042" href="Data.Fin.Dec.html#2024" class="Bound">f</a><a id="2043" class="Symbol">))</a> <a id="2046" class="Symbol">→</a>
              <a id="2062" class="Symbol">(∀</a> <a id="2065" class="Symbol">{</a><a id="2066" href="Data.Fin.Dec.html#2066" class="Bound">f</a><a id="2067" class="Symbol">}</a> <a id="2069" class="Symbol">→</a> <a id="2071" href="Data.Fin.Dec.html#restrictP" class="Function">restrictP</a> <a id="2081" href="Data.Fin.Dec.html#1979" class="Bound">Q</a> <a id="2083" href="Data.Fin.Dec.html#2066" class="Bound">f</a> <a id="2085" class="Symbol">→</a> <a id="2087" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="2091" class="Symbol">(</a><a id="2092" href="Data.Fin.Dec.html#restrictP" class="Function">restrictP</a> <a id="2102" href="Data.Fin.Dec.html#1953" class="Bound">P</a> <a id="2104" href="Data.Fin.Dec.html#2066" class="Bound">f</a><a id="2105" class="Symbol">))</a>
  <a id="2110" href="Data.Fin.Dec.html#restrict%E2%88%88" class="Function">restrict∈</a> <a id="2120" class="Symbol">_</a> <a id="2122" href="Data.Fin.Dec.html#2122" class="Bound">dec</a> <a id="2126" class="Symbol">{</a><a id="2127" href="Data.Fin.Dec.html#2127" class="Bound">f</a><a id="2128" class="Symbol">}</a> <a id="2130" href="Data.Fin.Dec.html#2130" class="Bound">Qf</a> <a id="2133" class="Symbol">=</a> <a id="2135" href="Data.Fin.Dec.html#2122" class="Bound">dec</a> <a id="2139" class="Symbol">{</a><a id="2140" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="2144" href="Data.Fin.Dec.html#2127" class="Bound">f</a><a id="2145" class="Symbol">}</a> <a id="2147" href="Data.Fin.Dec.html#2130" class="Bound">Qf</a>

<a id="decFinSubset" href="Data.Fin.Dec.html#decFinSubset" class="Function">decFinSubset</a> <a id="2164" class="Symbol">:</a> <a id="2166" class="Symbol">∀</a> <a id="2168" class="Symbol">{</a><a id="2169" href="Data.Fin.Dec.html#2169" class="Bound">p</a> <a id="2171" href="Data.Fin.Dec.html#2171" class="Bound">q</a> <a id="2173" href="Data.Fin.Dec.html#2173" class="Bound">n</a><a id="2174" class="Symbol">}</a> <a id="2176" class="Symbol">{</a><a id="2177" href="Data.Fin.Dec.html#2177" class="Bound">P</a> <a id="2179" class="Symbol">:</a> <a id="2181" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="2185" href="Data.Fin.Dec.html#2173" class="Bound">n</a> <a id="2187" class="Symbol">→</a> <a id="2189" class="PrimitiveType">Set</a> <a id="2193" href="Data.Fin.Dec.html#2169" class="Bound">p</a><a id="2194" class="Symbol">}</a> <a id="2196" class="Symbol">{</a><a id="2197" href="Data.Fin.Dec.html#2197" class="Bound">Q</a> <a id="2199" class="Symbol">:</a> <a id="2201" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="2205" href="Data.Fin.Dec.html#2173" class="Bound">n</a> <a id="2207" class="Symbol">→</a> <a id="2209" class="PrimitiveType">Set</a> <a id="2213" href="Data.Fin.Dec.html#2171" class="Bound">q</a><a id="2214" class="Symbol">}</a> <a id="2216" class="Symbol">→</a>
               <a id="2233" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="2245" href="Data.Fin.Dec.html#2197" class="Bound">Q</a> <a id="2247" class="Symbol">→</a>
               <a id="2264" class="Symbol">(∀</a> <a id="2267" class="Symbol">{</a><a id="2268" href="Data.Fin.Dec.html#2268" class="Bound">f</a><a id="2269" class="Symbol">}</a> <a id="2271" class="Symbol">→</a> <a id="2273" href="Data.Fin.Dec.html#2197" class="Bound">Q</a> <a id="2275" href="Data.Fin.Dec.html#2268" class="Bound">f</a> <a id="2277" class="Symbol">→</a> <a id="2279" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="2283" class="Symbol">(</a><a id="2284" href="Data.Fin.Dec.html#2177" class="Bound">P</a> <a id="2286" href="Data.Fin.Dec.html#2268" class="Bound">f</a><a id="2287" class="Symbol">))</a> <a id="2290" class="Symbol">→</a>
               <a id="2307" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="2311" class="Symbol">(∀</a> <a id="2314" class="Symbol">{</a><a id="2315" href="Data.Fin.Dec.html#2315" class="Bound">f</a><a id="2316" class="Symbol">}</a> <a id="2318" class="Symbol">→</a> <a id="2320" href="Data.Fin.Dec.html#2197" class="Bound">Q</a> <a id="2322" href="Data.Fin.Dec.html#2315" class="Bound">f</a> <a id="2324" class="Symbol">→</a> <a id="2326" href="Data.Fin.Dec.html#2177" class="Bound">P</a> <a id="2328" href="Data.Fin.Dec.html#2315" class="Bound">f</a><a id="2329" class="Symbol">)</a>
<a id="2331" href="Data.Fin.Dec.html#decFinSubset" class="Function">decFinSubset</a> <a id="2344" class="Symbol">{</a><a id="2345" class="Argument">n</a> <a id="2347" class="Symbol">=</a> <a id="2349" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a><a id="2353" class="Symbol">}</a>          <a id="2364" class="Symbol">_</a>    <a id="2369" class="Symbol">_</a>    <a id="2374" class="Symbol">=</a> <a id="2376" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2380" class="Symbol">λ{}</a>
<a id="2384" href="Data.Fin.Dec.html#decFinSubset" class="Function">decFinSubset</a> <a id="2397" class="Symbol">{</a><a id="2398" class="Argument">n</a> <a id="2400" class="Symbol">=</a> <a id="2402" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="2406" href="Data.Fin.Dec.html#2406" class="Bound">n</a><a id="2407" class="Symbol">}</a> <a id="2409" class="Symbol">{</a><a id="2410" href="Data.Fin.Dec.html#2410" class="Bound">P</a><a id="2411" class="Symbol">}</a> <a id="2413" class="Symbol">{</a><a id="2414" href="Data.Fin.Dec.html#2414" class="Bound">Q</a><a id="2415" class="Symbol">}</a> <a id="2417" href="Data.Fin.Dec.html#2417" class="Bound">decQ</a> <a id="2422" href="Data.Fin.Dec.html#2422" class="Bound">decP</a> <a id="2427" class="Symbol">=</a> <a id="2429" href="Data.Fin.Dec.html#2446" class="Function">helper</a>
  <a id="2438" class="Keyword">where</a>
  <a id="2446" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2453" class="Symbol">:</a> <a id="2455" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="2459" class="Symbol">(∀</a> <a id="2462" class="Symbol">{</a><a id="2463" href="Data.Fin.Dec.html#2463" class="Bound">f</a><a id="2464" class="Symbol">}</a> <a id="2466" class="Symbol">→</a> <a id="2468" href="Data.Fin.Dec.html#2414" class="Bound">Q</a> <a id="2470" href="Data.Fin.Dec.html#2463" class="Bound">f</a> <a id="2472" class="Symbol">→</a> <a id="2474" href="Data.Fin.Dec.html#2410" class="Bound">P</a> <a id="2476" href="Data.Fin.Dec.html#2463" class="Bound">f</a><a id="2477" class="Symbol">)</a>
  <a id="2481" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2488" class="Keyword">with</a> <a id="2493" href="Data.Fin.Dec.html#decFinSubset" class="Function">decFinSubset</a> <a id="2506" class="Symbol">(</a><a id="2507" href="Data.Fin.Dec.html#restrict" class="Function">restrict</a> <a id="2516" href="Data.Fin.Dec.html#2417" class="Bound">decQ</a><a id="2520" class="Symbol">)</a> <a id="2522" class="Symbol">(</a><a id="2523" href="Data.Fin.Dec.html#restrict%E2%88%88" class="Function">restrict∈</a> <a id="2533" href="Data.Fin.Dec.html#2410" class="Bound">P</a> <a id="2535" href="Data.Fin.Dec.html#2422" class="Bound">decP</a><a id="2539" class="Symbol">)</a>
  <a id="2543" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2550" class="Symbol">|</a> <a id="2552" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2555" href="Data.Fin.Dec.html#2555" class="Bound">¬q⟶p</a> <a id="2560" class="Symbol">=</a> <a id="2562" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2565" class="Symbol">(λ</a> <a id="2568" href="Data.Fin.Dec.html#2568" class="Bound">q⟶p</a> <a id="2572" class="Symbol">→</a> <a id="2574" href="Data.Fin.Dec.html#2555" class="Bound">¬q⟶p</a> <a id="2579" class="Symbol">(λ</a> <a id="2582" class="Symbol">{</a><a id="2583" href="Data.Fin.Dec.html#2583" class="Bound">f</a><a id="2584" class="Symbol">}</a> <a id="2586" href="Data.Fin.Dec.html#2586" class="Bound">q</a> <a id="2588" class="Symbol">→</a> <a id="2590" href="Data.Fin.Dec.html#2568" class="Bound">q⟶p</a> <a id="2594" class="Symbol">{</a><a id="2595" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="2599" href="Data.Fin.Dec.html#2583" class="Bound">f</a><a id="2600" class="Symbol">}</a> <a id="2602" href="Data.Fin.Dec.html#2586" class="Bound">q</a><a id="2603" class="Symbol">))</a>
  <a id="2608" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2615" class="Symbol">|</a> <a id="2617" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2621" href="Data.Fin.Dec.html#2621" class="Bound">q⟶p</a> <a id="2625" class="Keyword">with</a> <a id="2630" href="Data.Fin.Dec.html#2417" class="Bound">decQ</a> <a id="2635" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>
  <a id="2642" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2649" class="Symbol">|</a> <a id="2651" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2655" href="Data.Fin.Dec.html#2655" class="Bound">q⟶p</a> <a id="2659" class="Symbol">|</a> <a id="2661" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2665" href="Data.Fin.Dec.html#2665" class="Bound">q₀</a> <a id="2668" class="Keyword">with</a> <a id="2673" href="Data.Fin.Dec.html#2422" class="Bound">decP</a> <a id="2678" href="Data.Fin.Dec.html#2665" class="Bound">q₀</a>
  <a id="2683" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2690" class="Symbol">|</a> <a id="2692" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2696" href="Data.Fin.Dec.html#2696" class="Bound">q⟶p</a> <a id="2700" class="Symbol">|</a> <a id="2702" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2706" href="Data.Fin.Dec.html#2706" class="Bound">q₀</a> <a id="2709" class="Symbol">|</a> <a id="2711" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2714" href="Data.Fin.Dec.html#2714" class="Bound">¬p₀</a> <a id="2718" class="Symbol">=</a> <a id="2720" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2723" class="Symbol">(λ</a> <a id="2726" href="Data.Fin.Dec.html#2726" class="Bound">q⟶p</a> <a id="2730" class="Symbol">→</a> <a id="2732" href="Data.Fin.Dec.html#2714" class="Bound">¬p₀</a> <a id="2736" class="Symbol">(</a><a id="2737" href="Data.Fin.Dec.html#2726" class="Bound">q⟶p</a> <a id="2741" class="Symbol">{</a><a id="2742" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a><a id="2746" class="Symbol">}</a> <a id="2748" href="Data.Fin.Dec.html#2706" class="Bound">q₀</a><a id="2750" class="Symbol">))</a>
  <a id="2755" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2762" class="Symbol">|</a> <a id="2764" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2768" href="Data.Fin.Dec.html#2768" class="Bound">q⟶p</a> <a id="2772" class="Symbol">|</a> <a id="2774" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2778" href="Data.Fin.Dec.html#2778" class="Bound">q₀</a> <a id="2781" class="Symbol">|</a> <a id="2783" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2787" href="Data.Fin.Dec.html#2787" class="Bound">p₀</a> <a id="2790" class="Symbol">=</a> <a id="2792" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2796" class="Symbol">(λ</a> <a id="2799" class="Symbol">{</a><a id="2800" href="Data.Fin.Dec.html#2800" class="Bound">_</a><a id="2801" class="Symbol">}</a> <a id="2803" class="Symbol">→</a> <a id="2805" href="Data.Fin.Dec.html#2827" class="Function">hlpr</a> <a id="2810" class="Symbol">_)</a>
    <a id="2817" class="Keyword">where</a>
    <a id="2827" href="Data.Fin.Dec.html#2827" class="Function">hlpr</a> <a id="2832" class="Symbol">:</a> <a id="2834" class="Symbol">∀</a> <a id="2836" href="Data.Fin.Dec.html#2836" class="Bound">f</a> <a id="2838" class="Symbol">→</a> <a id="2840" href="Data.Fin.Dec.html#2414" class="Bound">Q</a> <a id="2842" href="Data.Fin.Dec.html#2836" class="Bound">f</a> <a id="2844" class="Symbol">→</a> <a id="2846" href="Data.Fin.Dec.html#2410" class="Bound">P</a> <a id="2848" href="Data.Fin.Dec.html#2836" class="Bound">f</a>
    <a id="2854" href="Data.Fin.Dec.html#2827" class="Function">hlpr</a> <a id="2859" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>    <a id="2867" class="Symbol">_</a>  <a id="2870" class="Symbol">=</a> <a id="2872" href="Data.Fin.Dec.html#2787" class="Bound">p₀</a>
    <a id="2879" href="Data.Fin.Dec.html#2827" class="Function">hlpr</a> <a id="2884" class="Symbol">(</a><a id="2885" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="2889" href="Data.Fin.Dec.html#2889" class="Bound">f</a><a id="2890" class="Symbol">)</a> <a id="2892" href="Data.Fin.Dec.html#2892" class="Bound">qf</a> <a id="2895" class="Symbol">=</a> <a id="2897" href="Data.Fin.Dec.html#2768" class="Bound">q⟶p</a> <a id="2901" href="Data.Fin.Dec.html#2892" class="Bound">qf</a>
  <a id="2906" href="Data.Fin.Dec.html#2446" class="Function">helper</a> <a id="2913" class="Symbol">|</a> <a id="2915" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2919" href="Data.Fin.Dec.html#2919" class="Bound">q⟶p</a> <a id="2923" class="Symbol">|</a> <a id="2925" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2928" href="Data.Fin.Dec.html#2928" class="Bound">¬q₀</a> <a id="2932" class="Symbol">=</a> <a id="2934" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2938" class="Symbol">(λ</a> <a id="2941" class="Symbol">{</a><a id="2942" href="Data.Fin.Dec.html#2942" class="Bound">_</a><a id="2943" class="Symbol">}</a> <a id="2945" class="Symbol">→</a> <a id="2947" href="Data.Fin.Dec.html#2969" class="Function">hlpr</a> <a id="2952" class="Symbol">_)</a>
    <a id="2959" class="Keyword">where</a>
    <a id="2969" href="Data.Fin.Dec.html#2969" class="Function">hlpr</a> <a id="2974" class="Symbol">:</a> <a id="2976" class="Symbol">∀</a> <a id="2978" href="Data.Fin.Dec.html#2978" class="Bound">f</a> <a id="2980" class="Symbol">→</a> <a id="2982" href="Data.Fin.Dec.html#2414" class="Bound">Q</a> <a id="2984" href="Data.Fin.Dec.html#2978" class="Bound">f</a> <a id="2986" class="Symbol">→</a> <a id="2988" href="Data.Fin.Dec.html#2410" class="Bound">P</a> <a id="2990" href="Data.Fin.Dec.html#2978" class="Bound">f</a>
    <a id="2996" href="Data.Fin.Dec.html#2969" class="Function">hlpr</a> <a id="3001" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>    <a id="3009" href="Data.Fin.Dec.html#3009" class="Bound">q₀</a> <a id="3012" class="Symbol">=</a> <a id="3014" href="Data.Empty.html#%E2%8A%A5-elim" class="Function">⊥-elim</a> <a id="3021" class="Symbol">(</a><a id="3022" href="Data.Fin.Dec.html#2928" class="Bound">¬q₀</a> <a id="3026" href="Data.Fin.Dec.html#3009" class="Bound">q₀</a><a id="3028" class="Symbol">)</a>
    <a id="3034" href="Data.Fin.Dec.html#2969" class="Function">hlpr</a> <a id="3039" class="Symbol">(</a><a id="3040" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="3044" href="Data.Fin.Dec.html#3044" class="Bound">f</a><a id="3045" class="Symbol">)</a> <a id="3047" href="Data.Fin.Dec.html#3047" class="Bound">qf</a> <a id="3050" class="Symbol">=</a> <a id="3052" href="Data.Fin.Dec.html#2919" class="Bound">q⟶p</a> <a id="3056" href="Data.Fin.Dec.html#3047" class="Bound">qf</a>

<a id="all∈?" href="Data.Fin.Dec.html#all%E2%88%88%3F" class="Function">all∈?</a> <a id="3066" class="Symbol">:</a> <a id="3068" class="Symbol">∀</a> <a id="3070" class="Symbol">{</a><a id="3071" href="Data.Fin.Dec.html#3071" class="Bound">n</a> <a id="3073" href="Data.Fin.Dec.html#3073" class="Bound">p</a><a id="3074" class="Symbol">}</a> <a id="3076" class="Symbol">{</a><a id="3077" href="Data.Fin.Dec.html#3077" class="Bound">P</a> <a id="3079" class="Symbol">:</a> <a id="3081" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="3085" href="Data.Fin.Dec.html#3071" class="Bound">n</a> <a id="3087" class="Symbol">→</a> <a id="3089" class="PrimitiveType">Set</a> <a id="3093" href="Data.Fin.Dec.html#3073" class="Bound">p</a><a id="3094" class="Symbol">}</a> <a id="3096" class="Symbol">{</a><a id="3097" href="Data.Fin.Dec.html#3097" class="Bound">q</a><a id="3098" class="Symbol">}</a> <a id="3100" class="Symbol">→</a>
        <a id="3110" class="Symbol">(∀</a> <a id="3113" class="Symbol">{</a><a id="3114" href="Data.Fin.Dec.html#3114" class="Bound">f</a><a id="3115" class="Symbol">}</a> <a id="3117" class="Symbol">→</a> <a id="3119" href="Data.Fin.Dec.html#3114" class="Bound">f</a> <a id="3121" href="Data.Fin.Subset.html#_%E2%88%88_" class="Function Operator">∈</a> <a id="3123" href="Data.Fin.Dec.html#3097" class="Bound">q</a> <a id="3125" class="Symbol">→</a> <a id="3127" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="3131" class="Symbol">(</a><a id="3132" href="Data.Fin.Dec.html#3077" class="Bound">P</a> <a id="3134" href="Data.Fin.Dec.html#3114" class="Bound">f</a><a id="3135" class="Symbol">))</a> <a id="3138" class="Symbol">→</a>
        <a id="3148" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="3152" class="Symbol">(∀</a> <a id="3155" class="Symbol">{</a><a id="3156" href="Data.Fin.Dec.html#3156" class="Bound">f</a><a id="3157" class="Symbol">}</a> <a id="3159" class="Symbol">→</a> <a id="3161" href="Data.Fin.Dec.html#3156" class="Bound">f</a> <a id="3163" href="Data.Fin.Subset.html#_%E2%88%88_" class="Function Operator">∈</a> <a id="3165" href="Data.Fin.Dec.html#3097" class="Bound">q</a> <a id="3167" class="Symbol">→</a> <a id="3169" href="Data.Fin.Dec.html#3077" class="Bound">P</a> <a id="3171" href="Data.Fin.Dec.html#3156" class="Bound">f</a><a id="3172" class="Symbol">)</a>
<a id="3174" href="Data.Fin.Dec.html#all%E2%88%88%3F" class="Function">all∈?</a> <a id="3180" class="Symbol">{</a><a id="3181" class="Argument">q</a> <a id="3183" class="Symbol">=</a> <a id="3185" href="Data.Fin.Dec.html#3185" class="Bound">q</a><a id="3186" class="Symbol">}</a> <a id="3188" href="Data.Fin.Dec.html#3188" class="Bound">dec</a> <a id="3192" class="Symbol">=</a> <a id="3194" href="Data.Fin.Dec.html#decFinSubset" class="Function">decFinSubset</a> <a id="3207" class="Symbol">(λ</a> <a id="3210" href="Data.Fin.Dec.html#3210" class="Bound">f</a> <a id="3212" class="Symbol">→</a> <a id="3214" href="Data.Fin.Dec.html#3210" class="Bound">f</a> <a id="3216" href="Data.Fin.Dec.html#_%E2%88%88%3F_" class="Function Operator">∈?</a> <a id="3219" href="Data.Fin.Dec.html#3185" class="Bound">q</a><a id="3220" class="Symbol">)</a> <a id="3222" href="Data.Fin.Dec.html#3188" class="Bound">dec</a>

<a id="all?" href="Data.Fin.Dec.html#all%3F" class="Function">all?</a> <a id="3232" class="Symbol">:</a> <a id="3234" class="Symbol">∀</a> <a id="3236" class="Symbol">{</a><a id="3237" href="Data.Fin.Dec.html#3237" class="Bound">n</a> <a id="3239" href="Data.Fin.Dec.html#3239" class="Bound">p</a><a id="3240" class="Symbol">}</a> <a id="3242" class="Symbol">{</a><a id="3243" href="Data.Fin.Dec.html#3243" class="Bound">P</a> <a id="3245" class="Symbol">:</a> <a id="3247" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="3251" href="Data.Fin.Dec.html#3237" class="Bound">n</a> <a id="3253" class="Symbol">→</a> <a id="3255" class="PrimitiveType">Set</a> <a id="3259" href="Data.Fin.Dec.html#3239" class="Bound">p</a><a id="3260" class="Symbol">}</a> <a id="3262" class="Symbol">→</a>
       <a id="3271" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="3283" href="Data.Fin.Dec.html#3243" class="Bound">P</a> <a id="3285" class="Symbol">→</a> <a id="3287" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="3291" class="Symbol">(∀</a> <a id="3294" href="Data.Fin.Dec.html#3294" class="Bound">f</a> <a id="3296" class="Symbol">→</a> <a id="3298" href="Data.Fin.Dec.html#3243" class="Bound">P</a> <a id="3300" href="Data.Fin.Dec.html#3294" class="Bound">f</a><a id="3301" class="Symbol">)</a>
<a id="3303" href="Data.Fin.Dec.html#all%3F" class="Function">all?</a> <a id="3308" href="Data.Fin.Dec.html#3308" class="Bound">dec</a> <a id="3312" class="Keyword">with</a> <a id="3317" href="Data.Fin.Dec.html#all%E2%88%88%3F" class="Function">all∈?</a> <a id="3323" class="Symbol">{</a><a id="3324" class="Argument">q</a> <a id="3326" class="Symbol">=</a> <a id="3328" href="Algebra.html#Fin.Subset.BA.%E2%8A%A4" class="Function">⊤</a><a id="3329" class="Symbol">}</a> <a id="3331" class="Symbol">(λ</a> <a id="3334" class="Symbol">{</a><a id="3335" href="Data.Fin.Dec.html#3335" class="Bound">f</a><a id="3336" class="Symbol">}</a> <a id="3338" href="Data.Fin.Dec.html#3338" class="Bound">_</a> <a id="3340" class="Symbol">→</a> <a id="3342" href="Data.Fin.Dec.html#3308" class="Bound">dec</a> <a id="3346" href="Data.Fin.Dec.html#3335" class="Bound">f</a><a id="3347" class="Symbol">)</a>
<a id="3349" class="Symbol">...</a>      <a id="3358" class="Symbol">|</a> <a id="3360" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="3364" href="Data.Fin.Dec.html#3364" class="Bound">∀p</a> <a id="3367" class="Symbol">=</a> <a id="3369" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="3373" class="Symbol">(λ</a> <a id="3376" href="Data.Fin.Dec.html#3376" class="Bound">f</a> <a id="3378" class="Symbol">→</a> <a id="3380" href="Data.Fin.Dec.html#3364" class="Bound">∀p</a> <a id="3383" href="Data.Fin.Subset.Properties.html#%E2%88%88%E2%8A%A4" class="Function">∈⊤</a><a id="3385" class="Symbol">)</a>
<a id="3387" class="Symbol">...</a>      <a id="3396" class="Symbol">|</a> <a id="3398" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="3401" href="Data.Fin.Dec.html#3401" class="Bound">¬∀p</a> <a id="3405" class="Symbol">=</a> <a id="3407" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a>  <a id="3411" class="Symbol">(λ</a> <a id="3414" href="Data.Fin.Dec.html#3414" class="Bound">∀p</a> <a id="3417" class="Symbol">→</a> <a id="3419" href="Data.Fin.Dec.html#3401" class="Bound">¬∀p</a> <a id="3423" class="Symbol">(λ</a> <a id="3426" class="Symbol">{</a><a id="3427" href="Data.Fin.Dec.html#3427" class="Bound">f</a><a id="3428" class="Symbol">}</a> <a id="3430" href="Data.Fin.Dec.html#3430" class="Bound">_</a> <a id="3432" class="Symbol">→</a> <a id="3434" href="Data.Fin.Dec.html#3414" class="Bound">∀p</a> <a id="3437" href="Data.Fin.Dec.html#3427" class="Bound">f</a><a id="3438" class="Symbol">))</a>

<a id="decLift" href="Data.Fin.Dec.html#decLift" class="Function">decLift</a> <a id="3450" class="Symbol">:</a> <a id="3452" class="Symbol">∀</a> <a id="3454" class="Symbol">{</a><a id="3455" href="Data.Fin.Dec.html#3455" class="Bound">n</a><a id="3456" class="Symbol">}</a> <a id="3458" class="Symbol">{</a><a id="3459" href="Data.Fin.Dec.html#3459" class="Bound">P</a> <a id="3461" class="Symbol">:</a> <a id="3463" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="3467" href="Data.Fin.Dec.html#3455" class="Bound">n</a> <a id="3469" class="Symbol">→</a> <a id="3471" class="PrimitiveType">Set</a><a id="3474" class="Symbol">}</a> <a id="3476" class="Symbol">→</a>
          <a id="3488" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="3500" href="Data.Fin.Dec.html#3459" class="Bound">P</a> <a id="3502" class="Symbol">→</a> <a id="3504" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="3516" class="Symbol">(</a><a id="3517" href="Data.Fin.Subset.html#Lift" class="Function">Lift</a> <a id="3522" href="Data.Fin.Dec.html#3459" class="Bound">P</a><a id="3523" class="Symbol">)</a>
<a id="3525" href="Data.Fin.Dec.html#decLift" class="Function">decLift</a> <a id="3533" href="Data.Fin.Dec.html#3533" class="Bound">dec</a> <a id="3537" href="Data.Fin.Dec.html#3537" class="Bound">p</a> <a id="3539" class="Symbol">=</a> <a id="3541" href="Data.Fin.Dec.html#all%E2%88%88%3F" class="Function">all∈?</a> <a id="3547" class="Symbol">(λ</a> <a id="3550" class="Symbol">{</a><a id="3551" href="Data.Fin.Dec.html#3551" class="Bound">x</a><a id="3552" class="Symbol">}</a> <a id="3554" href="Data.Fin.Dec.html#3554" class="Bound">_</a> <a id="3556" class="Symbol">→</a> <a id="3558" href="Data.Fin.Dec.html#3533" class="Bound">dec</a> <a id="3562" href="Data.Fin.Dec.html#3551" class="Bound">x</a><a id="3563" class="Symbol">)</a>

<a id="3566" class="Keyword">private</a>

  <a id="restrictSP" href="Data.Fin.Dec.html#restrictSP" class="Function">restrictSP</a> <a id="3588" class="Symbol">:</a> <a id="3590" class="Symbol">∀</a> <a id="3592" class="Symbol">{</a><a id="3593" href="Data.Fin.Dec.html#3593" class="Bound">n</a><a id="3594" class="Symbol">}</a> <a id="3596" class="Symbol">→</a> <a id="3598" href="Agda.Builtin.Bool.html#Side" class="Datatype">Side</a> <a id="3603" class="Symbol">→</a> <a id="3605" class="Symbol">(</a><a id="3606" href="Data.Fin.Subset.html#Subset" class="Function">Subset</a> <a id="3613" class="Symbol">(</a><a id="3614" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="3618" href="Data.Fin.Dec.html#3593" class="Bound">n</a><a id="3619" class="Symbol">)</a> <a id="3621" class="Symbol">→</a> <a id="3623" class="PrimitiveType">Set</a><a id="3626" class="Symbol">)</a> <a id="3628" class="Symbol">→</a> <a id="3630" class="Symbol">(</a><a id="3631" href="Data.Fin.Subset.html#Subset" class="Function">Subset</a> <a id="3638" href="Data.Fin.Dec.html#3593" class="Bound">n</a> <a id="3640" class="Symbol">→</a> <a id="3642" class="PrimitiveType">Set</a><a id="3645" class="Symbol">)</a>
  <a id="3649" href="Data.Fin.Dec.html#restrictSP" class="Function">restrictSP</a> <a id="3660" href="Data.Fin.Dec.html#3660" class="Bound">s</a> <a id="3662" href="Data.Fin.Dec.html#3662" class="Bound">P</a> <a id="3664" href="Data.Fin.Dec.html#3664" class="Bound">p</a> <a id="3666" class="Symbol">=</a> <a id="3668" href="Data.Fin.Dec.html#3662" class="Bound">P</a> <a id="3670" class="Symbol">(</a><a id="3671" href="Data.Fin.Dec.html#3660" class="Bound">s</a> <a id="3673" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="3675" href="Data.Fin.Dec.html#3664" class="Bound">p</a><a id="3676" class="Symbol">)</a>

  <a id="restrictS" href="Data.Fin.Dec.html#restrictS" class="Function">restrictS</a> <a id="3691" class="Symbol">:</a> <a id="3693" class="Symbol">∀</a> <a id="3695" class="Symbol">{</a><a id="3696" href="Data.Fin.Dec.html#3696" class="Bound">n</a><a id="3697" class="Symbol">}</a> <a id="3699" class="Symbol">{</a><a id="3700" href="Data.Fin.Dec.html#3700" class="Bound">P</a> <a id="3702" class="Symbol">:</a> <a id="3704" href="Data.Fin.Subset.html#Subset" class="Function">Subset</a> <a id="3711" class="Symbol">(</a><a id="3712" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="3716" href="Data.Fin.Dec.html#3696" class="Bound">n</a><a id="3717" class="Symbol">)</a> <a id="3719" class="Symbol">→</a> <a id="3721" class="PrimitiveType">Set</a><a id="3724" class="Symbol">}</a> <a id="3726" class="Symbol">→</a>
              <a id="3742" class="Symbol">(</a><a id="3743" href="Data.Fin.Dec.html#3743" class="Bound">s</a> <a id="3745" class="Symbol">:</a> <a id="3747" href="Agda.Builtin.Bool.html#Side" class="Datatype">Side</a><a id="3751" class="Symbol">)</a> <a id="3753" class="Symbol">→</a> <a id="3755" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="3767" href="Data.Fin.Dec.html#3700" class="Bound">P</a> <a id="3769" class="Symbol">→</a> <a id="3771" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="3783" class="Symbol">(</a><a id="3784" href="Data.Fin.Dec.html#restrictSP" class="Function">restrictSP</a> <a id="3795" href="Data.Fin.Dec.html#3743" class="Bound">s</a> <a id="3797" href="Data.Fin.Dec.html#3700" class="Bound">P</a><a id="3798" class="Symbol">)</a>
  <a id="3802" href="Data.Fin.Dec.html#restrictS" class="Function">restrictS</a> <a id="3812" href="Data.Fin.Dec.html#3812" class="Bound">s</a> <a id="3814" href="Data.Fin.Dec.html#3814" class="Bound">dec</a> <a id="3818" href="Data.Fin.Dec.html#3818" class="Bound">p</a> <a id="3820" class="Symbol">=</a> <a id="3822" href="Data.Fin.Dec.html#3814" class="Bound">dec</a> <a id="3826" class="Symbol">(</a><a id="3827" href="Data.Fin.Dec.html#3812" class="Bound">s</a> <a id="3829" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="3831" href="Data.Fin.Dec.html#3818" class="Bound">p</a><a id="3832" class="Symbol">)</a>

<a id="anySubset?" href="Data.Fin.Dec.html#anySubset%3F" class="Function">anySubset?</a> <a id="3846" class="Symbol">:</a> <a id="3848" class="Symbol">∀</a> <a id="3850" class="Symbol">{</a><a id="3851" href="Data.Fin.Dec.html#3851" class="Bound">n</a><a id="3852" class="Symbol">}</a> <a id="3854" class="Symbol">{</a><a id="3855" href="Data.Fin.Dec.html#3855" class="Bound">P</a> <a id="3857" class="Symbol">:</a> <a id="3859" href="Data.Fin.Subset.html#Subset" class="Function">Subset</a> <a id="3866" href="Data.Fin.Dec.html#3851" class="Bound">n</a> <a id="3868" class="Symbol">→</a> <a id="3870" class="PrimitiveType">Set</a><a id="3873" class="Symbol">}</a> <a id="3875" class="Symbol">→</a>
             <a id="3890" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="3902" href="Data.Fin.Dec.html#3855" class="Bound">P</a> <a id="3904" class="Symbol">→</a> <a id="3906" href="Relation.Nullary.html#Dec" class="Datatype">Dec</a> <a id="3910" class="Symbol">(</a><a id="3911" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="3913" href="Data.Fin.Dec.html#3855" class="Bound">P</a><a id="3914" class="Symbol">)</a>
<a id="3916" href="Data.Fin.Dec.html#anySubset%3F" class="Function">anySubset?</a> <a id="3927" class="Symbol">{</a><a id="3928" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a><a id="3932" class="Symbol">}</a> <a id="3934" class="Symbol">{</a><a id="3935" href="Data.Fin.Dec.html#3935" class="Bound">P</a><a id="3936" class="Symbol">}</a> <a id="3938" href="Data.Fin.Dec.html#3938" class="Bound">dec</a> <a id="3942" class="Keyword">with</a> <a id="3947" href="Data.Fin.Dec.html#3938" class="Bound">dec</a> <a id="3951" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a>
<a id="3954" class="Symbol">...</a> <a id="3958" class="Symbol">|</a> <a id="3960" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="3964" href="Data.Fin.Dec.html#3964" class="Bound">P[]</a> <a id="3968" class="Symbol">=</a> <a id="3970" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="3974" class="Symbol">(_</a> <a id="3977" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="3979" href="Data.Fin.Dec.html#3964" class="Bound">P[]</a><a id="3982" class="Symbol">)</a>
<a id="3984" class="Symbol">...</a> <a id="3988" class="Symbol">|</a> <a id="3990" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="3993" href="Data.Fin.Dec.html#3993" class="Bound">¬P[]</a> <a id="3998" class="Symbol">=</a> <a id="4000" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="4003" href="Data.Fin.Dec.html#4020" class="Function">helper</a>
  <a id="4012" class="Keyword">where</a>
  <a id="4020" href="Data.Fin.Dec.html#4020" class="Function">helper</a> <a id="4027" class="Symbol">:</a> <a id="4029" href="Data.Product.html#%E2%88%84" class="Function">∄</a> <a id="4031" class="Bound">P</a>
  <a id="4035" href="Data.Fin.Dec.html#4020" class="Function">helper</a> <a id="4042" class="Symbol">(</a><a id="4043" href="Data.Vec.html#Vec.%5B%5D" class="InductiveConstructor">[]</a> <a id="4046" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4048" href="Data.Fin.Dec.html#4048" class="Bound">P[]</a><a id="4051" class="Symbol">)</a> <a id="4053" class="Symbol">=</a> <a id="4055" href="Data.Fin.Dec.html#3993" class="Bound">¬P[]</a> <a id="4060" href="Data.Fin.Dec.html#4048" class="Bound">P[]</a>
<a id="4064" href="Data.Fin.Dec.html#anySubset%3F" class="Function">anySubset?</a> <a id="4075" class="Symbol">{</a><a id="4076" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4080" href="Data.Fin.Dec.html#4080" class="Bound">n</a><a id="4081" class="Symbol">}</a> <a id="4083" class="Symbol">{</a><a id="4084" href="Data.Fin.Dec.html#4084" class="Bound">P</a><a id="4085" class="Symbol">}</a> <a id="4087" href="Data.Fin.Dec.html#4087" class="Bound">dec</a> <a id="4091" class="Keyword">with</a> <a id="4096" href="Data.Fin.Dec.html#anySubset%3F" class="Function">anySubset?</a> <a id="4107" class="Symbol">(</a><a id="4108" href="Data.Fin.Dec.html#restrictS" class="Function">restrictS</a> <a id="4118" href="Agda.Builtin.Bool.html#Bool.inside" class="InductiveConstructor">inside</a>  <a id="4126" href="Data.Fin.Dec.html#4087" class="Bound">dec</a><a id="4129" class="Symbol">)</a>
                              <a id="4161" class="Symbol">|</a> <a id="4163" href="Data.Fin.Dec.html#anySubset%3F" class="Function">anySubset?</a> <a id="4174" class="Symbol">(</a><a id="4175" href="Data.Fin.Dec.html#restrictS" class="Function">restrictS</a> <a id="4185" href="Agda.Builtin.Bool.html#Bool.outside" class="InductiveConstructor">outside</a> <a id="4193" href="Data.Fin.Dec.html#4087" class="Bound">dec</a><a id="4196" class="Symbol">)</a>
<a id="4198" class="Symbol">...</a> <a id="4202" class="Symbol">|</a> <a id="4204" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="4208" class="Symbol">(_</a> <a id="4211" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4213" href="Data.Fin.Dec.html#4213" class="Bound">Pp</a><a id="4215" class="Symbol">)</a> <a id="4217" class="Symbol">|</a> <a id="4219" class="Symbol">_</a>            <a id="4232" class="Symbol">=</a> <a id="4234" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="4238" class="Symbol">(_</a> <a id="4241" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4243" href="Data.Fin.Dec.html#4213" class="Bound">Pp</a><a id="4245" class="Symbol">)</a>
<a id="4247" class="CatchallClause Symbol">...</a><a id="4250" class="CatchallClause"> </a><a id="4251" class="CatchallClause Symbol">|</a><a id="4252" class="CatchallClause"> </a><a id="4253" class="CatchallClause Symbol">_</a><a id="4254" class="CatchallClause">            </a><a id="4266" class="CatchallClause Symbol">|</a><a id="4267" class="CatchallClause"> </a><a id="4268" href="Relation.Nullary.html#Dec.yes" class="CatchallClause InductiveConstructor">yes</a><a id="4271" class="CatchallClause"> </a><a id="4272" class="CatchallClause Symbol">(_</a><a id="4274" class="CatchallClause"> </a><a id="4275" href="Data.Product.html#%CE%A3._%2C_" class="CatchallClause InductiveConstructor Operator">,</a><a id="4276" class="CatchallClause"> </a><a id="4277" href="Data.Fin.Dec.html#4277" class="CatchallClause Bound">Pp</a><a id="4279" class="CatchallClause Symbol">)</a> <a id="4281" class="Symbol">=</a> <a id="4283" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="4287" class="Symbol">(_</a> <a id="4290" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4292" href="Data.Fin.Dec.html#4277" class="Bound">Pp</a><a id="4294" class="Symbol">)</a>
<a id="4296" class="Symbol">...</a> <a id="4300" class="Symbol">|</a> <a id="4302" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="4305" href="Data.Fin.Dec.html#4305" class="Bound">¬Pp</a>       <a id="4315" class="Symbol">|</a> <a id="4317" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="4320" href="Data.Fin.Dec.html#4320" class="Bound">¬Pp&#39;</a>      <a id="4330" class="Symbol">=</a> <a id="4332" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="4335" href="Data.Fin.Dec.html#4356" class="Function">helper</a>
    <a id="4346" class="Keyword">where</a>
    <a id="4356" href="Data.Fin.Dec.html#4356" class="Function">helper</a> <a id="4363" class="Symbol">:</a> <a id="4365" href="Data.Product.html#%E2%88%84" class="Function">∄</a> <a id="4367" class="Bound">P</a>
    <a id="4373" href="Data.Fin.Dec.html#4356" class="Function">helper</a> <a id="4380" class="Symbol">(</a><a id="4381" href="Agda.Builtin.Bool.html#Bool.inside" class="InductiveConstructor">inside</a>  <a id="4389" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4391" href="Data.Fin.Dec.html#4391" class="Bound">p</a> <a id="4393" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4395" href="Data.Fin.Dec.html#4395" class="Bound">Pp</a><a id="4397" class="Symbol">)</a>  <a id="4400" class="Symbol">=</a> <a id="4402" href="Data.Fin.Dec.html#4305" class="Bound">¬Pp</a>  <a id="4407" class="Symbol">(_</a> <a id="4410" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4412" href="Data.Fin.Dec.html#4395" class="Bound">Pp</a><a id="4414" class="Symbol">)</a>
    <a id="4420" href="Data.Fin.Dec.html#4356" class="Function">helper</a> <a id="4427" class="Symbol">(</a><a id="4428" href="Agda.Builtin.Bool.html#Bool.outside" class="InductiveConstructor">outside</a> <a id="4436" href="Data.Vec.html#Vec._%E2%88%B7_" class="InductiveConstructor Operator">∷</a> <a id="4438" href="Data.Fin.Dec.html#4438" class="Bound">p</a> <a id="4440" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4442" href="Data.Fin.Dec.html#4442" class="Bound">Pp&#39;</a><a id="4445" class="Symbol">)</a> <a id="4447" class="Symbol">=</a> <a id="4449" href="Data.Fin.Dec.html#4320" class="Bound">¬Pp&#39;</a> <a id="4454" class="Symbol">(_</a> <a id="4457" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4459" href="Data.Fin.Dec.html#4442" class="Bound">Pp&#39;</a><a id="4462" class="Symbol">)</a>

<a id="4465" class="Comment">-- If a decidable predicate P over a finite set is sometimes false,</a>
<a id="4533" class="Comment">-- then we can find the smallest value for which this is the case.</a>

<a id="¬∀⟶∃¬-smallest" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="4616" class="Symbol">:</a>
  <a id="4620" class="Symbol">∀</a> <a id="4622" href="Data.Fin.Dec.html#4622" class="Bound">n</a> <a id="4624" class="Symbol">{</a><a id="4625" href="Data.Fin.Dec.html#4625" class="Bound">p</a><a id="4626" class="Symbol">}</a> <a id="4628" class="Symbol">(</a><a id="4629" href="Data.Fin.Dec.html#4629" class="Bound">P</a> <a id="4631" class="Symbol">:</a> <a id="4633" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="4637" href="Data.Fin.Dec.html#4622" class="Bound">n</a> <a id="4639" class="Symbol">→</a> <a id="4641" class="PrimitiveType">Set</a> <a id="4645" href="Data.Fin.Dec.html#4625" class="Bound">p</a><a id="4646" class="Symbol">)</a> <a id="4648" class="Symbol">→</a> <a id="4650" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="4662" href="Data.Fin.Dec.html#4629" class="Bound">P</a> <a id="4664" class="Symbol">→</a>
  <a id="4668" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="4670" class="Symbol">(∀</a> <a id="4673" href="Data.Fin.Dec.html#4673" class="Bound">i</a> <a id="4675" class="Symbol">→</a> <a id="4677" href="Data.Fin.Dec.html#4629" class="Bound">P</a> <a id="4679" href="Data.Fin.Dec.html#4673" class="Bound">i</a><a id="4680" class="Symbol">)</a> <a id="4682" class="Symbol">→</a> <a id="4684" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="4686" class="Symbol">λ</a> <a id="4688" href="Data.Fin.Dec.html#4688" class="Bound">i</a> <a id="4690" class="Symbol">→</a> <a id="4692" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="4694" href="Data.Fin.Dec.html#4629" class="Bound">P</a> <a id="4696" href="Data.Fin.Dec.html#4688" class="Bound">i</a> <a id="4698" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="4700" class="Symbol">((</a><a id="4702" href="Data.Fin.Dec.html#4702" class="Bound">j</a> <a id="4704" class="Symbol">:</a> <a id="4706" href="Data.Fin.html#Fin%E2%80%B2" class="Function">Fin′</a> <a id="4711" href="Data.Fin.Dec.html#4688" class="Bound">i</a><a id="4712" class="Symbol">)</a> <a id="4714" class="Symbol">→</a> <a id="4716" href="Data.Fin.Dec.html#4629" class="Bound">P</a> <a id="4718" class="Symbol">(</a><a id="4719" href="Data.Fin.html#inject" class="Function">inject</a> <a id="4726" href="Data.Fin.Dec.html#4702" class="Bound">j</a><a id="4727" class="Symbol">))</a>
<a id="4730" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="4745" href="Agda.Builtin.Nat.html#Nat.zero" class="InductiveConstructor">zero</a>    <a id="4753" href="Data.Fin.Dec.html#4753" class="Bound">P</a> <a id="4755" href="Data.Fin.Dec.html#4755" class="Bound">dec</a> <a id="4759" href="Data.Fin.Dec.html#4759" class="Bound">¬∀iPi</a> <a id="4765" class="Symbol">=</a> <a id="4767" href="Data.Empty.html#%E2%8A%A5-elim" class="Function">⊥-elim</a> <a id="4774" class="Symbol">(</a><a id="4775" href="Data.Fin.Dec.html#4759" class="Bound">¬∀iPi</a> <a id="4781" class="Symbol">(λ()))</a>
<a id="4788" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="4803" class="Symbol">(</a><a id="4804" href="Agda.Builtin.Nat.html#Nat.suc" class="InductiveConstructor">suc</a> <a id="4808" href="Data.Fin.Dec.html#4808" class="Bound">n</a><a id="4809" class="Symbol">)</a> <a id="4811" href="Data.Fin.Dec.html#4811" class="Bound">P</a> <a id="4813" href="Data.Fin.Dec.html#4813" class="Bound">dec</a> <a id="4817" href="Data.Fin.Dec.html#4817" class="Bound">¬∀iPi</a> <a id="4823" class="Keyword">with</a> <a id="4828" href="Data.Fin.Dec.html#4813" class="Bound">dec</a> <a id="4832" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>
<a id="4837" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="4852" class="Symbol">(</a><a id="4853" class="InductiveConstructor">suc</a> <a id="4857" href="Data.Fin.Dec.html#4857" class="Bound">n</a><a id="4858" class="Symbol">)</a> <a id="4860" href="Data.Fin.Dec.html#4860" class="Bound">P</a> <a id="4862" href="Data.Fin.Dec.html#4862" class="Bound">dec</a> <a id="4866" href="Data.Fin.Dec.html#4866" class="Bound">¬∀iPi</a> <a id="4872" class="Symbol">|</a> <a id="4874" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="4877" href="Data.Fin.Dec.html#4877" class="Bound">¬P0</a> <a id="4881" class="Symbol">=</a> <a id="4883" class="Symbol">(</a><a id="4884" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a> <a id="4889" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4891" href="Data.Fin.Dec.html#4877" class="Bound">¬P0</a> <a id="4895" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="4897" class="Symbol">λ</a> <a id="4899" class="Symbol">())</a>
<a id="4903" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="4918" class="Symbol">(</a><a id="4919" class="InductiveConstructor">suc</a> <a id="4923" href="Data.Fin.Dec.html#4923" class="Bound">n</a><a id="4924" class="Symbol">)</a> <a id="4926" href="Data.Fin.Dec.html#4926" class="Bound">P</a> <a id="4928" href="Data.Fin.Dec.html#4928" class="Bound">dec</a> <a id="4932" href="Data.Fin.Dec.html#4932" class="Bound">¬∀iPi</a> <a id="4938" class="Symbol">|</a> <a id="4940" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="4944" href="Data.Fin.Dec.html#4944" class="Bound">P0</a> <a id="4947" class="Symbol">=</a>
  <a id="4951" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="4960" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="4964" class="Symbol">(</a><a id="4965" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="4974" href="Function.html#id" class="Function">id</a> <a id="4977" href="Data.Fin.Dec.html#5180" class="Function">extend′</a><a id="4984" class="Symbol">)</a> <a id="4986" href="Function.html#_%24_" class="Function Operator">$</a>
    <a id="4992" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="5007" href="Data.Fin.Dec.html#4923" class="Bound">n</a> <a id="5009" class="Symbol">(λ</a> <a id="5012" href="Data.Fin.Dec.html#5012" class="Bound">n</a> <a id="5014" class="Symbol">→</a> <a id="5016" href="Data.Fin.Dec.html#4926" class="Bound">P</a> <a id="5018" class="Symbol">(</a><a id="5019" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5023" href="Data.Fin.Dec.html#5012" class="Bound">n</a><a id="5024" class="Symbol">))</a> <a id="5027" class="Symbol">(</a><a id="5028" href="Data.Fin.Dec.html#4928" class="Bound">dec</a> <a id="5032" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5034" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a><a id="5037" class="Symbol">)</a> <a id="5039" class="Symbol">(</a><a id="5040" href="Data.Fin.Dec.html#4932" class="Bound">¬∀iPi</a> <a id="5046" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="5048" href="Data.Fin.Dec.html#5066" class="Function">extend</a><a id="5054" class="Symbol">)</a>
  <a id="5058" class="Keyword">where</a>
  <a id="5066" href="Data.Fin.Dec.html#5066" class="Function">extend</a> <a id="5073" class="Symbol">:</a> <a id="5075" class="Symbol">(∀</a> <a id="5078" href="Data.Fin.Dec.html#5078" class="Bound">i</a> <a id="5080" class="Symbol">→</a> <a id="5082" href="Data.Fin.Dec.html#4926" class="Bound">P</a> <a id="5084" class="Symbol">(</a><a id="5085" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5089" href="Data.Fin.Dec.html#5078" class="Bound">i</a><a id="5090" class="Symbol">))</a> <a id="5093" class="Symbol">→</a> <a id="5095" class="Symbol">(∀</a> <a id="5098" href="Data.Fin.Dec.html#5098" class="Bound">i</a> <a id="5100" class="Symbol">→</a> <a id="5102" href="Data.Fin.Dec.html#4926" class="Bound">P</a> <a id="5104" href="Data.Fin.Dec.html#5098" class="Bound">i</a><a id="5105" class="Symbol">)</a>
  <a id="5109" href="Data.Fin.Dec.html#5066" class="Function">extend</a> <a id="5116" href="Data.Fin.Dec.html#5116" class="Bound">∀iP[1+i]</a> <a id="5125" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>    <a id="5133" class="Symbol">=</a> <a id="5135" href="Data.Fin.Dec.html#4944" class="Bound">P0</a>
  <a id="5140" href="Data.Fin.Dec.html#5066" class="Function">extend</a> <a id="5147" href="Data.Fin.Dec.html#5147" class="Bound">∀iP[1+i]</a> <a id="5156" class="Symbol">(</a><a id="5157" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5161" href="Data.Fin.Dec.html#5161" class="Bound">i</a><a id="5162" class="Symbol">)</a> <a id="5164" class="Symbol">=</a> <a id="5166" href="Data.Fin.Dec.html#5147" class="Bound">∀iP[1+i]</a> <a id="5175" href="Data.Fin.Dec.html#5161" class="Bound">i</a>

  <a id="5180" href="Data.Fin.Dec.html#5180" class="Function">extend′</a> <a id="5188" class="Symbol">:</a> <a id="5190" class="Symbol">∀</a> <a id="5192" class="Symbol">{</a><a id="5193" href="Data.Fin.Dec.html#5193" class="Bound">i</a> <a id="5195" class="Symbol">:</a> <a id="5197" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5201" href="Data.Fin.Dec.html#4923" class="Bound">n</a><a id="5202" class="Symbol">}</a> <a id="5204" class="Symbol">→</a>
            <a id="5218" class="Symbol">((</a><a id="5220" href="Data.Fin.Dec.html#5220" class="Bound">j</a> <a id="5222" class="Symbol">:</a> <a id="5224" href="Data.Fin.html#Fin%E2%80%B2" class="Function">Fin′</a> <a id="5229" href="Data.Fin.Dec.html#5193" class="Bound">i</a><a id="5230" class="Symbol">)</a> <a id="5232" class="Symbol">→</a> <a id="5234" href="Data.Fin.Dec.html#4926" class="Bound">P</a> <a id="5236" class="Symbol">(</a><a id="5237" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5241" class="Symbol">(</a><a id="5242" href="Data.Fin.html#inject" class="Function">inject</a> <a id="5249" href="Data.Fin.Dec.html#5220" class="Bound">j</a><a id="5250" class="Symbol">)))</a> <a id="5254" class="Symbol">→</a>
            <a id="5268" class="Symbol">((</a><a id="5270" href="Data.Fin.Dec.html#5270" class="Bound">j</a> <a id="5272" class="Symbol">:</a> <a id="5274" href="Data.Fin.html#Fin%E2%80%B2" class="Function">Fin′</a> <a id="5279" class="Symbol">(</a><a id="5280" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5284" href="Data.Fin.Dec.html#5193" class="Bound">i</a><a id="5285" class="Symbol">))</a> <a id="5288" class="Symbol">→</a> <a id="5290" href="Data.Fin.Dec.html#4926" class="Bound">P</a> <a id="5292" class="Symbol">(</a><a id="5293" href="Data.Fin.html#inject" class="Function">inject</a> <a id="5300" href="Data.Fin.Dec.html#5270" class="Bound">j</a><a id="5301" class="Symbol">))</a>
  <a id="5306" href="Data.Fin.Dec.html#5180" class="Function">extend′</a> <a id="5314" href="Data.Fin.Dec.html#5314" class="Bound">g</a> <a id="5316" href="Data.Fin.html#Fin.zero" class="InductiveConstructor">zero</a>    <a id="5324" class="Symbol">=</a> <a id="5326" href="Data.Fin.Dec.html#4944" class="Bound">P0</a>
  <a id="5331" href="Data.Fin.Dec.html#5180" class="Function">extend′</a> <a id="5339" href="Data.Fin.Dec.html#5339" class="Bound">g</a> <a id="5341" class="Symbol">(</a><a id="5342" href="Data.Fin.html#Fin.suc" class="InductiveConstructor">suc</a> <a id="5346" href="Data.Fin.Dec.html#5346" class="Bound">j</a><a id="5347" class="Symbol">)</a> <a id="5349" class="Symbol">=</a> <a id="5351" href="Data.Fin.Dec.html#5339" class="Bound">g</a> <a id="5353" href="Data.Fin.Dec.html#5346" class="Bound">j</a>


<a id="5357" class="Comment">-- When P is a decidable predicate over a finite set the following</a>
<a id="5424" class="Comment">-- lemma can be proved.</a>

<a id="¬∀⟶∃¬" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC" class="Function">¬∀⟶∃¬</a> <a id="5455" class="Symbol">:</a> <a id="5457" class="Symbol">∀</a> <a id="5459" href="Data.Fin.Dec.html#5459" class="Bound">n</a> <a id="5461" class="Symbol">{</a><a id="5462" href="Data.Fin.Dec.html#5462" class="Bound">p</a><a id="5463" class="Symbol">}</a> <a id="5465" class="Symbol">(</a><a id="5466" href="Data.Fin.Dec.html#5466" class="Bound">P</a> <a id="5468" class="Symbol">:</a> <a id="5470" href="Data.Fin.html#Fin" class="Datatype">Fin</a> <a id="5474" href="Data.Fin.Dec.html#5459" class="Bound">n</a> <a id="5476" class="Symbol">→</a> <a id="5478" class="PrimitiveType">Set</a> <a id="5482" href="Data.Fin.Dec.html#5462" class="Bound">p</a><a id="5483" class="Symbol">)</a> <a id="5485" class="Symbol">→</a> <a id="5487" href="Relation.Unary.html#Decidable" class="Function">U.Decidable</a> <a id="5499" href="Data.Fin.Dec.html#5466" class="Bound">P</a> <a id="5501" class="Symbol">→</a>
        <a id="5511" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="5513" class="Symbol">(∀</a> <a id="5516" href="Data.Fin.Dec.html#5516" class="Bound">i</a> <a id="5518" class="Symbol">→</a> <a id="5520" href="Data.Fin.Dec.html#5466" class="Bound">P</a> <a id="5522" href="Data.Fin.Dec.html#5516" class="Bound">i</a><a id="5523" class="Symbol">)</a> <a id="5525" class="Symbol">→</a> <a id="5527" href="Data.Product.html#%E2%88%83" class="Function">∃</a> <a id="5529" class="Symbol">λ</a> <a id="5531" href="Data.Fin.Dec.html#5531" class="Bound">i</a> <a id="5533" class="Symbol">→</a> <a id="5535" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="5537" href="Data.Fin.Dec.html#5466" class="Bound">P</a> <a id="5539" href="Data.Fin.Dec.html#5531" class="Bound">i</a>
<a id="5541" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC" class="Function">¬∀⟶∃¬</a> <a id="5547" href="Data.Fin.Dec.html#5547" class="Bound">n</a> <a id="5549" href="Data.Fin.Dec.html#5549" class="Bound">P</a> <a id="5551" href="Data.Fin.Dec.html#5551" class="Bound">dec</a> <a id="5555" href="Data.Fin.Dec.html#5555" class="Bound">¬P</a> <a id="5558" class="Symbol">=</a> <a id="5560" href="Data.Product.html#map" class="Function">Prod.map</a> <a id="5569" href="Function.html#id" class="Function">id</a> <a id="5572" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="5578" href="Function.html#_%24_" class="Function Operator">$</a> <a id="5580" href="Data.Fin.Dec.html#%C2%AC%E2%88%80%E2%9F%B6%E2%88%83%C2%AC-smallest" class="Function">¬∀⟶∃¬-smallest</a> <a id="5595" href="Data.Fin.Dec.html#5547" class="Bound">n</a> <a id="5597" href="Data.Fin.Dec.html#5549" class="Bound">P</a> <a id="5599" href="Data.Fin.Dec.html#5551" class="Bound">dec</a> <a id="5603" href="Data.Fin.Dec.html#5555" class="Bound">¬P</a>

<a id="5607" class="Comment">-- Decision procedure for _⊆_ (obtained via the natural lattice</a>
<a id="5671" class="Comment">-- order).</a>

<a id="5683" class="Keyword">infix</a> <a id="5689" class="Number">4</a> <a id="5691" href="Data.Fin.Dec.html#_%E2%8A%86%3F_" class="Function Operator">_⊆?_</a>

<a id="_⊆?_" href="Data.Fin.Dec.html#_%E2%8A%86%3F_" class="Function Operator">_⊆?_</a> <a id="5702" class="Symbol">:</a> <a id="5704" class="Symbol">∀</a> <a id="5706" class="Symbol">{</a><a id="5707" href="Data.Fin.Dec.html#5707" class="Bound">n</a><a id="5708" class="Symbol">}</a> <a id="5710" class="Symbol">→</a> <a id="5712" href="Relation.Binary.Core.html#Decidable" class="Function">B.Decidable</a> <a id="5724" class="Symbol">(</a><a id="5725" href="Data.Fin.Subset.html#_%E2%8A%86_" class="Function Operator">_⊆_</a> <a id="5729" class="Symbol">{</a><a id="5730" class="Argument">n</a> <a id="5732" class="Symbol">=</a> <a id="5734" href="Data.Fin.Dec.html#5707" class="Bound">n</a><a id="5735" class="Symbol">})</a>
<a id="5738" href="Data.Fin.Dec.html#5738" class="Bound">p₁</a> <a id="5741" href="Data.Fin.Dec.html#_%E2%8A%86%3F_" class="Function Operator">⊆?</a> <a id="5744" href="Data.Fin.Dec.html#5744" class="Bound">p₂</a> <a id="5747" class="Symbol">=</a>
  <a id="5751" href="Relation.Nullary.Decidable.html#map" class="Function">Dec.map</a> <a id="5759" class="Symbol">(</a><a id="5760" href="Function.Equivalence.html#sym" class="Function">Eq.sym</a> <a id="5767" href="Data.Fin.Subset.Properties.html#NaturalPoset.orders-equivalent" class="Function">NaturalPoset.orders-equivalent</a><a id="5797" class="Symbol">)</a> <a id="5799" href="Function.html#_%24_" class="Function Operator">$</a>
  <a id="5803" href="Relation.Nullary.Decidable.html#map%E2%80%B2" class="Function">Dec.map′</a> <a id="5812" href="Data.Vec.Equality.html#PropositionalEquality.to-%E2%89%A1" class="Function">PropVecEq.to-≡</a> <a id="5827" href="Data.Vec.Equality.html#PropositionalEquality.from-%E2%89%A1" class="Function">PropVecEq.from-≡</a> <a id="5844" href="Function.html#_%24_" class="Function Operator">$</a>
  <a id="5848" href="Data.Vec.Equality.html#DecidableEquality._%E2%89%9F_" class="Function Operator">VecEq.DecidableEquality._≟_</a> <a id="5876" href="Data.Bool.html#decSetoid" class="Function">Bool.decSetoid</a> <a id="5891" href="Data.Fin.Dec.html#5738" class="Bound">p₁</a> <a id="5894" class="Symbol">(</a><a id="5895" href="Data.Fin.Dec.html#5738" class="Bound">p₁</a> <a id="5898" href="Algebra.html#Fin.Subset.BA._%E2%88%A9_" class="Function Operator">∩</a> <a id="5900" href="Data.Fin.Dec.html#5744" class="Bound">p₂</a><a id="5902" class="Symbol">)</a>
</pre></body></html>

APT Browse - Built by Thomas Orozco.