From c78d8dd8916488a04a6374be0df56307292c35f6 Mon Sep 17 00:00:00 2001
From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com>
Date: Fri, 12 Apr 2024 17:44:16 -0400
Subject: [PATCH] Wiki updates (#40)
---
wiki/pages/deterministic-declaration.elf | 2 +-
wiki/pages/general-description-of-twelf.elf | 21 +-
...nguages-to-use-hypothetical-judgements.elf | 653 +++++++++++++-----
wiki/src/assets/serverok.png | Bin 0 -> 142441 bytes
wiki/src/content/docs/contributing.mdx | 11 +-
5 files changed, 503 insertions(+), 184 deletions(-)
create mode 100644 wiki/src/assets/serverok.png
diff --git a/wiki/pages/deterministic-declaration.elf b/wiki/pages/deterministic-declaration.elf
index caa713d3..5f1a8e27 100644
--- a/wiki/pages/deterministic-declaration.elf
+++ b/wiki/pages/deterministic-declaration.elf
@@ -8,7 +8,7 @@
We define a tree with labeled nodes, and a distinguished tree ``testtree``.
-![A starry night sky.](../../../assets/smalltree.png)
+![Visual description of a balanced tree with four labeled leaves.](/src/assets/smalltree.png)
Graphical representation of the tree ``testtree`` used in this example.
diff --git a/wiki/pages/general-description-of-twelf.elf b/wiki/pages/general-description-of-twelf.elf
index 626260b9..81fc846f 100644
--- a/wiki/pages/general-description-of-twelf.elf
+++ b/wiki/pages/general-description-of-twelf.elf
@@ -1,20 +1,21 @@
%%! title: "General description of Twelf"
+%%! description: "A quick introduction to Twelf, aimed at folks without any specific technical background"
%{! _This quick introduction to Twelf is aimed at people without any specific technical background. If you want more information, you can find it on the [documentation](/wiki/documentation/) page._
-[[Image:ServerOK.png|thumb|_Using Twelf with the Emacs text editor._ The red, blue, and black text at the top is Twelf code, and the black text at the bottom is the output from the Twelf program reading the code.]]**Twelf** is a piece of computer software, and it is also a computer language understood by the Twelf software. This is a common ambiguity in computer systems - you can "install Java on your computer" (Java, a piece of computer software), or you can "write programs in Java for work" (Java, the computer language that is understood and interpreted by the software).
+
+**Twelf** is a piece of computer software, and it is also a computer language understood by the Twelf software. This is a common ambiguity in computer systems - you can "install Java on your computer" (Java, a piece of computer software), or you can "write programs in Java for work" (Java, the computer language that is understood and interpreted by the software).
+
+
+![A Twelf file open in Emacs, showing Twelf's output and the "Server OK" message that means Twelf loaded the file with no errors.](/src/assets/serverok.png)
+
+_Using Twelf with the Emacs text editor. The red, blue, and black text at the top is Twelf code, and the black text at the bottom is the output from the Twelf program reading the code._
+
C code and Java code describe programs, HTML code describes graphical web pages, and Twelf code describes _logical systems._ Logical systems are sometimes strange to think about, because the only logical system that most people have used is basic arithmetic (addition, subtraction, division, etc.), or maybe set theory if they're particularly ambitious. Most people that use Twelf aren’t interested in using it to do basic arithmetic, because there are a great deal more interesting logical systems than just the ones that we learn about in high school.
The reason someone might want to use Twelf code to describe a logical system is that once they’ve described it, they can write more Twelf code that uses that logical system. You could use Twelf to write out a statement about basic arithmetic (for instance, “if a + b = c, then b + a = c”), and then use Twelf to write out a justification of why that statement is true (i.e. a _proof_). When you do so, Twelf will check your proof, making sure that what you said actually is true!
-Twelf is by no means the only program you can use to do this sort of thing. ACL2, AUTOMATH, Coq, HOL, HOL Light, LEGO, Isabelle, MetaPRL, NuPRL PVS, and TPS are just a few (!) of the systems that will let you define logical systems and prove things with them. A lot of really amazing work is done using these different systems: one project at the University of Pittsburgh is using HOL Light to check a proof of the Kepler conjecture [http://code.google.com/p/flyspeck/], and The Economist wrote an article about it [http://www.economist.com/science/displayStory.cfm?story_id=3809661] (unfortunately, it is no longer freely available).
-
-But here’s where, for people that use Twelf, it gets interesting: it turns out that while basic arithmetic, set theory, and interesting logics are logical systems, _programming languages_ are also logical systems - and Twelf has a couple of unique features that make it a great tool to use when the logical systems you are working with are programming languages... !}%
+Twelf is by no means the only program you can use to do this sort of thing. ACL2, Agda, AUTOMATH, HOL, HOL Light, Lean, LEGO, Isabelle, MetaPRL, NuPRL PVS, Rocq, and TPS are just a few (!) of the systems that will let you define logical systems and prove things with them. A lot of really amazing work is done using these different systems: one project at the University of Pittsburgh used HOL Light to [check a proof of the Kepler conjecture](https://arxiv.org/abs/1501.02155). [The Economist wrote an article about it](http://www.economist.com/science/displayStory.cfm?story_id=3809661), though that article is unfortunately no longer freely available.
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/General_description_of_Twelf).
-!}%
+But here’s where, for people that use Twelf, it gets interesting: it turns out that while basic arithmetic, set theory, and interesting logics are logical systems, _programming languages_ are also logical systems - and Twelf has a couple of unique features that make it a great tool to use when the logical systems you are working with are programming languages... !}%
\ No newline at end of file
diff --git a/wiki/pages/reformulating-languages-to-use-hypothetical-judgements.elf b/wiki/pages/reformulating-languages-to-use-hypothetical-judgements.elf
index ff1e46e5..12285a91 100644
--- a/wiki/pages/reformulating-languages-to-use-hypothetical-judgements.elf
+++ b/wiki/pages/reformulating-languages-to-use-hypothetical-judgements.elf
@@ -1,133 +1,214 @@
%%! title: "Reformulating languages to use hypothetical judgements"
+%%! description: "Using parallel reduction in the lambda calculus, this article explores different ways to use LF to represent relations that have special cases for variables."
-%{! It's easy to represent [hypothetical judgement](/wiki/hypothetical-judgment/)s in LF, exploiting [higher-order](/wiki/higher-order-judgements/) representation techniques. This tutorial presents some object-language judgements which are **not** typically phrased as hypothetical judgements, but can easily be reformulated as such, making the correspondence with their LF representation quite clear.
-In particular, we discuss parallel reduction and complete development for the lambda-calculus; thanks to [[User:rpollack]] for suggesting this example.
+%{! It's easy to represent [hypothetical judgements](/wiki/hypothetical-judgment/) in LF, exploiting [higher-order](/wiki/higher-order-judgements/) representation techniques. This tutorial presents some object-language judgements which are **not** typically phrased as hypothetical judgements, but can easily be reformulated as such, making the correspondence with their LF representation quite clear. In particular, we discuss parallel reduction and complete development for the lambda-calculus; thanks to Randy Pollack for suggesting this example.
-Before reading this tutorial, you should learn about hypothetical judgements and their representation in LF: [Proving metatheorems: Representing the judgements of the STLC](/wiki/proving-metatheorems-representing-the-judgements-of-the-stlc/) shows how object-language hypothetical judgements can be represented using LF binding. [Proving metatheorems: Proving totality assertions in non-empty contexts](/wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/) shows an additional example, and discusses proving totality assertions about higher-order judgements. [Proving metatheorems: Proving metatheorems in non-empty contexts](/wiki/proving-metatheorems-proving-metatheorems-in-non-empty-contexts/) shows how to use totality assertions to prove metatheorems about higher-order judgements.
+Before reading this tutorial, you should learn about hypothetical judgements and their representation in LF:
+
+ - [Representing the judgements of the STLC](/wiki/proving-metatheorems-representing-the-judgements-of-the-stlc/) shows how object-language hypothetical judgements can be represented using LF binding.
+ - [Proving totality assertions in non-empty contexts](/wiki/proving-metatheorems-proving-totality-assertions-in-non-empty-contexts/) shows an additional example, and discusses proving totality assertions about higher-order judgements.
+ - [Proving metatheorems in non-empty contexts](/wiki/proving-metatheorems-proving-metatheorems-in-non-empty-contexts/) shows how to use totality assertions to prove metatheorems about higher-order judgements.
## Syntax is a hypothetical judgement
First, we need to define the syntax of the untyped lambda-calculus:
-<code>
-M ::= x | lam x.M | app M1 M2
-</code>
+```math
+M ::= x \mid \mathsf{lam}(x.M) \mid \mathsf{app}(M_1, M_2)
+```
-A traditional story about this definition is that variables ``x`` are some piece of first-order data such as strings or de Bruijn indices, ``lam x.M`` is a binder (which means it can be <math>\alpha</math>-converted and can be substituted for) and so on.
+A traditional story about this definition is that variables are some piece of first-order data such as strings or de Bruijn indices, is a binder (which means it can be -converted and can be substituted for) and so on.
-However, suppose we were given a single untyped datatype of tree-structured data with binding as a primitive notion, where such trees consist of variables ``x``, binders ``x.t``, and applications of constants such as ``lam`` and ``app``. Then we can save ourselves the trouble of recapitulating the construction of binding for each object language by simply carving out those trees that represent the language in question. We can do so with a hypothetical judgement of the form ``x1 trm ... xn trm |- M trm``, where the subjects of the judgement ``trm`` are untyped binding trees. This judgement is defined as follows:
+However, suppose we were given a single untyped datatype of tree-structured data with binding as a primitive notion, where such trees consist of variables , binders , and applications of constants such as and . Then we can save ourselves the trouble of recapitulating the construction of binding for each object language by simply carving out those trees that represent the language in question. We can do so with a hypothetical judgement of the form
-<code>
-x trm in G
-----------
-G |- x trm
+```math
+x_1\,\mathtt{trm} \; \ldots \; x_n\,\mathtt{trm} \vdash M\,\mathtt{trm}
+```
-G |- M1 trm G |- M2 trm
--------------------------
-G |- (app M1 M2) trm
+where the subjects of the judgement "" are untyped binding trees. This judgement is defined as follows:
+```math
+{
+ {x\,\mathtt{trm} \in \Gamma}
+ \over
+ {\Gamma \vdash x\,\mathtt{trm}}
+}
+\qquad
+{
+ {\Gamma \vdash M_1\,\mathsf{trm} \qquad \Gamma \vdash M_2\,\mathsf{trm}}
+ \over
+ {\Gamma \vdash \mathsf{app}(M_1, M_2)\,\mathtt{trm}}
+}
+```
-G , x trm |- M trm
-------------------
-G |- lam (x.M) trm
-</code>
+```math
+{
+ {\Gamma, x\,\mathtt{trm} \vdash M\,\mathtt{trm}}
+ \over
+ {\Gamma \vdash \mathsf{lam}(x.M)\,\mathtt{trm}}
+}
+```
-A variable is a term if it was assumed to be a term; at a binder, we extend the context by assuming a new term. The important point about this style of definition is that variables are inherently _scoped_ and given meaning only by assumption: ``x`` is only meaningful if we are in a context where we have some assumptions about it. Consequently, ``x1 trm ... xn trm |- M trm`` captures exactly the terms with free variables ``x1``...``xn``.
+A variable is a term if it was assumed to be a term; at a binder, we extend the context by assuming a new term. The important point about this style of definition is that variables are inherently _scoped_ and given meaning only by assumption: is only meaningful if we are in a context where we have some assumptions about it. Consequently,
-When you're working with an inherently scoped type of binding trees, you can't give an unconditional definition of what it means to be a term with rules like
+```math
+x_1\,\mathtt{trm} \; \ldots \; x_n\,\mathtt{trm} \vdash M\,\mathtt{trm}
+```
-<code>
------
-x trm
+captures exactly the terms with free variables ....
-M trm
--------------
-lam (x.M) trm
-</code>
+When you're working with an inherently scoped type of binding trees, you can't give an unconditional definition of what it means to be a term with rules like
+
+```math
+\color{red}
+{
+ \over
+ {x\,\mathtt{trm}}
+}
+\qquad
+{
+ M\,\mathtt{trm}
+ \over
+ \mathsf{lam}(x.M)\,\mathtt{trm}
+}
+```
where the first rule means "all those trees that happen to be variables are terms": it would break the abstraction of variables-as-scoped-data to state a rule about all those trees that happen to be variables.
The moral of the story is that syntax with binding can be thought of as a hypothetical judgement.
-The LF encoding of this syntax can be thought of as an [intrinsic encoding](/wiki/intrinsic-and-extrinsic-encodings/) of the above judgement ``x1 trm ... xn trm |- M trm``. LF provides typed binding trees, so we can define terms by specifying typed operators, rather than a predicate over untyped trees: !}%
+The LF encoding of this syntax can be thought of as an [intrinsic encoding](/wiki/intrinsic-and-extrinsic-encodings/) of the above judgement . LF provides _typed_ binding trees, so we can define terms by specifying typed operators, rather than a predicate over untyped trees: !}%
trm : type.
lam : (trm -> trm) -> trm.
app : trm -> trm -> trm.
-%{! Then the judgement ``x1 trm ... xn trm |- M trm`` becomes the LF judgement
-``x1 : trm ... xn : trm |- M : trm`` where ``x`` and ``M`` are LF variables and terms.
-
-## Parallel reduction
-
-Parallel reduction is traditionally defined as follows. For conciseness, we write ``\x.M`` for ``lam x.M`` and ``M1 M2`` for ``app M1 M2``
-
-<pre>
-------- var
-x => x
-
-M => M' N => N'
--------------------- beta
-(\x.M) N => M'[N'/x]
-
-M => M' N => N'
----------------- app
-(M N) => (M' N')
-
- M => N
-------------- lam
-\x.M => \x.N
-</pre>
+%{! Then this judgement:
-However, if we want to treat variables as scoped data, we must be explicit about scoping:
+```math
+x_1\,\mathtt{trm} \; \ldots \; x_n\,\mathtt{trm} \vdash M\,\mathtt{trm}
+```
-<pre>
-G ::= . | G , x trm
+becomes the following LF judgment:
-x trm in G
------------ var
-G |- x => x
-
-G, x trm |- M => M' G |- N => N'
---------------------------------- beta
-G |- (\x.M) N => M'[N'/x]
+```math
+x_1 : \mathtt{trm} \; \ldots \; x_n : \mathtt{trm} \vdash M : \mathtt{trm}
+```
-G |- M => M' G |- N => N'
--------------------------- app
-G |- (M N) => (M' N')
+where the and are LF variables and terms.
-G, x trm |- M => N
-------------------- lam
-G |- \x.M => \x.N
-</pre>
+## Parallel reduction
-Now at least the judgement only talks about well-scoped data. However, the ``var`` rule is somewhat problematic. In the abstract, it says "derive ``G |- J'`` if ``J`` is in ``G``", where ``J`` and ``J'`` are _different judgements_. This isn't one of the structural principles of a [hypothetical judgement](/wiki/hypothetical-judgment/), and allowing this strange sort of access to the context could invalidate the substitution principle (if I substitute for ``J``, I can no longer derive ``J'``!). So what are we to do?
+Parallel reduction is traditionally defined as follows. For conciseness, we write instead of and instead of
+
+```math
+{
+ \over
+ x \Rightarrow x
+}\mathit{var}
+\qquad
+{
+ M \Rightarrow M' \qquad N \Rightarrow N'
+ \over
+ (\lambda x.M)\,N \Rightarrow M'[N'/x]
+}\mathit{beta}
+```
+
+```math
+{
+ M \Rightarrow M' \qquad N \Rightarrow N'
+ \over
+ M\,N \Rightarrow M'\,N'
+}\mathit{app}
+\qquad
+{
+ M \Rightarrow M'
+ \over
+ \lambda x.M \Rightarrow \lambda x.M'
+}\mathit{lam}
+```
+
+But there's a problem with this presentation: it's not explicit about scoping! The first rule has the exact same problem as the "bad" rule above that had as a premise and no conclusion.
+
+If we want to treat variables as scoped data, we must be explicit about scoping. This suggests the following presentation:
+
+```math
+\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}
+```
+```math
+{
+ x\,\mathtt{trm} \in \Gamma
+ \over
+ \Gamma \vdash x \Rightarrow x
+}\mathit{var}
+\qquad
+{
+ \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x]
+}\mathit{beta}
+```
+```math
+{
+ \Gamma \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash M\,N \Rightarrow M'\,N'
+}\mathit{app}
+\qquad
+{
+ \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M'
+ \over
+ \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M'
+}\mathit{lam}
+```
+
+Now at least the judgement only talks about well-scoped data. However, the rule that concludes can be a stumbling block for encoding in LF. It has the form "derive if " where and are _different judgements_. That's not one of the structural principles of a [hypothetical judgement](/wiki/hypothetical-judgment/), and allowing this strange sort of access to the context could invalidate the substitution principle (if I substitute for , I can no longer derive !). So what are we to do?
+
+We'll give three possibilities here. The third is in some sense the "most faithful" to the informal specification above. However, when one is not committed to a specific presentation, it's often best to let the formalization guide the informal specification!
### Reformulation 1: Hypothetical reductions
-While a rule that says "derive ``G |- J'`` if ``J`` is in ``G``" is suspicious, a rule that says
-"derive ``G |- **J**`` if ``J`` is in ``G``" is just the usual hypothesis/identity axiom that we expect from all hypothetical judgements. So, one solution is to change the notion of context we consider so that ``var`` is just an instance of hypothesis. In particular, whenever we assume a variable ``x trm``, we also _assume_ a derivation ``x => x``:
-
-<pre>
-G ::= . | G , x trm,x => x
-
-x => x in G
------------ var
-G |- x => x
-
-G, x trm, x => x |- M => M' G |- N => N'
------------------------------------------ beta
-G |- (\x.M) N => M'[N'/x]
-
-G |- M => M' G |- N => N'
--------------------------- app
-G |- (M N) => (M' N')
-
-G, x trm, x => x |- M => N
---------------------------- lam
-G |- \x.M => \x.N
-</pre>
-
-Now the ``var`` rule is unobjectionable. In the premies of the rules ``beta`` and ``lam``, which deal with binding forms, the context is extended with the assumption that ``x => x`` for the bound variable ``x``. The derivations of this version are isomorphic to the first definition of ``G |- M => N``, but the ``var`` rule here has a more generally acceptable form.
+While a rule that says "derive if " is suspicious, a rule that says
+"derive if " is just the usual hypothesis/identity axiom that we expect from all hypothetical judgements. So, one solution is to change the notion of context we consider so that is just an instance of hypothesis. Whenever we assume a variable , we also _assume_ a derivation :
+
+```math
+\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x \Rightarrow x
+```
+```math
+{
+ x \Rightarrow x \in \Gamma
+ \over
+ \Gamma \vdash x \Rightarrow x
+}\mathit{var}_1
+\qquad
+{
+ \Gamma, x\,\mathtt{trm}, x \Rightarrow x \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x]
+}\mathit{beta}_1
+```
+```math
+{
+ \Gamma \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash M\,N \Rightarrow M'\,N'
+}\mathit{app}_1
+\qquad
+{
+ \Gamma, x\,\mathtt{trm}, x \Rightarrow x \vdash M \Rightarrow M'
+ \over
+ \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M'
+}\mathit{lam}_1
+```
+
+In this presentation, the rule is totally unobjectionable. In the premies of the rules and , which deal with binding forms, the context is extended with the assumption that for the bound variable . The derivations of this version are isomorphic to the first definition of , but the rule here works as a use of hypothetical judgements.
The LF representation of this formulation is quite direct: !}%
@@ -145,40 +226,73 @@ The LF representation of this formulation is quite direct: !}%
%block =>b : block {x : trm} {=>/x : x => x}.
%worlds (=>b) (=> _ _).
-%{! Derivations using ``var`` are represented by LF variables representing the reduction assumptions in ``G``. The Twelf ``%worlds`` declaration documents the form of ``G`` in our informal definition.
+%{! Derivations using are represented by LF variables representing the reduction assumptions in . The Twelf ``%worlds`` declaration documents the form of in our informal definition.
-#### Substitution
+#### Adequacy
-This reformulation elucidates a substitution principle for parallel reduction, as an instance of the general substitution principle for hypothetical judgements:
+This is an [adequate encoding](/wiki/adequacy/) of the informal judgment we started with: there's a 1-to-1 correspondence between derivations like this with the rules subscripted with :
-: If ``G, x trm, x => x |- M => N`` and ``G |- M' trm`` and ``G |- M' => M'`` then ``[M'/x]M => [M'/x]N``
+```math
+x_1\,\mathtt{trm}, x_1 \Rightarrow x_1, \ldots, x_k\,\mathtt{trm}, x_k \Rightarrow x_k \vdash M \Rightarrow M'
+```
-In the LF representation, this substitution principle comes "for free" from the general substitution principle for LF terms.
+and with LF derivations $D$ such that the following is derivable according to the rules of LF:
-### Reformulation 2: Change the definition
+```math
+x_1 : \mathtt{trm}, d_1 : x_1 \Rightarrow x_1, \ldots x_k : \mathtt{trm}, d_k : x_k \Rightarrow x_k \vdash D : M \Rightarrow M'
+```
-Another option is to change the definition of the judgement so that it doesn't have a variable-specific rule. In this case, we can generalize the variable rule to a general reflexivity rule:
-<pre>
-G ::= . | G , x trm
+#### Substitution
+
+This reformulation elucidates a substitution principle for parallel reduction, as an instance of the general substitution principle for hypothetical judgements:
------------ refl
-G |- M => M
-
-G, x trm |- M => M' G |- N => N'
---------------------------------- beta
-G |- (\x.M) N => M'[N'/x]
+> If \
+> and \
+> and ,\
+> then .
+
+In the LF representation, this substitution principle comes "for free" from the general substitution principle for LF terms.
-G |- M => M' G |- N => N'
--------------------------- app
-G |- (M N) => (M' N')
+### Reformulation 2: Change the relation
-G, x trm |- M => N
-------------------- lam
-G |- \x.M => \x.N
-</pre>
+Another option is to change the definition of the judgement so that it doesn't have a variable-specific rule. In this case, we can generalize the variable rule to a general reflexivity rule:
-In this case, this reformulation changes the structure of derivations (these are **not** isomorphic to what we started with) but does not change the relation defined by them, as reflexivity was admissible above. This reformulation clearly would not be an option if reflexivity were not admissible, as in the example of complete development (below).
+```math
+\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}
+```
+```math
+{
+ \over
+ \Gamma \vdash M \Rightarrow M
+}\mathit{refl}_2
+\qquad
+{
+ \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x]
+}\mathit{beta}_2
+```
+```math
+{
+ \Gamma \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash M\,N \Rightarrow M'\,N'
+}\mathit{app}_2
+\qquad
+{
+ \Gamma, x\,\mathtt{trm} \vdash M \Rightarrow M'
+ \over
+ \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M'
+}\mathit{lam}_2
+```
+
+This is a _different definition_ than the informal one we started with: derivations
+with the rules subscripted are _not_ isomorphic to those subscripted . However, the while this change changes the possible derivations, it does not change the relation , because reflexivity was admissible before. Maybe that's an acceptable change, that actually simplifies the definition.
The LF representation looks like this: !}%
@@ -197,55 +311,239 @@ The LF representation looks like this: !}%
%block trmb : block {x : trm}.
%worlds (trmb) (=> _ _).
-%{! ### Reformulation 3 : tagged variables
-(coming soon!)
-## Complete development
-Parallel reduction is non-deterministic: any left-hand term that can be reduced by the ``beta`` rule can also be reduced by the ``app`` rule. Complete development is a restriction of parallel reduction where ``beta`` takes precedence over ``app``. In each step of complete development, all of the beta-redices in the left-hand term are reduced.
+%{!
-Informally, we add a side condition to the ``app`` rule:
-<pre>
-G |- M ==> M' G |- N ==> N' (M is not a lambda)
------------------------------------------------- app
-G |- (M N) ==> (M' N')
-</pre>
+#### Substitution
+
+The substitution principle implied by this LF development looks a bit simpler than the previous one, though this is only because it lacks the premise , which as we've previously mentioned is always derivable even in the first reformulation.
+
+> If \
+> and \
+> then .
+
+### Reformulation 3 : Tagged variables
+
+If we're really committed to the original informal specification, with the rule that said we could immediately derive the reflexive conclusion when was specifically a variable in the context, then it's possible to capture that by having an new judgment , which is only ever derivable from a hypothetical judgment.
+
+```math
+\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x\,\mathtt{isvar}
+```
+
+Then, we can use the judgment as a regular, uncontroversial hypothetical judgment, where a premise allows you to prove the conclusion
+
+```math
+{
+ x\,\mathtt{isvar} \in \Gamma
+ \over
+ \Gamma \vdash x\,\mathtt{isvar}
+}
+\qquad
+{
+ \Gamma \vdash M\,\mathtt{isvar}
+ \over
+ \Gamma \vdash M \Rightarrow M
+}
+```
+
+This presentation is pedantically appropriate, but it's entirely more common to take these two rules and compress them into the single on-paper rule shown below:
+
+```math
+{
+ x\,\mathtt{isvar} \in \Gamma
+ \over
+ \Gamma \vdash x \Rightarrow x
+}\mathit{var}_3
+\qquad
+{
+ \Gamma, x\,\mathtt{trm}, x\,\mathtt{isvar} \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x]
+}\mathit{beta}_3
+```
+```math
+{
+ \Gamma \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash M\,N \Rightarrow M'\,N'
+}\mathit{app}_3
+\qquad
+{
+ \Gamma, x\,\mathtt{trm}, x\,\mathtt{isvar} \vdash M \Rightarrow M'
+ \over
+ \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M'
+}\mathit{lam}_3
+```
+
+When all is said and done, this actually looks a lot like the first reformulation, but we're using a one place relation instead of the two-place relation where hypothetical occurrences are, by invariant, always reflexive.
+
+Unlike the first reformulation, where the rule came "for free" from LF, this formulation has four rules. The rule looks a little different in LF than in the on-paper derivation, because we use the uppercase `M` in LF instead of the lowercase in , but the meaning is the same, since we will only ever derive a term of type `isvar M` when `M` is a variable in the context.
+
+!}%
+
+=> : trm -> trm -> type. %infix none 10 =>.
+isvar : trm -> type.
+
+=>/var : M => M
+ <- isvar M.
+=>/beta : (app (lam M) N) => M' N'
+ <- ({x:trm} isvar x -> M x => M' x)
+ <- N => N'.
+=>/app : (app M N) => (app M' N')
+ <- N => N'
+ <- M => M'.
+=>/lam : lam M => lam M'
+ <- ({x:trm} isvar x -> M x => M' x).
+
+%block isvarb : block {x : trm} {isvar/x : isvar x}.
+%worlds (isvarb) (isvar _) (=> _ _).
+
+
+%{!
+
+#### Substitution
+
+As always when we are defining judgments in non-closed worlds, LF provides us a substitution principle for free. But, this time, the substitution principle is basically useless:
-How can we state this side condition more precisely? We need a judgement ``notlam M`` which holds whenever ``M`` is not ``\x.M'``. It's easy to define this as a hypothetical judgement if we choose our contexts correctly:
+> If \
+> and \
+> and ,\
+> then .
-<pre>
-G ::= . | G , x trm, notlam x
+We only ever get to prove when is a variable! The for-free substitution properties in the last two formulations actually told us something, but here we've got. It _is_ possible to prove the substitution theorem that we expect --- the same substitution theorem that LF gave for free in the first reformulation --- but we have to prove a metatheorem to do so. It's quite a bit of development for what is, at the end of the day, a straightforward proof by induction:
-notlam x in G
--------------
-G |- notlam x
+!}%
+
+subst : ({x : trm}{d : isvar x} M x => N x) -> M' => M' -> M M' => N M' -> type.
+%mode subst +D1 +D2 -D3.
+
+- : subst ([x][dx: isvar x] =>/var dx) (D2: M' => M') D2.
+- : subst ([x][dx: isvar x] =>/var D) (D2: M' => M') (=>/var D).
+
+- : subst
+ ([x][dx: isvar x] =>/beta
+ (D1 x dx : M2 x => N2 x)
+ ([y][dy: isvar y] D1' x dx y dy : M1 x y => N1 x y))
+ (D2: M' => M')
+ (=>/beta D3 D3' : app (lam [y] M1 M' y) (M2 M') => N1 M' (N2 M'))
+ <- subst D1 D2 (D3: M2 M' => N2 M')
+ <- ({y}{dy: isvar y} subst ([x][dx: isvar x] D1' x dx y dy) D2
+ (D3' y dy : M1 M' y => N1 M' y)).
+
+- : subst
+ ([x][dx: isvar x] =>/app (D1 x dx : M1 x => N1 x) (D1' x dx : M2 x => N2 x))
+ (D2: M' => M')
+ (=>/app D3 D3' : app (M1 M') (M2 M') => app (N1 M') (N2 M'))
+ <- subst D1 D2 (D3 : M1 M' => N1 M')
+ <- subst D1' D2 (D3' : M2 M' => N2 M').
+
+- : subst
+ ([x][dx: isvar x] =>/lam
+ ([y][dy: isvar y] D1 x dx y dy : M x y => N x y))
+ (D2: M' => M')
+ (=>/lam D3 : (lam [y] M M' y) => (lam [y] N M' y))
+ <- ({y}{dy: isvar y} subst ([x][dx: isvar x] D1 x dx y dy) D2
+ (D3 y dy : M M' y => N M' y)).
+
+%{! The `%worlds` for the metatheorem is the same `isvarb` block used in the third reformulation. !}%
+
+%{!! begin checked !!}%
+%worlds (isvarb) (subst _ _ _).
+%total T (subst T _ _).
+%{!! end checked !!}%
+
+
+%{!
+
+### Conclusion: the cost of losing substitution
+
+The third reformulation above was almost without a doubt the one most akin to the initial presentation. But the cost was that the substitution principle needed to be established separately, which requires a bit of work.
+
+This is sometimes the correct call: in the development of [structural focalization](/wiki/focusing/) on the wiki, there were two "focal substitution principles." It was ultimately the most convenient to balance clarity and convenience prove one of the two principles by hand (as in the third reformulation above) while letting the other be inhereted from LF's substitution principles (as in the first two reformulations above).
+
+## Complete development
------------------------
-G |- notlam (app M1 M2)
-</pre>
+Parallel reduction is non-deterministic: any left-hand term that can be reduced by the ``beta`` rule can also be reduced by the ``app`` rule, which is why the relation can be reflexive. Complete development is a restriction of parallel reduction where ``beta`` takes precedence over ``app``. In each step of complete development, all of the beta-redices in the left-hand term are reduced.
+
+Informally, we add a side condition to the ``app`` rule:
+
+```math
+{
+ \Gamma \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \qquad
+ (M \textit{ is not a lambda})
+ \over
+ \Gamma \vdash M\,N \Rightarrow M'\,N'
+}\mathit{app}
+```
+
+
+How can we state this side condition more precisely? We need a judgement which holds whenever does not have the form . It's easy to define this as a hypothetical judgement if we choose our contexts correctly:
+
+```math
+\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}
+```
+```math
+{
+ x\,\mathtt{notlam} \in \Gamma
+ \over
+ \Gamma \vdash x\,\mathtt{notlam}
+}
+\qquad
+{
+ \over
+ \Gamma \vdash (M_1\,M_2)\,\mathtt{notlam}
+}
+```
That is, with each variable, we make the additional assumption that it is not a lambda.
Then complete development is easy to define:
-<pre>
-G ::= . | G , x trm, notlam x, x ==> x
-
-x ==> x in G
------------- var
-G |- x ==> x
-
-G, x trm, notlam x, x => x |- M ==> M' G |- N ==> N'
------------------------------------------------------ beta
-G |- (\x.M) N ==> M'[N'/x]
-
-G |- M ==> M' G |- N ==> N' G |- notlam M
--------------------------------------------- app
-G |- (M N) ==> (M' N')
-
-G, x trm, notlam x, x => x |- M ==> N
-------------------------------------- lam
-G |- \x.M ==> \x.N
-</pre>
+
+```math
+\Gamma ::= \cdot \mid \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x
+```
+```math
+{
+ x \Rightarrow x \in \Gamma
+ \over
+ \Gamma \vdash x \Rightarrow x
+}\mathit{var}_c
+```
+```math
+{
+ \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \over
+ \Gamma \vdash (\lambda x.M)\,N \Rightarrow M'[N'/x]
+}\mathit{beta}_c
+```
+```math
+{
+ \Gamma \vdash M \Rightarrow M'
+ \qquad
+ \Gamma \vdash N \Rightarrow N'
+ \qquad
+ M\,\mathtt{notlam}
+ \over
+ \Gamma \vdash M\,N \Rightarrow M'\,N'
+}\mathit{app}_c
+```
+```math
+{
+ \Gamma, x\,\mathtt{trm}, x\,\mathtt{notlam}, x \Rightarrow x \vdash M \Rightarrow M'
+ \over
+ \Gamma \vdash \lambda x.M \Rightarrow \lambda x.M'
+}\mathit{lam}_c
+```
The LF representation is direct: !}%
@@ -259,8 +557,6 @@ notlam/app : notlam (app _ _).
Then complete development is a simple twist on parallel reduction: !}%
-%{! (options removed from twelftag: check="true") !}%
-
==> : trm -> trm -> type. %infix none 10 ==>.
==>/beta : (app (lam M) N) ==> M' N'
@@ -269,7 +565,7 @@ Then complete development is a simple twist on parallel reduction: !}%
==>/app : (app M N) ==> (app M' N')
<- N ==> N'
<- M ==> M'
- <- notlam M.
+ <- notlam M.
==>/lam : lam M ==> lam M'
<- ({x:trm} notlam x -> x ==> x -> M x ==> M' x).
@@ -280,21 +576,40 @@ Then complete development is a simple twist on parallel reduction: !}%
#### Substitution
-As above, this formulation gives a "free" substitution principle for complete development: if we have a complete development derivation ``G , x trm, notlam x, x ==> x |- M ==> N``
-and ``G |- M' trm`` and ``G |- notlam M'`` and `` G |- M' ==> M'``
-then ``G |- M[M'/x] ==> N[M'/x]``. The form of the context ensures that we need a derivation of ``notlam M'`` to make this substitution: it's not obvious that you can substitute lambdas for variables while preserving complete development, since you'd have to replace instances of ``app`` with something else.
+As above, this formulation gives a "free" substitution principle for complete development:
+
+> If \
+> and \
+> and \
+> and ,\
+> then .
+
+The form of the context ensures that we need a derivation of to make this substitution. This restriction is similar to the restriction that made the third reformulation's "free" substitution principle useless, but it's more reasonable in this case: it's not obvious that you can substitute lambdas for variables while preserving complete development, since you'd have to replace instances of ``app`` with something else.
+
+#### Examples
+
+We can give a few examples of parallel reduction in action using the [`%query`](/wiki/percent-query/) mechanism.
+
+!}%
+
+%{!! begin checked !!}%
+%query 1 * app (lam [x] app x x) (lam [x] app x x) ==> N.
+%{!! end checked !!}%
+
+%{!! begin checked !!}%
+z = lam [f] lam [x] x.
+s = lam [n] lam [f] lam [x] app f (app (app n f) x).
+
+%query 1 * app (app s z) (lam [f] lam [x] app f (app f x)) ==> N.
+%{!! end checked !!}%
+
+
+%{!
## See also
* [Hypothetical judgement](/wiki/hypothetical-judgment/)s
* [Higher-order judgement](/wiki/higher-order-judgements/)s
-* The case study on [Church-Rosser via complete development](/wiki/church-rosser-via-complete-development/) for some proofs about the judgements defined here, illustrating the use of [regular world](/wiki/percent-worlds/)s.
+* The case study on [Church-Rosser via complete development](/wiki/church-rosser-via-complete-development/) for some proofs about the judgements defined here, illustrating the use of [regular worlds](/wiki/percent-worlds/).
-\{\{tutorial\}\} !}%
-
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Reformulating_languages_to_use_hypothetical_judgements).
!}%
diff --git a/wiki/src/assets/serverok.png b/wiki/src/assets/serverok.png
new file mode 100644
index 0000000000000000000000000000000000000000..32e38942819ed372156607f72dc7c4ff170e55a8
GIT binary patch
literal 142441
zcmce7cUV(Rw=YF0(i9Mo7OIFy7myYZlq#U~jx<9@Izk{I2m%61l^TkGfE4K+3?&pH
z^eVkq2_+^Fk{iG8JLkOT-v4i&XFq%P%&eI`Yp?Q~wI(sob=7HZu-+gdBBIgMc%n~4
zL=r-{CMd`VHTI5m21G=}#?Gp$&oxz5xt@D_zH)YRBqF-^$^B!ywu&udA0+L?mk2}q
zkE4uV-_OHcXz3|qLS+2fGu2!g_v0y8FBmf4qTUx9ztb?EXMOvX%RB<5{61-+*}Qb>
zjchi6j!u-0&iCwIW?C&N=54+}LGn@2=Iww#RQ~Ku)vJb+1xyKWd%M-k2EB7@utcNv
zepTG}iSjEg!Io78bDciB%}!jyu1-;0*)KXXXxT2=tO5+lp;{ZL7pR>697fIrVg0GsqBaf!wTLMRHR}0)yk2mP1!S0O;$(h-
zSq79{^12m#j~kJ@Q^V3k8CUR$S6JaG@ofO-DpBa%$EnlbxXk%!j%U=A3NligWFv??
zd_^hECBN3q`;wUjLP{0$WvDfCvC)_6lr6M6r+&9u)bmg;Gk^0>e9KYZ=Cw3dB1W^>
zQ+^&N?j$hU*wIw;m5vV4eL|Unh&bAr=o+C!Ot@GH7ZDL@QWOz6;Z9Gup5&4IS1UdpkOM_&9m`etKvDCJZ(0Y-s9hs`E_F-qT&g*1^-xQ6$j)
z^&@Gzty5VT>t9g>#E3Os`H#n)zjONOIk!s
zM2rV`gNutx!Q0`LocMa3jUB_xCi
zJ%oMUc=*}|3VZnQ{(F%B8s~|lkG;3^YhPzi53axC+S+;g`6}}8{GI5(fB$|@$3W-*
znaRWFKg%L4Q1ow$sJMuj=zot*AXWHVEBD+v(9zB8iL*O_J%l-cG7^#s|LXt$wEWME
z|DZJeA4+LSnSWCLqvijmH1cuuR`qlzOz8{!pD*(t;(s>&hfqQE@5=wdiGQ>CU$q22
z18*pZ{`WTn-k9#v^&=uuCenQJ*f5azAcr!{>S-!YDCg+lQpJ>nk1vwLOp1r=K1poY
zz1aRoFtL$G2|@`&O=4f~eJwmuzx6!h$BQSoM#K093n*^X+>4{2Pf{k)?C%IDsrAKe
zoBRo>D)(HPUaXSmmL>Nn+xup;y=3uczh#K($AIL@onz`iG6m9HVni6I>;Lzo%THw}
z>$zn`@EtCMn|p&4pWh~+gF==s*R7Eyu|;d6ZY;W_!AN^AKQ008xy-zAO~0}<7&o92
ztlNJpD?vV0ZV8J%Jw>DYK|BVFM9ln{~
z7v8C}dn-NGDUAlyzKR_+lesotDJJu|coY_mOy}U10~%gnwoelgopa)OvMJu6PTZH~
z;|tw1Vyg$&TUbIvlk(y%WwU@lTwhlLj60HJ?1n
zR5?ygMTbc7{@YmBKQ$3EDPK6ipE-2zRj_{YGM(Z-P!@YK|A~w#UnZqCV)>;QoRw+2@s6uaq)Z
z_3^0L0Sw0jtAWvEpxw6$OoKx>NdJxd=343>C*wS0qH5a8U5V;8hp!yrp|OYBS6
z-|PD+;cM87;0Xx=j(W`}rwBwR76TJ6Sm#%a@;&%cl)$Ssb&B)-5R=&M%g>NVKR=DE
zwQhTc=WmuL*Du-tCg!fYefpoL^6`2coJgc_a5)p41WJW1CJ{Xs48dqD6dxfqRl>CnA&5=@
zL@wa(7gawMFd&1IZk&4lwuX%FXH^ba;(f2wbC1|ipWJ#(EcoS$wjgJ#wJ%I8LK&Bz
zh>Fs8y^%f7%qhyr=SVtI?t>-Rx@CX;=vLQlsC8EnyK9$7!`5>AsEJSLHXxURZMWM1
z-1|b%Y`!=_H1Rj)&pHC31ciWco0)n0F_ru+WM1I+peYUc)AQ&yCu~aHJ0B<2`=!aP
zXBR?jXt%n#NP!gB&E+Rg755et1@9~btEYm`({sM$JYFu{|MC))NB4vI#SCp>kNRG^
zH14)4M3F^kPg6Hbj_nIe5BzStD94#YRm4YWKdp0hWN*o{^BCe=23|(@fgQ744zsE~
zkJWK}g?yD4>Kq*BdKWb^pWvb!%FTIaSP-1Rp->zK+x=nXw5n2PLuDrYET~|g8XmW?
zuy>(tGtnG}dq0l*p&HfEr#^s%&YSvN^6>{=9#~Ba(NZVr+WCFtx)qi$((M2CY&_@v
zvmm*y>UVV$*XH%Ddf`zmzL_`Ng<_RI$vt5|+bvW!+>-<>Ps)Ww88)V&S(!t*&XZ^R
zxiEbGK%hi8lUtGYE^^^d$%$6R5d;D8|7mK@BdGURUA9m4{B@ml7w5K?D=qQ;EdH2%
zI=Fu6zGuL;O|Sj3Sb(!l5zoiC}8C{i2mw1miaI9byc6{rwVT9W*h&4}`p!nPc-!3y{~LX
zbgDXk%6}XY-OCPWF)qzb+Zo@wh~xCTC%igDe&O6|jg$(tE4j*RU;Iel*6ypp5bgg+
zGjjHg+ggeIGwJacF|-oWd-LCo535g$MDgs8V!JKACk-*9oI6*B)PVP5G(%JE>*J@m
zf$kb!8&uZy=$(!Ab@DPlY(@h?$wBZi0Hhv@&z29x`DNq5xPe!OP)My$#A$@(WYASA
zC;XPrEq-8~nbbwMfZ-4(n)9NCY5yX=;_D_n#UXn+Q^5PaoIR7+s?Zn3jWLrlm=|V(z^hUw
z==W72jzTHkDw(wjrGM#Q)jGCYc6EDs`m}0GF?BJA@NRQnTQ&)lw=V0`_H6=CNyvT_rxcWPVQu1D=_!4MOnVX4KJevMmCX7>e;x*mhLf^;Cy
z?)#Dk?3bW220f(UZD`BEJ-^qtY_2H{3n87>NmVL4o~W$?&PE?sqEBqJ!3T9kIAlJ$
zzdU|G*0gk4I~-+jr{3(0Xd~bkJ)kX(Z_K@yF$S+Iz09Cm&7E;s4N2
zL!QZs0+{9dRr{_@Ul}Wa&Hd!DnFtWb?K|7TVDsi{02n(a^Hm?G7<$=ZGGgct!Vg7n
zFDEJ~;Rg|TApYRdX(Ec>$69e)39FKltzCdUC+O-4w^izyNl0;IBA!uwRPC--Rn=ac
zL%VhH`=*%)0pe5*Q>`?u!1?f$JQw<5HT-#c3cU^`U~zIJ^XW2)&2b(WTPF-TK8|(=
zb{JoLEUcPMnYB&6NXh-qTO_gfQ43QTZ&iwBrIULTVt@OT3(DEav6BQiDfqQ91O_VN
zEdT_k=?G_l>*4}e(QDucUpInH*apC3-mj~`)jECx^yKHU-GQ=zhez0E82V1_*~jgw
z&P<4}^$V9;m&Oq#yH#!EDJDHTw4hM`;xAWnta-_*D>US_H2KWl=-5rl)>kN4_#K
zVsujETJSaf=-Tdc7ftDS=)9dCTQhq1J|BuC`-~VmUhBda_z_*-rw*m*tnUM5%RRcS
zCu_8@4wB`eOGS15o0DK15)-gs32_Tb=#l-p516UZnz6CkmK-`*#-5v?Hn;GTX+gja
z?2B#0{9BT4)tdRBQ?}fec9|GNdS4tr#@2K^u_hQTG
z@1SO@HBAUsfZ+`|>E#B-QwcW^{cpR!e(GsbrDSREJ3MGZaEPlxJ>q0WnGgd-t8QPN
zZl>HypZljXO6VFRup2k>2P4mJzwT8^rCouZmABSF^;FZ>KXT4D+c}$VR$KC<81hs2
zO}(35EyWAw{SaX5{QU8*QOrz&GP#O6n*w;eIH6K{_Z|?udrJwRNB((DbHT2Ly~DsL>J+UVJQ*}BPJ)Jlbbz}KPcPvP(X8o)2v=zqh@L#i9u
zbZ$A#xSfk=E8Io-8}*_sKqY8LCAQ>^#Ub`Q`HD}49H!Pmc>N7@*q1`|+N%1cO-uj7
zyL&e!dOv(nu|S?m>`t~Dj_(~cMXJ)0BqbkF@V_PA-mjZd;*X4s15NP|@pyea8y%yK
ziq1yI76QAXOF{?8fO50SCvlbvXgQ*BbgTf|*#;G-AEtzsu5&NWs4&6JX{b^keD-t~
zy*iMN4aB0@|7!hzaQs4*kEN*Z@XAI0zM7{E#J55KXebEu-YuF@I_JpUJ8*q34%0?J
zcDZKiIb{uRK)TYE+~%C@3#Gj#1vaNmd(k!d2VMoF?T@u8wUP>EsZ*|v=_VKPahsfA
za%ug}>KQ)Sm-E%GMdkWGVO2i|gE7ysZIIq&r_kF_dignT<>z|q+G>_lf~UySbrW!W
zsUa4N7V2&M$hqvDceR440^=~q8K9<5#{~vXO|K${$6%9(OEYIeaKezQ_1PD>Wmfop
z`-;=V%EX`h7_4h$NhBj63yVz@4%$7p@jLLvdET3xQgU#+3FPv9r^FYbXB9FCheOwf
z=%f`@v@{YQ>1ETalj<^X1Iwt{^;PP4R|e7|?GVLJxEYjtnB+0aca@GE%7HJVX;Ut=
z55LyhChPj{tTPP4({=U)05-VM@Q0yuWy}35n$RSjt9ln5WE(k;7t8`8mjdlLFHY5+-HY^G1o|c}&k$VR=PJg3Q8RW9l>k6ZkH^u1xGpk+x*h5x
zKmDN)_>jnHa+>QjD5-=WcU8NV>Vd*XodhK_?l-RUw1He?fJ&)SXR4^O@z@Y1NhG
znE3jso^-S;Zu=gO3=p4Y-86PyHGUrb>oLYh9D*AY@x$6?A(Rv_2AY8JeJFN68-BM!
zo7N_!Pw%nHpd
zcfg=eQWF#DKDh}_p!*d&{>lmJRAoE)uImW1#`Z@jgkxK2b7&iSz%qt~a!Ac}%K6_5
z!MS(hKILf501`@%vLSC4^fA#Tm_*!Y)FZq$(hpadY!}Z6;ZhX^*noTUbg0kc8urk}
zV9ets-X{gYZy&ONU2mpPKhP12;173J`L2_!YN7c_go~yi-bQP8)1Ft)F_sdb)Up|y
zAiWmnpiSM&Y&Vmj&nZOx}@Jf8)}j
zEm|m~Ms{I)***Ab)#;n>mHmi_-_^Q#hBf|c+-ynazM$W?xaf+&*?XaTiLT!&3ulX@
ze{y5ceX$DYn;oNthTrNEJnuoU`35HXc|mfH%38F3aututglq+EV)8@i;c0A|5Y{yTGExL0P-!kAjf*|axgd4XkR&Jr||6F4;|FI{E95GPZ0?^
zNuHJ>J9`*E2EVaP<+qOZ|IgurcLFBX;oeF-BO;};2>r~`I>rrZO;{7Gi_0Y_EuQq`L1
z^vXS&I)6OuE>PMTy!R2iy*@!lq1gLG{YsrobL4R$vU@^T=c)u1n?C5MXLB3yrU;$%
zSLhP}|A`IU)h+Z5Evm$1$)ybX;n3Ix$r-?jl_1{o)c0!UoGuG{o`@0V?_yOLWLiLD
z2ZI)>Bks*1+ytxbA+C6f`tI{qOYmHwC=7zT5DLbafYD|4qKbQqciCr>AKglMLe@WG
zK&_=CkuvV6?i9xQ&0(zsxTz{3nHajME>Fi*!Xa$sOLo3Ldr)o-i86|(0m3p$3~XS#JTVf
zY-B@2!>otP;NH#(xy8K+gk4_ThxpGaoXe-b;ZP{#=k1^5Ks*||KLb6of>@YOSIswh
z*$BMwxmQiZ@{09yScb15kGfjc2F0vd{SMn5K1DZ1(u|E`
zR(C(oKf4npkTt0)*)4^N!8^5z)@Ww=t;
zO%lH~?PzH>xt9ry56mT#Hu??K^W^y1P#Aq=k^TKe-Y&!T_qyV*Q%|(n3O3TJx;~%r
zm58de?J<+85jOq}Zb=sPvwg}bP{IsEq|thu-vE672)6l2kdh*oE(;Y;0qgK0QmX}gG3;_oi|RMn8As>$va1;z~7
z0QWh5KiW4i76qE9Fa9r9$dJ;|gmgzz26x)^f8<6ihx}QT6lVB_3I}xE5-cVPRu+sR
z?%zEsuBPOdOL2pV7$3eA%I1OebJu?w5;$+UN!zN8)*yecgj^|+=*l1~2+yZV?0J#I
zmG-!_Fgb1dL!?Kkkt*0(^?TLg^rAcJz^pNzRmvr)>f{r>z&~QYDa6LuG*KI1@c5Sj
z(7gN7n?7=TiYkgMCofIJmaWJKRjVd-{)?0F+`azN?n2r=ZZbYBFQDHc8u&%R)$hcH
z-9LRNTds0MEUa$A87`%)CGEzNa^`FhZ8#{Z;1(!InsKl~snb29>(YW=i(7W`+}0hx
z3Qm@N^Uomky;ouHxVx#UB*~!Or0QWp`fuTBYjnOV;YyKKXO;kWbbo2#&|RF
z6AM21`L*tSrdxILk?qg#k!q6Xg%5NpXN0kW_q1Zkcp?3cs_X;EINBZ;D0qikb8aG?
zTb_0>db!ZWUUW>3Rw1I64UCjXRO*p=!ROm0
zHcK@`(VF-1Byz}5O9aesh0ZCSbS{Y>R*rzDC9EXs57f9!auYxAsHHZyaG|5KnH>Op
zPkH3vcD%um!I?5yv5X7;-9Ez@a{6dlgK`cat8Z%K<^vys?<>8%;~$F#UPjh&F*R4(Lo
z21#+HEokuNJtG<^>kVE*cZwBe)gZG}_%9M0IXoo3
zsnxev^aYSbPsYAK)a>U%@AO+M%u`d_+-%Td)np{;)D?`77ySi39k!AbF>Sv(^rTa2J8JR3ytYRu>p5~oGj#E`xKmXUWhuk%wOoJD
zmIUWsxeZo^X-{7iea8D^uTOb8RX}0Zdwly?{gw$0_=fU0HRAbJ$%3N(zdBG
zPI}~rk=Ub_o-*J7
zdN~;!9p)iwRyOX;Qc50Q{e~$0%#jy8s6_y6XRB?I>eJ;#;qs)eGnF)nO1P%E5t?W~
zC|Z{WE7G*`_I1y#%V^%jOnU!0M~9t>UUkPzi|ObRXy)xu{H40e>HN*gcGSE}>zbn|
z{&E@5$t1kCZMm<_aQE3tN%!9VWczJNF^B%=%F9#@;R4sb5xKmiqj*5l@m!NbabB?a
z`ztpC6_~)}n6?ZqQ=b~6tS5c{w)P{69Nk;AE!sD9H9_2d&sL~_ImI-Zi4A+R_UdbA
z+kAfLlR_4B5|H10ZbfxHv+33FUbOd6!(IQsQsRF`O=Q}axGV`q)k5R*s?zjiyi8u=
zu$Wa($fX5(-v-aRZ{PQU_IKlyNHDOeQZP&UaGIqgdtyC7UYb4Nm)B-bI}9M<>(qoP
zc7=5qpl)PIg92L7#by;YPm~k&Y?WPSq@$ItcE?_iZC6pa&V1WV#d(%%>@U(wzu$V3>4fk0K>t$GlxugFE$?C3j10BY9vf=b
zj6`X(WQcb-wI?rQn6udeWJTd98+=?W#KNk=l5uJwxtIUE6>#ZLUM*RYr&L2!S?U
zw)yeLqKTjnMwZvVR6g2ye0E(P?3-~dMQ&Z0qv#969t&{iCNT9{pzlpZKX!tbNui**
zm%17!jbn_v{n%}#cA)cMGqFaGfY(;L&_
zY91-w(Y=Gs>DW~5?!BqD$)-
z>3OvdkFRTz-)W;*x#8z9{&Ao#29%cVaZ$D5)M*)y5f{%bLwU#X5;&&G#ff}V0f@CJ+u_I|ZZ?DMC)
z-{G9W4}LaXRleS@=$zfk^R)8udC8l&d#&PE>F*Sx4w{MzL7_S`{h7wPs8~+1ySJD<7JL65Y>e)~dr(=Qtw`t2Cc$5R+h<}yKRpz0ziK_r!oDDhdg;veKsCo8
zxkZf9J?y%CT)JGB;^cMeF;#(H-pQ#37ryzAU|Z5#+8tlx_}~e0;y+BJBG|*lYfED&
zp4^ls8NZ`NqM!b(3t=j5yT^qbEfEgEbfvY}J-SJ3Fc0`@-$q7xmUTpK
z|C`6+o>hBLD)C^xEkf~+m=cX`Zy6zq|LGPlS>!F=s7RW9i*?B;)hOyYt&&ETFeZ_x
zUrR?8rlq_fHffKaUE1THii?Ytm!3RBvB|jAEo^AR)_Tc;g2Ja~E9{AaIzunIRN;C1
z(-lGqC52x)gpE&XrW9Jm%$CeAADUZ=yins)nnU)S`{-&O3M}JQQtePo5%d7|9A_&n_carr!eA@wc9IX`D*l}KAdocT53iIY-x1@YtY~bnu
zBr~si8U2noQK9B;=Ym$u_Hfz*GrKTb1g(&+Xxp)hY4yu+;&-=fJFn3E+$H*VUg{(6
zqQ2F=a{IH}{Zwk5_<)E8HC)*ge@C*<`qd*IFzyuExL~D3@hj+R77jEX4AE(mT=oxo
zbXaEq5$c
z^qne7P;Q$|(_zDM56FT}@$7c*BNI!nr*prUQmuqHmx%*G)dyScB>w-{_p7`es1*!tEL<;UdzFX^LB|e
zh`#XM<4$od*hv2|VC_Gv(sR3@sPc(j1TAoq8RInMv5;qNGj9jklwJ;Xb!xs$7?s<`
z?6l#546rVlY(}!2pr9Rl2+}{Qp)RAd1j3mKLQqs_Lx-{Pb28MKXT@SWVF9x?u{o!W
zW7sQ)X+(F`)(8dS0Rnp{>msNIGx2po5g1xw6>~tsU=cF*jnlx6h)A)ze}ScZUoOP#47e
zd^I4Y*-DHIG=96x8c>?C@J`i@+GmlcY72
zpujBaoUJ*2|Be^&8Bxcdwo~+L?AW>r9yrv!pP0k`$`T)rw%i(YjB~5^f7*23C#1b4
zz5FNLzV&!qz!{+rwWXpTA;S^5J|~BKjTcdv)3Ev6|K!sn&C&d8jnCH-^-;#c^euvF
z47w^N{yWuE&q}+^KTuq|#dr9HtmFq*1iXvSz(O;*a)W>vXf*uj;{X&J$+YyL^UUBI
z98Z_YUkDoiqK}m~%WW+vUDptm32iB@blZi`p<K
zx%ix}RUga%Zjj0#Xx5|XsIO21cYo5bSyPwiw(vZ7^U9nhWUx_n`Eh+klCX;zI}Wo%
z_ikId)5#M|L#v9q!*KZrykBs9Ze|jdm7B#B`WoBV-4tGrDYw~j`E%AqO4mbmIHuk?
z?orad=yB(qt^^v|vS`Q3n4pN7&E(j0KWhK8bgYE;aStT81Hf{B&)5rfj@$Umkg0NO
zquS*|O(elkgdET+zuucn-)0GtfLaFn?Hlt?JZs|unY^GvFc?WYng+unDOWd=^=Jup
z;e)bgea?*KP3HExd(SePOg>`{9$19uPHc*t&LwjAKy=rGx$BEJ|qn
zT@fP4?@DbeUOU{E(Tn~Zpe~p83OQ6FVyZr(Tg?@8u|Lxo`5U|)dz|~HO=cT?CX@x8g}x`*cHgZgoJy%liQ0R6g-?eh_RU|7R?}
ziX?QB_*&RF6nB>P8jGyjHyTxkL@m@tcSpO2ETpB=CheB^XzmrGc1xhPiSiFVctTIU
z{kj9n<_tx~*)TzM)(sx*oRJ|5)ULUsc%Fe`uu{?uy{R1siNwLw+}1~O`=xC_&)p^8
z^>f>vFvryoGP#Uo((}S#Qm~*`HVw8&BxGr=bcJz>6G
zel=k>nqHtwG8XmlW}w^N2Xu;Wrjh)6X|^vvxYHGj+m@09i%pYv@e
z3YzoZYz^BU6K^xBrk4E@yDV;k33N54DrrwVZ~dsyi0(a}n3IWy{A#S})EB>x48$E>
z>_hCTF!)|$P4jLc8;n-4vTPzeV(}=4$rDNlV#|ao{F${+ter|tUaP3r1Ft0`o2Ayk
zzk`=+ExxP5AoxEs-83@4ZgPT;xm&M$RVuCr7=AcC?xurN=A`~8$ql-{*Rd&FGB0UR
z((6$y-T%AwcSk>j5N?}0`~`w_Vuvo*o}Oj8b}-W_922?XwNq+ax`lym#@|ex5d%6g
zdppJyqOeJ=A1ule=%vAJ5D}
zHh06vK3Va-rvVEze3w?(rU904I&8b1IbCgsxo<&i&agFX_0qHbl_$-5mW(yqfr|D|
zG|DS~`Bom&TLX2^(_-mhA^#B5X1mlJ03?>kwyGU6NrA;@2rvvD`T8qP
zlK+=m;{%jI_}A)i+1dV8(6w-R~}ZXAUMWdsWa;WYRl%aiY=#j#cQSEUn4p
zoC{JV`A1);lsBssQsXH<`zPh`U4xZ$u>|#V1@2XoRg4sn+iK^84<;JLHTp@_<|Xq`
zV(mzgV?r17o0)+(CnGWs?*Kh^y~plp-(~ZVi_>YmzZ2{q)JCw4ZnFN
zD#$K8fgPaBu=5-slkS%yHeiSFuVv)B~O*2Sb}&F`u!U3^#M0=t6m
ztWQ;i`ekPm*h=otRybu`zT^Oy(Jzr8sm56-Rr8zbw7gk+<||W0`IFb?
zN+j1ve*v*S{zOY5hUuyl9h7JN4DFrn6JyB|<^-sJIo9N`6?Px32T*0rDAD@_!zim3
zxs`2JS+=;y4PLJnhTU<2bRi!zk|i
zN~zxDCRI+^laC`GNp3|Z#IWQ^qbJAmzf`ms@ru7jYq1CUaspd=G_SbqC)zc9ukmbJ
z_@lcxq47Tvj$1qo0lCu)rwTg32~{rr6-(!ck;<}}mW|y}&*c}kRE5H-XPwJo#iJLn
zkhFFy~N!-nBXp|(vMN!mR9Ywu{Rb-zAQ=X_&W_gLLu
zArf&ol445y#ZzG-pr1RM5xTp+UMPsPBM?@wW7E{`YM^oJ
z?1ktv>Xcr2663`3x8HP$8L7$*BgkmPMr#I)l`rh(4(rxzBSMPpk4~vzN3Dk(A{{$P
zqYjYD2Ju_I=Q7RxmE3Lgd#Ut5`K+vlZ3W@9J<6&*ioHuuylS*z#%SnAl@Q)%%kh$dfDsHT|8%d
zHHfjDwT_OqPyD3_K4_1Q7PY*ZG4FQ!6Eqj=(!)<}KKs^6lMVYLl{GY|Izp<8edP{%
zl3Qzjr&jP2I!{D#l`o$NT{e^e>?(;AXf~1$(C}qCyQM*-!;yFD<{L@NJ+m@??PXTw
zNPf96N85K^0B6SrGZ42U>3{N+W4V+rP+UB7wqmi>0ptp3Ri2Eui`w5#YFOE1&^FdmV3CT-v*IU
zRk@Umosye`kTTm8hRPIx+DsPz)sYAJMSIIAHe~XJdK3tnb4R2Td-8fnxbuDE`{qTf
zqvjrS@4_Z)e;!h4wrW_9H~?Q*M-!W@oh`gF*JFn#LIpMmSY!-_@`rU22e{RLyh!jksH*623_}1vxG5(^AKF+Rf4jQ&
zIfSuEw+_6?8a!#6(B5@oXO{RbB`xK2w^`g?eYOG_zS`eScfZuYb8E`P#=YxLImfRP
z|Gj|D%f%(k#`_RR;?rng18i<4p`@}BMq0c*9L#NPIJbJu@N9Jb$hZf5AK~TAsmG=JDi4;AS9^C$^X#9VadT|cnBbjEip(DaesHHw
z?mplMD-q`SELZt>TysNkIdjZduK(e^y?I7;e()L<5xos?dIjr9o7`AfhyeN0
zxFdfRy_a@`UXx)V&YrHCuDZi1tU%D(S8I3TiUySz0J)6RmXe#rDt3mxSSgD4PJVp`
zg1kAUOb?=G*8DmKl>MZCfn`NtV+dxytqe&rRHB*I_n5$&D$uB6jT;S
zk@W_b+4>WK`1I*dId8Tykf{BuKX`G4)1Q*7Bl5pLEMzT%T`Y4{1&VU}b@m{j3Q4ms
zjH20n-yRBYxL1Ric0IR4k`+NSA@g=nS2IrCz(dN_^Qz#8MVwnqxo;8nE^`6x+9O)h
zTC59cp6HTVy{*3TuIy~z
z63dM%k6v5*&6~xOrCXkCqT7TLUB2`H-0bv4t~>y1h;*nh~<-t$*W}jENa~=C#>8IVPxQB^oolE@}ea-a8&10s=yj@Mu_A
zXb9{mSSLp43(=OVhs~`EDXGY0waSLZAPd;6c+qcj-*)DOX$jdG4T&rw^H{~%$AUKU
zPq-4PxD<34VNYi_4(qxFzkm8&C&F=&XNrCS{l~+UQf`u
zit$5@Y>}RmS-VJ^qqiR<)o#;~kl=a$P1Yy3mOO$PPABd&lw^@vAZSqBv-kByA*m?)
z@h`?6Duysl#ZKl7MKs;=&VBV{f!}Os>Kmek+1`T#FXC~?n#f$L2cWEz@2hh^=t6c>
zZ~gS%&ob&%!XXo%j>6Sb&1g1T!xywY#>EeA`pK6{!#AQjxlzrWbK2tqAU_6
z;tr`H<0#4yf4ZIN;~(S;Hg$UQRm_%*v~oLLVy@HQXdBJnX!50=9h*;qxs$I
z9iFv_2Nh_`2MCknShKEvv?`$I3GT7J$Z1!drZ6yEj|s#tt=IUZ_0%!yykiqA;63cn@b
zgpw(=!_U8>**XqaRqKP_D9|bn(@(thGGl$Ww+I`#^cL+z)%m*MHvrh^l%c3K`bxC7
z{>&86@NOOUhCKHrL%2*ACkX=y$fa<|T9vM#l7>Ut?Kq!aArjc|rj0k7A@N#rp^)Vh
z4#3B?LON~+Q3b_5M3~#2sxs&sWnvI{1v*sbNp(p&IY3l4CSuXuk
z#Z)uNi|2T^r_V)h`a#i0OJA$NQlaIZ$sth@jlO;siOG?-JI?I`DD9t>%*$Nt&@3;m
zcMpNf|0QK2jX~TVyOni>9wC2d3zyFh%a(V#qkbPBE
zww@acz%OWxEri)R&=!qq?Br1L|EX7u{J^1nT-kbb|5pn|!^!y%v>Sr3zi?Y-x)fZb
zjppz-#ahPV#_uaUXLH=d304%UeyyAOqM7V=ex!5j?0Y7Bq5H%DEe5iD)4EfDfFpW|
zUIKy-zN49tr6nEZ=s2F5U6vyI13Cy=6~%QWB|c3^ldzj;p=Zws=|9BShh+oD^GJ}h
zuSKi5hZg*BmdexbClP}zQB1iY-qC>{52w0^utv7a7qetJefw#ALGnXErs)G-F9$1}qW*hMLk`}|`EDlvRVf8GFEY*deR#Jyf
zouB02vJPgn34aF{cl2IJ3=5n;m|?mcv8~-q^jDq86LUD`3dTv|?ksnQjQk?aY;IWe
zn_27)#KI^MSLc)vN?~`>Zf$L2W=Hww?j*>q{-p%B!(S`T+P?!_)=SP41JkPcnN&?^v5P47m;-Of2eYYvLpmh74<2RXpGBXm06cHXBk+DvHc
zN$mjdA4(#JzFsgMQJI`Wo?Ai>wYm
z&Gp;8PdNSODec2%vZCA3bhWsw{3f@v!lw||o;^e*($p22cF={6NvL-tg4T$_eN4Y(0J0ZDOv$>&Jf%Bq3BY;NSD3vyj(KsCid;)|uJ0;qxlXi{{rSn&4-x
zQV*<;Cc0cIO$X@?ikwk8j>uBFX&ALjt@qDn5uf+WpxB7vBj=D4SrB|SDv6X8j
z-YXkk&g!{+1B(PL8z}r}Y3`B^i|8W#Ohy8)4wqb+yTck|QFqKW^+_{9gqaO%OXs1v
zdA#~~XHDBZFv(uk>JfPc_(cu3sCH^q;NdG@dVK-LCmg&KT~r&A4Dob!Cp`TaSsw|?jG4O*eDsYaw=^lJR#QK)Z9XBuYdrQn)-pMG71k3pH9
zs5+&)#Cz0PL6A8M{-s*LGa+mY&3P>FRl@-paeVY0d9MR
zPef5udtqM>WPwW$8pL~lZ+Qu2ddOK(?2YN?N5BF
zeGuAaBee>bHr?JPUK6YF`+07nR*vl}g@0PND_tk+bT+g3rLL-Z|IWp{hVn?-qyB*J
zzw(I|o+BaK*|MaF*k?l^3EksrgVA8wd
z_ax7aRZv%K!!JiJh4;PfWP>5^?l3D$Ge#7SaDKra!72>YsJX}15qAITgbcfF-})=s
zoHuKm#E!x&@Qy4w*zj)_fS4B%kccT@n=k~li`eY`lwV9U%C(im`hk*&l`fqij$m4P
z^0{Zx=T*2?uolqI+VL*q!*F5tw%y{}O*QmTw!}MJ@&9e`U@i}zJ$U*faNl?Ek(RLk
z%ngMqwbm10w%TmltY>Jv6N*P?FQF$G0G?cPBF41Fn15^G`zCF?Z$)rSl+erGre+(c
z9+)ZRGQjUzIg}d1v&UZ|=dr~X-u_cFmF)Yr^?rk
zHE!HqT8GmylD)6ie}|ke^cC~12(_xOdQ@|%)gjL{!-HcvCvz@*I@3A*Gc2qP9i$r`
zzndM!l)j&5SE@Lk69f_7Vbg9eYkE9&>w?O7gnPA$Sd-$NaOczQP3-jJv1HH*E@;hO
zpe9ErOV~Z!XELI@0JSZ#!bYr~8I&P}8^{7CWpoMZW3--#z{(uQ$;J(F!zNhF&+pLZ
z>;fOL%#Wm$Dw+hG*LUsDelB&{JE+UNl7C=Ij71%FDyk{h{!wzzOz#^ht81lh9UQum
zySo2*8UM5Xi;fQLx~~2+?0L|3p;>R$u`++%H|7oIMXc_9=~Iq=juKxXAMm3#L1*5e
zh24W`7wMMf(P_QF+*XtEhIdXiB0;aK*u-}>Sw43WuB7`SIx4rEyDB?X*v8uR7BJn`(H5h=
z@D0@U8kOQNqIiMGE{3no$KQS*bz*kaP`^yC*Qxu%^vFB-koNDh@buK9)WhjgC$iy#
z<~LAWf&AO2I7+piSTFSEjCv&)%3Mqxz6Bh%PCACB%%2%Yp`2NGYbiS1qG$7C7^`q*
zDj@u?kKrya`=Km^_vcod(!>XU49yPrtc!1D!2;fSPn=;yAqbF6Vt2-MF9Yoo(EndI`CWhsmS?2_ZklkvnS
zbZVD^(aAr5cM9!)pf_lP+WR=4s$LG}UkadHWzx=v@VmI^tdjCs?+gm)WlIrNzzUS3Kq)bEgoP{Zs
zbAr!#Q!0d{$3<#p!m^HB(x%1NWN^kOP+iV>S;Swy+`GaXii0h4r)W(lC(~kpegSRb1Wt~
z%EleoupuX!54W-`xdN@_f#XKsZiqM}qv~l!3xi5@1m;Me1hc;rm;JFV>E1hvHJS))
ztJJhC`WzudK8L6Z4RcXO7nP%udO+s$DJV_763isT43j
zVy3@~iNABjNCUN$!;b}l>45KL%{38r<8v1w#FSiK(^JD;0YgdtWm!i1Ty%Ccm(2^{
z?s59vemG6N+m=9x-esm$Fm}IEA{RBRweV4!alJ3WEx3Q+gPQzzcuaUdus#Pq>R@mr
z_rU{7Gc*tZm7&bC8t%ITD{Nuo1~p?3dU3T^)77eY>`UN!57cz2zo-UnQfX8ND-`bF
z5eM?q=Zmw0apM^2ogB5n?g`jR@+OkV{C??1mu$S1)Z16Bj$&8S7b=T$e>cgGMvyYX
z(8yJOICzdY>hO~SV}MV?*^=KdZ$rO(z^fXnE^8n
zJdhvDbA{LyKM-JyZA!63jwPfwN%5U06t-d!MkZ%M7ojzSPw#ZR38MEp!8KBBE9y?X
zNrIQ+t~T5)_7F{YB%UuEp*SY+8%Ob$AW+o_{g8+#Q~bV|;0g~0FW_|Y6lu>E9Em(3
z_wGA|N&N}#am)zXm))XJAaV`jiS+5(Jr_pdnygZm$onfR`VauoMKPdNkn%Y-jq>_>
zx*DB=*WAody>1C5_NRD)XpcAf83kkjdM{5FA9h@=ervcYgZl}#6eblipXbGr!e(;d
zq$a&d<|9;K+feZkwXPyxEcogGKVoS9p=d-PYLgC=sCeFez|pe{$u0$%`SR&4>z>_RVW1SV~A4+-7_Y?
z(G)Uw*XT+Bhx;n61>^Z!GqM{+!sY7vm$RsGg~I#xo73vJbFeUiM|I`vgFV}3)%O@Qu!YWsuBh$N2LDY+DICbenZ{C)$#$m
z&)f>1?2bG(>{(cdT8Kg(KPfH^g{B>)Z4js`GPx%Z-cBVq#1HK)gmuXdP~)0DWtD!M
zV0G+T9>cto{h0i=PKJU)a98Sv-h+z-zP8OoE$Hp=I^o`ag7)!#NXv`)sb9)zt-s5;
zznM)EN(6UWurje!Hjr=xK1#MBWIqoTTvtf~J;obfi3-uqGa|lWP6X#80Bw^B=seV|
zS-m80b6$&}9CIOJxpZb89y(mSGFA<*NhRcjbyqhTP%-1XGBfn#Q4GKTY_=I6Sp4s~
z_n&(z+cKXI>aCKyz7?*#<&}KMg2n|?T*pV>VX)5Vgq)*LN=Sec1#&hnIOtwNhYkma
z_^m;=??X7x?4%7ZRK1euyfVpnGVe%BsBt@qKae_qtcMpo-Y){q76MmM0iMfNQ`-MK
zs%Gxt`d{|da;}oD0t5&eo;0xcf)IHMCMevDnnilFtRzu8Drl%zL0=l)SOteliTt>#B<2jfDc#W;W@>kJWaM1*TZ+EW2ViC(2H$T)8(>~N*p7;2fsfzMrH
zj^jmY;zi{z&Ot8kF1Mo$tg8u?wzneG44eEO_=1b+!mEnL@u-MBOmB6aqhk7oQgtQrS^ReK@iBu(^_`^
zk9%T&lb$7IZ(qR=ASYItd;{?%xgiqaF`d(ES4nyDi6a!B6YEwN4^~vdZ7@-yTpU%9
z00#-M3>BfkAfcQhS4Dx9^u=H-OBq{q?n%vLRpD1UgodPIl_i?i>;p*HdGd*M!OD&A
zpDr@RN24<{*mr_B%mcNV5d@NRD|Z4z5gL(@qR%-BJgTe^b0GQ_M3a@0rurp&Z($H<
ze?wpN7Vt#L%X3I8j3Q->m3+iiu8`SF-RZVGGbzx=Q}vz`Sg4)O5GV
zGaLW_A(){QppRt4%zb^B7Ea6OKeJZ5!%`{5mjB5OnL$n;f?iG|YaOQFj^!%!o2@Db
znB>Y<^zuu#)7qeb65fv7h!Ea5Os^PAo+V=3e#B
zD)4W(!TIPP>m(xi;@f)cw~G?)05u5Ve6g!l6mhrXdI{iKz?_inY@eElGBs!!*$@-M
zxtu<(7Ieo7p6R*s8EQE7@3@;HC4%L>`}hc>Z>~_e66pZYiLdX)wBreMno$#v>X77<
zVe&7IUyz70#))J;rDu|@Hpt%Q7(b}jp&5X;=1HO-U=sxsMz6}6*Sy40eN|ZKb+i?x
zz~5Z+E^ONP`sPVi+dQ8a0E%8;rM^LeEJmH1sV{4!^!2{Jr?$O1ep|UV*d7{B2%?Hb
zFKk6EW{6nH8=w*0t3^?K_YPkcAJ>^Y@OKCPAOu1l%-aE4xrHF)kW?0kLXZnPuCTfi=LviHpn@v%`J@KfQ!`v|L)QXb
zs5DSf!l&C>Yt5`YFEFW?IYCyOrQ@wCR6MW^Vqa87BIEl~
zoqFACf#hfC2}r0PUjuXL>+8m%X8Xk^fy*rjAlW+kLmi(Plk>Z37oSru2+yalqE|JQ
zD`)Neb-cPi7N8zJKbrRL6;D1DHa{*BI5*h}k?)#C-*-$uk+Gw_cs3|WjL6P
zUdk5s`<(9Yx!y?_mJSEsL;q|!dz%cq@hf}+L4ZJj+c9dZMf}E$r#_2&5;Ntmoz)F4
zwiLQjgnc3<5ycvBYx!HuOGGzqI5IZhVF(|(FXrRGH)-136UGuQrUvbf&*|;2X8Z|B
zNt@e#Jhn*9h5t;LD37gB>GU1ge(-9MTD^Jir-0=RZdb-u3oq6Shn$qBQC*+X9(Ct{
zt`zC2mahfj#fvf^)S2s0jgf2?K?Xr_4Yc)xNv+k#4<_e|e8|5H&Jwl+wlf(izrFB}
zMSTVib$sG+(JZ9ny67M&pQn^CmlcqJrmj}lJ)V!aD_X4FGFb@4aMUeDBRmZ!WvHOf
ztij{&uUTXTHwfvyFeDvEhuAF1cMHzIX+x1tCtfBN5CcJsp}gcrO<#8z{@1qd%34&~zV
zLO-Tqn#_`xp_7`c$eU}IDmJ?2U%@v_`kOy}r<=QuCJLx+lKV_`K0Vv9b8!Wo4r;t@
zQ&a1`!bkDa0dQ?wu@N
ztrKYhOPDHN(+%+cRbpnRKFT&~%I_MozzhPNB4BlQLD8N&m3eOj
zv8_lm?_kNB3`f_{Q%UnpsmNqRuv%bfipMNy*DT`>jM8z4!Sv9DRQSv&0f5K$vd6fQ
z{sRX+s#MHrVtUn={(5MKc
zG)o!kF87(YUlZN-Y>BA!>9{IxlGsG6(Het5nZ|Q4Mw&RsyoBt_me)r
zu6{)U=&mSw^>g{Ht&vUh-r`n>8-X%GEQ4Kr$S}P1JF<$ke%`G=Y$}vEN2^62cH&@>
zUv_x)GiwA;xZtir+6jK6URQrKB}_>3vr9%0!)0EDSfuJ
z3y}GC`yb6P$PUeZnxv0G%JQTXl5@qdLFJU@_R|o7ABb+*qpnoe2GkKpYRC`#qiz|@
zA;&YNx?zmtVBAc?L#4&FZwlP3wooXuNM_;EOwQl1^=cLA62OLd*ztC%r2DY_`f+qs
za(jVA_Y+y|_R)ISje*OVerw;6O-1Vuznq(acwiE5?_TyyvHUqw*ZmRnu+3t7$*(_o
z%B{bJ^9?-p8rA=Cu#G_H{adoz%~`Hb=$x{Bu73qE^v!>ojV!#Tky&~KxzLggIZnM=kO|8#I%|PM{exYSG>J;U0a>Ec5Mf@p=aqaqcdH
z$^w~=RH^IyC`OZTnR{T43k)@=T1MUkIVEDHTlf^_D(iHoIGnT==W{sD)`&SS#U1E5cLNw7aXJ&CC-8xpPw$JI
z8d}BAhn{}?TItU@MO9(jPEGY3xG-KI+xF&TgfbH)wW{#ES(E?%I~9Eoh6DPMuVqG%
ztvBg4{8%n}Okovx^G?3gU*^U4%UC0PXa}sjLD}wJRXL>lMm)
z1iXV0YC*qSy9V;y@z`ZBRkFmYjgwCCtfIuy&cNnjN!pPf)iuI>tVgk}slfOALi^=_
zVv#o6bE>7_&egF72{mT-2ji=^HErvXhw(?VLWD4Yb+F(UjTR^OjAol8fB01|s{h>aG1+k}w)&U=Vgd%*
z&JA&2CeD9dxL7`U+^_dAs;Q+zsH4sK+r8br>oZvHb!4H$nXN}JGvD!FOZmJeMtch;
zh85ZITnBP}k>OcLSOXwKpEpR8z=_sZ6x??YgN>2JvdL?O{yCW!(S7Hz?H7+(D;ZVv
zUr@CPzafrODi8XIn}e%?n@M)b*s#@^h+FciQkK^
zoJwNxi`J--o!Kh=+~v{UzyVfVcIiO~>;QiewPd{RfS8g0yg`K`LvcI4nd80z7F!ux
z*Y;RFe$jq3Leh>YA)LPWcUxp#)U&DLnmAm+913#Qdi|{sCznO;`T}wYxnv*2ettrFECs5P3t9lnj
zvSf93w_YC(*?`rnPqRv(rX9bo?5xGZMUQb$-5!Yi}`G#>VX;hBOEx4!YY-kvD6R
z%e)6;n5vyIE-h(ixZuYRAKr}l<|~ERYP*Y+*>!+I$l|_m#eW2u8Hz`7rNQR1w|
zJ^4gb1BfA{lDy*)4VYr_jGNF@Y&!Q9CmOWoH7iy(+t4n*
z4ozymo*IgLli4gzxL;vZ_Vq|lQdaL?tmFB8#pNK}H5K4ml{+E!4{_Prp7l51b}g^d
zI!1cpo%Jsxt_Y0WIQVzUl+HKvlj^>vi*LwPXL9>VnAQp=iF1CMEj4QrDqrxznwyGN
z9hu*g)F9&i3sNA7JAV&%s(k%?dFcv+Hfq(?KOq#x`t{JrAn3Jo>M&49XrA|3D4&a(=ed;qRE
z=hh@~oHtHjulZ|Rz<73%Lq}4Nc0W&5H~)1=KvgIJLqPSep28XnqB8SFh35fFy~{Xw
zIX43hIG&eX=cmH3rO`DTUneEKX!Zx&QhcJD7iKmKzgL%B^+3MqrsTTwD<)0+;%l#8
z*WGi$OvCpvdi*6jo13`%VFMX|u~0hH6R;7u45;AS#@MHd$gthMSoh4%xmz$gz(O!z
zK!@NVF@TW`8d4_Baw62WUm0X}3%06&EHlh>)r*-F#D8K2%%{Xto=4Oa2hTjg5W>Rc
zR%CrYIUs6wc(0k~?lME?1~$y{tNy(go=n0<;L+ho;mT$8_TNjdt1f
zz{OEQiX2?uQUR#QR5(8a|Gz}yq%R#mV)^-R!8W{lzpVpYm6>3ZxHlW?B)s{^(D;zx
zL*ZU;UHl0htYjSfq$eLHksQD{K}iDDJ30zsYTnhFcdAkWB{XA>7~UZGiWOqBPRsPA
zC-qNRGBYTFen5(hpq%`aoNtHfTHrFX19Crl4DOEVm)j&B)#c^E=5e=?#_Iz}YdrKK
zYD{#7CeI7QbkN{6(k^@_2zNyNj6)=9VK}sQehU&S|qP45xnlWI9Fqk
z(>&bRskex3+2xmE-=8nC=pFWD55r;8D&UBtWkMT8NXoH%+;=Ow#qsK>*PGI4af
zh&W9J+BbxBi4PvmvQ5}deFRE|&-Xmr)xPGIpvGLW&-eoJhqkOUAia9Zch{>E^n;Le
zasowovm&_4Uy_1BVY3`dC$i(NKV<04pgZ*33-qN7*OlZ_F|ZE#F0<(H
zHhuP_5(@PYAL4AaZEC+DLA0P^coS;-r5Aq;kJ)(sgJ%jn0e3-6zK?q~QXIba{7bLt
z_)f3LL|8&{T}g!6xs8@3t&B&c>Z(vGPbqegN-<81V9BFJtD+Ne(g;?A25{K8H3b@XYv_(EZ6~~JK_71+(0m1R@(yBVz
zyru}h#}%egh;8ra9t(snR@c5{#}-Kzs0to8n4FD^&mb`46n$AANQWkHw&6w
z!~Yn;S{p3KaVN9|csBwz-dn4TDqJJNZ@9-p9G){Q&tNHlW6`3+f&{mrY;QQMcdj)WiHKL*WX}|Oe~)$_QbxxATZk{>z&+^#bqPpC
zz-n-~@9VljF;j(cAT5xdIXbUH-+g7QKo0Z81_F!{9GfY8o>~?W*|suB>y3J&uZ`a5
zRDI<3ud|v;FU-*e^ZkhjXbTF&1SSyQDP852D)Nx?7Al7Ah~kZoM>0UkIl)QHB{W{d
zd?sEY!g3K(A+6|-7$7;yW=9Jd!Igyx9n(%>?SCt-Mt00$v`sOP`#3Z5?+ThxgqM=n
zIdI2FmQw4|am<_7CjW421-oIg?-6b=md&kO{0F2?`v{o`Gi-1PjZC(<#^75G4t1=`
zN64=W{|ZWJHTojjYx2xu!fWiaz~Z4*kVSbUZYlmTaSt(qIB?bA^llucuPb{p{xfDQ
zG)@sk4&*rD)qEOx6}o#9_mM8QdX&T2c%R0)6A?{3^5c&9hK1x2D4deoVeZbV
zquS2Nz3xa=zYBsrvs<&Hd5o68h&CawAK8ZN6lUIa{#&@I@m-CT=vv%rlUVTVp;(Rm
zyu|cFtzBwJPx3@(5_WpA*ImlsOjMuYW4Z7{Ez7i~Oeam)$#BM{{i>^%*34L`jJt%&
zW!3*IbU6bSpqV)n158wYt
zdY`l<``$EdjhjgYv7h%QoUjL%wg1<3tKU`XH&ef|SFL`ZPxX%5D)vmi9WC^4oma%{
z{W{95;WmUmCBSC{qn<2P7W!`LkU63z?yyN!9c$xouWjufF5s2A3snW{9qT&oXS&UK
z9-eQ_A9AQXJbW}qJSuPGXi>84JM4|>;}LdUlQVMv)q0vrsb2Y@@TWsMMzPV(*k2Sm
zBK)4~0%7>&n^*kmS83T<)s&vmtmwC@tJC>ukFWcUCrzGJe(DlmX_mcGoxt`9WhS*l
zOwB0E`AdCTyQ)%vd;N{q^t{U1VrrSiF@=Ib76sdWT`s)tYahHG*X1hl0Sx)HdDCOU
zaiAaK+!{v8BUIsf3lAqqnwgvkPuLnyS;RdY)*-k;6^yH{qO0W{Ihp#;V4z^R{#<
zXv!pKYQm|AEJ>y-e14LNdD!&3z~+VTiVLy5y6TIrO9ep%j+S==arZOwE9PV&;9;g#
zM7!hWUd4O~?5f0TXKt$L?7+dK`K+=aQ|fcTk%8SukKtK4u6Pof`;}}Tpw#g#z9!9H
zpPk@heN3$@Z|+Zdh%8(C*DuWppJd1lzRQiR{+aG*Da)l%hi&RNc2GZWM3PmXe*~)f
z$>8D$H*t@sDw*~8{B{2q{wv;OiMhW<0y7}yvQM+$@Ry3*xH9&Hy^u)1(Yd<&PELw~
zJ~tT>P16-d7Bt{yo~quX9z`JSh%?^2nJzId3QdBiRAD)ITt)JaX;agBV*o@>oENa`
zA^rX0Vg55<&7xB(>?+e~zsL39WrowKlJ~*5rE!b$rKH2uJVvI<==fT16Ogf@ooeD7
z*J4Lo&glE#89Uzzi~M{RYhZOVPt;UMmB%xq6MD89r?M>k
zx-+YZdWo
zww%N1{%o1!>qx_s_r539RTG8tSC9|(!
z#et!6Ys_BvvEb@Xjd%tk!lsC1lt
z=r>jI*>9{O*CA?S%IejxWI|B26Pd&p4T*Zmujroq_Byef%BV#*wElq=Mxk}mYf5n)
z3Z~KF>(sumGvs|;u-|{R|%WvzsI(f$5v9#hJExq#|jKUvRydE1v6JF=3
zeRe#o1xJc@hR6-bwNMq(NMH%ty48?NhBN!J+vvoJ>_>JNEYwuz`?`0TzYwe3Q9(M>
zbQ_5I`NG0s5!03-H5*D8)9vAxG^b><{^{O|^u4+<`N#gt-iO~OoAtf571RoEbz=Z;
zWw4uT>N(5qmnTbx4WrJY2nT5{FNGBkl>sI^e;n?)EETJ1FN2QW2myxdOKc&w0JJxOP{A@v|zlw
zLl@4F841{#Y`ThX3u6l|kTF;`T@S%HIHW}w@Fa`woaZg$Os(cyz{e`b?Mfbque(xG
zddm!5qJ+NT&2GJSp<=D&dr@JsTiQYo`0l(V>m&pczP7LBzKHDAIN#X%R81aia(%Z1
z?E6DuEjY*xtjwWl6L-%w5Xj4D9b%_$y%g?ax~MlHS9CG}C}9bH(3z_dn^k
zMozjpusl?SnbqTXxTWiIW|bd7Z+ITH+;HzGY}s7n9DXt0Z8E8U`!IrS&`fx4$oEiV
zui40fV)mtzeX*un%`uO(h1#1?>{veLZUte^&UY!k;}f^Y5A9c%z8=?L1!e8>>XGyi
zYWf@E-KZw;YkmSa&ijp;&;J}YD{pM8GDBOc8PWZBDfsd#1e^6;Yx;yN-vxTMt4R8#h6R)=go?g9n90E<%J$yA8g-mQo^HswrpxyE;R
z{xNAqH2H&q7QN$y2Air8MKn7e|1#i$YGz-y`EOH;&bTbJXwSs|8vR)=E>XeHZmeyaL;r9;4s=s;+z>+fYm7P8>J8cI7Sw)Np?m4HR>
zpQNwDJX(AHymbxua{ens(qG{S)Ifd|LaQ0&R{lb>QQev9wF>cj#dns2p}+GfDR{S
z1C-GVTTyWpm^0>iav|6C4yycJ=zC}^k3)P+%3Vgwk9QOGH^_lj=M()|DZvYjGmrIR
z7A~B`TK%?^xMm+`p{tRBci#k@x+vzGt~OV7VG`+
zdJIx;-o7wHFE-(LY!{1kc3;F5p^lr3J3KSu0=9BwxK;Y<|>Ug{IGu@&79RalH_}pE}Tth=A4K{KI4_ztw&;Qs!aY
z`5nsBCC9<@mYXn0jg1D_;?nqHSslF+{|jbOuU`Ki#K37J;jyjV_8Si@RHiN
z<#`7yPzB`lcV0$V$Y*=nl9OTIi~{U9DzI2lgp9Zp{1h5FUr`FSPCq#Fo%^&`?ycS5
z?uFIZ7hJ3feS(`ZDxp=ZpcGK|(5@3Xk}mj~IClcyd+<3HNlt~*OU>ws_d^_JeM802
z*I$pg1;vN0}jsMrupqvP@C1FJkzM#g{YBXeAN=0@b_
zcr@-cYdP-n4$(C(VJ?C3J$<L#U`pl$scFY{%q*0oZv6jd$Pb
z;=O19&aKwIV{NJHq2h_wZBfMhkcOWrzS5h~|CUI=mqtyV_TC;(b0b}WX7$dCr5Yp7
zn;4|#qlB4u*bR*hgH$Tb;Qtnf8pmB?lho3A03W
z7Zymr+a;EZicpmMBv-1%(7OQ#S_Fmn?K)I{!3Op93