From 59ca4775b9882e3d0e0295fc44632a6b618fc121 Mon Sep 17 00:00:00 2001 From: "github-merge-queue[bot]" Date: Thu, 14 Nov 2024 11:44:09 +0000 Subject: [PATCH] =?UTF-8?q?Deploying=20to=20web=20from=20@=20plfa/plfa.git?= =?UTF-8?q?hub.io@c2314e96e8f272bcabe3aae6ee216c7432ed93fc=20=F0=9F=9A=80?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Negation/index.html | 66 +++++++++++++++--------------- TSPL/2022/Assignment2/index.html | 2 +- TSPL/2023/Assignment2/index.html | 2 +- TSPL/2024/Assignment2/index.html | 2 +- plfa.epub | Bin 4835670 -> 4835652 bytes plfa.html | 68 +++++++++++++++---------------- rss.xml | 2 +- 7 files changed, 71 insertions(+), 71 deletions(-) diff --git a/Negation/index.html b/Negation/index.html index 3dfe8876e..ffcc63385 100644 --- a/Negation/index.html +++ b/Negation/index.html @@ -29,40 +29,40 @@ → ¬ ¬ ¬ A ------- → ¬ A -¬¬¬-elim ¬¬¬x = λ x → ¬¬¬x (¬¬-intro x) -

Let ¬¬¬x be evidence of ¬ ¬ ¬ A. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then by the previous result, we can conclude ¬ ¬ A, evidenced by ¬¬-intro x. Then from ¬ ¬ ¬ A and ¬ ¬ A we have a contradiction, evidenced by ¬¬¬x (¬¬-intro x). Hence we have shown ¬ A.

Another law of logic is contraposition, stating that if A implies B, then ¬ B implies ¬ A:
contraposition : ∀ {A B : Set}
-  → (A → B)
-    -----------
-  → (¬ B → ¬ A)
-contraposition f ¬y x = ¬y (f x)
-

Let f be evidence of A → B and let ¬y be evidence of ¬ B. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then from A → B and A we may conclude B, evidenced by f x, and from B and ¬ B we may conclude ⊥, evidenced by ¬y (f x). Hence, we have shown ¬ A.

Using negation, it is straightforward to define inequality:
_≢_ : ∀ {A : Set} → A → A → Set
-x ≢ y  =  ¬ (x ≡ y)
-
It is trivial to show distinct numbers are not equal:
_ : 1 ≢ 2
-_ = λ()
-
This is our first use of an absurd pattern in a lambda expression. The type M ≡ N is occupied exactly when M and N simplify to identical terms. Since 1 and 2 simplify to distinct normal forms, Agda determines that there is no possible evidence that 1 ≡ 2. As a second example, it is also easy to validate Peano’s postulate that zero is not the successor of any number:
peano : ∀ {m : ℕ} → zero ≢ suc m
-peano = λ()
+¬¬¬-elim ¬¬¬x x  =  ¬¬¬x (¬¬-intro x)
+

Let ¬¬¬x be evidence of ¬ ¬ ¬ A. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then by the previous result, we can conclude ¬ ¬ A, evidenced by ¬¬-intro x. Then from ¬ ¬ ¬ A and ¬ ¬ A we have a contradiction, evidenced by ¬¬¬x (¬¬-intro x). Hence we have shown ¬ A.

Another law of logic is contraposition, stating that if A implies B, then ¬ B implies ¬ A:
contraposition : ∀ {A B : Set}
+  → (A → B)
+    -----------
+  → (¬ B → ¬ A)
+contraposition f ¬y x = ¬y (f x)
+

Let f be evidence of A → B and let ¬y be evidence of ¬ B. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then from A → B and A we may conclude B, evidenced by f x, and from B and ¬ B we may conclude ⊥, evidenced by ¬y (f x). Hence, we have shown ¬ A.

Using negation, it is straightforward to define inequality:
_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y  =  ¬ (x ≡ y)
+
It is trivial to show distinct numbers are not equal:
_ : 1 ≢ 2
+_ = λ()
+
This is our first use of an absurd pattern in a lambda expression. The type M ≡ N is occupied exactly when M and N simplify to identical terms. Since 1 and 2 simplify to distinct normal forms, Agda determines that there is no possible evidence that 1 ≡ 2. As a second example, it is also easy to validate Peano’s postulate that zero is not the successor of any number:
peano : ∀ {m : ℕ} → zero ≢ suc m
+peano = λ()

The evidence is essentially the same, as the absurd pattern matches all possible evidence of type zero ≡ suc m.

Given the correspondence of implication to exponentiation and false to the type with no members, we can view negation as raising to the zero power. This indeed corresponds to what we know for arithmetic, where

0 ^ n  ≡  1,  if n ≡ 0
-       ≡  0,  if n ≢ 0
Indeed, there is exactly one proof of ⊥ → ⊥. We can write this proof two different ways:
id : ⊥ → ⊥
-id x = x
+       ≡  0,  if n ≢ 0
Indeed, there is exactly one proof of ⊥ → ⊥. We can write this proof two different ways:
id : ⊥ → ⊥
+id x = x
 
-id′ : ⊥ → ⊥
-id′ ()
-
But, using extensionality, we can prove these equal:
id≡id′ : id ≡ id′
-id≡id′ = extensionality (λ())
-

By extensionality, id ≡ id′ holds if for every x in their domain we have id x ≡ id′ x. But there is no x in their domain, so the equality holds trivially.

Indeed, we can show any two proofs of a negation are equal:
assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
-assimilation ¬x ¬x′ = extensionality (λ x → contradiction x ¬x)
-

Evidence for ¬ A implies that any evidence of A immediately leads to a contradiction. But extensionality quantifies over all x such that A holds, hence any such x immediately leads to a contradiction, again causing the equality to hold trivially.

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

-- Your code goes here
-

Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

-- Your code goes here
-

Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

-- Your code goes here
-

Do we also have the following?

¬ (A × B) ≃ (¬ A) ⊎ (¬ B)

If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?

Intuitive and Classical logic

In Gilbert and Sullivan’s The Gondoliers, Casilda is told that as an infant she was married to the heir of the King of Batavia, but that due to a mix-up no one knows which of two individuals, Marco or Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say that I am married to one of two gondoliers, but it is impossible to say which?” To which the response is “Without any doubt of any kind whatever.”

Logic comes in many varieties, and one distinction is between classical and intuitionistic. Intuitionists, concerned by assumptions made by some logicians about the nature of infinity, insist upon a constructionist notion of truth. In particular, they insist that a proof of A ⊎ B must show which of A or B holds, and hence they would reject the claim that Casilda is married to Marco or Giuseppe until one of the two was identified as her husband. Perhaps Gilbert and Sullivan anticipated intuitionism, for their story’s outcome is that the heir turns out to be a third individual, Luiz, with whom Casilda is, conveniently, already in love.

Intuitionists also reject the law of the excluded middle, which asserts A ⊎ ¬ A for every A, since the law gives no clue as to which of A or ¬ A holds. Heyting formalised a variant of Hilbert’s classical logic that captures the intuitionistic notion of provability. In particular, the law of the excluded middle is provable in Hilbert’s logic, but not in Heyting’s. Further, if the law of the excluded middle is added as an axiom to Heyting’s logic, then it becomes equivalent to Hilbert’s. Kolmogorov showed the two logics were closely related: he gave a double-negation translation, such that a formula is provable in classical logic if and only if its translation is provable in intuitionistic logic.

Propositions as Types was first formulated for intuitionistic logic. It is a perfect fit, because in the intuitionist interpretation the formula A ⊎ B is provable exactly when one exhibits either a proof of A or a proof of B, so the type corresponding to disjunction is a disjoint sum.

(Parts of the above are adopted from “Propositions as Types”, Philip Wadler, Communications of the ACM, December 2015.)

Excluded middle is irrefutable

The law of the excluded middle can be formulated as follows:
postulate
-  em : ∀ {A : Set} → A ⊎ ¬ A
-
As we noted, the law of the excluded middle does not hold in intuitionistic logic. However, we can show that it is irrefutable, meaning that the negation of its negation is provable (and hence that its negation is never provable):
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
-em-irrefutable = λ k → k (inj₂ (λ x → k (inj₁ x)))
-

The best way to explain this code is to develop it interactively:

em-irrefutable k = ?

Given evidence k that ¬ (A ⊎ ¬ A), that is, a function that given a value of type A ⊎ ¬ A returns a value of the empty type, we must fill in ? with a term that returns a value of the empty type. The only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k ?

We need to fill the new hole with a value of type A ⊎ ¬ A. We don’t have a value of type A to hand, so let’s pick the second disjunct:

em-irrefutable k = k (inj₂ λ{ x → ? })

The second disjunct accepts evidence of ¬ A, that is, a function that given a value of type A returns a value of the empty type. We bind x to the value of type A, and now we need to fill in the hole with a value of the empty type. Once again, the only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k (inj₂ λ{ x → k ? })

This time we do have a value of type A to hand, namely x, so we can pick the first disjunct:

em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })

There are no holes left! This completes the proof.

The following story illustrates the behaviour of the term we have created. (With apologies to Peter Selinger, who tells a similar story about a king, a wizard, and the Philosopher’s stone.)

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realised that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said, “Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

(Parts of the above are adopted from “Call-by-Value is Dual to Call-by-Name”, Philip Wadler, International Conference on Functional Programming, 2003.)

Exercise Classical (stretch)

Consider the following principles:

Show that each of these implies all the others.

-- Your code goes here
-

Exercise Stable (stretch)

Say that a formula is stable if double negation elimination holds for it:
Stable : Set → Set
-Stable A = ¬ ¬ A → A
-

Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.

-- Your code goes here
-

Standard Prelude

Definitions similar to those in this chapter can be found in the standard library:
import Relation.Nullary using (¬_)
-import Relation.Nullary.Negation using (contradiction; contraposition)
+id′ : ⊥ → ⊥
+id′ ()
+
But, using extensionality, we can prove these equal:
id≡id′ : id ≡ id′
+id≡id′ = extensionality (λ())
+

By extensionality, id ≡ id′ holds if for every x in their domain we have id x ≡ id′ x. But there is no x in their domain, so the equality holds trivially.

Indeed, we can show any two proofs of a negation are equal:
assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
+assimilation ¬x ¬x′ = extensionality (λ x → contradiction x ¬x)
+

Evidence for ¬ A implies that any evidence of A immediately leads to a contradiction. But extensionality quantifies over all x such that A holds, hence any such x immediately leads to a contradiction, again causing the equality to hold trivially.

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

-- Your code goes here
+

Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

-- Your code goes here
+

Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

-- Your code goes here
+

Do we also have the following?

¬ (A × B) ≃ (¬ A) ⊎ (¬ B)

If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?

Intuitive and Classical logic

In Gilbert and Sullivan’s The Gondoliers, Casilda is told that as an infant she was married to the heir of the King of Batavia, but that due to a mix-up no one knows which of two individuals, Marco or Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say that I am married to one of two gondoliers, but it is impossible to say which?” To which the response is “Without any doubt of any kind whatever.”

