<div dir="ltr">Ulf,<div><br></div><div>Any further progress with this?</div><div><br></div><div>Wen downloaded HEAD, but cannot execute even four steps of reduction on his 2010 MacBook Pro. </div><div><br></div><div>I have not downloaded HEAD (I'm cautious about Agda updates because if I break Agda I'm on my own trying to fix it). With the version below, four steps of reduction takes five minutes, and full reduction does not complete overnight.</div><div><br></div><div>I'm wondering if perhaps the issue is not version of Agda but available memory? How much is on your machine?</div><div><br></div><div>Any other progress at tracking down what the issue might be?</div><div><br></div><div>Thank you very much for your help. Cheers, -- P</div><div><br></div><div> </div><div><br></div><div> Agda version 2.6.0-4654bfb-dirty</div><div>
<span></span>
<p class="gmail-p1" style="margin:0px 0px 0px 160.7px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>System Version:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>macOS 10.12.6 (16G29)</p>
<p class="gmail-p1" style="margin:0px 0px 0px 160.7px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Kernel Version:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>Darwin 16.7.0</p>
<p class="gmail-p1" style="margin:0px 0px 0px 160.7px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Boot Volume:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>Macintosh HD</p>
</div><div>
<span></span>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Model Name:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>MacBook Pro</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Model Identifier:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>MacBookPro11,5</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Processor Name:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>Intel Core i7</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Processor Speed:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>2.8 GHz</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Number of Processors:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>1</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Total Number of Cores:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>4</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>L2 Cache (per Core):<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>256 KB</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>L3 Cache:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>6 MB</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Memory:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>16 GB</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>Boot ROM Version:<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>MBP114.0172.B25</p>
<p class="gmail-p1" style="margin:0px 0px 0px 140.5px;font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:11px;line-height:normal;font-family:"Helvetica Neue""><span class="gmail-Apple-converted-space"> </span>SMC Version (system):<span class="gmail-Apple-tab-span" style="white-space:pre"> </span>2.30f2</p>
<br></div></div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
<br><div class="gmail_quote">On 4 May 2018 at 16:30, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div><div><div>Something is indeed strange. Some observations:<br><br></div><div>- _x_1862 is an unsolved metavariable. If I paste in the term in your example there<br></div><div> is indeed some yellow. When printing a term Agda hides all implicit arguments without<br></div><div> regard for whether they can actually be inferred (since this is impractical to figure out).<br></div><div> This means that you often cannot take a printed term and type check it without ending<br></div><div> up with some yellow.<br></div><div><br></div>- On recent development Agda I can normalise (C-c C-n) `normalise 15 ⊢four`<br> in a handful of milliseconds. (It requires 15 fuel, and since you forgot the Suc<br></div> in the recursive case of ⊢plus, normalises to two instead of four).<br></div> However, trying to prove that it reaches a normal form I get stuck:<br><br><div style="margin-left:40px"><span style="font-family:monospace,monospace">IsNormal : ∀ {M A} {⊢M : ε ⊢ M ⦂ A} → Normalise ⊢M → Set<br>IsNormal (out-of-gas _ _) = ⊥<br>IsNormal (normal _ _ _) = ⊤<br><br>prf : IsNormal (normalise 15 ⊢four)<br>prf = tt -- does not come back<br></span></div><br></div> On the other hand the following variant works fine:<br><br><div style="margin-left:40px"><span style="font-family:monospace,monospace">prf' : IsNormal (normalise 15 ⊢four) ≡ ⊤<br>prf' = refl -- checks in no time<br></span></div><br></div>It's all very mysterious. I'll investigate deeper when I get a chance.<br><div><br>/ Ulf<br></div></div><div class="gmail_extra"><br><div class="gmail_quote"><div><div class="h5">On Fri, May 4, 2018 at 7:44 PM, Philip Wadler <span dir="ltr"><<a href="mailto:wadler@inf.ed.ac.uk" target="_blank">wadler@inf.ed.ac.uk</a>></span> wrote:<br></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><div dir="ltr">I have an Agda formalisation of reduction on raw terms (inspired by a formalisation of McBride acting on a deBruijn representation). The formalisation is here:<div><br></div><div> <a href="https://wenkokke.github.io/sf/TypedFresh" target="_blank">https://wenkokke.github.io/s<wbr>f/TypedFresh</a></div><div><br></div><div>Although more elaborate than I would like in parts, at least I succeed in proving progress and preservation for the system. Combining the two allows me to write a function that computes the reduction sequence for a term bounding by a given length. If the reduction sequence is longer than the specified length n, it returns the sequence of length n with the indicator "out of gas". I then tried to compute the reduction sequence for two plus two. </div><div><br></div><div>Computing the first four reduction steps takes a couple of minutes rather than a couple of seconds. Attempting to normalise the term fully (which should take fourteen reduction steps) does not complete even if run overnight!</div><div><br><pre class="m_-175859399968362365m_1859021589596388910gmail-Agda" style="margin:0px 0px 15px;padding:0.4em;font-size:0.85em;border:1px solid rgb(201,225,246);border-radius:3px;background:rgb(232,242,251);overflow-x:auto;font-family:"Source Code Pro",Consolas,Menlo,Monaco,"Lucida Console","Liberation Mono","DejaVu Sans Mono","Bitstream Vera Sans Mono","Courier New",monospace,serif;color:rgb(17,17,17);font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><a id="m_-175859399968362365m_1859021589596388910gmail-19561" class="m_-175859399968362365m_1859021589596388910gmail-Comment" style="color:rgb(178,34,34);text-decoration:none">{-
_ : normalise 4 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟨ ξ-·₁ (ξ-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟨ ξ-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ 0 ⇒
`if0 `suc (`suc `zero) then ` 0 else
(`Y
(`λ 1 ⇒
(`λ 2 ⇒ (`λ 3 ⇒ `if0 ` 2 then ` 3 else ` 1 · (`pred ` 2) · ` 3))))
· (`pred (`suc (`suc `zero)))
· ` 0)
· (`suc (`suc `zero))
⟶⟨ β-⇒ (Suc (Suc Zero)) ⟩
`if0 `suc (`suc `zero) then `suc (`suc `zero) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
⟶⟨ β-if0-suc (Suc Zero) ⟩
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred (`suc (`suc `zero)))
· (`suc (`suc `zero))
∎)
_ = refl
-}</a></pre><p style="margin:0px 0px 15px;padding:0px;color:rgb(17,17,17);font-family:-apple-system,system-ui,"Segoe UI",Roboto,Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:16px;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(253,253,253);text-decoration-style:initial;text-decoration-color:initial">To try to uncover the problem, I attempted a single step at a time. The first reduction step is fine.</p><pre class="m_-175859399968362365m_1859021589596388910gmail-Agda" style="margin:0px 0px 15px;padding:0.4em;font-size:0.85em;border:1px solid rgb(201,225,246);border-radius:3px;background:rgb(232,242,251);overflow-x:auto;font-family:"Source Code Pro",Consolas,Menlo,Monaco,"Lucida Console","Liberation Mono","DejaVu Sans Mono","Bitstream Vera Sans Mono","Courier New",monospace,serif;color:rgb(17,17,17);font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><a id="m_-175859399968362365m_1859021589596388910gmail-20814" class="m_-175859399968362365m_1859021589596388910gmail-Comment" style="color:rgb(178,34,34);text-decoration:none">{-
_ : normalise 1 ⊢four ≡
out-of-gas
((`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟨ ξ-·₁ (ξ-·₁ (β-Y Fun refl)) ⟩
(`λ 0 ⇒
(`λ 1 ⇒
`if0 ` 0 then ` 1 else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` 0)
· ` 1))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
_ = refl
-}</a></pre>The second reduction step yields a huge term. It contains the free variable _x_1862 where I would have expected a fresh variable name to be computed. Looking at the four-step reduction above we see the name computed properly, but when going from the first step to the second it is not. The huge size of the type derivation suggests why it did not terminate after one day.<br><br>Help! Why doesn’t the term reduce? Is there some way to force it to reduce?</div><div><br></div><div>Cheers, -- P</div><div><br><pre class="m_-175859399968362365m_1859021589596388910gmail-Agda" style="margin:0px 0px 15px;padding:0.4em;font-size:0.85em;border:1px solid rgb(201,225,246);border-radius:3px;background:rgb(232,242,251);overflow-x:auto;font-family:"Source Code Pro",Consolas,Menlo,Monaco,"Lucida Console","Liberation Mono","DejaVu Sans Mono","Bitstream Vera Sans Mono","Courier New",monospace,serif;color:rgb(17,17,17);font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;word-spacing:0px;text-decoration-style:initial;text-decoration-color:initial"><a id="m_-175859399968362365m_1859021589596388910gmail-22098" class="m_-175859399968362365m_1859021589596388910gmail-Comment" style="color:rgb(178,34,34);text-decoration:none">{-
_ : normalise 1
(⊢λ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z)
(⊢Y
(⊢λ
(⊢λ
(⊢λ
(⊢if0 (Ax (S m≢n Z)) (Ax Z)
(Ax (S p≢n (S p≢m Z)) · ⊢pred (Ax (S m≢n Z)) · Ax Z)))))
· ⊢pred (Ax (S (fresh-lemma CollectionDec.here) Z))
· Ax Z)))
· ⊢suc (⊢suc ⊢zero)
· ⊢suc (⊢suc ⊢zero))
≡
out-of-gas
((`λ _x_1862 ⇒
(`λ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ⇒
`if0 ` _x_1862 then
` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)) else
(`Y
(`λ 0 ⇒
(`λ 1 ⇒ (`λ 2 ⇒ `if0 ` 1 then ` 2 else ` 0 · (`pred ` 1) · ` 2))))
· (`pred ` _x_1862)
· ` (suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))))
· (`suc (`suc `zero))
· (`suc (`suc `zero))
⟶⟨ ξ-·₁ (β-⇒ (Suc (Suc Zero))) ⟩
(`λ
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
`if0
(((λ w →
((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
then
(((λ w →
((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
else
(`Y
(`λ
suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))
⇒
(`λ
suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⇒
(`λ
suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⇒
`if0
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
then
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
else
`
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
·
(`pred
`
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))
·
`
(suc
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))))))
⊔
(suc
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
(suc
(foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
⊔
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬?
(_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))))))))
·
(`pred
(((λ w →
((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
_x_1862
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
·
(((λ w →
((λ x → ` x) , _x_1862 ↦ `suc (`suc `zero)) w | w ≟ _x_1862)
, suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ↦
`
foldr _⊔_ 0
(map suc
(filter (λ x → ¬? (x ≟ _x_1862))
(filter
(λ x → ¬? (x ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
(_x_1862 ∷
[ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) , _x_1862 ,
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ])
| ¬? (_x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))))))
(suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005))
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_2005) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887)))
· (`suc (`suc `zero))
∎)
(⊢λ
(⊢if0
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈) CollectionDec.here
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(S (fresh-lemma CollectionDec.here) Z)
| _x_1862 ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016)
(CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there CollectionDec.here)
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
Z
| suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887) ≟
suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(⊢subst
(λ {w} w∈′ {z₁} →
.Typed.Σ′
(λ {w₁} w∈ {z₂} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w₁ ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016) w∈′
| w ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
(.Typed.⊢ρ′
(λ {w} w∈ {z₁} y∈ →
.Typed.Σ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)) w∈ y∈
| w ≟ _x_1862)
(.Typed.⊢ρ
(⊢λ
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(⊢suc (⊢suc ⊢zero)))
(λ {_} x∈ → x∈)
(⊢if0 (Ax (S (fresh-lemma CollectionDec.here) Z)) (Ax Z) _2016))
(λ {z₁} x →
CollectionDec.\\-to-∷ ℕ _≟_ (λ {_} x∈ → x∈)
(CollectionDec.there (CollectionDec.there x))
| z₁ ≟ suc _x_1862 ⊔ foldr _⊔_ 0 (map suc _xs_1887))
_2016))
· ⊢suc (⊢suc ⊢zero))
-}</a></pre><br></div><div><div><br><br>. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br>. / \ and Senior Research Fellow, IOHK<div><div><div class="m_-175859399968362365m_1859021589596388910gmail_signature"><div dir="ltr"><div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/<wbr>wadler/</a></span></div></div></div></div></div>
</div></div></div></div>
<br></div></div>The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br></blockquote></div><br></div>
</blockquote></div><br></div>