Logic comes in many varieties, and one distinction is between classical and intuitionistic. Intuitionists, concerned by assumptions made by some logicians about the nature of infinity, insist upon a constructionist notion of truth. In particular, they insist that a proof of A ⊎ B must show which of A or B holds, and hence they would reject the claim that Casilda is married to Marco or Giuseppe until one of the two was identified as her husband. Perhaps Gilbert and Sullivan anticipated intuitionism, for their story’s outcome is that the heir turns out to be a third individual, Luiz, with whom Casilda is, conveniently, already in love.

Intuitionists also reject the law of the excluded middle, which asserts A ⊎ ¬ A for every A, since the law gives no clue as to which of A or ¬ A holds. Heyting formalised a variant of Hilbert’s classical logic that captures the intuitionistic notion of provability. In particular, the law of the excluded middle is provable in Hilbert’s logic, but not in Heyting’s. Further, if the law of the excluded middle is added as an axiom to Heyting’s logic, then it becomes equivalent to Hilbert’s. Kolmogorov showed the two logics were closely related: he gave a double-negation translation, such that a formula is provable in classical logic if and only if its translation is provable in intuitionistic logic.

Propositions as Types was first formulated for intuitionistic logic. It is a perfect fit, because in the intuitionist interpretation the formula A ⊎ B is provable exactly when one exhibits either a proof of A or a proof of B, so the type corresponding to disjunction is a disjoint sum.

(Parts of the above are adopted from “Propositions as Types”, Philip Wadler, Communications of the ACM, December 2015.)

Excluded middle is irrefutable

The law of the excluded middle can be formulated as follows:
postulate
+  em : ∀ {A : Set} → A ⊎ ¬ A
+
As we noted, the law of the excluded middle does not hold in intuitionistic logic. However, we can show that it is irrefutable, meaning that the negation of its negation is provable (and hence that its negation is never provable):
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
+em-irrefutable = λ k → k (inj₂ (λ x → k (inj₁ x)))
+

The best way to explain this code is to develop it interactively:

em-irrefutable k = ?

Given evidence k that ¬ (A ⊎ ¬ A), that is, a function that given a value of type A ⊎ ¬ A returns a value of the empty type, we must fill in ? with a term that returns a value of the empty type. The only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k ?

We need to fill the new hole with a value of type A ⊎ ¬ A. We don’t have a value of type A to hand, so let’s pick the second disjunct:

em-irrefutable k = k (inj₂ λ{ x → ? })

The second disjunct accepts evidence of ¬ A, that is, a function that given a value of type A returns a value of the empty type. We bind x to the value of type A, and now we need to fill in the hole with a value of the empty type. Once again, the only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k (inj₂ λ{ x → k ? })

This time we do have a value of type A to hand, namely x, so we can pick the first disjunct:

em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })

There are no holes left! This completes the proof.

The following story illustrates the behaviour of the term we have created. (With apologies to Peter Selinger, who tells a similar story about a king, a wizard, and the Philosopher’s stone.)

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realised that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said, “Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

(Parts of the above are adopted from “Call-by-Value is Dual to Call-by-Name”, Philip Wadler, International Conference on Functional Programming, 2003.)

Exercise Classical (stretch)

Consider the following principles:

Show that each of these implies all the others.

-- Your code goes here
+

Exercise Stable (stretch)

Say that a formula is stable if double negation elimination holds for it:
Stable : Set → Set
+Stable A = ¬ ¬ A → A
+

Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.

-- Your code goes here
+

Standard Prelude

Definitions similar to those in this chapter can be found in the standard library:
import Relation.Nullary using (¬_)
+import Relation.Nullary.Negation using (contradiction; contraposition)

The standard library uses contradiction, which combines our ¬-elim and ⊥-elim.

Unicode

This chapter uses the following unicode:

¬  U+00AC  NOT SIGN (\neg)
 ≢  U+2262  NOT IDENTICAL TO (\==n)
\ No newline at end of file diff --git a/TSPL/2022/Assignment2/index.html b/TSPL/2022/Assignment2/index.html index 995cb4483..d76cac027 100644 --- a/TSPL/2022/Assignment2/index.html +++ b/TSPL/2022/Assignment2/index.html @@ -55,7 +55,7 @@ open import Data.Product using (_×_) open import plfa.part1.Isomorphism using (_≃_; extensionality) 
  open import plfa.part1.Negation
-    hiding (Stable)
+    hiding (Stable)

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

  -- Your code goes here

Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

  -- Your code goes here

Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

  -- Your code goes here
diff --git a/TSPL/2023/Assignment2/index.html b/TSPL/2023/Assignment2/index.html
index d2dcd6c08..909f05260 100644
--- a/TSPL/2023/Assignment2/index.html
+++ b/TSPL/2023/Assignment2/index.html
@@ -25,7 +25,7 @@
   open import Data.Nat using (ℕ; zero; suc)
   open import plfa.part1.Isomorphism using (_≃_; extensionality)
   open import plfa.part1.Connectives
-  open import plfa.part1.Negation hiding (Stable)
+  open import plfa.part1.Negation hiding (Stable)

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

  -- Your code goes here

Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

  -- Your code goes here

Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

  -- Your code goes here
diff --git a/TSPL/2024/Assignment2/index.html b/TSPL/2024/Assignment2/index.html
index f4a56837c..3eaee1916 100644
--- a/TSPL/2024/Assignment2/index.html
+++ b/TSPL/2024/Assignment2/index.html
@@ -26,7 +26,7 @@
   open import plfa.part1.Isomorphism using (_≃_; extensionality)
   open import plfa.part1.Connectives
   open import plfa.part1.Negation
-    hiding (Stable)
+    hiding (Stable)

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

  -- Your code goes here

Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

  -- Your code goes here

Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

  -- Your code goes here
diff --git a/plfa.epub b/plfa.epub
index 7e464644d29152100da514975769de97e6ae720b..c3e0bf6a9be801f6a049b5f0e174cc6bd563dde5 100644
GIT binary patch
delta 15619
zcmaKz1yozl_U{wirMSDhyHko4iWRp4rMSBUr+Cp|MT$EVcXx;4uEpIc@KWx*@BQ!Z
zzt+pjXPv#1Z}#42&YWRLW@h6Gpn4#neo%mh!3F>j0038A+gMaSXvm@J-4AGJ2VL9v
zBk0xF<0wo!2;ysJz4MuLEcDEXu3hi2KXk7~`v#Hb^077VH@E!D~w56|vO9;X~ur}oDjsMWO
zC=JnF5FW!b{h5ruDVL7Ymox3nE|8`O=M?wbLQsH&jsZY=QZM%%>em?m?RQRG{boQln%B)HkG?@MNPWS5kaL+@Ev-oUSFd_CxKtoBOK
z>-nw>x(cFN{kB>!`8sKlKEE({c?p0h$QI8*9q9Ik!6_<`9%g`0xd~inGl)0xov`N+gyW@
zXFP?FWHOfYMpr`!b38Uvr?Dm+yWk`FC0o@QeJJ6&3I=ge
zt!K~I5!s*~0Z0RhfX>#_r;Qh%w&(9FEXEKr@VKSGlGxanNvQshyDKmns@n;_;zGU=
z+68O=9*vl)BFYo`3LR8%Z_!XX@A!5{Tvn1s$N7;tD0&7qD#G3dE0aGwEqA}6-KYIb
zP4HaKa6h+#>HEA2)AEL+Ql-UDop4Zj85PS1FEafN%8CdSyQ=00Q
zpNrkF;EEUjK>3sxdLxz1#+NPE`?k#U4+UF!GFaUt)>j#~F!c3)&f>%2St6?i1%4?+
z5h<72|88R?ZnY4qw^>Lmiiik%40R36XJ2id
z7dZH;P&i_y@7!89lk@?Nx|T@MCJQT(LcP>+uleG~Ha&^x1#Du%?|f8_F6z(!{qBO@5kU6bc`v8121iKJqz}LK0ZQeT$Fy
zVVhG+loq9NT0kUj)e>L%os13iIeKa%j)jb;Oz{mXd}SzO?iUMZt@3A-)~#bvE8C3-j=3ZRb?{J+aZQ*3b_2q-NWGHhlqbH6#=cg1%ia|W
zSgea7=hJBUH@U?Er&+~M2h+l)&(+GX>?b7tf5K^7mh%S>cW!tZ<0h0n{P>_@aK0YzlfmlubLNbY=oRRLxWY=aN*{@FtDhEu_>4)9<@Y+v9oH;
z?>`=oxOBY}{r!0|VT{Q*&6{`lE!X7R;oPm+Devx5it_Xi*;sWz6U(>VnFtFEL0b%N
z-U8vr+>Jy7BWa)(V(HWxX;!4Ybel<9o3~85_?n}IQpgiBsn!+!GNw%eE!ljQOI|6q
zF<&^99=B8iZy2nc7h7{D$*vxwR8pxOmQP)@mRBuSx^=dM_8qH2SjnItgmUOY@L&~5
z1mHp+*^Sw1G}(985h-yN(sEm1SgmG^IEiVKt;ItMz6^jCOQ*AHxY22>4!wg#v5URE
zZoSQ8@jJh-+8-2W5qr@(2~eGSq#~=$8n)_bpsOiEHTnrRPiD3iqqR(P883h0;}pch
ztdfJHo{vJZjkBS;Ffz}fxV0_7$@0xoTW`6QjGglo#ECh=c$5;ve%DQ9EL}w&`reVY
z_bRqE{N)?Sz~$igiPuc?+U><{vF($en56&5v4Pn3m?~D3BP+u^2Rf4arTsT1PdAwS
z;>jY3scFi%AzbbE30g4tiZ@Oa1HosoP_VSWrD+N91U!JAiWKEk6Gr7|_d!e-dL#GJ
zgkc>4gUH72lzQ~R_zY8(gxrnq{BC}1DA-2U=)_8aux7M$TI>e0@Wj?!3bs?oQm9coEO7+FKn9pb>+S|r>|mZ0*Wv>Jz@
zh%^w0$RSGN7*^ea%duR;bMTUZ51;>Ahba5803Vp1K_%-2$QA_D&)9>d?F#^)aSF8F
zE8fUtnB&v0gD6P~3(puOD1ryXxH#!Tbyohw|90|6tS*gwk~fHN^_I!-QnN>4z(-gY
z$Q(`}b_hKy@8hSpLow*u{sb=nS;vSgYh&H=CED}?8^Beh2jljNqEBwtw{qq
zyVUt~g>~D7joTG>t7CF8(?Ir7#zA8@c-xxsT`~>}+z^?9R?C{G(1g6jNY}IlJaeK>
z6?w&zVpgT!dH=V~LaX=DJJx+s>iDoOem8Vo+l8`=VN#!bFWKnwO*54_WIJy7IO|O-
zMotDfMX8+f(av7(cDba9W&LWch%dW9L@4G$S^j+Q9fu^AoPZwaAr{|P9f##qC8BHE
zyTturR_(!wN`cGE9d-CvUV`KSDSVY%T@CF^XiTP-)Y8vB#@MEz$*u43uq!qFy6y*z
z94lDa*92|L<6r{cfU8{KSScSp{ij^{wr~2v0$KvorRB`==-Z)>UloEH@|oBWw+*hA8H(5Z-oc4h%7Hd6>JXFp9r
z{{{*j4h`F$cA7iz2r)j_IyllCM5_*!(jj__g^gP&>Mt2}p(cBrRtY^sQQxx;STQWZ
zkadbRqzPb%Sc2Jz6Ey
zyR|{xQRXJ9O&S&bONM>*1TSV||5^5&enB9e@i1^f#1gmuqbDvH!_++*q|NGC@&P@T
z^rI{&Oozxz{129$Dd|uCj6F$yy1}B5M3_LND>9mwC-hxC9Cr|{%yN@`jc0)H`@Lz$
zrEJ=$%L{j$`i+z7W|r9V4jl`XVP!GzpOeLk?1TPfgV-+YztGooq%Hj#{p*sYvPB1s
zlH{6#JGE@B{VU^+Hk5oHK^=eUWdJnH0+{#eOkqyK-(ECHIf+jiy1ob8_+OZ(V1E0i
zXOt`mST%Gn*IVC5eCP8Xp@5%Mws(*NK8i`}8PuJt2fhB3JRZ2jK~GVSxXnFBpRB~c
zwZq^69VFh{0j&H3+Y=H@O-63lM{ZMAeWpgi-p>lX{s3E_(Sp9b4Why>@cUh`nHn!;
zs3S<@15Z^WXwES1$90PIk~!Hh|&)?lEXLAcSVJX)E{~6X%;NdRwN*&U7d|MIWl8q
ze-x_0>FO)EzlOi#_SXqsVRa@f56yMcWFo9_QrhP|v~d$8JMjs5LCXH)K3?w;hhU}b
z%=jZaF!s*g^Wm$Gxvy|i81|4zo9G8tu?;cnRcdRo*6
z5am}FxOwO>>*tX1o!s;+x56FGOyCVzW1W-QR?nY^%0URHfrQ$&9;!Z~
zXQjAfMRM~7GUb$A_Jy@23ll2rAX&G!cwB0ziRvkvAOgKTi2Aq}MR_g5bR`q(nS6S|SVbU}LA_4q~g
z4U%>os&)>+tDkaLH<4O+fiH7x@MHlb4A8_knEE0D{&F*PSnT;}k1zcD*
zG(fTX5)zmAnJ5S5;MiYT*dHS`+-z+`d$Zn$eQc_#xV+lRBaK;LInxS#Az!KgQqIhq
zhTvLe=7IXm)bCGrUB-Nzu?m_kN)8e;_G!;f#B53=BlsmU-CuV{q@3TiBFUFlX4Xjs
z+c3Q-{C%N{s|dzHP&;GHx(2aKyxL5+BuRJ8_wme+3SQCHH7B@IBe6}?Yr(zNBmJBN
z>!aP9xisg4_f6Ndy4SR=p7Fk|gITlNw*8MJ@t&ts|L+OIcMurB=l@okQIli%W7%-*MwL%zK6;7K2c!~
zL!L&@KrWZkPQ23Sd}%(yc%>@J1BpRdUPPL8~7SxUWl;vf*Js**!&xU
z4nbCS*|E`3>I94q4de!m$E>q879V6(eAkYv<%&yh?oL_UFMoX;JnS{!vh9}hYf9|h
zt+r;mEPc;J+=+S$+xoups7?I-HdL$`^k;QN8)h`C2yb;MyOx&q_)h)*tBS$n*h?{w?hS(2|wfV>A2%-IGA%$H6tf
zfH#H{nRjBtDOg2M_7wdG(ONK;AcBFn57!DSPvmni<%jMS(pk%1LRVJ&YK)7Rla|>h
z$I=Isg7~2u(aEruo^}N*v-;hEr8f0ZsAwoPjp4Z+VW%aAy<_*S-$UE*7}yp;K!6)S
z_W|r5iS;NBiZtg$&~T3VS_oVbk^SP}wypdzHOuW6C8B@&FDlMT6#gk)U$Tuu6K!irlpghN!Mn|u?tBmXDs_7l8BiDDP
zp!%Mvu+LrR>zU^}R`8&}m!LZr=3KsP3Rc6=v7N&zkaO^1rhrMZA-Z4J12uv$f7-zJ
zt>&M8tHZ%UiB~T-c${CG9tT68Z0F=1UK({+o{WAv3E$FHm7I_cm^gTew;KFxI0YA8
z1OZNnP5OCVtm$l$b5K0ZoWWc;7@Ek!Zt_bPR$|z-=}Ee9Lviwu~MV93-}P
zF1bfAph4m2Zj82b+$>Zn+x0N;nD+*}iq>|ND2K$$owM(Ks%ZC{8!Hy$al#~vO*ZWK
zn$~V#g2)UgtO*smjUdwqxnz|`lzAc2T9VA?Mlu=(}@G-wXgQku0wEo=q
zIiz(=C48a?-b=)B42PK57`tPQUk-n8XS7Pwphtwo+7^AYG7NR`)Gcix>*@KMf|Duu
z2Bb!yaoV}fgca4P!nHJVFt_q~HVYSvHVF892zH$xJD+KPp~E66xvBdZO_-`u;nf}e
zP>bZfdWF_pTM%llK{b7dZkud?ACpooRLa7JMkFxt_zsn1?}msiGmjX5f<*f`S;e@61KsXHrWz(LP%mUzvryU?}nsv)+|gPQ69`F`jzS
z2hO%!%@rQi)t2`VDf3cka+T$J%f8Af7N
z^F}$uq&4Y1F&_K+9<96u<$j4Qh0;{(MYyhBh-Ii+Xaw;9on)uWlLac1jsNH&z(m2P
z=#x^TRb*GX`)1cc!f2n!YI>~)9()83Bm?m+_muOQQ+m#i)P8eOzttHK{A7r1L%Sd)
zCaXl;M9!8Xzc-1r-9tb}-7J#P{je-(9in?2(s0dQExRU$`qW6q{8@>=eJne{s*kut
z)Bg$=#ciH#2~9Xe=ty&{=@-Q<>iZ@|(0wo=^i8kO)7r%^aJTP0`6trrTxa%z$zf2M
z0h}|>pa~12L+++g*Xr9SS;SDaU|Ln
zp8PtOGw^+RqvQ0^YMw0NPd{JHYH3aPnQ#)x%`oK^8eULq;`24L{Vp0K`-Afydi8O-
z@1lTjdGZ@)etI&HX8R*F-hithjg?ZpSY8NpvmB}MRM&wcT>a0811zzdby*Kk2T4VX
z-)#eVX?>)l2j02I*r!vf+1>}wZwP-fr6mO44Z3NLcKYS8W4;NMR0<;YXODsYgUOBj
z#U9>_>uo@f6U(PLnA#F*1bd7+dW(Mix16pf!kDTK$_;yc%~Qjuz|dt<63h%OMvfS%
zZ#NfuiOPsr?mzi`z0vr^m3N|4KsCc(F2mkzVq?;!m+zzJP8`2HcjIkJb~uI=Y${B1
zP~r5>;}0lfRZ2I>T1-u@SXsDoKgxdkfci%MO%-%rPa_JzO29E*2~Q48S?b)ji9JRu
zE{ai@9n6x=j}@xoj~QozL4@`BH{;i?sBg2K?v=S|i@UpuW!Dd1zGp3)!+^Mo#PI?n
z8AEI-*gEzzFQ&F1vK4Zne0QRgE6E))xexJWO;x1&QjwtUgOlYY!Ni>PNnchZ^2pgu
zs;S0@Y_0Oc0ql%uJ1=+PsCnK#53upktx~uoPMFL~B&dKN#7sT3hM;C6iX_1<$QY1n
zIE6{26>qsd0YiWKf#(1X4n(~2g-YmrkC*;5fMt)D-x9$I_e5ajBwH+#iEU9}b#3i8
zRwv_HzO6)1_u}&lkvc0JM
z$z!s1=nx7`!9H=1yvO;#<;8AZ=AAEHNGXYiYh3CGGo-H?+(tSE>>)Iu=Xaiz
zQHCEOn%k84`faKOW1e!N+c1D(2XXt&A42GED$W@Ks<)+|W#%z#+u)b^<4@F=whq5U
zX(+fmmU9m$nP*p6YiNaezAr(ER$_O8&a_CrZYu3obYXP
z&}Opq8IWgf8(trtY)+l~mm?K1Z
z3FanO7mWxWM1gi@SDq{3Wu3HA6~mJ*M7%1-&a?XNTRD8)Q0bTgcu?<=w+-wD2wK6-
z#EkPi=@gG@cA=SgLG_i#qB4!PYw%^{j<Ec1hL=AeTioJof8&T
zEO9)6q3>zkb|}Bk<5Q8IwJJ
z%_n{b+Bfqdv`@9DO&r>Lh%&`J40k)Db1nPUooMLyRudixX*9
z6TiSB6jy&)aymz{nkC0
zQ?JS9rIJ=_Ejk6DZAY?88?co$cXo$ouR8*yMcQwEG>oyFUu*WHA6hq&ke0={ld$V&
zfojP@p|7DmXF98wr)}sNAGld>Qn4v61Sh-|Kytw)~VXA2Mce-sd?TeEnd<
zgYgyWRKHO=PW296M+>_qZZlyVJ(oWgH`(+{ItB9HdV%WAT9b=&+#9guwOXXoYK=f1
zR$@G5nqow;a&|@i>cW$E?vZD?a{!cb9q0-kC+@oi4&=bMWSxVQm2ixep)&Iu_S+3p
z7iEf!2FSigAmZ`fU5#rK(W_^1FvW*a|1yVT>me|_*}0Bjj!eDhxYFf|pXw_5h>pAZ
z{GC|Vu76|wS+w?Z}Sfs5dB(LdDERt9)4X*B(-3tiGA*@4QTA7
zpYsT-sP21!Ay+n)mh3mGflA=5xXDqgq8va#z2n@l2}b|Xxqy7TtwH*E`2H;v{`GhB
zK&2QB`x5OmT$u`8QEYL0&?YgFaV=>x^UclaTYaBP5+ac?m8MuM0q9jDrt~-&JlJF-
zKe?l<{@7j7Nx7B|nJ%dnpWJ{CvJ+eEgwYAjI-V<8-SUXPMis#5inSJy4~xcs+Jh&mTr^#W$P)6qnk-r!jlDeMS8PzV^i;M$y|{YK^X~+ms{eB-vJ|i
zT42io#_{((T|FV5$s4Tk?CLHK_k>14P3|NMk@td_%Jgr=4AIBPOuB@f9XqhQR~;ks
z@RCv@F60*06@baI+UD{MqG(#q4anC{5%`!yb-hk>T%pZoA6hLx+&@`c=Br}1ROVIR
zPr3&J*P*rSja5&eK!NVYN*QdpZ47*V*9W|beur;(Jc}Cd0mEa#Nc5XtA^1V@^2~Dk
zA#EQxsjTC;KbKbhIh|Df4z1bYkhqvV$cbihzZuC
z(v7`F!5o&g`4EIQWQnRtQw3*M`&pkR+f&ktjv=YDlS`58A)zr&ov}b2=lh|qs^%^y
z;dtfQw?hLbMG)Sh?j&M(C=Yue{cIuBi1Xw}{boFMsBl-^by#PlVm%%brf!414pz2F
z9n*3_oJ4hHc_=K}t3|#-Tqm=m2=3IAWtCxX3Fc%kauO#p8}SJg+-FtT{N!Y*yCOME
z^J9IjAG3fCLl2`xBM(l3j`d_o?7ZHv*uW5XlFWT0(GhY&a*M8Y>1X7ia1Pjj+O?^Fx)d)m!9k+30rg
z-0*`dt>XLsgG!h{TZ6^?v7q|)(y=VpkH{TH=CzfKqCY=ath>X~+uaB#^{FwEL|{>`
z;cHfIGJ+se5Ab`y4_6vFzs^SZg|F9M^@gP8T^0LAE?OSwO&+~*KQBXosy6X(M%K3<
zSJUPXHOy%4yq>=5!#zYDUsEY1%f?5lByOmDs8ZT2r1_M?v))LQZ4fZWpNy;6wy(bB
z$CW5g%Q&HOux8uk-F9zV;xlVD12r{TGGGy6J_V|=n&I^W!YQNhQT=J2jk#YXo7h@L
zSgBFKU#j*RSj>2TIcKQ*)7?kY@uo&pAuifjWBjM}@{
zW_i%iBrUB{+YoTI{fEC~K9WciCGw5lL{LJo=-Be)II82$k>AeO>I*wQ(?`k}Kzzzx
zt6yrI>xb(OoZI}_V$ZjJZfaJOC5tGZ(26rLj41Sl0tX4T#PaL8OC@@(G)E$I{8adS
zamCMOr-}^$lZ0BOx8nb&>|A
z?BGm6ncmT$&`d#zUQd>?Q+DO2?b4PAw_#nek^@Apx<5l^k*yI0wF1c(CwFOC?8EmU
zx6$Zb6m5fFF3sg7K(4(9YU~3J&89YzBL+7YDfvj=-Qr^f;O~g@
zmiL(OFM6=sIC|B$UGBn5e}+tksh7zwemSn_n0{J*bAe(rQ>A#aIm@iD_Z1p!Gkm~T
zG!u-}r&M@z`yJrkqk)%Ye+qA@sNI1D;*rCPBQ2@htFk=2JBMBTb*HYJJU=Yvl7oIB
zJ_Roajimj5vX}F53M2Sf!7I5a&Ye#xMpgfAkHBGJ%NEZ>^V_
zBzCE0Sd!H3KI!H4-%c}}E*w*QUxfX!23DgdaRoU)TW)$;WvrCh*bI;5rTxAr6Ygy{
zQY49{81ps~IF>bQVb3V1RsFR4?%BJx9f7)rxI~xDbe2zFGDxCgqR{#}qku_6&J9x)
z7&md0K?JVC2hzZjmCe+)f|u}t1R!O!#P;W_(&c+U8Fn*~infOeC|}5w*6o>rEpjLa
z-q*449hdh7@96xr3r7(Ttjs3`r%rWmqE+WP8nZK*F!2xbC20yL65V1~Ew;x5cCg9a`x}K+w}iYxgJ1k<$VD!~#
zVv<<=*PflrYlc6o77izn67%41vb!;L7=P_Ory@HQ=dnA0ZcIpOe
zeL@N>7X9&ohD@xOoO>sabZEkXF779Z?9xQh;DC!eieg@L9+CIQ
zk^@zQZ!{Q82-JfjRRUiV0-4EF>=VhXP~A8CbLhi{e0MsAjQMe8g)lg607=r{eI&u+
zL_iYEwStHwc^hxi7^Q_nvXXAMZm=y8kPM2F8XQ9eWQJ;W0JjnWnNZN}pmOdwtU0zL
z#wEa4L_h;#=zM!y*!Wrzww0tiYFFQtDdTU$DPrT3d5P-sU|V7!BT+<&iA>1qc+awU
zX=MkK2T}b|)<`jNh|d#^Y$udBMNky>5jxB4hvHyIcS-{7#CN7==cya(pNTmU-
z4aFQ<6QjfVRs{KvH;;m6@P4l)Fi46cZ+aA^JS;p)cTZ4
zY;sG!&y5-VVqu;l>r`Y;LJ}x9ik7-W7$N-9a9CdoGg53c9dk-aAQhQO3B0Vt>NA3r
z7t|$2C(9Tjw*`9$wW%c`O!4g1SF|DJ#`lkL823
z&gR01!}s7j#jZYo)R3+N3IbgYq)p~U5t6;mZaSHE?;r&e%7wQT)3u;QFB(+Oz`R1Y
zBhe!*eAhL^>+kBs8=UHgqcJ77jg1^rBDITuHa`RXXS-#~F29)Ag)Q7G=3hnaz1@6E
zP8A-DQ_-NTHQy4-=5mQ-2+x&VtrP8YvuDBE`p-JN-5QeT;nXdw86G(2^{s+ju
zD!GpeC-`(>$tfiakbwr-eOpMNzHtRtx9g+aIDI>(=WjfYx+j<*Cd8?p;xiCru=AQL5L9ZHeStxNaD)QI>e9qw2g8o>`EM(}#e>sP%
zV&s@OQ$#Wc!%j#q3isgvm#o^O@yb;c(^)~z%*6_i3>sf7f78TI>3GwmPUHOK&CB`*
z%{3p3oku6-XpBL9R-8>05+lz~qC42cRd6L4kPx&w(5a4DJBnghT_R896xe5NU}Lh<
z(%@S$PsRH|e{~m!&lc{qNttRssn^&2hhzZp&cTx=xYoX9yrS(nRj57uO4SvEQhXyQ
z@L;!AavLBmP;H6q`>Azo20=`tg=K7~Am^C#c1|gGxf^!wY}#)Aa%+!|NWhGUt9=i7AN!Y+IuECsget#6_pF5X)2%ILC^*M5`(p&E_T_|t*mID+Vd|HQO9vy1AD(PS&X
z$Nq)LglylRF9!;=tO7CxS|iJHmi07h(*~gC?Zi#$$W6GcCQo7ya(j|UOrQK8qxu8Y
zt#9^9bs9>%5w8;*m4Zlx+~hS6%BO6pb&P7#23hvIyVl=CKZ&oEui26qYLsr9e`&IE
zV^NV=x=;`ap%^Or=+Bs@=pDKIHI8qXQ7E4{z?f$>mwhyt%Qw$zoBHjpYNmv9GrJv<9)Au81w17pkfo>P
z!ZE4!%D#tQYYW~V^KE{zgLZ=-Qg@>PT?C6SSX^Q0Ysra4pyl$mIXdp=Mc3oyb*P8O
zVeHYmaS&1=O|5e}8$uOL07(kY)u|=prFS_l_#ZMCKizU|)&y5bSz?nYk2|NxpX)WU
zW9z>i^Q%rgR4tN2(Q_QYva6f`^1tbh9h{VMy_Qc_d?Na;{1-^A^BuT#G!a?
zAj@3@Wm)n!BP?zMJtnQRQW%G}XbqX!F*J%p2O2(6t#cPa)6erY
z;vl~#1{;a29rxYGY{^sB4VTm`kOKaJ|K)~u!vw#?l_eX;leDnonE@{jPPWtTemeAa
z>O{=S<7N?hB+GX>nQB}!YH2vg|EnK3#-$T1i?UTLD$s3NiByuritwkvQRTYne7<1?i~SF$7wG1LuZT4f|V5a#)8t6Do@7ELx~Ya||j!ym?F
zw-UiAjDj>{N;)UbLDp1D4J63$4d+{>7^d7UGaxjR)rU6s5W6OCV)LPCh-y9^3?g%X1sRF&~
z%FN@IDV*T921qlRws5nXTS6~c
zmf4|;;M4YelPDcU#3-DT=G(1>GPO6Pv?9|%FwhhV(&Wn=LBfR~SskE%U{wto1NPwp
zQ)6KgUEezo^Z0usPOGWyI`|^h_}pq?PN3PQ#V(Wg5g{r?_Vsr~<#+43EGxcW&4&>C
z7ze{-jgC)JLvwGq8(MWGM$LeEF&1W2-;)k(Xn%@C#K`xvp;QzkB3~||`Rk#{Mt@GI
z^g~2RD9ie-?N&(*nxR+tqB12trsh%3+|Q{(?H$RhNltV?3v%|lnRHzst5V{vQ@Qc@pIdG;ov^Q>Pxb`WOH
z_ZieZ_eN%e?J9m+INyPaD0P+8Ju#A6L%y3f7rWJG=w4UB0Isr9u9N{a}|#z|3E
z*+#;(CVffWPNXTj#OyUDReW-4S}Or5tvQ=Q*R4v!#ry1q$y>Nk^CF2{>itT5(9vGmUohr1@7J-UHk
z39qy^Z##p&S>W8OQYcCcPg$?}wt3l;*;B|-p-qMs`R*CxKjXU(*g0+g70?3Tm;cck|wKqKU
zzo7rm#Wl9|$n?N0zt8*($$U?Osp|Z(gmmXeh(iW{qNEoo4i;!pArBd&J`ZK0R_YYlXc3$*E2XkhnBp)
zzsA3(UQz`B4ACRLzF$8@4AWBe8ZLGW#w_X8x;KTL)_t|cJ76E2Uab*sxZu85OZ^cp
z6#ms(g@QK*zJ_(lfTv5<1^|{Vq5l=u7zVyX`&EQ)0B=P6DiRugoa7b-04x)r{#9FR
zH>9>?Pk2$$SLH$j{B05H-?QKg4GiOeEHGLHOPC^H*Pnkvkowoj^O+(z{L3maLjVcA
zevBm>;mZEiqJD$u>HcbEha*bAf3^1J5dZxNy#++Pe>Jcx5mFr+w4JVPD4PNj1Y`&(
z5KtkYK|qIq0Ra=j8wgksup!_;z=ePZ0l%J2fxsH{8YN?hAT(o$5CRbdVhAJUi1fifAfngogMT9vfOr1mqqNBpK?8w6Fc}bt3l?vaLwQa3
z|CYb~Ghsj2s_oxZebQN>8b{GV0DfY1LUS_{7=
zVv_^_&PD$z8U=H=|GRYEc1Wpg%urwhW++^6O#8o^F5~aZSzb`!aW5!b$T$Xs!iN64
zS@Lzq40r?bF3=nN1PStbVm&Q+%QTt*fVT+DKWbhDi+B861es^lsX+q(LC63A;eRzZ
zFF3G6j^VW>D>@)~I}f11X9rNYO#jIHKgYR$j;#8@R#6CMDNdh^eV&I8VZh+fNqq0(~sJM^tV`0uXR4h0WBfr7^cKX(1Q
z9HeeY0xB?V_rJ?|5AmVT^x?r|2Jrv8oNs^CYT#0c`d@b!lypgd5ddI9jQEdCP2ki2
zi2mgmMDMO*&LtqFJ^Zio2EjcL(d$(@?1iKk0mJwG
z+h^^A_?lq(zdq!T0NCNLj{%PAlVg4L+aNwPXovtTrhr5U9vC7(0T=c|n*6U8vmc_h
z1GDtYalHD*5FhHq4eZ-5$NPHyx<+>5DItB^3lRVy`metIsXz`KTOddLU-uAXXiXY`
zglq*94?s>F;%fJ0)ajH%BFsVdBmZ{~7z7*sM>Md$8;}GUu{a>N(0_}H!9O4(XvnAx
g9{d~G3B2>yheQUW3_|=6F#Vt$JzP?g9HhGc13urg?EnA(

delta 15541
zcmaL81yEc~v-rKZ6WrZhg1ZEl;O?H_?yy*Jw}lYg-QAtw1c%@rB*7iN4e$H>Z{6os
zeH6di?m68(eP(8-&YtQSNGyh20E40|4+V_{0KfwPM1FP&C_GT$k6P(GC@5S%yQCAS
z^|#Ln=x!ib*C9Nu$0>yY06a(m0Av6FAgQb&&g$x5#$s>g*{EaSvciw%_q%%ft}8Vl
zhI|0(Xg9xgHk~ucXI6LvJr&T{v@7Qf`F!nRp|@F7Fe7t{Sy$^mHB;ptw|C!er;{Vi
zfQ{*kK1iDnuabq-cjt}n_u|TtCi#1EW8A9?C?uE?EtMojM4mP}PqFgJz@mR^c6Jt_
zSK;(yi2l3oxGBroTrX#Mm#~?8!jOH!$O!zNngRmKSoyZ_a6?NjO7u~f#pGj2b@{A$
zN5&|puiNwV_yvs4{4!QYwvMS(^}WzL=IOCR`OB_2xm!*dA)4N^^#t8_1vmt_x1NgC
zK#2)Ahtb19dg}GB2p(>&1s5aH_tS})mEmW2ChJ
zk07p!TJh-oD6Za1lS@yt8V9S%^Brk@H=3<&L$)e(%BT@TWGR(LkH;Qn!ykR?f5K+Q
ziG`bae&112UrL&15nDrDcOxQa+48h80Z|$G8sLEu!v4h1G0@c|1G;KQfovPmQcg%`
z)jmuy@=@oK>aufC=Nv3iCtopAdF1aXtIS3W2U1;^P=_AwvMRTu!iVj{e^VQ5eS_^G
zUM;j`zBg7}t9emux@A-7J3HvT9uo;f(V$(kcT^LxPLIFJ#`>QJ+SyiF3g2=v;&
zD99fBe%vbPrgth(VH1Irl4~F0sdlB_)21X)ve2Yd_pPn>wMRBH!(swWU7%KcjCf@O
zDaUa|Woh+di_K-{4=eM^_z2ULbR@h1`{cMCbVY$5Rltvm{05JM4@cuMKOP;pSkl%l
zMq<(Sp;cPgs>sKv2IU-=QXrxy`GHakVefK1chf$}C5vkk7RkZSZsl!Vlei<3i-c`z9M0y}!givqgWdbg($v{l_mmYh`JU;MYJRSXy
zvh8Y26O20`t~Un2-*j}V@5SzX^0dfl1ZRO+8q9(lq;N2hoA
zlh>EKU>j2XMyO*)xANnar&&ZvU4Oul(KD03CMUR$HfYH=eo|w9_i+$7Fp99V7L}PF
z+Y&OWzaY72qi2V(C#u@sJBP}zf-gSE5Z1-WDi`}>3(81E*2{hcjZ)!92hz6)^uw^T
z4S>}5m(#rZJ;`AeTHk#|d;Azj&hNT94P{84*O+zC)RmCUTBdFv4rag|SOWN38Gdo=
zhSe@>UpuuyH2eq-Ieh|pvb!Xsf^462K3gO@3IzzMlS|6y_d8!(9V*^DRyYw=QDbN^
zvrkTQ?TN2~`r+i~l*Fh+=)&i=eom=~U5NRrOQJbFjeg_x-?etb_DhpR$dhOh}fdTF)Irq6n$i8;1yfg-w!^iLmQi_qpC8~dhfT2#x`0SYw(5lmgcWY+}!zjY)1NMT`57vsLMWo{;
zm3+ZD`NH%nJ?v#*_xp_!PW9{!L)Br;f~(HwP_lw*xGjtWqhMj%m|1_KB2*{GIU?M9
zEtV`qxrGMkYVt9g`2m+C!_}YXW^*
z?z&D|bvu!VrH0VlYzf8jPmav9D8ra{LAMWd
zC0`)Yt%WfzGewb8zNRtPSz8sEa=YTsMzz&^bXK#P{XBGBJ4(op&y~7QXvrnqtpD&a
zjUc)d9oe74T;L#;dc1Crt|{@(A4sNFTyKgd`*Rb2D%Yh5eW72frtXWAM)XQEz>eyC
z!P{1XDx;r}m$~^H=6B5zU1siIG>r>%M+>^0n$-)%4O%uFQel;rb0==zt1)oeHolCu
zLyOac`O?7ZdF^_^uu@9eO~(V;lSXHZp%Wpo5UTc_5bPewN<@Xoe&{3=8Q?1x@~5OG
zYZL9X$HYdrCUH_nosLdmS93U*m8Ko9n}%|<5O#W6;yb4AEiAvP4Xer?OKG$8MYA$D
zl{VDj)=TLZ-D@#FrJM((@xox7K=aL>r|zdWbMyxAwXgkA7MZ4ZT!&-%Ui($yjzd7=
zH6B&6cQf23i*>{#Qy*T~%Mw_fCsLqQ`K#5Z%=_^(tB6M9CDh9w7&%?$&@=L(w(0t6
zKBYX(_txA=)I$%a9F75O?eAxrvr&+(+#mV4;n~topeDa#d+W}_(C^@Tp?E8h
zRZ&hGSD`Ma$vXE~*)lbV8u#wrvkC4mfW)JBBaBdfjgyPE_im!h>f!;ZzvtfAkU>`9
zBF9RmBH;b5cDrDALxfm(2mAXyY4B~jWKYP1u_FQoOjs``x`KUo{93LVJuKoKDH0OHXlAsEjPQk0F&*M{@wwSl}qIsa+@sWOcB&02dirQ>yx4cm{ZX!qP<$~f)DP|%w4TjY}GczLml}iL^dLqQhYrTiDP7nLG&kmvKIAR(zbq|Ku}7
z{=1j0a^Aq6Pqy!Sg0l-Umds}Ka)Tqm?mj`&VA|3wB)URoC^7EP^J$S0IVLmN#cwBO
za)E&pp_QC~H6pCZP=X|%#=!fb_d;=I$a3lf3-m4FC#5iQt9IF|He)UqB+eN06*@Uj
zs12{>X`l9!fJx8ltyFHjaS*4h@45SHI@b(-Zz++-iZvrkMcU;&VJ|YFhjvtdxSII@
z<3p)Ez_ojTx7igZQ9FuPp^#?a3wQXMFo?OdB_0~2s!Dq`nc+C%&PFHt)Eruy_LOKL
zuA@*kd!CT3lY!_sOHPLY`3@Ep%aJ^h>dOg2Qh}@Q5RhZwk~ZmwT=Dzw
z#W!wC5Ek)zrj7w;4u$Uu@Z;1li(6%spMS9?6^Tb-%sU9H4t{@N
zP{uliTw~3&{IJ9ps~qOLR-)`Ichk@&h4Stb2}h?g&3=0SpWIc$;^1QcF^FX$Ya9Va
zp-UV1_e{WkCfqfRk}#Qfj0Npdl`#fnFQu~-mpVjI8k3dSyZXIyL1Hiu?{;2a;9RN@
zJGwVNSXPMW3Q1d{#9$A
zgUB*{AT#JD-~zXFKR#aHBy9z5-H4B-^5BU6gP-D`VqR34!4U+g7$YTB^v71p*(Gc#f$tsrCzjX}@@UTs)6iJpVD%(>Is#T6xkI|G{WV
zQb8WzGTI>h<~?7x$u1fmStuUDP2fIhm?^TrmW{T5j+GSe_;-mV+lN9GB`iL)dxw)_
zD`CvnM?F3Y=wa=s((Y8Yr4)&P2s!~D&I1Bb2bECc1ZuVLmkl*dI
z^?b%|WrKgxS+#!#Ar8~~<7eMxaG9!;(tK8Fd{O*gjBy%)N|BYsO>-?F&
z?;rdZ!jSD9p;c3-@fbc0gm}%#4Kl0AcY@VH_Z;T_(GT>_VyBzDjV@ro!mu4v(Y}t$4!nj`&X=QG~p_BRvKW
zLvKucOC`on9E@gzpjD}DcR5D^nVDiPLI?renj?5Pr~*~65FYVKxTwOrVUt~JJP^lc$D1Y_lI$(p3m)?Qz$!o~9>jy?kS4NTd
zC2&PkcIP}eN-dqiRf~jUK~{*4?X_O~^>#(#&ZZh2f|<*oFm(ehqnb3CdAeS2&LN~>
z(-eL~BiWBK`1#z_om*e>?jT_5+F@v9G?Xc>%+q9AC)qd3R<9HoeRl5N@#`yCX*X%~
z=(qkIIuBe&DeolI^x>(vvDZFbt66Dp`2YP^Y4pgq{w+1X9#hsysNus?c4M!8x^@`o
z(M%{Q!QvmADRU;g6Tr3jqKmAP$y3ftCb_$Y;D1$J8>cj`rC3FP(%)MvexM3KRq(@V4!A(ns9O47lxSb-NywfAlira~rqODiD=}&w1VF
zBT!GL`;(7Xn+0@g(R~VM1!u6@^p2%w0+qXMNA9pQzaw+UBcw$@%{d6zlbwLs`pZ-B
z*wx3*8h9)ES|AcO!*EZiti0{=fca|0=R(m)%Cf7yh8`t)$_mvg)9s%NY$x4)*l;8M
zodTci;}GVLVkIXjK%vV#*O@6}AOW|-_7lBcRPpy|!)lw2XME#nQ*CcxAh%Wm7Vo*=
z_3;v4ck|`+EybSXBP(DN)mZ-ZeY}(D@2GPH*xbl7babwqb~ps)v)HHaa+p`Kx&xGo
z^V9M3=}biuONPZRo|~)ypo*=lv{{_N!TU&cz*Q$`P?YHlpnZ>^pwnYHsTA?-S
zRs34^za!V{*V*0Md}G$m!cTsuYV*%1@RB@nboricI{e8->yG_$MZ-C;cRbzdE0kL0
z_{?F2e0dC^tep)V2xo=a>f)<~GwsvrSe*E>@gfeZ;vsThvvI0R4?OEuE-xfiaF0EB
zp>m&JgYsgsM=e>D$GKg@(8xmT$uv7zDvCWVKygVHtByW%E`sd4$!v!cMJO0Pk4nd+
z_`nq4%P_5u@-()Xq;7A8ZKF5&KK=FmgmE#w-jee$88@u;3oLPa1T!aaq*A$(ne)(2dh6i)DG~+R
zDE-rwK#Xm+SU1zI=c?7T6{#}4*hljc&P5cTg?WNg9^mHZhG4Pc8%u(#uW8G)X>NHI`+<3h*
zbBq#UpL->M2Q{XKtKo6^bwOiTq|(>$NwuaPX&k0W!HldQUS4R6;Q7jcB&(~LID5+|
zEwOR7d?X=-N#`E0aVEj9cW^-gg-wB>3}UIcVXlgoO2Wqw-b
z^Bs)dXWu3)OtB68?sl7{kEuQK_D<3774SOO70-R(FF~&mSQ}4!pkp`)QsCmxfhry=
z3Vz#t-4Xr@A7*pny6P|7Nhi6aRJ5oD@gN22t4}b_+tHYbYeZA|4?n%@z
z^$@(aSYjoW7|+j2M&0N1_5!M%rISjr+fr#8yP?y+GuSI7J=p)Gy?4FD*n;pbdeuG&
zYKjA>?(?T6-JQZ3cRkDz-b*|Z#yh7WBVKe}a_ZqcxE=0lBQ@NT;UIuBo3$HL7K#0G
zO_uK4k**SZ>iV9|R9uOeo^RQ}+&dPdsX)$L$Qo4FuXOZMjO;1_?7l!Kn#nlqd(#5=
zK;_Al_-Tl>cor{CMM5A$(GQgQOn%|-W4{f>Z6>XWui>a)&$%jj7*E**<1FGHEYQ8f
zkowl;UcGU6UEr|s{P?fp>Q2A;ukiU-rD0rsQWkz$e|m}2CtE#AuHajHO6Dh6QoMjq
z!qEhAw4@lQXW!MrNsj`d&OG;EI)-6Po=50F9_ZNzOgF-&1{KwC5k0T6SOqT0z8>>L
z$h?S{mAm%PxQS*JAali31kqjrW50-&zc*YSXo?a|!XbmSk=o%)Wx
zzK9~Oy@dT1!NrA4l^4V|N{huWr5hR&_5T_`{X`UO6$Gn2vhV
z0-!yXkm1@U(}rbIc!^!?$PIB3D2l>ti!hkZ8;uwpPZYeA#wMU8hGiepfI1XRy*9_q
zV`W{rD18jQCrk-UlZ9!+GgoJKMe>69_?ir&(RybOlEoDRwP5&=A*qicT5$w2;UP6tv`&gy0j
z`M6HYfopr%i*HrOrvpzQFk1<_+&7~Q20gU#`E{{GA6fmuL9xfmsho#^-y_OOd+VYd
z=_ak?X#b3JBJBx%Y&G<=CIET8=yQmw^!R*fk^0BSS9mVnX~)z+ObbN!ve2Mdef6JD
zM=1}pDEyYdHYObs7wXQMlGY+onM=~ry!Eys{G_@pdLVzYpJlSbVVidMimWtxp%XX#
zAG`CpxacNX9tAOE0)eMnjuSe`7J$v?6B*pASvDRG(TS7ZZ;cnF7`c(~eA*$kqv&)V
zve*yayl`kPg468>!c6MB-zF$LzGMp$SHJ2=;UP`}rBS#ZE2*WNpi{N+aN6Y@U{EYS
zMVGWS>#yaTq~vd8@avxmkDiVepZkWiQuuKrPgZp-qv-Z($Mz}-M*YMJb+
z1J;%yC|mnJJuw_d9~*_bVi&XTSJn9!534q?9Z+jBXx6bMX9057nt2;}>+h
zjC2ve&q{atA;eTJrm&N@D8#VpVY`Z)lWYf>1+;@DY?T~>&H46|KYi!v5D;{Y;H
zxIl&nVLv1A@1HByzm
zHShJ*@*fw`R^i)#_xdh3J5shtx@SloyVO{iw9-7+Lqole{5H+o&`B=4oSj3
zhJKfD6su7_ubjAxJ|C%~f;x(ISXMmdTwOyV_1fsi^tgcJ>B5~h3e?;LSCb{)2vj$V
zg0U^-nL?aFpi~Lp49eq@H0K^KP>%I@Hegnvyi#3i(SfR7TdO0Orw{qY8
zoTig9V-R2ZhNibRMZV6;W3&iS3%8cBuJpd_+Zz2UNI_%rtgb4&)Jq5~q;lbK-?yDm
z#jmRGo!EPEfo%-POYZrjCotv}ZP49++Zi4%cS>d2oy_Qfd@`Ca)PNC9E}sLzKL(Mw
zR_rN!;c`0WEsO{A9SmWI!YjzG_NVg6l|tSzLW=wWE`!?L2Qy(Gofk<`r)o&M4iW=A
z$W1^oxK-}fTKY1!wQ8t*+ZSzxX3;+CJdCKKH8SfpjQvesg54&)d{C+H4m!CWDS!ty
zntKmE8`pSY1F9_-lfbsgFW2+U^WQSu+Db?&6Q{{*@^TtU!ysQ#&3MWX6RPVps#*#^
z-cfq!boz@JHt8VZ?kWCEnYA_@Q3#zhJiqXrUAuo6pPs9M#!Ky}ov|p{8<(rl5R00+`Es|;z?TPWQeovu5
z6kPs6O0>YO43Jv3_}=szAa@_Ix9s6(s9pm8hISpR2@y<&-#moV{zPXC3RyyOZ!kFT
zTdk#g4369+ZIWCjUD`9tsw@B`U-%oR?h!5#IW>(D`U&f(yXppMZHw?vAB$yrCSHhn4=`E7`2og1y+eglT$c~
zq${S7=sriP?v-OyU74?8bM>kAOQnK1HbXI-Q&JzUyn#NT_ud~bnhG;GuC#dAFO*(P
zCLVo>bkosn4o#h)TN(5oX&0C8XXiQ=T}ESc*$vmj*Er3Ep=|PXx-r^k6REq|k*hw9
zzB1^u?#{mVUq#bINXlR_Qlri(M5bv8!Gsav&B|+5!0L(*_)cH0TXZwVWAvJ$H(TsL
zTI-4@00IiCXhdSF7>`1?=W!D(8rL&2cwaD|l-URseX(0*g0Nbph8S+Nvu*eFul;US
zZ_~J5)M=wNC;uA6Qz%wE8}N#i^T%EKbT0&*aQY7fqP&hR^l#X_Rk%zRfr)4Cavca^
zB2cuwp*%4RT1QH|E=e%2W!#j?gWKhHw3b5gMhPNo
zM@rjnOqW?t$l!Ya*kSq5DfUOqw-Nk51bSP^oNaVH`f%gLa6+-1w-J-Hu-q6Vzs@MJ
zL&Sqf!UDYte$M|mhFwEFNR{VdH4tW-e;=SKFhXLS?6Ti(i|3$4=I#Qg_dbl|67NXU
z+^P<^n6KBqv`O}wY>s1Ct7m*su$@H;XZj1;n0u(rT0#@rfdYp{VZPtoCtYHoENW~K
zKso1jHDWmqs_+z_hrB2}dSc%{`#=k)z<$C!tPNwD-b$C9jM9Y_fUx3Llx(*fAQ{%K
z-2D{Z+iIdG=<(jAMGtnq95!WRs>qjdeg_Gt*H!}{a9{)Y0+3h~7#xfR*~hL+vH
zzG2CQiQ}GL3S6+AJ8A{ubC{Jos%IAbT8F2mb2fe1g~Xrli*uNsF@nF~?rdfHw#Q5R
zmV26mozFr^kDWwu+#POZnwlzhI-Xa9h<0IPY$X?>WSA%$#n7$iKhi+rSu|Q2Q0M-T
zvZ1Bd-0kI1Abm)dNWxMquE5W9*H_g7?!PCPs)0>BHgr6Z=Pp7YtWaUHw_)UVS2aST_@UI%^V0*)rqREivZh*q6x=Vml
z`@7H1%B7y{L4F;O$)_X$+pe!bnw-Ax4R+Ct+D<8LUX^1s0F^FM%Pee7tC3c?8KnW{)$0#O@3(3V9T!VUbD^yy1{)TbXn_&
z{ATG%qu7qE)Z@aV2ci$nKz~`=Qo3I!o!^^eqIs4^Y6{Db6grzPYHFY^}4u??>
zavMLw7w_>DmPRqpg|ds9INwSis{EeJ1|#gk4pk|}Nx-sSfQJmG?k
z`pr1$c+DY#AN1UqlG^Zl4dmwPBEX`#xtLlzd=`wqvYQJKPyLhykA?>UAVX5$8`xz)mg{fa
z(J6MB>&hWcKUw)>0gp)}{TN#uO;Y1h0o0XG%UugXRdhC^u>W(}YMtJOcjUsG)q`L@
zwe$&z7@vddyi=NM>TIE@$znA{qh+AmSb;c}eA3sL?^MP@&^@b)M%8p*`o*`g8=k6x
zsGN}1e1XS6JVfl>c8TqERxzW7tOvR(MB?;GmJO&74}uzIV`|=F2sDKUfe)-EP3eAl
zs`z;yAjO6)1>PNvV4l`}?>FwX2H6Xv7k;8T1>+E$Nz1i81By*eJsYl2I
zjmNyvAko6uA8>`d((2;%kifWP&meYes~`E{<8ga+og~bGN>)N>0kyo#P%jUeOMlQ7
zS2&hr$*B=xuU+Zrwn+QJjE2AGBD9srtt;t4c0b?ie+EqyD1+#Qc&*t6*gP0}Ou`4x
zDM^2eayk5J?pbI$dA81jh=}C;z+g|dLjNPL@Zd#wF!N3&>dZjPp9!>&5Alu&o1b<7
z$xvVJ$1zts6=U@+$yx1mddW0d#?Iw22%P|eh;g0m!+0PwXjy!p74b2bevq~)VsM#o0Z5wwf*1!TEJeG|!KK2T$QaO!z@4}1L>c8D2#O+r
z(1%=i1RW7TFacE^Q%G%4JhzAQ=^{q`_j*Q6cyVL|(B9htQYA9|6bk!96&R5BAsce<
zTP5al?VzRWaP)bDIlr#4wdQA!My1Nx`Ig3gTrS_3=%*cD6qaHuo9xsKv?|D-v@$xZ
zP0$mi>-kMr5MU2tf!b)C{U6gkVH=2!PDL
zW4C4BjhYe#9TGwq66uvW+QTF@3bC%G-toHo&;BrpA4?aRnkh`dvIChCK`=lbcYtDv
zAaEg(nLx!v5Y#{x#n%Kwd);EEdtP=qj4rh(LRI-C>s;j}H_!b(JW6Rjq>S4Qu4Ekk
zkR;=+?heSl{k@OLgC){Ci{?M>I+=yTon$tzaY$Zy2tR(L@s1*!%I7*#OL>LdH8(FS
z43FDnnAp^a1MQ>PM;YZra@4&Uk9D}aZb+fYm_)Zk?;-2S7?2A7MTSXRdbmoI|
zcW<3~MK%{T4+$S;Dp#C=uaAjM*gTz5^X20h^!FHX+ekgnUjcd2Q55W6ijOB_$_*;=
z>G}ou()7$gSwck_O)oU8gYMM!PzpTYS3b&uOlMA9&2KENnfecD*m4Li37doAr<~(H
z&z%-|;V&~D$_7yfM+_&zNpub4!qagsxdxQ9FF`V~Fj}Hq%PqP&;SB@z={x*L=cOSr
zP=v@|=0Ch|GQ}FuY4G8n4h~a__P>V*4N25R85Y|B8*k+Zu3+U=elPhg)v}#*Vg3>*
z_4nS)p)oMC&n#@)R4>PzP
zr{x#`_D_oVw>I7)7wv
zbCz>;e4fMoH9G$o`gK5yKkVyI*2N=%ZOV=z@%&B=e|^~v!gwzO!QeyN0iOu{&%ZB-
zS*@{JjUppQ?AKcgY8ME7!ZoVK3@f4JCy?OS3@#h+YsxH^?^pWMyPLuxlgcY1i$N`k
zvt~CB+At{u%P3Dlaw4E?QV0T|{ho1I_=;s{^|D4`Oskj~cXd;3CNOQjVuSG}
z97P?}>@^re*z2Qx`x$zbppG=FB%UlRlc}n*t>Vj$-_3q`_0lC{HIe}Q%)St=y_O*J
zIC4ULc^1+}P_}lp3s;{~*!5IT|LObN#g7Faj%l8*^v<5N3&VJvA+37q1b;FD3k$ZG
zH)X!4Q&LpUZOOGsz&=Lw5sa{ZbnBT+Ic6OxkgrN~W5RywYO5#dR~AGcV02RY$@+!)
zFo@!dvdr3}hO>^oZ=MH_i@<3i&(LRul<`i%3ZM|>-65Q~l3MMY>~gT=?e=cr*sUlf
z{$+kCYkJErUZyF#3vKCIs)C{q@H7!FDTyu8Cg9gEr`^CFH#VuO^hjJ#GSlLsY*z~N|*P8otdy~0hY(1ocG^m
zn_cYwex*B$Vl4|wVHloP*FbU&w`GWV&EbaPxJxbJcm5I37e#bkv#0S#Q9rG_K(FA5
zg3wCsnxH!76=4uHTLtIy)w`iH3ro+&2x4Vjeiv_ShwaO|#Uz)jAROHAq9iOznHF7v
zcgOXv7po3~gX^$osL7>ga==}rz`EH(tG1d%|6F1jJKw$CAM(Twta5>+Sk&axif5*r
zQdkAO7KdHXs<}}7A9qS+LTDn!&32uxL>dRriU&R;8HLT!@n>Zny-(S0bvB`Ei~I&*
z#kg3gnuOP~8&A7#oD1bh6-u1B)uqSZ4RO~iamkMw$09-b7nMY;9k=cF;z+if&?qP
z0gxa_#uNJMfEP)BU3Sr>waHI?IV95*nSgDa#sndfdrOn|+Z#rdU6!pdZLhR*2b?;6
zjGB=laJBSpgg(pYYsihcS3spaLoOYg1xoXo1$v{
zu#Y;FASA3c#4L_|A5KZbSv^XeF-}iQW;`jwE{M6xw{SOt1vHOO30P
z9!7zUI{rp@C4*iv^-Og)tBJ*J~Q`BpH)wwS?tDFYK4AR*z*J`=0bE!1l{t1v4?
z$6ZX)T=tqT6nwXPr&>rOYvpAQIXW;qu64J>MIbJIERdcR+as&jc8@ldj2W$wh?&r{
zvc~mJ_Vlx(4^Pn7F-SSm*-3w@nfi#(Y-Ji97U?m5Mm!<&=-(>f9RZ>U&_MU(3uQxkqZ
zdqqB3A&=ECl6kHO>;Sg&f&8Yl0iAt=Lu)_1U1x;Ml2nf8d+v`{_T8&Hp4tkJiOt*h
zIEIJ;^VQEQ?;-Eev-I}K=R{ZdgO;mchnPDpq2YnGKV}K{u{5_RXS-5Ga7^ah^T^RA
zZ>*R6BKuvQ9Gck#hojb~>re>kE~1Qi{eMrC9QZ;l^T~USE@_38Si#9Uhf^)Y%;YR$
zC?<8(6}SoK@s0#V1(cGd1LuJKSYW=E`%ob~>%YcDx^=&7gU
zxc)uDday$7^o^?Qn1VQ}zFBukc#WagnzjS5YZpX2@wPN91#PkNA-y;H>jnE`(+s$$
zOe4b}eL+UVM2>t#G?{Aln>vDu6c~H56{LE^J}4B{chosOO4m{@*N{6jurw}E#z)q#Et(Q3F7%x67Kf>QJB);
zS$EKnx?9w)ZU|DJP7@`dpx@QqQPgbMJ7FAF;XtX|Gq2;UYHPbq<6R}qJ0tz)omaU3
zRfyhvPYaO~@Kzx6tpq|q>`huZf-n+)lLVO{?Uml7N*~B&j5jGF7Siag+NSw94pKww
zt?k1BWcXW&PV?k1NV3qkwsS|Q%JMfUmk4^b_Dup#LR+N1NeAXIvwCk*XAjJS%bV23
z3HxQ}twd+sL?v1a4gmOo@wY^$+4vFmGu)fWI3%3Oe>!J_h8xv+YkM|;GbVbIjJ@H&
z?^yp<`wX|h-Il&dy{7Oc|Ec@I)(%@10~ZZlLx6)~HA|SotNtfcx&=H?;LVsY7yioe
zO~SxH@b-L@;vx|w6yKzUMFgk+c*rdy;QnWX%n1>jSfQ}}?81oU5y2pVK?Z{Y1{KUZ
zFlb=V!C-*F1cLU_MEt2meeVFef0~kgyOkkM7uz+C&!v=;O%zH2#U^u~W
zf#C+j)9m}m>+Aa#<`Y!fuxpdlPipWwjCh-vK&MTe~bf
z>EDvEf1kJjAG&z^D+ts8A$G`;zJ+7zkR^mL1<7>C62Cb$j1KyJg8~4|!D|uw9}nrhLrN7TnH1r^Qu)^|bQJ!i)&c;0g`od6
z9)CbAJ^wZ0%lg!$2A-7=BmjWmf6a;v$f-w`{%t%md%)u{`wJ4Z{tFW4|IEYY->Wx{
zP#_2=C>&5p=YL0QgZEIqycPf$r9=2v_eCI)URf&gx0U4EV$PKc0E9)t{L3h05*idY
z35^5#+AI53bqFf$1>fHZXb|lCmet8$y$=N6_g|g053F~C!#t!~oY=HUSt8xZ312%fg(k%;)_Nxv6@Y5RVUq)Qea3E1=I2;gD|9`U-=m)P@
zNJEfzzbxfjn*QJhC<|{mkfS%;{~f$u@KuO$&|3e0ljaEvj`*9;`v1vi2t+pUU!(uo
zegB;_1IP?)^ww|W0620MsOTSk;;&8yI{HUP8wBgPAg00p2IVFk*uhc+0D9g3y#|v(
z4*wWQU&WpO-S;26(TRq@`ezXD5coQHcLy2$)hR$eL$WMy
zdIeaAN*KilG0P(ofOdyu@!pzW|C$AY2#00a-*ly6@W=u@LAJxP+;0=yH@=rd0baX4
z2mk=#|604Qpx$9whQC`N=nU)yF$F>#0e24GCPC~YV0{&&2-ZpeZj2+F`$4JTv%&1(
zFTnp^03D!suo3xRqXCwD→ ¬ ¬ ¬ A
     -------
   → ¬ A
-¬¬¬-elim ¬¬¬x  =  λ x → ¬¬¬x (¬¬-intro x)
-

Let ¬¬¬x be evidence of ¬ ¬ ¬ A. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then by the previous result, we can conclude ¬ ¬ A, evidenced by ¬¬-intro x. Then from ¬ ¬ ¬ A and ¬ ¬ A we have a contradiction, evidenced by ¬¬¬x (¬¬-intro x). Hence we have shown ¬ A.

Another law of logic is contraposition, stating that if A implies B, then ¬ B implies ¬ A:
contraposition : ∀ {A B : Set}
-  → (A → B)
-    -----------
-  → (¬ B → ¬ A)
-contraposition f ¬y x = ¬y (f x)
-

Let f be evidence of A → B and let ¬y be evidence of ¬ B. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then from A → B and A we may conclude B, evidenced by f x, and from B and ¬ B we may conclude ⊥, evidenced by ¬y (f x). Hence, we have shown ¬ A.

Using negation, it is straightforward to define inequality:
_≢_ : ∀ {A : Set} → A → A → Set
-x ≢ y  =  ¬ (x ≡ y)
-
It is trivial to show distinct numbers are not equal:
_ : 1 ≢ 2
-_ = λ()
-
This is our first use of an absurd pattern in a lambda expression. The type M ≡ N is occupied exactly when M and N simplify to identical terms. Since 1 and 2 simplify to distinct normal forms, Agda determines that there is no possible evidence that 1 ≡ 2. As a second example, it is also easy to validate Peano’s postulate that zero is not the successor of any number:
peano : ∀ {m : ℕ} → zero ≢ suc m
-peano = λ()
+¬¬¬-elim ¬¬¬x x  =  ¬¬¬x (¬¬-intro x)
+

Let ¬¬¬x be evidence of ¬ ¬ ¬ A. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then by the previous result, we can conclude ¬ ¬ A, evidenced by ¬¬-intro x. Then from ¬ ¬ ¬ A and ¬ ¬ A we have a contradiction, evidenced by ¬¬¬x (¬¬-intro x). Hence we have shown ¬ A.

Another law of logic is contraposition, stating that if A implies B, then ¬ B implies ¬ A:
contraposition : ∀ {A B : Set}
+  → (A → B)
+    -----------
+  → (¬ B → ¬ A)
+contraposition f ¬y x = ¬y (f x)
+

Let f be evidence of A → B and let ¬y be evidence of ¬ B. We will show that assuming A leads to a contradiction, and hence ¬ A must hold. Let x be evidence of A. Then from A → B and A we may conclude B, evidenced by f x, and from B and ¬ B we may conclude ⊥, evidenced by ¬y (f x). Hence, we have shown ¬ A.

Using negation, it is straightforward to define inequality:
_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y  =  ¬ (x ≡ y)
+
It is trivial to show distinct numbers are not equal:
_ : 1 ≢ 2
+_ = λ()
+
This is our first use of an absurd pattern in a lambda expression. The type M ≡ N is occupied exactly when M and N simplify to identical terms. Since 1 and 2 simplify to distinct normal forms, Agda determines that there is no possible evidence that 1 ≡ 2. As a second example, it is also easy to validate Peano’s postulate that zero is not the successor of any number:
peano : ∀ {m : ℕ} → zero ≢ suc m
+peano = λ()

The evidence is essentially the same, as the absurd pattern matches all possible evidence of type zero ≡ suc m.

Given the correspondence of implication to exponentiation and false to the type with no members, we can view negation as raising to the zero power. This indeed corresponds to what we know for arithmetic, where

0 ^ n  ≡  1,  if n ≡ 0
-       ≡  0,  if n ≢ 0
Indeed, there is exactly one proof of ⊥ → ⊥. We can write this proof two different ways:
id : ⊥ → ⊥
-id x = x
-
-id′ : ⊥ → ⊥
-id′ ()
-
But, using extensionality, we can prove these equal:
id≡id′ : id ≡ id′
-id≡id′ = extensionality (λ())
-

By extensionality, id ≡ id′ holds if for every x in their domain we have id x ≡ id′ x. But there is no x in their domain, so the equality holds trivially.

Indeed, we can show any two proofs of a negation are equal:
assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
-assimilation ¬x ¬x′ = extensionality (λ x → contradiction x ¬x)
-

Evidence for ¬ A implies that any evidence of A immediately leads to a contradiction. But extensionality quantifies over all x such that A holds, hence any such x immediately leads to a contradiction, again causing the equality to hold trivially.

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

-- Your code goes here
-
Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

-- Your code goes here
-
Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

-- Your code goes here
-

Do we also have the following?

¬ (A × B) ≃ (¬ A) ⊎ (¬ B)

If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?

Intuitive and Classical logic

In Gilbert and Sullivan’s The Gondoliers, Casilda is told that as an infant she was married to the heir of the King of Batavia, but that due to a mix-up no one knows which of two individuals, Marco or Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say that I am married to one of two gondoliers, but it is impossible to say which?” To which the response is “Without any doubt of any kind whatever.”

Logic comes in many varieties, and one distinction is between classical and intuitionistic. Intuitionists, concerned by assumptions made by some logicians about the nature of infinity, insist upon a constructionist notion of truth. In particular, they insist that a proof of A ⊎ B must show which of A or B holds, and hence they would reject the claim that Casilda is married to Marco or Giuseppe until one of the two was identified as her husband. Perhaps Gilbert and Sullivan anticipated intuitionism, for their story’s outcome is that the heir turns out to be a third individual, Luiz, with whom Casilda is, conveniently, already in love.

Intuitionists also reject the law of the excluded middle, which asserts A ⊎ ¬ A for every A, since the law gives no clue as to which of A or ¬ A holds. Heyting formalised a variant of Hilbert’s classical logic that captures the intuitionistic notion of provability. In particular, the law of the excluded middle is provable in Hilbert’s logic, but not in Heyting’s. Further, if the law of the excluded middle is added as an axiom to Heyting’s logic, then it becomes equivalent to Hilbert’s. Kolmogorov showed the two logics were closely related: he gave a double-negation translation, such that a formula is provable in classical logic if and only if its translation is provable in intuitionistic logic.

Propositions as Types was first formulated for intuitionistic logic. It is a perfect fit, because in the intuitionist interpretation the formula A ⊎ B is provable exactly when one exhibits either a proof of A or a proof of B, so the type corresponding to disjunction is a disjoint sum.

(Parts of the above are adopted from “Propositions as Types”, Philip Wadler, Communications of the ACM, December 2015.)

Excluded middle is irrefutable

The law of the excluded middle can be formulated as follows:
postulate
-  em : ∀ {A : Set} → A ⊎ ¬ A
-
As we noted, the law of the excluded middle does not hold in intuitionistic logic. However, we can show that it is irrefutable, meaning that the negation of its negation is provable (and hence that its negation is never provable):
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
-em-irrefutable = λ k → k (inj₂ (λ x → k (inj₁ x)))
-

The best way to explain this code is to develop it interactively:

em-irrefutable k = ?

Given evidence k that ¬ (A ⊎ ¬ A), that is, a function that given a value of type A ⊎ ¬ A returns a value of the empty type, we must fill in ? with a term that returns a value of the empty type. The only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k ?

We need to fill the new hole with a value of type A ⊎ ¬ A. We don’t have a value of type A to hand, so let’s pick the second disjunct:

em-irrefutable k = k (inj₂ λ{ x → ? })

The second disjunct accepts evidence of ¬ A, that is, a function that given a value of type A returns a value of the empty type. We bind x to the value of type A, and now we need to fill in the hole with a value of the empty type. Once again, the only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k (inj₂ λ{ x → k ? })

This time we do have a value of type A to hand, namely x, so we can pick the first disjunct:

em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })

There are no holes left! This completes the proof.

The following story illustrates the behaviour of the term we have created. (With apologies to Peter Selinger, who tells a similar story about a king, a wizard, and the Philosopher’s stone.)

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realised that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said, “Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

(Parts of the above are adopted from “Call-by-Value is Dual to Call-by-Name”, Philip Wadler, International Conference on Functional Programming, 2003.)

Exercise Classical (stretch)

Consider the following principles:

Show that each of these implies all the others.

-- Your code goes here
-
Exercise Stable (stretch)
Say that a formula is stable if double negation elimination holds for it:
Stable : Set → Set
-Stable A = ¬ ¬ A → A
-

Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.

-- Your code goes here
-

Standard Prelude

Definitions similar to those in this chapter can be found in the standard library:
import Relation.Nullary using (¬_)
-import Relation.Nullary.Negation using (contradiction; contraposition)
+       ≡  0,  if n ≢ 0
Indeed, there is exactly one proof of ⊥ → ⊥. We can write this proof two different ways:
id : ⊥ → ⊥
+id x = x
+
+id′ : ⊥ → ⊥
+id′ ()
+
But, using extensionality, we can prove these equal:
id≡id′ : id ≡ id′
+id≡id′ = extensionality (λ())
+

By extensionality, id ≡ id′ holds if for every x in their domain we have id x ≡ id′ x. But there is no x in their domain, so the equality holds trivially.

Indeed, we can show any two proofs of a negation are equal:
assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
+assimilation ¬x ¬x′ = extensionality (λ x → contradiction x ¬x)
+

Evidence for ¬ A implies that any evidence of A immediately leads to a contradiction. But extensionality quantifies over all x such that A holds, hence any such x immediately leads to a contradiction, again causing the equality to hold trivially.

Exercise <-irreflexive (recommended)

Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

-- Your code goes here
+
Exercise trichotomy (practice)

Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

Here “exactly one” means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.

-- Your code goes here
+
Exercise ⊎-dual-× (recommended)

Show that conjunction, disjunction, and negation are related by a version of De Morgan’s Law.

¬ (A ⊎ B) ≃ (¬ A) × (¬ B)

This result is an easy consequence of something we’ve proved previously.

-- Your code goes here
+

Do we also have the following?

¬ (A × B) ≃ (¬ A) ⊎ (¬ B)

If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?

Intuitive and Classical logic

In Gilbert and Sullivan’s The Gondoliers, Casilda is told that as an infant she was married to the heir of the King of Batavia, but that due to a mix-up no one knows which of two individuals, Marco or Giuseppe, is the heir. Alarmed, she wails “Then do you mean to say that I am married to one of two gondoliers, but it is impossible to say which?” To which the response is “Without any doubt of any kind whatever.”

Logic comes in many varieties, and one distinction is between classical and intuitionistic. Intuitionists, concerned by assumptions made by some logicians about the nature of infinity, insist upon a constructionist notion of truth. In particular, they insist that a proof of A ⊎ B must show which of A or B holds, and hence they would reject the claim that Casilda is married to Marco or Giuseppe until one of the two was identified as her husband. Perhaps Gilbert and Sullivan anticipated intuitionism, for their story’s outcome is that the heir turns out to be a third individual, Luiz, with whom Casilda is, conveniently, already in love.

Intuitionists also reject the law of the excluded middle, which asserts A ⊎ ¬ A for every A, since the law gives no clue as to which of A or ¬ A holds. Heyting formalised a variant of Hilbert’s classical logic that captures the intuitionistic notion of provability. In particular, the law of the excluded middle is provable in Hilbert’s logic, but not in Heyting’s. Further, if the law of the excluded middle is added as an axiom to Heyting’s logic, then it becomes equivalent to Hilbert’s. Kolmogorov showed the two logics were closely related: he gave a double-negation translation, such that a formula is provable in classical logic if and only if its translation is provable in intuitionistic logic.

Propositions as Types was first formulated for intuitionistic logic. It is a perfect fit, because in the intuitionist interpretation the formula A ⊎ B is provable exactly when one exhibits either a proof of A or a proof of B, so the type corresponding to disjunction is a disjoint sum.

(Parts of the above are adopted from “Propositions as Types”, Philip Wadler, Communications of the ACM, December 2015.)

Excluded middle is irrefutable

The law of the excluded middle can be formulated as follows:
postulate
+  em : ∀ {A : Set} → A ⊎ ¬ A
+
As we noted, the law of the excluded middle does not hold in intuitionistic logic. However, we can show that it is irrefutable, meaning that the negation of its negation is provable (and hence that its negation is never provable):
em-irrefutable : ∀ {A : Set} → ¬ ¬ (A ⊎ ¬ A)
+em-irrefutable = λ k → k (inj₂ (λ x → k (inj₁ x)))
+

The best way to explain this code is to develop it interactively:

em-irrefutable k = ?

Given evidence k that ¬ (A ⊎ ¬ A), that is, a function that given a value of type A ⊎ ¬ A returns a value of the empty type, we must fill in ? with a term that returns a value of the empty type. The only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k ?

We need to fill the new hole with a value of type A ⊎ ¬ A. We don’t have a value of type A to hand, so let’s pick the second disjunct:

em-irrefutable k = k (inj₂ λ{ x → ? })

The second disjunct accepts evidence of ¬ A, that is, a function that given a value of type A returns a value of the empty type. We bind x to the value of type A, and now we need to fill in the hole with a value of the empty type. Once again, the only way we can get a value of the empty type is by applying k itself, so let’s expand the hole accordingly:

em-irrefutable k = k (inj₂ λ{ x → k ? })

This time we do have a value of type A to hand, namely x, so we can pick the first disjunct:

em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })

There are no holes left! This completes the proof.

The following story illustrates the behaviour of the term we have created. (With apologies to Peter Selinger, who tells a similar story about a king, a wizard, and the Philosopher’s stone.)

Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars. Of course, I get to choose whether I offer (a) or (b).”

The man was wary. Did he need to sign over his soul? No, said the devil, all the man need do is accept the offer.

The man pondered. If he was offered (b) it was unlikely that he would ever be able to buy the wish, but what was the harm in having the opportunity available?

“I accept,” said the man at last. “Do I get (a) or (b)?”

The devil paused. “I choose (b).”

The man was disappointed but not surprised. That was that, he thought. But the offer gnawed at him. Imagine what he could do with his wish! Many years passed, and the man began to accumulate money. To get the money he sometimes did bad things, and dimly he realised that this must be what the devil had in mind. Eventually he had his billion dollars, and the devil appeared again.

“Here is a billion dollars,” said the man, handing over a valise containing the money. “Grant me my wish!”

The devil took possession of the valise. Then he said, “Oh, did I say (b) before? I’m so sorry. I meant (a). It is my great pleasure to give you one billion dollars.”

And the devil handed back to the man the same valise that the man had just handed to him.

(Parts of the above are adopted from “Call-by-Value is Dual to Call-by-Name”, Philip Wadler, International Conference on Functional Programming, 2003.)

Exercise Classical (stretch)

Consider the following principles:

Show that each of these implies all the others.

-- Your code goes here
+
Exercise Stable (stretch)
Say that a formula is stable if double negation elimination holds for it:
Stable : Set → Set
+Stable A = ¬ ¬ A → A
+

Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.

-- Your code goes here
+

Standard Prelude

Definitions similar to those in this chapter can be found in the standard library:
import Relation.Nullary using (¬_)
+import Relation.Nullary.Negation using (contradiction; contraposition)

The standard library uses contradiction, which combines our ¬-elim and ⊥-elim.

Unicode

This chapter uses the following unicode:

¬  U+00AC  NOT SIGN (\neg)
 ≢  U+2262  NOT IDENTICAL TO (\==n)

Quantifiers: Universals and existentials

module plfa.part1.Quantifiers where

This chapter introduces universal and existential quantification.

Imports

import Relation.Binary.PropositionalEquality as Eq
diff --git a/rss.xml b/rss.xml
index 093e64bca..2daa7bec1 100644
--- a/rss.xml
+++ b/rss.xml
@@ -8,7 +8,7 @@
     
     en
     
-    Wed, 13 Nov 2024 15:33:32 +0000
+    Thu, 14 Nov 2024 11:20:43 +0000
         
       Migration to Agda 2.7.0
       https://plfa.github.io//2024/09/05/migration-to-agda-2-7-0/index.html