From 4e09bd8f448b8e2dd0bece6819f0fb07a867643d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Metin=20Ersin=20Ar=C4=B1can?= Date: Wed, 14 Aug 2024 22:00:31 +0300 Subject: [PATCH] completed the proof of the categoricity of dlo --- AutoBlueprint/Latex/Basic.lean | 315 ---- FormalTextbookModelTheory.lean | 118 +- FormalTextbookModelTheory/ForMathlib/DLO.lean | 246 ++- .../ForMathlib/Language.lean | 87 -- .../ForMathlib/Matrix.lean | 20 +- .../ForMathlib/Order.lean | 324 ---- .../ForMathlib2/Cardinal.lean | 7 - .../ForMathlib2/DLO.lean | 218 --- .../ForMathlib2/Matrix.lean | 25 - blueprint/lean_decls | 44 +- blueprint/print/print.aux | 57 +- blueprint/print/print.fdb_latexmk | 13 +- blueprint/print/print.fls | 3 + blueprint/print/print.log | 48 +- blueprint/print/print.out | 7 +- blueprint/print/print.pdf | Bin 30762 -> 29260 bytes blueprint/print/print.synctex.gz | Bin 8791 -> 6179 bytes blueprint/src/chapters/basics.tex | 292 +--- blueprint/src/chapters/main.tex | 7 +- blueprint/src/chapters/model_theory.tex | 67 + blueprint/src/content.tex | 10 +- blueprint/src/web.paux | Bin 7226 -> 9130 bytes blueprint/web/dep_graph_document.html | 604 ++------ blueprint/web/index.html | 33 +- blueprint/web/sect0001.html | 1357 +---------------- blueprint/web/sect0002.html | 427 +++++- blueprint/web/sect0003.html | 154 ++ create_content.py | 72 - lakefile.lean | 2 + 29 files changed, 1152 insertions(+), 3405 deletions(-) delete mode 100644 AutoBlueprint/Latex/Basic.lean delete mode 100644 FormalTextbookModelTheory/ForMathlib/Language.lean delete mode 100644 FormalTextbookModelTheory/ForMathlib/Order.lean delete mode 100644 FormalTextbookModelTheory/ForMathlib2/Cardinal.lean delete mode 100644 FormalTextbookModelTheory/ForMathlib2/DLO.lean delete mode 100644 FormalTextbookModelTheory/ForMathlib2/Matrix.lean create mode 100644 blueprint/src/chapters/model_theory.tex create mode 100644 blueprint/web/sect0003.html delete mode 100644 create_content.py diff --git a/AutoBlueprint/Latex/Basic.lean b/AutoBlueprint/Latex/Basic.lean deleted file mode 100644 index 3d5ad0a..0000000 --- a/AutoBlueprint/Latex/Basic.lean +++ /dev/null @@ -1,315 +0,0 @@ --- import Mathlib.ModelTheory.Basic -import Mathlib.Tactic.Linarith - -section - -def ite_lt [LT α] {x y : α} {flag : Prop} [Decidable flag] {z : α} (h₁ : x < z) (h₂ : y < z) - : (if flag then x else y) < z := by - by_cases hf : flag <;> {simp only [hf]; assumption} - -private def parse_line? (line : String) (field : String) : Option String := - let line := line.trim - if line.startsWith ("\\" ++ field ++ "{") && line.endsWith "}" then - let value := String.mk line.data.toArray[field.length + 2:line.length - 1].toArray.toList - if value.length > 0 then some value else none - else none - -private def parse_first_line? (line : String) : Option String := - parse_line? line "begin" - -private def parse_last_line? (line : String) : Option String := - parse_line? line "end" - -private def parse_label? (line : String) : Option String := - parse_line? line "label" - -private def parse_name? (line : String) : Option String := - parse_line? line "lean" - -private def parse_uses? (line : String) : Option (List String) := - let content := parse_line? line "uses" - match content with - | none => none - | some content => - let lst := List.map String.trim (content.splitOn ",") - some lst - -private def parse_content (lines : List String) : String := - String.intercalate "\n" (lines.filter (fun line => ¬ line.startsWith "\\")) - -private def split_environments? (s : String) : Option (String × String) := - let lines := List.map String.trim (s.splitOn "\n") - let begins := List.findIdxs (fun line => not (parse_first_line? line).isNone) lines - let ends := List.findIdxs (fun line => not (parse_last_line? line).isNone) lines - match hb : begins.length, he : ends.length with - | 2, 2 => - let begin₁ := begins[0] - let end₁ := ends[0] - let begin₂ := begins[1] - let end₂ := ends[1] - some ⟨String.intercalate "\n" (lines.toArray[begin₁:end₁ + 1].toArray.toList), - String.intercalate "\n" (lines.toArray[begin₂:end₂ + 1].toArray.toList)⟩ - | _, _ => none - - -end - -structure EnvironmentWithoutProof where - type : String - leanok : Bool - uses : List String - content : String - -namespace EnvironmentWithoutProof --region - -instance : ToString EnvironmentWithoutProof where - toString env := - "\\begin{" ++ env.type ++ "}\n" ++ - (if env.leanok then "\\leanok\n" else "") ++ - "\\uses{" ++ (String.intercalate ", " env.uses) ++ "}\n" ++ - env.content ++ "\n" ++ - "\\end{" ++ env.type ++ "}\n" - -def parse? (s : String) : Option EnvironmentWithoutProof := - let lines := List.map String.trim (s.splitOn "\n") - let len := lines.length - match h : len with - | 0 | 1 | 2 => none - | n + 3 => - let type_first? := parse_first_line? lines[0] - let type_last? := parse_last_line? lines[len - 1] - match type_first?, type_last? with - | _, none | none, _ => none - | some type, some type' => - if type ≠ type' then none else - let leanok := lines[1] == "\\leanok" - let uses_idx := if leanok then 2 else 1 - let uses? := parse_uses? (lines[uses_idx]'(by apply ite_lt <;> linarith)) - match uses? with - | none => none - | some uses => - let content := parse_content lines - some {type := type, leanok := leanok, uses := uses, content := content} - -end EnvironmentWithoutProof --end - -structure ProofEnvironment where - leanok : Bool - uses : List String - content : String - -def EnvironmentWithoutProof.toProofEnvironment {env : EnvironmentWithoutProof} (_ : env.type = "proof") - : ProofEnvironment := - {leanok := env.leanok, uses := env.uses, content := env.content} - -namespace ProofEnvironment --region - -def toEnvironmentWithoutProof (env : ProofEnvironment) : EnvironmentWithoutProof := - {env with type := "proof"} - -instance : Coe ProofEnvironment EnvironmentWithoutProof where - coe env := env.toEnvironmentWithoutProof - -instance : ToString ProofEnvironment where - toString env := toString (env : EnvironmentWithoutProof) - -def parse? (s : String) : Option ProofEnvironment := - let env? := EnvironmentWithoutProof.parse? s - match env? with - | none => none - | some env => - if h : env.type ≠ "proof" then none else - some $ env.toProofEnvironment (by push_neg at h; exact h) - -end ProofEnvironment --end - -structure EnvironmentWithProof where - type : String - label : String - name : String - leanok : Bool - uses : List String - content : String - proof : ProofEnvironment - -namespace EnvironmentWithProof --region - -instance : ToString EnvironmentWithProof where - toString env := - "\\begin{" ++ env.type ++ "}\n" ++ - "\\label{" ++ env.label ++ "}\n" ++ - "\\lean{" ++ env.name ++ "}\n" ++ - (if env.leanok then "\\leanok\n" else "") ++ - "\\uses{" ++ (String.intercalate ", " env.uses) ++ "}\n" ++ - env.content ++ "\n" ++ - "\\end{" ++ env.type ++ "}\n" ++ - toString env.proof - -def parse? (s : String) : Option EnvironmentWithProof := - let s? := split_environments? s - match s? with - | none => none - | some (s₁, s₂) => - let lines := List.map String.trim (s₁.splitOn "\n") - let len := lines.length - match h : len with - | 0 | 1 | 2 | 3 | 4 => none - | n + 5 => - let type_first? := parse_first_line? lines[0] - let type_last? := parse_last_line? lines[len - 1] - match type_first?, type_last? with - | _, none | none, _ => none - | some type, some type' => - if type ≠ type' then none else - let label? := parse_label? lines[1] - match label? with - | none => none - | some label => - let name? := parse_name? lines[2] - match name? with - | none => none - | some name => - let leanok := lines[3] == "\\leanok" - let uses_idx := if leanok then 4 else 3 - let uses? := parse_uses? (lines[uses_idx]'(by apply ite_lt <;> linarith)) - match uses? with - | none => none - | some uses => - let content := parse_content lines - let proof? := ProofEnvironment.parse? s₂ - match proof? with - | none => none - | some proof => - some {type := type, label := label, name := name, leanok := leanok, - uses := uses, content := content, proof := proof} - -end EnvironmentWithProof --end - -structure TheoremEnvironment where - label : String - name : String - leanok : Bool - uses : List String - content : String - proof : ProofEnvironment - -def EnvironmentWithProof.toTheoremEnvironment {env : EnvironmentWithProof} (_ : env.type = "theorem") - : TheoremEnvironment := - {label := env.label, name := env.name, leanok := env.leanok, - uses := env.uses, content := env.content, proof := env.proof} - -namespace TheoremEnvironment --region - -def toEnvironmentWithProof (env : TheoremEnvironment) : EnvironmentWithProof := - {env with type := "theorem"} - -instance : Coe TheoremEnvironment EnvironmentWithProof where - coe := toEnvironmentWithProof - -instance : ToString TheoremEnvironment where - toString env := toString (env : EnvironmentWithProof) - -def parse? (s : String) : Option TheoremEnvironment := - let env? := EnvironmentWithProof.parse? s - match env? with - | none => none - | some env => - if h : env.type ≠ "theorem" then none else - some $ env.toTheoremEnvironment (by push_neg at h; exact h) - -end TheoremEnvironment --end - -structure LemmaEnvironment where - label : String - name : String - leanok : Bool - uses : List String - content : String - proof : ProofEnvironment - -def EnvironmentWithProof.toLemmaEnvironment {env : EnvironmentWithProof} (_ : env.type = "lemma") - : LemmaEnvironment := - {label := env.label, name := env.name, leanok := env.leanok, - uses := env.uses, content := env.content, proof := env.proof} - -namespace LemmaEnvironment --region - -def toEnvironmentWithProof (env : LemmaEnvironment) : EnvironmentWithProof := - {env with type := "theorem"} - -instance : Coe LemmaEnvironment EnvironmentWithProof where - coe env := env.toEnvironmentWithProof - -instance : ToString LemmaEnvironment where - toString env := toString (env : EnvironmentWithProof) - -def parse? (s : String) : Option LemmaEnvironment := - let env? := EnvironmentWithProof.parse? s - match env? with - | none => none - | some env => - if h : env.type ≠ "lemma" then none else - some $ env.toLemmaEnvironment (by push_neg at h; exact h) - -end LemmaEnvironment --end - -namespace BlueprintLatex.Test --region - -def env₁ : ProofEnvironment where - leanok := false - uses := ["thm:merhaba"] - content := "This is a proof." - -def env₂ : TheoremEnvironment where - label := "thm:current_theorem" - name := "FirstOrder.Language.mytheorem" - leanok := true - uses := ["thm:old-theorem", "lem:old-lemma", "def:old-definition"] - content := "This is a very important theorem." - proof := env₁ - -#eval env₁ -#eval env₂ - -open EnvironmentWithoutProof - -def test_parse_line? : IO Unit := do - let line := "\\begin{merhaba}" - IO.println (parse_line? line "begin") - -def test_parse₁? : IO Unit := do - let stream ← IO.FS.Handle.mk "proof.tex" IO.FS.Mode.read - let s ← stream.readToEnd - let env? := parse? s - match env? with - | none => IO.println "No environment found" - | some env => - IO.println $ "type: " ++ env.type - IO.println $ "leanok: " ++ reprStr env.leanok - IO.println $ "uses: " ++ env.uses.toString - IO.println $ "content: " ++ env.content - -def test_splitEnvironment? : IO Unit := do - let stream ← IO.FS.Handle.mk "theorem.tex" IO.FS.Mode.read - let s ← stream.readToEnd - let envs? := split_environments? s - match envs? with - | none => IO.println "No environments found" - | some (env₁, env₂) => do - IO.println env₁ - IO.println env₂ - -def test_parse?_theorem : IO Unit := do - let stream ← IO.FS.Handle.mk "theorem.tex" IO.FS.Mode.read - let s ← stream.readToEnd - let env? := TheoremEnvironment.parse? s - match env? with - | none => IO.println "No theorem found" - | some env => IO.println env - -#eval test_parse_line? -#eval test_parse₁? -#eval test_splitEnvironment? -#eval test_parse?_theorem - -end BlueprintLatex.Test --end diff --git a/FormalTextbookModelTheory.lean b/FormalTextbookModelTheory.lean index 74bd313..3c10936 100644 --- a/FormalTextbookModelTheory.lean +++ b/FormalTextbookModelTheory.lean @@ -1,116 +1,2 @@ -import FormalTextbookModelTheory.ForMathlib2.Matrix -import FormalTextbookModelTheory.ForMathlib2.Cardinal -import FormalTextbookModelTheory.ForMathlib2.DLO - ----region automatically create leanblueprint - -import Lean.Elab.Print -import Mathlib.Lean.Expr.Basic -import Batteries.Tactic.PrintDependents - -set_option linter.hashCommand false - -open Lean Elab Command - -abbrev excludedRootNames : NameSet := NameSet.empty - |>.insert `Init - |>.insert `Lean - |>.insert `Qq - |>.insert `ImportGraph - |>.insert `ProofWidgets - |>.insert `Std - |>.insert `Aesop - |>.insert `Batteries - |>.insert `Mathlib - -def userDefinedModules (env : Environment) : Array Name := by - let allowedImports := env.allImportedModuleNames.filter (!excludedRootNames.contains ·.getRoot) - exact allowedImports.qsort Name.lt - -def test_userDefinedModules : CommandElabM Unit := do - let env ← getEnv - let modules := userDefinedModules env - logInfo modules.toList.toString - -def moduleNameToFileName (moduleName : Name) : System.FilePath := - System.FilePath.addExtension (System.mkFilePath $ moduleName.toString.splitOn ".") "lean" - -def test_moduleNameToFileName : CommandElabM Unit := do - let env ← getEnv - let modules := userDefinedModules env - let mut fnames := #[] - for module in modules do - fnames := fnames.push (moduleNameToFileName module) - logInfo fnames.toList.toString - -def userDefinedDecls (env : Environment) : Array Name := Id.run do - let mut modIdx : HashSet Nat := .empty - let mut modsSeen : NameSet := .empty - let allowedImports := userDefinedModules env - for imp in allowedImports do - if let some nm := env.getModuleIdx? imp then - modIdx := modIdx.insert nm - modsSeen := modsSeen.insert imp - -- - let consts := env.constants - let newDeclNames := consts.fold (init := ({} : NameSet)) fun a b _c => - match env.getModuleIdxFor? b with - | none => a - | some idx => if modIdx.contains idx then a.insert b else a - -- - let mut newDeclNamesFiltered := #[] - for decl in newDeclNames do - if decl.isAnonymous then - continue - if decl.isNum then - continue - if decl.isAuxLemma then - continue - if decl.isInternal then - continue - if decl.isInternalDetail then - continue - if decl.isImplementationDetail then - continue - if decl.isInaccessibleUserName then - continue - newDeclNamesFiltered := newDeclNamesFiltered.push decl - return newDeclNamesFiltered.qsort Name.lt - - -def test_userDefinedDecls : CommandElabM Unit := do - let env ← getEnv - let decls := userDefinedDecls env - logInfo decls.size.repr - logInfo decls.toList.toString - -def getDocstring (env : Environment) (decl : Name) : IO $ Option String := do - return ← findDocString? env decl - -def test_getDocstring : CoreM Unit := do - let env ← getEnv - let doc ← getDocstring env `FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo - IO.println doc - - -/-- extracts the names of the declarations in `env` on which `decl` depends. -/ --- source: --- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Counting.20prerequisites.20of.20a.20theorem/near/425370265 -def getVisited (env : Environment) (decl : Name) : NameSet := - let (_, { visited, .. }) := Elab.Command.CollectAxioms.collect decl |>.run env |>.run {} - visited - -def getDependencies (decl : Name) : CommandElabM (Array Name) := do - let env ← getEnv - let visited := (getVisited env decl).toArray - let decls := userDefinedDecls env - let visited := visited.filter $ fun name => name ∈ decls ∧ name ≠ decl - return visited - -#eval test_userDefinedModules -#eval test_moduleNameToFileName -#eval test_userDefinedDecls -#eval test_getDocstring -#eval (getDependencies `FirstOrder.Language.Order.orderStructure_of_LE) - ---end +import FormalTextbookModelTheory.ForMathlib.Matrix +import FormalTextbookModelTheory.ForMathlib.DLO diff --git a/FormalTextbookModelTheory/ForMathlib/DLO.lean b/FormalTextbookModelTheory/ForMathlib/DLO.lean index 83e7352..fb08c28 100644 --- a/FormalTextbookModelTheory/ForMathlib/DLO.lean +++ b/FormalTextbookModelTheory/ForMathlib/DLO.lean @@ -6,31 +6,241 @@ import Mathlib.ModelTheory.Satisfiability import Mathlib.ModelTheory.Bundled import Mathlib.ModelTheory.Order import Mathlib.Order.CountableDenseLinearOrder -import FormalTextbookModelTheory.ForMathlib.Order + +import FormalTextbookModelTheory.ForMathlib.Matrix + open Cardinal -open FirstOrder -open Language -open Order +open FirstOrder Language Structure Theory Order +open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) + +namespace FirstOrder.Language.Order --region + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] + +/-- +The interpretation of the unique binary relation symbol of the language `Language.order` on a type `M` gives a +natural binary relation on `M` and it is written with `≤`. +-/ +instance instLE : LE M where + le := fun x y => instStructure.RelMap leSymb ![x, y] + +/-- +Given a type `M` and `𝓜 : Language.order.Structure`, the `Language.order.Structure M` instance induced by the `LE M` +instance which is induced by `𝓜` is equal to `𝓜`. In other words, for a fixed type `M`, `@orderStructure M` is the +left-inverse of `@instLE M`. +-/ +@[simp] +lemma orderStructure_of_LE : @orderStructure M (@instLE M instStructure) = instStructure := by + ext1 + · funext _ r + exfalso + exact IsEmpty.elim (by infer_instance) r + · funext n r x + match n with + | 0 | 1 | _ + 3 => + exfalso + simp only [Language.order, mk₂_Relations, Sequence₂] at r + exact IsEmpty.elim (by infer_instance) r + | 2 => + rw [Vector_eq_VecNotation₂ x, (by apply Subsingleton.allEq : r = leSymb)] + simp only [orderStructure, LE.le, Structure.relMap_apply₂] + +/-- +By definition, the binary relation `≤` is equal to the interpretation of the unique binary relation symbol of the +language `Language.order`. +-/ +instance : @OrderedStructure Language.order M _ instLE instStructure := by + simp only [OrderedStructure, orderLHom_order, orderStructure_of_LE] + exact @LHom.id_isExpansionOn Language.order M instStructure + +end + +section + +variable {M : Type w} [Language.order.Structure M] +variable {N : Type w} [Language.order.Structure N] + +/-- +An order embedding `φ : M ↪o N`, induces and embedding of structures with the same underlying function. +-/ +def toLEmbedding (φ : M ↪o N) : M ↪[Language.order] N where + toEmbedding := φ.toEmbedding + map_fun' := by + intro n f + exfalso + exact IsEmpty.elim (by infer_instance) f + map_rel' := by + intro n r x + match n with + | 0 | 1 | _ + 3 => + exfalso + simp [Language.order, Sequence₂] at r + exact IsEmpty.elim (by infer_instance) r + | 2 => + rw [Vector_eq_VecNotation₂ x, comp_VecNotation₂ φ.toFun, + (by apply Subsingleton.allEq : r = leSymb), relMap_leSymb, relMap_leSymb] + exact φ.map_rel_iff + +/-- +An order isomorphism `φ : M ≃o N`, induces and isomorphism of structures with the same underlying function. +-/ +def toLIso (φ : M ≃o N) : M ≃[Language.order] N where + toEquiv := φ.toEquiv + map_fun' := (toLEmbedding (φ.toOrderEmbedding)).map_fun' + map_rel' := (toLEmbedding (φ.toOrderEmbedding)).map_rel' + +end + +namespace DLO --region + +section + +variable (M : Type w) [Language.order.Structure M] +variable [M ⊨ Language.order.dlo] + +/-- +Models of the theory `Language.order.dlo` satisfies the reflexivity sentence. +-/ +protected lemma realize_reflexive : M ⊨ (leSymb (L := Language.order)).reflexive := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; left; rfl -namespace FirstOrder.Language.Order +/-- +Models of the theory `Language.order.dlo` satisfies the transitivity sentence. +-/ +protected lemma realize_transitive : M ⊨ (leSymb (L := Language.order)).transitive := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; right; right; left; rfl --- def to_Lle_homomorphism {M N : Type w} [L≤.Structure M] [L≤.Structure N] (f : M →o N) : M →[L≤] N := --- by sorry +/-- +Models of the theory `Language.order.dlo` satisfies the antisymmetric sentence. +-/ +protected lemma realize_antisymmetric : M ⊨ (leSymb (L := Language.order)).antisymmetric := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; right; left; rfl -theorem aleph0_categorical_of_dlo : aleph0.Categorical L≤.dlo := by +/-- +Models of the theory `Language.order.dlo` satisfies the totality sentence. +-/ +protected lemma realize_total : M ⊨ (leSymb (L := Language.order)).total := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + left; right; right; right; rfl + +/-- +Models of the theory `Language.order.dlo` satisfies the densely ordered sentence. +-/ +protected lemma realize_denselyOrderedSentence : M ⊨ Language.order.denselyOrderedSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; right; right; rfl + +/-- +Models of the theory `Language.order.dlo` satisfies the noBotOrder sentence. +-/ +protected lemma realize_noBotOrderSentence : M ⊨ Language.order.noBotOrderSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; right; left; rfl + +/-- +Models of the theory `Language.order.dlo` satisfies the noTopOrder sentence. +-/ +protected lemma realize_noTopOrderSentence : M ⊨ Language.order.noTopOrderSentence := by + apply realize_sentence_of_mem Language.order.dlo + unfold dlo linearOrderTheory + right; left; rfl + +end + +section + +variable {M : Type w} [instStructure : Language.order.Structure M] +variable [instModel : M ⊨ Language.order.dlo] + +instance instPreorder : Preorder M where + le := (@instLE M instStructure).le + le_refl := by + have := DLO.realize_reflexive M + simp only [Relations.realize_reflexive] at this + exact this + le_trans := by + have := DLO.realize_transitive M + simp only [Relations.realize_transitive] at this + exact this + +@[simp] +lemma toLE_of_Preorder + : (@instPreorder M instStructure instModel).toLE = @instLE M instStructure := rfl + +noncomputable instance instLinearOrder : LinearOrder M where + toPreorder := @instPreorder M instStructure instModel + le_antisymm := by + have := DLO.realize_antisymmetric M + simp only [Relations.realize_antisymmetric] at this + exact this + le_total := by + have := DLO.realize_total M + simp only [Relations.realize_total] at this + exact this + decidableLE := by apply Classical.decRel + +@[simp] +lemma toLE_of_LinearOrder + : (@instLinearOrder M instStructure instModel).toLE = @instLE M instStructure := rfl + +instance : @NoMinOrder M instLinearOrder.toLT where + exists_lt := by + have := DLO.realize_noBotOrderSentence M + simp only [noBotOrderSentence] at this + intro a + replace this := this a + simp at this + rcases this with ⟨b, h⟩ + use b + exact h + +instance : @NoMaxOrder M instLinearOrder.toLT where + exists_gt := by + have := DLO.realize_noTopOrderSentence M + simp only [noTopOrderSentence] at this + intro a + replace this := this a + simp at this + rcases this with ⟨b, h⟩ + use b + exact h + +instance : DenselyOrdered M where + dense := by + have := DLO.realize_denselyOrderedSentence M + simp only [denselyOrderedSentence] at this + intro a₁ a₂ h + replace this := this a₁ a₂ + simp only [BoundedFormula.realize_imp, Term.realize_lt, Term.realize_var, + BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this + replace this := this h + rcases this with ⟨a, h₁, h₂⟩ + use a + exact ⟨h₁, h₂⟩ + +end + +theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by unfold Categorical rintro ⟨M⟩ ⟨N⟩ hM hN simp only at * - constructor - - have instLinearOrderM : LinearOrder M := by exact inst_LinearOrder_of_dlo L≤ - have instLinearOrderN : LinearOrder N := by exact inst_LinearOrder_of_dlo L≤ - have instDensolyOrderedM : @DenselyOrdered M (inst_Preorder_of_dlo L≤).toLT := by - exact inst_DenselyOrdered_of_dlo L≤ - - sorry + apply Nonempty.map toLIso + have : Countable M := by apply mk_le_aleph0_iff.mp; rw [hM] + have : Countable N := by apply mk_le_aleph0_iff.mp; rw [hN] + apply iso_of_countable_dense -#check iso_of_countable_dense +end DLO --end -end FirstOrder.Language.Order +end FirstOrder.Language.Order --end diff --git a/FormalTextbookModelTheory/ForMathlib/Language.lean b/FormalTextbookModelTheory/ForMathlib/Language.lean deleted file mode 100644 index 5efd461..0000000 --- a/FormalTextbookModelTheory/ForMathlib/Language.lean +++ /dev/null @@ -1,87 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.ModelTheory.Basic -import Mathlib.ModelTheory.Satisfiability -import Mathlib.ModelTheory.Order - -universe u v w - -open Cardinal -open FirstOrder Language Structure - -namespace FirstOrder.Language - -class IsRelational₂ (L : Language.{u, v}) extends IsRelational L : Prop where - only_rel₂ : ∀ {n}, n ≠ 2 → IsEmpty (L.Relations n) - -namespace Structure --region Structure - -variable {L : Language.{u, v}} {M : Type w} - -section Relational - -lemma funMap_eq_funMap_of_relational [IsRelational L] (𝓜₁ 𝓜₂ : L.Structure M) - : @funMap L M 𝓜₁ = @funMap L M 𝓜₂ := by - rw [Subsingleton.elim (@funMap L M 𝓜₁) (@funMap L M 𝓜₂)] - -lemma funMap_eq_funMap_of_relational' [IsRelational L] (𝓜₁ 𝓜₂ : L.Structure M) - {n} (nFun : L.Functions n) (x : Fin n → M) - : 𝓜₁.funMap nFun x = 𝓜₂.funMap nFun x := by - rw [Subsingleton.elim (𝓜₁.funMap) (𝓜₂.funMap)] - -@[ext] -lemma structure_eq_structure_of_relational [IsRelational L] - {𝓜₁ 𝓜₂ : L.Structure M} (h : @RelMap L M 𝓜₁ = @RelMap L M 𝓜₂) : 𝓜₁ = 𝓜₂ := by - ext1 - · apply funMap_eq_funMap_of_relational - · apply h - -lemma structure_eq_of_structure_of_relational_iff [IsRelational L] - {𝓜₁ 𝓜₂: L.Structure M} : 𝓜₁ = 𝓜₂ ↔ @RelMap L M 𝓜₁ = @RelMap L M 𝓜₂ := by - constructor <;> intro h - · simp only [h, implies_true] - · ext1; exact h - -lemma structure_eq_of_structure_of_relational_iff' [IsRelational L] - {𝓜₁ 𝓜₂: L.Structure M} : 𝓜₁ = 𝓜₂ ↔ ∀ {n} r x, @RelMap L M 𝓜₁ n r x = @RelMap L M 𝓜₂ n r x := by - constructor <;> intro h - · simp only [h, implies_true] - · ext1; funext n r x; exact h r x - -end Relational - -section Relational₂ - -lemma RelMap_eq_RelMap_of_relational₂ [IsRelational₂ L] (𝓜₁ 𝓜₂ : L.Structure M) - {n} (hn : n ≠ 2) : @RelMap L M 𝓜₁ n = @RelMap L M 𝓜₂ n := by - have : IsEmpty (L.Relations n) := by exact IsRelational₂.only_rel₂ hn - rw [Subsingleton.elim (@RelMap L M 𝓜₁ n) (@RelMap L M 𝓜₂ n)] - -lemma RelMap_eq_RelMap_of_relational₂' [IsRelational₂ L] (𝓜₁ 𝓜₂ : L.Structure M) - {n} (hn : n ≠ 2) (nRel : L.Relations n) (x : Fin n → M) : - 𝓜₁.RelMap nRel x ↔ 𝓜₂.RelMap nRel x := by - have : IsEmpty (L.Relations n) := by exact IsRelational₂.only_rel₂ hn - rw [Subsingleton.elim (𝓜₁.RelMap) (𝓜₂.RelMap)] - -@[ext] -lemma structure_eq_structure_of_relational₂ [IsRelational₂ L] - {𝓜₁ 𝓜₂ : L.Structure M} - (h : @RelMap L M 𝓜₁ 2 = @RelMap L M 𝓜₂ 2) : 𝓜₁ = 𝓜₂ := by - ext1 - funext n - by_cases h' : n = 2 - · subst h' - exact h - · apply RelMap_eq_RelMap_of_relational₂ - exact h' - -lemma structure_eq_of_structure_of_relational₂_iff [IsRelational₂ L] - {𝓜₁ 𝓜₂ : L.Structure M} : 𝓜₁ = 𝓜₂ ↔ @RelMap L M 𝓜₁ 2 = @RelMap L M 𝓜₂ 2 := by - constructor <;> intro h - · simp only [h, implies_true] - · ext1; exact h - -end Relational₂ - -end Structure --end - -end FirstOrder.Language diff --git a/FormalTextbookModelTheory/ForMathlib/Matrix.lean b/FormalTextbookModelTheory/ForMathlib/Matrix.lean index 7543902..817b50e 100644 --- a/FormalTextbookModelTheory/ForMathlib/Matrix.lean +++ b/FormalTextbookModelTheory/ForMathlib/Matrix.lean @@ -3,7 +3,7 @@ import Mathlib.Logic.Equiv.Fin namespace Matrix -variable {α : Type*} +variable {α β: Type*} lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by simp only [vecCons] @@ -14,14 +14,12 @@ lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by simp only [Fin.cons_zero, Fin.cons_one, true_and] apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq -end Matrix - -/- -lemma Vector_eq_VecNotation (v : Fin 2 → α) : v = ![v 0, v 1] := by - simp only [vecCons] +@[simp] +lemma comp_VecNotation₂ (f : α → β) (x y : α) : f ∘ ![x, y] = ![f x, f y] := by + ext x + rcases x with ⟨i, h⟩ + match i with + | 0 => rfl + | 1 => rfl - repeat induction (‹_› : Fin _ → α) using Fin.consCases; simp only [Fin.cons_eq_cons] - - simp [Fin.cons_zero, Fin.cons_one] - apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq --/ +end Matrix diff --git a/FormalTextbookModelTheory/ForMathlib/Order.lean b/FormalTextbookModelTheory/ForMathlib/Order.lean deleted file mode 100644 index cd6e434..0000000 --- a/FormalTextbookModelTheory/ForMathlib/Order.lean +++ /dev/null @@ -1,324 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.ModelTheory.Basic -import Mathlib.ModelTheory.Satisfiability -import Mathlib.ModelTheory.Order -import Mathlib.Order.CountableDenseLinearOrder -import Mathlib.Order.Basic -import FormalTextbookModelTheory.ForMathlib.Matrix -import FormalTextbookModelTheory.ForMathlib.Language - -universe u v w - -open Cardinal -open Matrix -open FirstOrder Language Theory Order Structure - -namespace FirstOrder.Language.Order --{{{ - -section Language.order - -scoped notation "L≤" => Language.order - -instance instIsRelational₂: IsRelational₂ L≤ where - empty_functions := Language.instIsRelational.empty_functions - only_rel₂ := by - intro n hn - simp only [Language.order, Language.mk₂, Sequence₂] - match n with - | 0 => exact instIsEmptyPEmpty - | 1 => exact instIsEmptyEmpty - | 2 => contradiction - | _ + 3 => exact instIsEmptyPEmpty - -end Language.order - -section LE - -#check (@orderStructure) - -#check (@orderLHom) - -#check (@OrderedStructure) -/- -tabiki L≤.Structure yapisi orderStructure ile LE M den infer ediliyor. -orderLHom : L≤ →ᴸ L homomorphismasinin expansion oldugunu soyluyor. --/ - -#check (@orderedStructure_LE) -/- -bu baya trivial bir sey. orderLHom : L≤ →ᴸ L≤ zaten identity. bunun bir expansion oldugunu soyluyor. --/ - -def inst_LE_of_IsOrdered - (L : Language.{u, v}) [IsOrdered L] {M : Type w} [L.Structure M] : LE M where - le := fun x y => (@RelMap L M _ 2 leSymb) ![x, y] - -#check (@inst_LE_of_IsOrdered) -/- -burada da ordered bir languageden LE M turetiyoruz. --/ - -@[simp] -lemma orderStructure_of_LE_of_structure {M : Type w} [inst : L≤.Structure M] - : @orderStructure M (inst_LE_of_IsOrdered L≤) = inst := by - ext r₂ m - simp only [orderStructure, inst_LE_of_IsOrdered] - rw [Vector_eq_VecNotation₂ m, relMap_apply₂] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd] - rw [←eq_iff_iff] - apply congrArg (fun s => RelMap s _) - apply Subsingleton.allEq -/- -bu aslinda onemli. L≤.Structure M --(inst_LE_of_IsOrdered)--> LE M --(orderStructure)--> L≤.Structure M isleminin -bizi ayni noktaya getirdigini soyluyor. --/ - -end LE - -section IsOrdered - -variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] -variable {M : Type w} [instStructure : L.Structure M] - -lemma OrderedStructure_of_IsOrdered - : @OrderedStructure L M instIsOrdered (inst_LE_of_IsOrdered L) instStructure := by - let inst : L≤.Structure M := by exact @orderStructure M (inst_LE_of_IsOrdered L) - simp only [OrderedStructure] - refine { - map_onFunction := by simp only [IsEmpty.forall_iff, implies_true] - map_onRelation := ?map_onRelation - } - intro n - match n with - | 0 | 1 | _ + 3 => - simp only [Language.order, mk₂_Relations, Sequence₂, instIsEmptyPEmpty, IsEmpty.forall_iff] - | 2 => - intro _ x - rw [Vector_eq_VecNotation₂ x] - simp only [inst_LE_of_IsOrdered, orderStructure_of_LE_of_structure, relMap_apply₂] - apply congrArg (fun r => @RelMap L M instStructure 2 r ![x 0, x 1]) - rfl - -section LinearOrder - -lemma linearOrderTheory_subset_dlo : L.linearOrderTheory ⊆ L.dlo := by - simp only [dlo] - exact Set.subset_union_left - -lemma reflexive_in_linearOrderTheory : leSymb.reflexive ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or] - -lemma transitive_in_linearOrderTheory : leSymb.transitive ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true] - -lemma antisymmetric_in_linearOrderTheory : leSymb.antisymmetric ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true, or_true] - -lemma total_in_linearOrderTheory : leSymb.total ∈ L.linearOrderTheory := by - simp only [linearOrderTheory, Set.mem_insert_iff, Set.mem_singleton_iff, true_or, or_true, or_true, or_true] - -lemma realize_reflexive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).reflexive := by - simp only [model_iff] at h - replace h := h leSymb.reflexive reflexive_in_linearOrderTheory - exact h - -lemma realize_transitive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).transitive := by - simp only [model_iff] at h - replace h := h leSymb.transitive transitive_in_linearOrderTheory - exact h - -lemma realize_antisymmetric_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).antisymmetric := by - simp only [model_iff] at h - replace h := h leSymb.antisymmetric antisymmetric_in_linearOrderTheory - exact h - -lemma realize_total_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) - : M ⊨ (leSymb (L := L)).total := by - simp only [model_iff] at h - replace h := h leSymb.total total_in_linearOrderTheory - exact h - -end LinearOrder - -section DLO - -section - -variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] - -lemma reflexive_in_dlo : leSymb.reflexive ∈ L.dlo := - linearOrderTheory_subset_dlo reflexive_in_linearOrderTheory - -lemma transitive_in_dlo : leSymb.transitive ∈ L.dlo := - linearOrderTheory_subset_dlo transitive_in_linearOrderTheory - -lemma antisymmetry_in_dlo : leSymb.antisymmetric ∈ L.dlo := - linearOrderTheory_subset_dlo antisymmetric_in_linearOrderTheory - -lemma total_in_dlo : leSymb.total ∈ L.dlo := - linearOrderTheory_subset_dlo total_in_linearOrderTheory - -lemma denselyOrderedSentence_in_dlo : L.denselyOrderedSentence ∈ L.dlo := by - simp only [dlo, Set.union_insert, Set.union_singleton, Set.mem_insert_iff, true_or, or_true] - -end - -section - -variable {L : Language.{u, v}} [instIsOrdered : IsOrdered L] -variable {M : Type w} [instStructure : L.Structure M] - -lemma realize_reflexive_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ (leSymb (L := L)).reflexive := by - simp only [model_iff] at h - replace h := h leSymb.reflexive reflexive_in_dlo - exact h - -lemma realize_transitive_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ (leSymb (L := L)).transitive := by - simp only [model_iff] at h - replace h := h leSymb.transitive transitive_in_dlo - exact h - -lemma model_linearOrderTheory_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ L.linearOrderTheory := by - simp [model_iff] at * - intro φ hφ - exact h φ (linearOrderTheory_subset_dlo hφ) - -lemma realize_denselyOrderedSentence_of_model_dlo (h : M ⊨ L.dlo) : M ⊨ L.denselyOrderedSentence := by - simp only [model_iff] at h - replace h := h L.denselyOrderedSentence denselyOrderedSentence_in_dlo - exact h - -end - -section - -variable (L : Language.{u, v}) [instIsOrdered : IsOrdered L] -variable {M : Type w} [instStructure : L.Structure M] [instModel : M ⊨ L.dlo] - -def inst_Preorder_of_dlo : Preorder M where - le := (inst_LE_of_IsOrdered L).le - le_refl := by - have := realize_reflexive_of_model_dlo instModel - simp only [Relations.realize_reflexive, Reflexive] at this - exact this - le_trans := by - have := realize_transitive_of_model_dlo instModel - simp only [Relations.realize_transitive, Transitive] at this - exact this - -noncomputable def inst_LinearOrder_of_dlo : LinearOrder M where - toPreorder := inst_Preorder_of_dlo L - le_antisymm := by - have := realize_antisymmetric_of_model_linearOrderTheory - (model_linearOrderTheory_of_model_dlo instModel) - simp only [Relations.realize_antisymmetric, Antisymm] at this - exact this - le_total := by - have := realize_total_of_model_linearOrderTheory - (model_linearOrderTheory_of_model_dlo instModel) - simp only [Relations.realize_total, Total] at this - exact this - decidableLE := Classical.decRel _ - -def inst_DenselyOrdered_of_dlo : @DenselyOrdered M (inst_Preorder_of_dlo L).toLT := by - - have : M ⊨ L.denselyOrderedSentence := realize_denselyOrderedSentence_of_model_dlo instModel - - simp only [Sentence.Realize, denselyOrderedSentence, Formula.Realize, BoundedFormula.realize_all, - BoundedFormula.realize_imp, BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this - - let _ : LT M := (inst_Preorder_of_dlo L).toLT - refine { - dense := ?dense - } - - intro a b h - replace this := this a b - simp only [ - @Term.realize_lt L _ M 2 instIsOrdered instStructure (inst_Preorder_of_dlo L) OrderedStructure_of_IsOrdered] at this - replace this := this h - rcases this with ⟨a₂, ⟨h₁, h₂⟩⟩ - use a₂ - simp only [ - @Term.realize_lt L _ M 3 instIsOrdered instStructure (inst_Preorder_of_dlo L) OrderedStructure_of_IsOrdered, - Function.comp_apply] at h₁ h₂ - exact ⟨h₁, h₂⟩ - -end - -end DLO - -end IsOrdered - -end FirstOrder.Language.Order --}}} - -namespace FirstOrder - -namespace Language - -/- -section - -variable {L : Language.{u, v}} [IsOrdered L] {M : Type w} [L.Structure M] - -theorem realize_sentence_of_mem_of_model_theory - {T : Theory L} (h : M ⊨ T) {p : L.Sentence} (hp : p ∈ T) : M ⊨ p := by - simp only [model_iff] at h - exact h p hp - -theorem model_theory_of_subset_of_model_theory {T T' : Theory L} (h : T' ⊆ T) (hT : M ⊨ T) : - M ⊨ T' := by - simp only [model_iff] at * - intro φ hφ - exact hT φ (h hφ) - -theorem realize_reflexive_of_model_linearOrderTheory (h : M ⊨ L.linearOrderTheory) : - M ⊨ (leSymb (L := L)).reflexive := - realize_sentence_of_mem_of_model_theory h reflexive_in_linearOrderTheory - -end --/ - -/- -section -- {{{ - -variable {M : Type w} [inst₁ : L≤.Structure M] - -theorem realize_reflexive_iff : M ⊨ (leSymb (L := L≤)).reflexive ↔ ∀ a : M, a ≤ a := by - simp only [Relations.realize_reflexive, Reflexive] - constructor <;> {intro; assumption} - -theorem realize_transitive_iff - : M ⊨ (leSymb (L := L≤)).transitive ↔ ∀ (a b c : M), a ≤ b → b ≤ c → a ≤ c := by - simp only [Relations.realize_transitive, Transitive] - constructor <;> {intro; assumption} - -instance [inst : M ⊨ L≤.dlo] : Preorder M where - le := (· ≤ ·) - le_refl := by - apply realize_reflexive_iff.1 - apply realize_sentence_of_mem_of_model_theory inst - apply reflexive_in_dlo - le_trans := by - apply realize_transitive_iff.1 - apply realize_sentence_of_mem_of_model_theory inst - apply transitive_in_dlo - -instance [inst : M ⊨ L≤.dlo] : DenselyOrdered M := by - apply realize_denselyOrdered_iff.mp - #check @realize_sentence_of_mem L≤ M inst₁ L≤.dlo inst L≤.denselyOrderedSentence - apply @realize_sentence_of_mem L≤ M inst₁ L≤.dlo inst L≤.denselyOrderedSentence - sorry - -#check realize_denselyOrdered_iff -#check realize_sentence_of_mem - -end -- }}} --/ - -end Language - -end FirstOrder diff --git a/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean b/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean deleted file mode 100644 index 7d4dfff..0000000 --- a/FormalTextbookModelTheory/ForMathlib2/Cardinal.lean +++ /dev/null @@ -1,7 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic - -namespace Cardinal - -instance countable_of_mk_eq_aleph0 {α : Type w} (h : #α = ℵ₀) : Countable α := by - apply mk_le_aleph0_iff.mp - rw [h] diff --git a/FormalTextbookModelTheory/ForMathlib2/DLO.lean b/FormalTextbookModelTheory/ForMathlib2/DLO.lean deleted file mode 100644 index e4a228b..0000000 --- a/FormalTextbookModelTheory/ForMathlib2/DLO.lean +++ /dev/null @@ -1,218 +0,0 @@ -import Mathlib.SetTheory.Cardinal.Basic -import Mathlib.ModelTheory.Basic -import Mathlib.ModelTheory.Syntax -import Mathlib.ModelTheory.Semantics -import Mathlib.ModelTheory.Satisfiability -import Mathlib.ModelTheory.Bundled -import Mathlib.ModelTheory.Order -import Mathlib.Order.CountableDenseLinearOrder - -import FormalTextbookModelTheory.ForMathlib2.Matrix -import FormalTextbookModelTheory.ForMathlib2.Cardinal - -open Cardinal -open FirstOrder Language Structure Theory Order -open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂) - -namespace FirstOrder.Language.Order --region - -section - -variable {M : Type w} [instStructure : Language.order.Structure M] - -instance instLE : LE M where - le := fun x y => instStructure.RelMap leSymb ![x, y] - -@[simp] -lemma orderStructure_of_LE : @orderStructure M instLE = instStructure := by - ext1 - · funext _ r - exfalso - exact IsEmpty.elim (by infer_instance) r - · funext n r x - match n with - | 0 | 1 | _ + 3 => - exfalso - simp only [Language.order, mk₂_Relations, Sequence₂] at r - exact IsEmpty.elim (by infer_instance) r - | 2 => - rw [Vector_eq_VecNotation₂ x, (by apply Subsingleton.allEq : r = leSymb)] - simp only [orderStructure, LE.le, Structure.relMap_apply₂] - -instance : @OrderedStructure Language.order M _ instLE instStructure := by - simp only [OrderedStructure, orderLHom_order, orderStructure_of_LE] - exact @LHom.id_isExpansionOn Language.order M instStructure - -end - -section - -variable {M : Type w} [Language.order.Structure M] -variable {N : Type w} [Language.order.Structure N] - -def toLEmbedding (φ : M ↪o N) : M ↪[Language.order] N where - toEmbedding := φ.toEmbedding - map_fun' := by - intro n f - exfalso - exact IsEmpty.elim (by infer_instance) f - map_rel' := by - intro n r x - match n with - | 0 | 1 | _ + 3 => - exfalso - simp [Language.order, Sequence₂] at r - exact IsEmpty.elim (by infer_instance) r - | 2 => - rw [Vector_eq_VecNotation₂ x, comp_VecNotation₂ φ.toFun, - (by apply Subsingleton.allEq : r = leSymb), relMap_leSymb, relMap_leSymb] - exact φ.map_rel_iff - -def toLIso (φ : M ≃o N) : M ≃[Language.order] N where - toEquiv := φ.toEquiv - map_fun' := (toLEmbedding (φ.toOrderEmbedding)).map_fun' - map_rel' := (toLEmbedding (φ.toOrderEmbedding)).map_rel' - -end - -namespace DLO --region - -section - -variable (M : Type w) [Language.order.Structure M] -variable [M ⊨ Language.order.dlo] - -protected lemma realize_reflexive : M ⊨ (leSymb (L := Language.order)).reflexive := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; left; rfl - -protected lemma realize_transitive : M ⊨ (leSymb (L := Language.order)).transitive := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; right; left; rfl - -protected lemma realize_antisymmetric : M ⊨ (leSymb (L := Language.order)).antisymmetric := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; left; rfl - -protected lemma realize_total : M ⊨ (leSymb (L := Language.order)).total := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - left; right; right; right; rfl - -protected lemma realize_denselyOrderedSentence : M ⊨ Language.order.denselyOrderedSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; right; right; rfl - -protected lemma realize_noBotOrderSentence : M ⊨ Language.order.noBotOrderSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; right; left; rfl - -protected lemma realize_noTopOrderSentence : M ⊨ Language.order.noTopOrderSentence := by - apply realize_sentence_of_mem Language.order.dlo - unfold dlo linearOrderTheory - right; left; rfl - -end - -section - -variable {M : Type w} [instStructure : Language.order.Structure M] -variable [instModel : M ⊨ Language.order.dlo] - -instance instPreorder : Preorder M where - le := (@instLE M instStructure).le - le_refl := by - have := DLO.realize_reflexive M - simp only [Relations.realize_reflexive] at this - exact this - le_trans := by - have := DLO.realize_transitive M - simp only [Relations.realize_transitive] at this - exact this - -@[simp] -lemma toLE_of_Preorder - : (@instPreorder M instStructure instModel).toLE = @instLE M instStructure := rfl - -noncomputable instance instLinearOrder : LinearOrder M where - -- le := (@instLE M instStructure).le - -- le_refl := by - -- have := DLO.realize_reflexive M - -- simp only [Relations.realize_reflexive] at this - -- exact this - -- le_trans := by - -- have := DLO.realize_transitive M - -- simp only [Relations.realize_transitive] at this - -- exact this - toPreorder := @instPreorder M instStructure instModel - le_antisymm := by - have := DLO.realize_antisymmetric M - simp only [Relations.realize_antisymmetric] at this - exact this - le_total := by - have := DLO.realize_total M - simp only [Relations.realize_total] at this - exact this - decidableLE := by apply Classical.decRel - -@[simp] -lemma toLE_of_LinearOrder - : (@instLinearOrder M instStructure instModel).toLE = @instLE M instStructure := rfl - -instance : @NoMinOrder M instLinearOrder.toLT where - exists_lt := by - have := DLO.realize_noBotOrderSentence M - simp only [noBotOrderSentence] at this - intro a - replace this := this a - simp at this - rcases this with ⟨b, h⟩ - use b - exact h - -instance : @NoMaxOrder M instLinearOrder.toLT where - exists_gt := by - have := DLO.realize_noTopOrderSentence M - simp only [noTopOrderSentence] at this - intro a - replace this := this a - simp at this - rcases this with ⟨b, h⟩ - use b - exact h - -instance instDenselyOrdered : DenselyOrdered M where - dense := by - have := DLO.realize_denselyOrderedSentence M - simp only [denselyOrderedSentence] at this - intro a₁ a₂ h - replace this := this a₁ a₂ - simp only [BoundedFormula.realize_imp, Term.realize_lt, Term.realize_var, - BoundedFormula.realize_ex, BoundedFormula.realize_inf] at this - replace this := this h - rcases this with ⟨a, h₁, h₂⟩ - use a - exact ⟨h₁, h₂⟩ - -end - -/-- -This is my docstring --/ -theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by - unfold Categorical - rintro ⟨M⟩ ⟨N⟩ hM hN - simp only at * - apply Nonempty.map toLIso - have := countable_of_mk_eq_aleph0 hM - have := countable_of_mk_eq_aleph0 hN - apply iso_of_countable_dense - -end DLO --end - -end FirstOrder.Language.Order --end diff --git a/FormalTextbookModelTheory/ForMathlib2/Matrix.lean b/FormalTextbookModelTheory/ForMathlib2/Matrix.lean deleted file mode 100644 index 817b50e..0000000 --- a/FormalTextbookModelTheory/ForMathlib2/Matrix.lean +++ /dev/null @@ -1,25 +0,0 @@ -import Mathlib.Data.Fin.VecNotation -import Mathlib.Logic.Equiv.Fin - -namespace Matrix - -variable {α β: Type*} - -lemma Vector_eq_VecNotation₂ (v : Fin 2 → α) : v = ![v 0, v 1] := by - simp only [vecCons] - induction (‹_› : Fin _ → α) using Fin.consCases - simp only [Fin.cons_eq_cons] - induction (‹_› : Fin _ → α) using Fin.consCases - simp only [Fin.cons_eq_cons] - simp only [Fin.cons_zero, Fin.cons_one, true_and] - apply (by infer_instance : Subsingleton (Fin 0 → α)).allEq - -@[simp] -lemma comp_VecNotation₂ (f : α → β) (x y : α) : f ∘ ![x, y] = ![f x, f y] := by - ext x - rcases x with ⟨i, h⟩ - match i with - | 0 => rfl - | 1 => rfl - -end Matrix diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 5a7a444..baedaa7 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,30 +1,16 @@ Matrix.Vector_eq_VecNotation₂ -FirstOrder.Language.Order.linearOrderTheory_subset_dlo -FirstOrder.Language.Order.reflexive_in_linearOrderTheory -FirstOrder.Language.Order.transitive_in_linearOrderTheory -FirstOrder.Language.Order.antisymmetric_in_linearOrderTheory -FirstOrder.Language.Order.total_in_linearOrderTheory -FirstOrder.Language.Order.realize_reflexive_of_model_linearOrderTheory -FirstOrder.Language.Order.realize_transitive_of_model_linearOrderTheory -FirstOrder.Language.Order.realize_antisymmetric_of_model_linearOrderTheory -FirstOrder.Language.Order.realize_total_of_model_linearOrderTheory -FirstOrder.Language.Order.reflexive_in_dlo -FirstOrder.Language.Order.transitive_in_dlo -FirstOrder.Language.Order.antisymmetric_in_dlo -FirstOrder.Language.Order.total_in_dlo -FirstOrder.Language.Order.realize_reflexive_of_model_dlo -FirstOrder.Language.Order.realize_transitive_of_model_dlo -FirstOrder.Language.Order.realize_antisymmetric_of_model_dlo -FirstOrder.Language.Order.realize_total_of_model_dlo -FirstOrder.Language.Order.model_linearOrderTheory_of_model_dlo -FirstOrder.Language.Order.inst_LE_of_IsOrdered -FirstOrder.Language.Order.inst_Preorder_of_dlo -FirstOrder.Language.Order.inst_LinearOrder_of_dlo -FirstOrder.Language.IsRelational₂ -FirstOrder.Language.Order.instIsRelational₂ -FirstOrder.Language.Structure.funMap_eq_funMap_of_relational -FirstOrder.Language.Structure.structure_eq_structure_of_relational_iff -FirstOrder.Language.Structure.RelMap_eq_RelMap_of_relational₂ -FirstOrder.Language.Structure.structure_eq_of_structure_of_relational₂_iff -FirstOrder.Language.Order.orderStructure_of_LE_of_structure -FirstOrder.Language.Order.aleph0_categorical_of_dlo \ No newline at end of file +Matrix.comp_VecNotation₂ +FirstOrder.Language.Order.DLO.realize_reflexive +FirstOrder.Language.Order.DLO.realize_transitive +FirstOrder.Language.Order.DLO.realize_antisymmetric +FirstOrder.Language.Order.DLO.realize_total +FirstOrder.Language.Order.DLO.realize_denselyOrderedSentence +FirstOrder.Language.Order.DLO.realize_noBotOrderSentence +FirstOrder.Language.Order.DLO.realize_noTopOrderSentence +FirstOrder.Language.Order.instLE +FirstOrder.Language.Order.orderStructure_of_LE +FirstOrder.Language.Order.DLO.instPreorder +FirstOrder.Language.Order.DLO.instLinearOrder +FirstOrder.Language.Order.toLEmbedding +FirstOrder.Language.Order.toLIso +FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo \ No newline at end of file diff --git a/blueprint/print/print.aux b/blueprint/print/print.aux index 6e454d2..4aa5171 100644 --- a/blueprint/print/print.aux +++ b/blueprint/print/print.aux @@ -7,40 +7,29 @@ \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} \@writefile{toc}{\contentsline {section}{\numberline {1.1}Vectors}{1}{section.1.1}\protected@file@percent } -\newlabel{lem:two-vector-notation}{{1.1.1}{1}{}{theorem.1.1.1}{}} +\newlabel{lem:vector-notation}{{1.1.1}{1}{}{theorem.1.1.1}{}} +\newlabel{lem:vector-notation-under-composition}{{1.1.2}{1}{}{theorem.1.1.2}{}} \@writefile{toc}{\contentsline {section}{\numberline {1.2}Theories}{1}{section.1.2}\protected@file@percent } -\newlabel{lem:linear-order-theory-in-dlo}{{1.2.1}{1}{}{theorem.1.2.1}{}} -\newlabel{lem:reflexive-in-linear-order-theory}{{1.2.2}{1}{}{theorem.1.2.2}{}} -\newlabel{lem:transitive-in-linear-order-theory}{{1.2.3}{1}{}{theorem.1.2.3}{}} -\newlabel{lem:antisymmetric-in-linear-order-theory}{{1.2.4}{1}{}{theorem.1.2.4}{}} -\newlabel{lem:total-in-linear-order-theory}{{1.2.5}{1}{}{theorem.1.2.5}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-reflexive}{{1.2.6}{1}{}{theorem.1.2.6}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-transitive}{{1.2.7}{1}{}{theorem.1.2.7}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-antisymmetric}{{1.2.8}{1}{}{theorem.1.2.8}{}} -\newlabel{lem:models-of-linearOrderTheory-realize-total}{{1.2.9}{2}{}{theorem.1.2.9}{}} -\newlabel{lem:reflexive-in-dlo}{{1.2.10}{2}{}{theorem.1.2.10}{}} -\newlabel{lem:transitive-in-dlo}{{1.2.11}{2}{}{theorem.1.2.11}{}} -\newlabel{lem:antisymmetric-in-dlo}{{1.2.12}{2}{}{theorem.1.2.12}{}} -\newlabel{lem:total-in-dlo}{{1.2.13}{2}{}{theorem.1.2.13}{}} -\newlabel{lem:models-of-dlo-realize-reflexivity}{{1.2.14}{2}{}{theorem.1.2.14}{}} -\newlabel{lem:models-of-dlo-realize-transitivity}{{1.2.15}{2}{}{theorem.1.2.15}{}} -\newlabel{lem:models-of-dlo-realize-antisymmetric}{{1.2.16}{2}{}{theorem.1.2.16}{}} -\newlabel{lem:models-of-dlo-realize-total}{{1.2.17}{2}{}{theorem.1.2.17}{}} -\newlabel{lem:models-of-dlo-models-of-linear-order-theory}{{1.2.18}{2}{}{theorem.1.2.18}{}} -\@writefile{toc}{\contentsline {section}{\numberline {1.3}Instances}{2}{section.1.3}\protected@file@percent } -\newlabel{def:le-instance-ordered-language}{{1.3.1}{2}{}{theorem.1.3.1}{}} -\newlabel{def:preorder-instance-models-of-dlo}{{1.3.2}{2}{}{theorem.1.3.2}{}} -\newlabel{def:linear-order-instance-models-of-dlo}{{1.3.3}{2}{}{theorem.1.3.3}{}} -\newlabel{def:binary-relational-language}{{1.3.4}{2}{}{theorem.1.3.4}{}} -\newlabel{lem:canonical-ordered-language-binary-relational}{{1.3.5}{2}{}{theorem.1.3.5}{}} -\@writefile{toc}{\contentsline {section}{\numberline {1.4}Structures}{3}{section.1.4}\protected@file@percent } -\newlabel{lem:structure-funmap-relational-language}{{1.4.1}{3}{}{theorem.1.4.1}{}} -\newlabel{lem:equality-of-structures-relational-language}{{1.4.2}{3}{}{theorem.1.4.2}{}} -\newlabel{lem:structure-relmap-binary-relational-language}{{1.4.3}{3}{}{theorem.1.4.3}{}} -\newlabel{lem:equality-of-structures-binary-relational-language}{{1.4.4}{3}{}{theorem.1.4.4}{}} -\newlabel{lem:orders-coincide-for-ordered-structures}{{1.4.5}{3}{}{theorem.1.4.5}{}} -\@writefile{toc}{\contentsline {chapter}{\numberline {2}Main Results}{4}{chapter.2}\protected@file@percent } +\newlabel{lem:realize-reflexivity}{{1.2.1}{1}{}{theorem.1.2.1}{}} +\newlabel{lem:realize-transitivity}{{1.2.2}{1}{}{theorem.1.2.2}{}} +\newlabel{lem:realize-antisymmetric}{{1.2.3}{1}{}{theorem.1.2.3}{}} +\newlabel{lem:realize-total}{{1.2.4}{1}{}{theorem.1.2.4}{}} +\newlabel{lem:realize-densely-ordered}{{1.2.5}{1}{}{theorem.1.2.5}{}} +\newlabel{lem:realize-no-min}{{1.2.6}{1}{}{theorem.1.2.6}{}} +\newlabel{lem:realize-no-max}{{1.2.7}{1}{}{theorem.1.2.7}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {2}Model Theory and The Rest of Mathlib}{2}{chapter.2}\protected@file@percent } \@writefile{lof}{\addvspace {10\p@ }} \@writefile{lot}{\addvspace {10\p@ }} -\newlabel{thm:dlo-aleph0-categorical}{{2.0.1}{4}{}{theorem.2.0.1}{}} -\gdef \@abspage@last{5} +\@writefile{toc}{\contentsline {section}{\numberline {2.1}Instances}{2}{section.2.1}\protected@file@percent } +\newlabel{def:le-instance-language-order}{{2.1.1}{2}{}{theorem.2.1.1}{}} +\newlabel{lem:order-structure-of-le}{{2.1.2}{2}{}{theorem.2.1.2}{}} +\newlabel{def:preorder-dlo}{{2.1.3}{2}{}{theorem.2.1.3}{}} +\newlabel{def:linearorder-dlo}{{2.1.4}{2}{}{theorem.2.1.4}{}} +\@writefile{toc}{\contentsline {section}{\numberline {2.2}Homomorphisms}{2}{section.2.2}\protected@file@percent } +\newlabel{lem:to-embedding}{{2.2.1}{2}{}{theorem.2.2.1}{}} +\newlabel{lem:to-isomorphism}{{2.2.2}{2}{}{theorem.2.2.2}{}} +\@writefile{toc}{\contentsline {chapter}{\numberline {3}Main Result}{3}{chapter.3}\protected@file@percent } +\@writefile{lof}{\addvspace {10\p@ }} +\@writefile{lot}{\addvspace {10\p@ }} +\newlabel{thm:dlo-aleph0-categorical}{{3.0.1}{3}{}{theorem.3.0.1}{}} +\gdef \@abspage@last{4} diff --git a/blueprint/print/print.fdb_latexmk b/blueprint/print/print.fdb_latexmk index ac84b00..372ed95 100644 --- a/blueprint/print/print.fdb_latexmk +++ b/blueprint/print/print.fdb_latexmk @@ -1,7 +1,7 @@ # Fdb version 4 -["pdflatex"] 1722842215.45552 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1722842216.35635 0 - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1722842216.13454 3389 9986f5bb805a7d456894f1ab84f2a2a4 "pdflatex" - "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1722842216.13454 684 cd11907768ebb096d11426bf84b99804 "pdflatex" +["pdflatex"] 1723661794.7511 "print.tex" "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.pdf" "print" 1723661795.69292 0 + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux" 1723661795.4694 2232 b6b67c3fcb3329da2c254c2d8baad30a "pdflatex" + "/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.out" 1723661795.4694 935 0e20a0f58d1d7838ffc59f27f356d900 "pdflatex" "/usr/local/texlive/2024/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 "" "/usr/local/texlive/2024/texmf-dist/fonts/tfm/adobe/zapfding/pzdr.tfm" 1136768653 1528 f853c4d1b4e0550255e02831fdc8496f "" "/usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" @@ -83,9 +83,10 @@ "/usr/local/texlive/2024/texmf-dist/web2c/texmf.cnf" 1719785820 42007 0b741a3c21a5ca32b40e3846e75b3548 "" "/usr/local/texlive/2024/texmf-var/web2c/xetex/xelatex.fmt" 1722380463 10868501 e521c25442cce99c56ff9a77d153050d "" "/usr/local/texlive/2024/texmf.cnf" 1722380410.43027 455 5b996dcaa0eb4ef14a83b026bc0a008c "" - "chapters/basics.tex" 1722842210.89455 9444 d7c98278eb22bd3c0fd530b347cabe4f "" - "chapters/main.tex" 1722838314.15515 270 abcdeb6fca3851372d9a5ff1023c4753 "" - "content.tex" 1722838307.94514 917 7d022bbdd7c27336a23d62a729ff0c4b "" + "chapters/basics.tex" 1723659066.66334 2441 b48c6cf0620ad41684aeac4b58dc95e7 "" + "chapters/main.tex" 1723661787.37893 321 18d95ad5a64d5d1a73dc8caacf660dd9 "" + "chapters/model_theory.tex" 1723659684.69707 2076 ed78731b4190e4a400ab523aaea36373 "" + "content.tex" 1723660673.45768 1004 792b81f5308bf1a333bd495ff2e0fd5a "" "macros/common.tex" 1722759673.52174 604 ca3e9443483cfefd693019fb112f2d18 "" "macros/print.tex" 1722422546.45932 1101 87627b2ec24fef68edc71c13f43f7bab "" "print.tex" 1722837065.5925 1131 bf5d368546e76888c21bf562766212eb "" diff --git a/blueprint/print/print.fls b/blueprint/print/print.fls index d7313d4..d5e0134 100644 --- a/blueprint/print/print.fls +++ b/blueprint/print/print.fls @@ -192,6 +192,9 @@ INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5 INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm INPUT /usr/local/texlive/2024/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm +INPUT ./chapters/model_theory.tex +INPUT ./chapters/model_theory.tex +INPUT chapters/model_theory.tex INPUT ./chapters/main.tex INPUT ./chapters/main.tex INPUT chapters/main.tex diff --git a/blueprint/print/print.log b/blueprint/print/print.log index 6524026..197a8f2 100644 --- a/blueprint/print/print.log +++ b/blueprint/print/print.log @@ -1,4 +1,4 @@ -This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 5 AUG 2024 10:16 +This is XeTeX, Version 3.141592653-2.6-0.999996 (TeX Live 2024) (preloaded format=xelatex 2024.7.31) 14 AUG 2024 21:56 entering extended mode restricted \write18 enabled. %&-line parsing enabled. @@ -683,36 +683,21 @@ LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be (Font) scaled to size 6.99925pt on input line 9. LaTeX Font Info: Font shape `TU/latinmodern-math.otf(3)/m/n' will be (Font) scaled to size 4.99947pt on input line 9. - - -LaTeX Warning: Reference `lem:reflexive-in-linearOrderTheory' on page 1 undefin -ed on input line 78. - - -LaTeX Warning: Reference `lem:transitive-in-linearOrderTheory' on page 1 undefi -ned on input line 89. - - -LaTeX Warning: Reference `lem:antisymmetric-in-linearOrderTheory' on page 1 und -efined on input line 100. - - -LaTeX Warning: Reference `lem:total-in-linearOrderTheory' on page 1 undefined o -n input line 111. - - +) [1 ] +Chapter 2. +(./chapters/model_theory.tex) -[2]) +[2 -[3] -Chapter 2. +] +Chapter 3. (./chapters/main.tex)) -[4 +[3 ] (/home/metinersin/projects/FormalTextbookModelTheory/blueprint/print/print.aux) @@ -720,20 +705,17 @@ Chapter 2. LaTeX2e <2024-06-01> patch level 2 L3 programming layer <2024-05-27> *********** - -LaTeX Warning: There were undefined references. - Package rerunfilecheck Info: File `print.out' has not changed. -(rerunfilecheck) Checksum: CD11907768EBB096D11426BF84B99804;684. +(rerunfilecheck) Checksum: 0E20A0F58D1D7838FFC59F27F356D900;935. ) Here is how much of TeX's memory you used: - 16803 strings out of 474240 - 310097 string characters out of 5742353 - 1932557 words of memory out of 5000000 - 39281 multiletter control sequences out of 15000+600000 + 16792 strings out of 474240 + 309351 string characters out of 5742353 + 1929557 words of memory out of 5000000 + 39267 multiletter control sequences out of 15000+600000 563440 words of font info for 85 fonts, out of 8000000 for 9000 1348 hyphenation exceptions out of 8191 - 90i,6n,116p,542b,467s stack positions out of 10000i,1000n,20000p,200000b,200000s + 90i,6n,116p,542b,463s stack positions out of 10000i,1000n,20000p,200000b,200000s Output written on /home/metinersin/projects/FormalTextbookModelTheory/blueprint -/print/print.pdf (5 pages). +/print/print.pdf (4 pages). diff --git a/blueprint/print/print.out b/blueprint/print/print.out index 465edbd..348243c 100644 --- a/blueprint/print/print.out +++ b/blueprint/print/print.out @@ -1,6 +1,7 @@ \BOOKMARK [0][-]{chapter.1}{\376\377\000B\000a\000s\000i\000c\000\040\000D\000e\000f\000i\000n\000i\000t\000i\000o\000n\000s\000\040\000a\000n\000d\000\040\000L\000e\000m\000m\000a\000s}{}% 1 \BOOKMARK [1][-]{section.1.1}{\376\377\000V\000e\000c\000t\000o\000r\000s}{chapter.1}% 2 \BOOKMARK [1][-]{section.1.2}{\376\377\000T\000h\000e\000o\000r\000i\000e\000s}{chapter.1}% 3 -\BOOKMARK [1][-]{section.1.3}{\376\377\000I\000n\000s\000t\000a\000n\000c\000e\000s}{chapter.1}% 4 -\BOOKMARK [1][-]{section.1.4}{\376\377\000S\000t\000r\000u\000c\000t\000u\000r\000e\000s}{chapter.1}% 5 -\BOOKMARK [0][-]{chapter.2}{\376\377\000M\000a\000i\000n\000\040\000R\000e\000s\000u\000l\000t\000s}{}% 6 +\BOOKMARK [0][-]{chapter.2}{\376\377\000M\000o\000d\000e\000l\000\040\000T\000h\000e\000o\000r\000y\000\040\000a\000n\000d\000\040\000T\000h\000e\000\040\000R\000e\000s\000t\000\040\000o\000f\000\040\000M\000a\000t\000h\000l\000i\000b}{}% 4 +\BOOKMARK [1][-]{section.2.1}{\376\377\000I\000n\000s\000t\000a\000n\000c\000e\000s}{chapter.2}% 5 +\BOOKMARK [1][-]{section.2.2}{\376\377\000H\000o\000m\000o\000m\000o\000r\000p\000h\000i\000s\000m\000s}{chapter.2}% 6 +\BOOKMARK [0][-]{chapter.3}{\376\377\000M\000a\000i\000n\000\040\000R\000e\000s\000u\000l\000t}{}% 7 diff --git a/blueprint/print/print.pdf b/blueprint/print/print.pdf index b9f8e315e32f17faaa89cca98ecc101b397db55b..df19e0930bddfe9c38bdcda56c8123d33d99bea1 100644 GIT binary patch delta 26191 zcmZtsV~{4n7A=5I+qP}nwr$%sziHdHZQHhOO!u^Hy*c;&c=x<}qW)w=Wo1O}m22;{ zS7qfb(DX4-JUf7epC8)A)!EF*4%%}wB)-R5gb6m}g+D~UKh~diBh)!e5c{wCEjssd z2dPR}?~n2uH&p=qfiZle>t_zlD-iHw93hKoRf8%g;A3QA?y2G$=W-X4Qi5D=o?cM7 zs021ZjYK)5HCG>L3B$OR3^Gw85h(=`u4f79>{9!)UICDzrIYiNE_317$ipU=wurnw zI^<8pKkBEMI`@1X0UBkalrr>MqeQb(BqDrqB+RWbc z|GViVCLjg?D?97|9fd0`zPKZH#H$CIM~Lb82Qg&LcF1^8Nsn=Np~xpMKe^g=YJh-9 zLb9Ze?iS1*n-(p4V_3GAgJkc5WNxpVedGHnIYLsJrEoSsKyB#e{pZi&`_#kZg9C2> z8*%^AgO&5HV6fFGF7{37>5+lL>L4Jh#j|nMuQhc-JK`Ph(fWnwv6=<*86fbJ5R`C7 z)RBv7EFnE$6a&H)`Zwi~0Dgr)-$fL#oM3`4M|n0$zXf`JiAtiiuS$2^B!G7h5YOQH zde>cYHH`<|WCh9=x_}Xow=|kHFUwb#bKaEjog6rbmm(83*7>I*XJ-Y20h-g|b#+m$sOr+T$N>ttyV@ECW%;m?{}6#8$HBq4+k&yl3pS zSHxg7);Q;|eReJ##;RO2&VI4k6>;}*H``lq82Mz!iVi3PPyjO_Z6jaVm>8)wDt}nK zySy)V{Du0>i%&;^A!=fxDJOyf2IQI}!=%^#7c{(=tW}fSc&!DaIs$OKH;@145BE|o zuKi|g`AE_$?uo9C_sLwd#4iOeKrw1hWlzgrJ3J+V=ECzqEI5tWilrrSVyz%;B)`=N z;ow3%S<`iUJV8BK)9h78JufoHl6NId4EtVu7M%^$MEgw6bIm{ligTog3VEvT1WdOl zSgDNgJTsL{Zjn+}1ZcnbgNccr2wiT|SZsAHPhKYsiWYSk z`9QK)bBBFwqgn>jwukXKd5ze+I%CZ&u6Mo7Tbtn)8Gs)1rX28EesMx9PHwgORk3iAy49L+eo*ZsJ*R8Fyl{MTu2(kvR8aVKC5vv5qeFmK{<`^e zXEY<5-)FNj_YT=8+9?qMq{et)Bu#suP39f4sP0-$i$@Wa(->*>w~$i5%IiW|)`Y2c z8eL`VvQjfSf#|Sn#M$ISZNwS;f#~0nJ2%kjdI#0tngI|HV_%WQjDNl(PI+C zq&t=;|Z5sb9DEY!FL z`?srr>S=YAsmn^i^$4ikUF7gK9bl+7XiyGA{neayL`W&0?o)@I24a95;jkX40P;BQ zhg?9sF3NbcTaq9mJas(F~4finqA4qmR9L_7PXrog$jL*~cFvLMc?(hclKY|q( zhI}DSkVZd6K)wi#!kb1RypkEM+r=@BrMj-}s1%L}a~LcCgDEbzk?N8nCS23VGSfwB z<;N4wub84^L8I@8&fZLZgLnmjF9^g42JobBFfITi(|;xPKN>u7s7$ceZ)k5I7|2^* zQe`ypzap-O-NOSrdP)u=t6o1i=cLRno}HpZ1JsLFI9mnAZjkDPVMYY#a3L*%9));& z7!Ozk1meC0E{8u9#D6EQ1|oF@&C3h_aw=n!E*r7`xzeY4EkMOjUR03A0w_;{`$K$d zAb9+Rby+_<__&r)7him%^fnCVF-BoU=NtBpHpjwC!EZ#qmy4KVOt5xUtxIltVhvp4 zpTv96h@@I%=Pyvw!ss+5)B&|kc*zk{a_U?l!X83^0U>{m>pCZvL!J=6A!gJ*H;g3b zVM3I_VGq4iRjq9r*~q*G2dK0(2EyJs5|0}Wz-z*nL>A-5omTf>H3?JyQpJ_<>FpdF zsQdjka_ieC8N+23){7)PghphAl-$ z>qz`j@qa|ALNFq;eEYJU=cQ;ZA)D4D^_1&I_IT8$@0#4y4b}+ zREc_pp6G?jg;|RSXeSO$7U3qJ2P^Z2?RKK7NVIKgv#xf_U?H7^Cj0DceRAkv(n+Q3 zsjI+W;Zf4S1+V*X0sL#~f)`mh&P&)Q!%;4Z-t#SMoiR3iwHzonqPPF@2{SDj-ppTK z>*m`?8-xt+$Gp-(R>S67xG~^K`BbE!^bKp=agK9V5aks$DuH&$fe9qBi(!tKCzC5n zN)S)~8h}e>TQuC*7?e27u-u;6+4^p;^@(dYd(U)wea5@j1vp$&);Mp*>z_@)nHl(; zZ2vixt=U|}RqvrI`|vt2n8m;@r$e&gAaK)L>059v^=#*g#;k=s`uzb2zC)ks@n~D) zfR)!C9C;s&venzW?U)U{69^optwNbdCGsEPmf*hq%|gKrl;nQAQCYRxmhXk4S$KOt zy47AYp&ajRm&)3VCuQA7<5|G)v~bLQDRQIsguMpshXc)RILl zJ3i5k8O!xZv#(WOES3E9WgdF0EuK-@##)u^F*=2r16V!f^#-8K1Cy=d zCHCcCGq0UDX31|-OASH5=DhyKB4w~Lp{Vcd)M?tc!_?xZJyqowQ1c*U6RzO-s5_sf zOx`^2Q}a;MGw>LY9=r-+&(&cSK|@H_0%NVseSEh=&|(Xel=K9{31DUA_`gM7j7nGRHY4oi1KMYRnW!`>nPG$2Z&JZd zk!>)lZX3@3h`c_6b0eME9iV~1`AFQ^XbI--Uja=70nC=u>CC*jHMc9d26d|nD88S> z{qQEH0ajqj$J35P_vN5V_ebZrbF*(NT;7}%10CshbFH0#t&u8B;@P&mr8aSNMHMVP zxkKb>;I~YN(hC^u!La^JkNCbf`gE@#{vW+?AjJ>pXH7DQ;Ys4GBw zmhSyZr5kKXM~!m)nOq0&xY-EiUq7xQj2`t!rDW>jpQ zvt(M~8(Uid*+Ay!tZCQghG(SuHXap6thcpIo@VA!X`@w|7gX4(T!$>aZ%WjM7YZC! zgF-r~=5Mwfh&c#qWA!{}>OvW7A>;6`K(I7!M_FD>L8ISTv%I?w!aC3$CCU%I1Y8(l zB(=q_1QOkQlnmp~*mA0$NcD;&c4IH-XE6D5Qu_!dpsgC_+<$Y!kSS0R`VM$_bHq_2 zbabv_H-caOI&(|k#HNR%aK$_>Rw02nt|m3~uwwIonGxJM&R-@39+*gu^V=H?eLCPO z5PSnO_`eMh?c-&>YN3cMPN;EKF=k2*`wh{bn$utJclNQ&z4V#U#Y1f**f! z3O`N31DWeY&oTp5GqSFPR|D}oZ1F``WlYRvQ_gst=A1`MNzt(}vFjP1QocS;WUJb`p2qx=@&`M~3OP12REgrlfq+ zBoBg-fQyG6-OZYVzUg&G?dby{#HDF!UkSTxb|UL2X~hPW=ISd&Bx;GC0%+B1)Rgi+ z!D3|AH_avGAkZ(ez-63*A?0|~&eF!HyJQ30OG(>khHuI`&|54w)5mk&I2qZkcr~sru{4D&uHIJ3%=nm;&~HEA zJb46ErOm}X*moKHtiB=i*I{AcviG`nY;LV?sNyF0aNr(v2H=We?!|TEHB4PD<>zl{ z7;r?)KrjTUS8$$77BRMN-P$r_iErCb^^ViM-bJ7iV5K&Mo>o1a<-GU~k5``Xrk`od zEq^u98z=+=C0-8RJ)Ea7nfT?ajG+3&FxzI@wQ{e4NppJBwEeQiD>fNVT=?5qNivxP z3`==@qKybz5^!c2g<2b-n~G_5m8?^UXEqU0F8mnKOk^h6Bg(Igi>O3fI!j!Mq0$q6 z9wINrWpYmIp7SR8!6CD)o-Xmn+&Ij5Bmqz{1J=-x$c)1PP*synIJ$wI=WT$O;7ylOjrPA}1}@ zEZ9&FV`Zd^efzo1l0`v7?`417PrE%_SyycewHt_QfWZ}7soDK4y(uMjDwV0i6+m>; zfs=jKaWlJVf9t&zn2ZhX`qcltOm*n`67ndy586;R09u_V z!YSXX6pvzc3wA^>`Lkt+e`uz3!O|mdkylE-R2k*T^(Tan>e>%b61z;uOEG23MbMok%4YISz$ea7Bnx0b_F~G$3~R$iIf3Oub_vx5b0NQ#br$eUm9%su zJ`hN}HSc!r-8#E3OYyU}b>lGCCF)vp=PKi~CPL%W=v(_rHro>@P@V+)ACM(6nUVuo z+5Q`(8T)@k3BKVCiL0m#2S}0zCkvJedP6KO=ky zR%xL>>ei`U8>AlD<8l`F?wNstNjF63f$EvQA~x|#=!$?^Rxol0xJV@y5IdwPAuh`@ zDp#R@y^t>_j8i9s*|B9LpW-hwSZE<6NG~E^aYsCyO~JFE{b`Ar_3b$ztUM%pHnvq) zNBcWo%(;$zkCM``#ib$%L;o7}d6$0gjXACN4-j^^s{fVn+5f|sq$dVK01Fq>e}kZ4 zGbo5Sa`T4j(~LS{;6W$ZFCHRTGh&I*GcscdVve%vdAr52!QuH=7`SgIgQLk|Z0=so z{#^gnpmhc8=}s@!``}$34$XWN`1xmmuouV$6My zy#y-A3b32DrmYYcCPyhIW&uioj~5ZnWq=l^qabHLTcb(KOZ54b?{{$}BAcq_Q<&!D zU_sN^(h)wvM6)gLbkj-0X6lXPX?1=q>{_-JX|Go?k$NJ$ON^;bjhmh z<+|Eef;TkuLc|N1$mo{Lm6%TnE=DLiiP`Lo3NXuun?;sz0?iB{rIw5z#6q#5My#5~ zBLkwY7OZ{)&kR!J(<%g(Xe38@PqvY0LTm;)@NfE+%&9C}j_8EXisqZ}S9Sm+Viwgm zVLWRfqCn4MG*}iw$PRQmN#U55+)`5rro3nW?W5vTJ zj0VX$=_=GEyJ&OX<+ZC7=U-ZdIH8)t`X7|x_)n4km)ZXRNTX*n$cP$x^FiZ$hB-uT zRVhsMC?b@em30j<{QMW1g|0#W^(HNQX~l>z;FOQROKP@RGtFk{(YCY2t|cfJ4@X6( zy;(yCh^N1T2?(RwzS5tNx2own(5hi!CyPI*>U;gf>-n?tW7KvNyL#g<;QQkbiu@XZ zok8z24So}LtZGxATmNwXg|kQ3qoaP7$y6e#q3!u(ri_DwZQ{xmP;U3Lz24er_WE(v zdO>5C`wl|(z#}c}BI=eCvlbUjn!JW#3ztxQuzd-wR!0iB;d$6=bS3=QxsJ{>I{j7- zub4LCOayZwn39w#;T>5bfHuK2pxBu>vH}?o*5j@(OQI;-1Uqe+3b&DJwg{rEF`Nn^ zXEKEtIk(V}|5;KvM1HD6)ePxRG3^cXyM}H|WMX-E7c#=+Wi4ghH1UsiAj9n{?fq;> zJd;xF@ZFVjgJ>j4aXRI&CK2-`@ygH39pKMD714ZdUGw3TEs;$|_Hz{z;AGm>`k>Yh z075JoXZ#;XasES!48YFyU&M;vu?}KH9lP<1blG5vG{|8@95}}v+>FsCAS9Q-D3=QN zKG>QgU5vt$-1q36+haIyME3>%k&xNkhvmbNJtD=BL*mA5za50cEPIfDE+bLOHP8+3 zOhg)(+v@K0@AcQScP1r8=L%(`t)Rx|8H?^1|zf0OtIU93@NYkVH;$ zAtM3iWc|-805dD=f7SF5bstw0HS9dr8QEaOjZjMS$?5$@T429`@_d+e;*iDEmgcY* zk`gQJe?1d#rn*ihE18^k7W)~@yQHM@rYr%ZUpa4Ovl=Qjaik_ZW!1%Gq^lmmhDL@c0Av>{jMq|-ws&G-&x=6eNMr^Gq z;gXk-NE6sd3P>iT;UVO5=s-76^fi*y*BfmOgKE)lF5-kJyx$#Q2{_}Jr}9b%WF?Sm zAwuIOeZnJ!5doW$Gvj1LO^c8x5P+5o-cN}sSXi;B;WVi>6RjyW(sHvuF91O8gd*rQ za!m45M@H!lus1c7?-o=OodLP4#dA|7$*$-rsB$HuDizu&1T!V*R#wz1DMibsDx0>{ zdMz=`=W5)1C9763VDA!z6_44vd}fR1_mtliDpsn}J=9Umi(1rpX5&gq5m-8l6;Ilm zf@G)H8VlZNXlPpJ51!j;4N4zU#gFCP0;p!C5lpoRlJ)y| zzyorCaXHIiscQfD=W>WSx?J-Di#ghJB(o+iT1D&VfU=N-F&=~?+Seo+P-2f4M#Y4H z>6>`ixb#fP0hU*}fqu<0XBn#;ob+@>Q2VqLNgKIr=*FOE5Q$5I_y&w(c?Kf&kH_u9 z3+SGEyoIPB)hpSHc4+qavbPSb?9c z0p;MX0iZ9`)1gnfYaYHG&*v4pl8};(29vF4$;Y?V$3$mW2^*pD$dLX?=1*sOu0Y`S zL(&^6Ni!NWW3UPHfy;w?kJ;8Z(^gVYmSCIKE+i(aKb^>DC1FkS zne!M3{~r3vAob$<;@$o(c&1OhbLV(-+-QGesh<}VHuVnujI(hcp^YH$FB;&Q-;-*7 z1>g+$yvk7m$AyA|W2#Tj2O(xfzuG#_v|m#4Vp<a!4?2!D z_L(N6T2A!+VfK9B+UFFXJh3yL>lDT{YR6pG)YG&51E4c`$BQ**i0DpP>HqD*Bw$koPV=iPHPrqJ z7fQ|HIMpgAUZZD>Kc1b#Z>g7yr~K=pU8;T<@5FggQ4A8f~@;ihj*MZ1<&m8Fu0(KSK2HU+}j zY90mne#dj=Y4@U$>z1Hec2^H^8}NdOr{Wu59xALl>KJJt!^;WYc~|=axCE6|w-Pp! zx{EzIB8?s*hj7rdaSS}?9@Kss8~_HxV{F6Ya&C{}=qx=UZl4Cx;S20dsy{A9+znxV z`|Hw!78BfA*57j%&$)-Ucb{4~=5g*q=_p~79o$lizkE2;|A(k=h_~OY0f3G}Lmg3s z9m9igYF@!nnk6I;fZwR%Q}?Pgp7ve$UnYG{#%H%i`*7t+bJ*Va@gPz9Q{fIQmQw`1 z?!;1`60b|D4s0t|n~80}b5IE}yUKo7`>iw|yT|8q?H!I6m8ZtYxPf|iC00Zr{%+=R z;Kr%*9m<3!lb@m$u^;6Q40s-RgXPF$=%gJBSC^2o^{h-$+ zD&F^d{j#GpCJuEl=z_Ap>7%MLO*&BN4%p0VE7j3Q)KD!A@XeMH>HOJkr z_5QllfDRwgKN`;FbXthCtNX2OU}57>zg|`2_}iN2uGZsmS?n{Z32_a%rFCMC3>+AYP%3WP%*Y|H&A=)d%w;2qeWk+HuQ zAkY=-Pn@+(uA|H;3TSBO|9<5*p6NIH()ygM%jFx39}{r>zREV9A$kL^ADx!rt>*0D zgqV}L7ZhT$@`sV_E_=n)wev}8U;fsfoAUhO8iHo<;)LT(DSsWYC(bw2bwBK@Il2F7 z!M3ur&z?C<4EcNv=$xXhbbtRl0FsY`Z0DT?TNeAWZ(iwGa&u{117@{vS!l{a-$^jiF(@A)*wdqN0+a zCgR|J|8HpQU*ex2ZvW%+e~S8_1Y}|1`mYs2G@vw5EZ+0tO@PH+v5pcJGK223^=d{8Iw-IaP3Ci+yVeo+ zv~($>(ns;3Nu1J$W{LY`Z&M{m(71&O21}IhNseQhE6EL!c9Tx1WHLA>Z@sTLw@c9! z7DLo*K)E4JnSzneg{H}w*wR*1cu#0x%+~Ychm=(d&AgMz>BjOC>3FOzC)CVv`wmqMb}!hWI_xq!H8ljKbjMVM>+8cw`&o)Y^z} zRN;l(DQeJ$G0eM{{Ev%Rf(b2KZl<7INvV>MDkED~rUai1 zp9EcLZdt1GR5{wRGMhtO-L_~@(N_858TT^#lyRAK zyu@WX6>pPC7-LdCHxKePj$v`ym3Us_MBfJ-zF= zWB3DkslqttNL?O`o;(JH0y&s+-!ejj?ML#ZIUSwt!E9X0_ z^;^YUaOkp}4>w8{a$34PDN8bb17=lDtGG2WV;P&WU+kuliTLqst>Wn?cYy#E)PcSc+%uyH#m z;ZNUB5sWzuz!DfU1o6g>01aZ=mpL8u?kF$TmyPXOw7Jwz{i-W_0*rMwCpgh7b%r(e zznV#v?uqgv-suGtK*@qjXo}|~B3(7{t^bfkm=EXehj1*dROny}Yw`LY;?nLz?R~?K z>T+vbS^rsEm@brnF7(@UyD2#k7s0GEdneKWz=jt6o zyxWwa&3)?jLI(pG^JygcEhkw6jAzF_8+k$mFbm6|Yi$n}iaatg` zg#v~;GzvMMF@8aCNbQSL>ECiW5bMs)D{Q~|1-XIaxj-=653ut+!I%Q2H?9)yW`e|6 zK*h2p_uNVI7LP1Y6x!qH4d@~7y%!#&p9R`0_Yc+m(E(ZT6D{QVW@=o!GY!iCKYtFX znqg}_<<$L&`sn>yCcGk#PcK#?5vwM|RYrUc&U?;?opr?Ig&DZ#@EP z?3!5RJggAS27KZIe@gP1xG}iE%15IP6>new63(`L86onm>Y{ zLD+S5OqfQ;MKR|#H#g@wwmA0=0<3?NYQni`2T`*+P#}$(RSRxolTtV&HDI`(% zh#`0iKYJ~fT$*JTq?lI5m1VpDaxxJj5S|F&gW+d_0ITFVN#0U&0{ooelcIMIE-G)d)_ zESoAm6|zQvD}@%#8wr!;j(84(P`74xCVh}zezMG2@bytKk82R#hzkvd37524+eMXH z8GUm1>gdawvA)8Pc3Glm>{=wEWM-bF+s9Mlyo}@p&Uf*Xlh6wzPA@;7KaEGOxwro$ zpaY~2o+nYB&z<|t4tSdqW2C|XHKnQVs?RBb+t*;!;uzQIk)IJG2ge~q zv}u}L0(r`ZQ=k~a;IpeQ{AE*ZPx-?@$mBDYKGVs$M=!7$fUJAU zAnxsnyV>d0_&k;#Pb{8`TH>vfM=y+P3}fwGkGR$p+`5+ty&RDKR>w?={s@*rrpzj? zY8~(6VS)UP&x<15xJ)W3PsffJ#5k;CP~^qy+?lm%W`=`AN5=N<;AMB9uv-XQCuyi$ zzX}pQ7k+3NJK8PSQ|+gpt&Y78pi$`MQZ~8OUrj77g(vZba&w@xU=S65>CrveqkTDo zI@YmHgT`b|S5)ni>{X5{`oIq_*xdlJ;Em=CZ;5xYRZqJ_E)4fiT$1V;r^H49u+~OE zpU^L#vL6^;xw=453exoy;#_h+r>xN5AP@B#SQ954#gvvv#EW0wV9X*A0N5)-Z&Cux z+8#qq2?hnp=I-#?H77@8U{Ty(NZ^}HUPs3hA?KXRHXe>ilRx&85*!K!y%TTdEiJ$h z{$>0@NO<;rF8gsk{Wb!xZGjkE4;GHCu8^tLdy>6zK^Gki=Rc3L6rDOmH^%rhCt(ch z^PLY*p(-mD7tZqb)PFX40QULF&-l=ClItJT8Q-lLZ5wjWv=W^rb$U4l;rGwy?#cNi zx@FL)mV=`+;{+;JQ&9@`$0LnHaxtCH!{8)i$8^l3eJOW&TH9M^~;*iP8M7AmsLhx3JlO%?d-$lr%u4~8YjoZKB4wukFb246mYD~W#{N; zN^JvFQbH{BxbMjo7iXvJb^7g=Hw`klEZDuJ8KHT*GX)fS3cjw7~ItK@RC5S2%x(VWbi~k`r9%x0?+8A~`-X6WE11uu05@^P^&@>R*OrJEr z&XZm4(yAuT@I+xx>A2GC$OVq1n(w-9-ahX{aVQWR^wVM`11L8<_NhOL*?7^PP6fc_ z@;$dyt`S$Jmc2u#6{*6z;ZP|v)O?)!L9mneUFxsmaY{IxQ?qwk?YPZ7U3;!b$F?2u z>TEii-)bT>0U>2scZ&XpO959_d*s;fn5pw)(zp%0y-!o6*IrNr^bMI2$8wqPJ*PFD z8w^#t&lkMe=$_J5AJ7MVl=T1Gg#mN@GwJ`2F^@#f$f#~Azn!?yzE6V!^NTPSwBrAr&-Ks8 z|3Ah(GvojLC&W)3MioT^J2&1GoGo-L-I|4yMIChczI-vPMUN7CJ+e6vp}GN)3{ey+ z@m9Uqko8y?5p?;Tl7R}1^gbD0GeudaWoI>IwX@}Fp@cyru2yeOz_bdtM^AAt3VNv8IUneVy=~K)x>{P5#JBFRBD<=rTvIhMuJAu7(6~9x+|AW zgi%IWpC|pDAkC!y8^U+ol3>LAk85E3AJ6tlc7|JZJ|aIk-r{>VtW4D=$jO*^r0Zc* zVG+xSJg9i2KKXm)MysBKKc*s~WHX5Z43wm#t_f5u0yK0hmItRH!GLMNq8j}^N#Lu- zBhI2+$H^nBeqO?KAM!8*%%O=~Mzgr?S{EXYKFoLvzbMv z1;iaqw3RvkT5`&)%nj`jdC;z{_Dr;J(Z{%@-fJl#D6p<;;GgebD7zs&~wINwkoR;D+9F#ahk{mWTL6U?W`An3* zL5_ZaLQf^4f}Rjfl2?RR51y~%YB#4(plmNqe4T|GL`~34F5PZWHA94B{ zyl*yE?C)<(oRMI8UC}}8bP)XdgrV<0*tA={)L(Gy-dCT4n&2N1Mf(!|?{@mfglh@) z6x@E}_TwYS>G@pAVeaV3R{+}PMjMyIMFXQ-SRUSQeh3j$ z5jtxwYdkHNM3>TPZq$+ec}0WEke0U7{w2n`n_Z!6sd;NhDy;>zU7fw_UB6-<2O1C* z>RVM4t}=86v=={E{{4$jeBLeRo-m;-*i9wRKzziPA#ONDhRu_g)nZ z_h_I#0)WtluAX|^j=4lvWXEN@+A1lz?aDzWU3Ss1zP(9n!J#nxi^^Mhxsid`pIqzb zo?4a`zG=$LK1Sd-lN2uVm-^fy0ax{A_9sgPiXOAw&Q8+j44S#$6v4ai_{-JD*vNw9 z;Wo}@w|Mc+4HryC@Znu zh%gl*r643I$XS||7b~lkV|h*bzoFd$$=9S2{3OKwvf+U}%K{qiZ*y{*_T%PPwPs}j$2IFTnBdrp0xMo=^>t6UIPi$gr%(XIpgz_o9ko4`G*WX z(k0ZZWc*$pG#xe`mYVkO(*w&<4Ptnb_*PL`kvf(L|8b*ze5GsR5`V;(Dw-ps^RYZC z{>S~GkfVWJxxaUCT0Q1F=+9-_hG79vF#sPD@*I%B!n(s-38%P^x2*O$gj}B0_>VFP zryrpe&cmOhFqrGrz5X6*dLx*N%%>`W+@}}IsI=-G;x9!qMK~2wd%;lf<^hk}rq_;m ztyibZHx7U%B!g}r2tIADav79ZdOvF^65`s&!UsfL!x+NLDgtv)Psk{EEk9h1CZNhs zl52rlHy*PMk6dceN4CG4Q904|kfPX6HYAk!W6Xj)| zki`>WL*9{|Trm8SI(YnGhUUk@Z6x|<&=~;|^juhR3COs*d_G%$qm$ctC=(L~MmiFI zVD1MV)$A0^)WuntlD3eZJ?Nc13UCk2+_yo%uJi(20Zw46mY0n6h@SnLLEjPCjD=k&~Gv$%?e z#!|wp%liXMJ%au%>+YBE%wR4hyKK8{@A$8m7YD&9qde#s0`Cb2H}kas<<@$*7~I9c zH7ujQ;LtB=#Y-eL`)ER|G=P41Dc+Jq&&gp*xqsE`$2)U+K%L53adlZA%;2P|fre92 zf_wHiZjRZkbjcMg#lGO(q#3mND*do&O)}w8N%E%y(4kAu4R8gDVWHq2YR`a*i*}lz zSXq|b)Ix|jy7quVzdvGK(dBm?1nByKJithgvFrj_ z_U7{b8@pX_AK8dI@Qf9QUZ_=+CD{pXj(gHyUx3+H?n7;zix)(}+v#kuxF{p%YsPL& zKv%1+D%-E@XgIfMx-GT@C+gDkT$ZM-w|csF>H530=TfdJ^_h0IPAp8bGl^3u5Ozj> zzCeqmt-99NgKkZK39!9gR5FM7btZxGG&&tzX5R~qoq7Tlj^FVWWFsNC4>rVDq!RBA z(h98!@p|9C2vGt@BqJ@-x}8|E<=(CnHKaro^d(hrp=to=;`#bDenSt*(JVOgDeUa+ zyx&-+kF&nHyt?CfpZwjwD&1Pq(lk4v>%+j!JBf(bp}A?$0MOTJ#!LBQ{Xpd%_KGak z)gkB{Su*<|uhmz4#hca|*H1Ph$CGSK)4J(2arxU>7gBv)2?(r>%#gn&u{h3#O7$JmYrAvAtGlJ+RP_+-GL)~u zfjPJTJ?x@)*hBCB(ed}#P_`RJs-m3Q`1rxx=#_NK1?o8!Gqu1Or4;WGx4OGG##%(( zNivz#(ewM`3Mc}ta@U7K2(ca<_)RJocxkT4+>5oy3LDM?_d?`;%h$Ti3V zWO`>5Bs7PSkJZhnof?G|_btCpzAm3xtF{jWp6u(4-_Os@dLDC9xfaYB7T*@VKVQ2y zUw~Z)O-WJELF0yNfZ3G0lYge=TVs1nV>7Ri`0Jtixsf$~I58z~fh77!me7oa3Jh_0 z9DBpk4-#9DKI#a5bY%Lr1cE^H$+sVHP8cCABZY6byFhe=c7L`LhbSL%@2&ZA(fBkL zBuqxgw2*%QZ}caGa1*g+Q?J)LV6EfPr@J<>bVxPn0(|l`ug%N2f25oi6=G105n2Ki7h7JivB((K^Bc1N8~CLo!o%!pSA#MB!qPX zRi5%rX5&2?z>>Q3SzioSLvkpr$o}BM;kwyw@;?ztXd;%dn8{V+@Y%WyEQcuKeG%XF z;rEt%v~bbyi}Tpid6_yL9pmN4!ui679M~bUt_yT?Kh%F74h6T5fiF*t0bJ)tNapP4 z12t`w4yvhn#{?8R$oZ$g8(XWzQmLD;V}MLsR@@@j;I$f-PpwDrSPK?uK)9kW8cwu^ zGR6&^R#5B)xG0q$d!C&tiWP9H6@g2)AgqV?3h4lDgiH{w9|OP>zuBsf7k%Nkq3enk zGJm0A7=FD$XF>OeY+K{a1FB|Dh(Q{PWZxoxG5oS?p;tV$rl{*zU)G1IhOh1zE^yz5hjLmo<2hN;%q96v+1mCdF=O8$d1+cXiz}^3*yVE2# zAjE(Uud2ssS+8FC^?+&1U9@V;jvVDyzFEyg!z9O6&S$-16En&zNSjNl)TER(JEo4O z{X-x9JK@&p6;o)gfWxumd^uRJowe<4(@4Pq;yAt*-SCNH2KVys&DoelWgE;A>7(t! z$=Pqi9|#g4^lT@zQoxR}3YUR19(P^sr0wc?csrYdTFO383CR(~);BhM*^9vE!jN@mou=(!VwFOZ+w2oBY`hb)-SfNMBMAoNHC>w zbCC_owk}%A>G+fIV2I`!IXC^TAj&Vb$&(%|mK9m;O2#6&n}3F?%YKg|JJJ`OCS+1? zZJuo2-iGjC$Z|?ousx1mY^XGuos~!02As2fuKmS1!9?}PZ>?=X^{PrS>1oSaW~^{4 zK{BBBOrhil^y z{HX@J#^$Nt{5lr3K1_+63WiAfx|@;ro=NicJ50z z&t36(A$o9Rsj`{+n`spQ(^${1wzRT8g)WT;gKywS#uXhPcpshVlYE(aDgnENDwc$EF0KeXD+R=dp*$vY7JoaNUn_sa_wO@ZrmX5w6ctW@+XwC`Q4GMSkx&g znjJW-h>Q_Se}D1gkVqLQ*gaL%oeVkx?ca`4x0k5XayjB zRAwy@%^?4Nc?|0XEQV)RQU9y_HV{p*&m1i+tB6lMEoruztg32RD^ zZlKX6n@TXJpT`)M5omwEJY$CbxFxC{gGP18&gFH#iU^(I)IYr-V0}1hv|~sNkuAY_ z5|hhrMc{adY-Md_K9d(;?&T?Tm&n*}hf!S5`soS&e+v1km^z?sTio5<3l!Il7k77e zceh<&Bm?Ip zs13@2f9^+MNc-lz4^t?7kW3K=17R*O>RVJ6%849xscSmm<=ili#SG({fA$dfSm4T< z;GNId&9nY9W_^`LA$}&qxT42QUn96IaxQz9jl0G4d~|2^tm!*e+VSw`5$#xDNw2w; z{N;Gd6R1_CYzXxUw5JI;4yC+0t?PXN-RD|;jE^w$?E5Do zwh_-wBlWloB5W9zjo9bajEN8izc}Tax6U~2T zS2|1y5&os}ndoTZGS163@>Ado#+6LVFJBwc12wc9>A|sPCdKQ5L`du%M6pBGb>AV)Nas5x^}hf5EMzEeSIhU`E?(zU@=BE zi?c&Hy^PZ;%bbzmcZIh`=Xfic{&#KVc0Yo#^QGWM!+zaM57gs>XOo0&f#%7c!qAmKds+Udr4HCJs3rIvkeW?88QJ;z^D0;u zh@Rd`E#=OSBhS=ei_T>tAnB753QN_{A#U^$#3o*|J10QFoEyYEV2rz~4DYrhmf$KR-5AY(%odmfC47V6F143);$q(aAdc3k!ohzQ749V6=WDEUW6 z(zyWQZ@cJ42^b4S6cP)Rcm_P|*+Qz)$L<0Lz)@<*vCAtS-5FIjpd*EG$y!m`aY6K1 z(=>{C8+3MDy&m(A^L+(gP;(EV+b!8Fq)N$JHbcfi5WBOGjgn*-$P2diFx94%mK>hX zYZ2genCi;pu$R@Xry}>mO~Y4 zoi_&C#ZYK^^dqMh?sbCcZTZyD`HHRUI$Par-S}FJ2dx>ikeV)v0`75xSqVKzxVP@m<>}>0 zS-&pv%1YXi+Dnipl_+1F72s!&E_T&AH}u%Aqf(xhYMBfRLWH$XZYUd*EK_>)@M^^n zAPz^3+slT#igjUXzwo;xBzQs0UQ|=vHu99ANtv`bX6aE^ZpK*;byMh0Z(Vx2SSGn9 zyMArIBpp;ez2DQs@nyt~`rcrfE@6FeC%yj(69t~!nllLKJ(;e#bJ?N0h+-DLT}C+w zPWGVckjeM}@#hs1@&9UQ_CZgH*uN|1R1vbtACxanXY+9^ODi{W_>pd!)opDg4{^Pc zgVc-vn&`sKf5kG3^J=O>F#zKvTAzsF9Y^r{wstqGL5X8Zn4T{tUx4f0i*Cc$5@Iyp z!bN@w<~#tt4n~L0dGII}FEt?BMDxq7ysVrRQElQgNU7N;Vn@gVJtrcs+)+R%dP`4K zmo)Pytly2IZGz)nRI-~lW6N+y;f~YSk9DP2{Kg8Appse9fMqW;6O3z{R7;#nZ*7aD zMoTblnx7|?6BA6!7mKp3rSq|1H|q`!hPfF*8UeTFuD+(c^<57I?BPCw5FKplzU(3F zetFYv(CNo9iU}{_9i3fR(wlX(2(!{}^bDTp=zGGbx{p0xZ<=K_b@BPRKWi7t15c?B z0)Zpvjfs>Ibv0=ATD~z+1QGm8_0+yHF0WI2pAJzsIm6&x6F#=61 z9QEwDV@(OUTQX6GT9pn#q()j}NA3MIev?`nkm1$I>Z8{)y}|SR#%GJRMkPZxk;ppPICYJ71*iOxbN56@Z)tn--Q|KMxba0N)|;b}FStZ$ z(E;H`5A*TGLiWuWtI#<{v>pNr23vr|1o&+tTj+}NJ4W&6e5C<+{c-SVX=$%_St{)n zD5SLC;7rkOv?Ds3{SGtwbz?FDxqRwiv2ANmv?@|9e%nEdXgr#P>m+M*x&qKiwlX;eZV_`^YCCifN)h>_PRNTmQJjfOll%dEKtCDnp`OfBmf9COe~8Q$;RpwE!l^QwMF@J@iRWF)*xEEO>}D$XHd z%09QRBn=J2CJitIl7~q%XGKtq-yPuRe?P^8E%!9iv8h3JiPXiEJuH{O;1*!}J$(@v zM_8A6Ez+|?h`VAum(x|Vm25|U6lnvr2*UfzYqLRJv-Zf%qAcXKKB12rabWxb=0N#DQRK}mhfV$ z_BLr&Hof#ko3(B$;hF7VyXS!>+#>C=6o{b|Vh9+??;U|81qKIrLFElbRVDvAT_=63 zo_)=7YpsX=+nF9%(9fYS*Cyfb=H>MFyIr2UIS@IgLU^BW$b^MbJQkxmsAQp0BFcb> zS*tYEA(7_PBJ#MmWo238Ty`Ic9x?=r<7*Q615QlVh4PrIu2Jo$vZH!LhdOzeu;(Dp z1sx%Z)u*||{gEJh+8dNN(aW*X!MDro&nSTq%>6MFjyw|uGXw%wwtOoVGpWCMyMH8f zyDdBmB`Os(D|zI9MQdbgfVc!a2IP^cEOhOB?cAc(xab@na}qH)W^unv{3?vdi6LuX z`E!6(6BmawQYFbKCRrDSy=ciG2|QO==u}ydDiJhJPD-p(!jCG6>do}5FgqLaTyPIn z>ZXy*Nuo*q5@q&9UxE)w%qW#9{n+B`2OdMTqO4}528VBFq~CEe3Mfj4QWob}22nSO zLy}6b!`8f-UX4~Wx=`)k1}aPf2a8HghNcjwgv0)zT6Z$%mrACfuND@h>hz=!Oi{-1 z79LgyfEGYw=Q&)(PHc>-dGeKfGL2p}TAdT;C&(;QIC6$!CV@R3b38-DgJc+iR?leK zC(|>Y`!Hc0dtDHa4-yLb>(C$FAKA}+Bt9nJG1nByCzCyxamX1fe1t2-Y@R_ld(T1s zJn=XFdB<|bW>eRxqv5Ob2oFo~`ZV}D&{902 zsFanR00lS?4WhJ$=FCvE!hR$sd30^T5lT&u((cmrDT~@;70$^hO`d8bYV3kxDR1S! zz-!uoDb9?mhyPJltth`_gRlnFuw!iFs{=)kA^ObyYL}+#%8Y<_U7?8C3}d}J=)3|> zrjhP3uhWIM)Kdw3;}TM9gTWi%_x%?}Gk0U0<7K3)bvZgD@OgmpdFqiET! z;!JNRzQEB8cH%vFXMH0Gc6T9rt(sjvy3JqLhwv2b>-^vwlhQ#_jeJ7!P=go9R>#HJ@i)sVcq=wORA}Ir(ia9S*f8Scz&;vQ~TDTE>kD`=t%y^UhfqM`3 zxA`_Q1R8qc4^cut%56Jl9vE7t?G9!=1#`%I$5+q%!!YI(l>jvI3V8QlhOXi9WRY+J}C|J3v%6{7JW%Fqbc2Kc$*m)KRpmuDyBJS#VbrbCu$P4@~bD z%OEDr%!>tc=uNS#Vttvyz#Tm(soIoQ1qn1g0j@e`3M+5N{Q3jJ@-N#{U8y#^B2^e6 zI=QK!z;FhE$Phe!Oej?+LvA`o1SLrNnJEwg6s3xu=5u`QklOnk20L#`N7kpr3C{-Y zJT*>#dlgF&GGcsmU~`M6l}^C(V1sXgO)80qwy!8MP*Gn9Ckrq{U`qi0B@0d$Ae!v~ zGDXuUyoEb3?%l1IAvZCD-S53-eg!n_<>0DF7)Qa2#TZev1w6ijMk*Cs5*6l)kZ7~- zXoErbko=ii4O1Rc=9x}gC+$1>_hC}ZB4klIirg0wEb??Dp+i9Q0wjDc-e?7i`gl zI}_!HA8X;uGxXz#{E*Lk&}00G_>BJ#yA;v_vfBXFV9R^SfV5dXs&TlAZ^(-jBVuL^ z)fj)c(28mrhY}e>{VcsY;t2ws3jW^Mdg-E0!~|w32NjJ%qAC?aLXs9+gFdN12X%k+ zTfF!N6Bc;ZX?rBaaY~d6j2A1A&EsArrBb!UAnYMRB_IS<=V+&Scv}+bV8+Az+-p0g zQCP~GpVo;~(F39#t9W!PFA%bCer6Fpe*87u!FN>3=k=r!ZM13Vy249aiL&0Vbm!b7 z8^n*$S*}WISslu^oq`xAYk!g>*5X)f0K`tn}C_A@7g zt?nvxc@%9E^jF>l@EOP={Xwdb3LLmn`YrRzcYCgo@Wcza6ePtG2c}i zm%J9hs-MO|okGv3D=bhglvo~aXkL05k*Y%2r zw^!)}?};+fy#FRn4AKt<6=!{A>GL*JtTYiSc3@GPeB#Q)hA>bb}y&xvD?v?eZvIpIyv#vlm96tr+^qi%zowcZD-TO=ib1Sgek#}v1U5d z$K*+~`9LjsIO>W%sbA~c%{B5DKUx?btL8xrpLELFZXB8$(ImQAIvq7WoCI+&B!2S0 z2vjv~Tep+}ATs+Win&|!-KTR$t146mKgpL(ggn7NU<|Q_PoL?6mXFU*-Fw5) zx@1!N&c*c8IJeCO(a!8FE2N|&VxiwBbCzDhU{uaMC|df#(&2_jv|=E?O74?|b@%9d zMn1WzVz;dSPd^w1=fipRK&xHW(G-l9yd}8(87QvSyrcdUw!3e6PzcV4?^=}z?}D$a z#dAfcrhi86LWS#)ebHPJddrc3YehXOKzMIpu(PUj?&({y9@s^cneSL5cw|{qz@nm# zte)%~qyRY0dd%=BU1Shxl^P?Yyge!Xbu|qL;cF9kaP&`e${#4?Nly{iaKdz;loj(e zMO}1eMOed6ElG7)o5I)$6E=jxJLU^SFrFJwfyu>!h@?C zQ?l=HI)7UVAzA>cjuog)CPvu4-4*$#I%(;2z%{7#?rtj_wX3SvV`N~c*+%R?{)^8> z5Gkbpe}VJ=gb}IycjlCSqT0WZf&Tsx5$k>!T3rGHA_RI1b5oO&V1Fd8$Amx#(K#v` zlrcz%Hzp|H|8?pAc*xn=_;~-f6wOit-2q#Zpl@rlt0NcJJ3i5KyXV##)6@|j%9JPx z6K=#Sv}Ra1uxMWYa|d{ImDLa$#*)4MSd)e-NyS-I6yhqzV_Jw2MTPbWF+s5aVHK5V znHA}JzMs3T&}|n?8^HRqJH@*9^mhE$Xg9(f4g?*35%pPg+j|5!nqYDd}EA&)e#(qV${1%%e-1ieoU4&Uy12g~_hCrrvt zEQ9_o`!TV?4>dqJzyXl6<90?qh7ogKwQbU**Jn3`3}hasm}8g$TT4}8rFaY14-+O0 zGoV%rRX`ntCSLt+4>diPyr{5CgrG?eEH86`l+CKDu#Xx-&}Git3=hOl$oBSh5uHN` zL?21YZ5rl!i1azuAS+Q6D1UsuJa_pV_)u{&C78wpXnUTO4v`j&1z@jZb zo$0gbky3>^GR}!?$(&FtjITkDDG=7(v+16Kox?sG(tf0Og!K6%=Y>xQ9D0_ZR$kza z#9xI|n0!lm)HXW8m6cr@vHW&^LIoKXw`Bc7Jsc-7Jf%cV+tV=a9y^TfVa?%=4a(y{ zSMCQ>RKdt}dSMD?n5w=5UY7I+EFFk?7_p|dppY|5%3})fb7Va7%`qek$`(C|+#|Uu zVHqk_4}?XYdj_wswT()a5N0)G-hRI+HQ2Gpf@*^zlj!QYUp5)5e^436^?RZy7v>bR zr$mh?H{LU)^XqzOTshzWo||881KmAO?3&w-76-iYxYB4wx=CU3$f1{CpLMfF-}vN6 zdj4`OzX?%LwlDB5>ad#vl=Ukm-Ir@+;dZt5iQ@~rt4wD|gqN#Qu1W4oGr1++_g}BE z8hyO>m+DE`|5Z*~D3{xxYC`bAoM#*c0jXNkd_*0<=&&;+!ylfjjG~ZRx*ckRM~-5;8ucH zDD~3taGk=V8PCa z3|5wRwb;n$YpxV414}~#Z!+5N9M0%ZZTD}R=4@n^wfBYuMC{5rCKUz)i`sdw0KKvEhH=e5w&uL=Vs_|Z&_X<1rk z>{(92jQgywQyTjU_EyD1=Q#h|99CffYr1VcG-1ox# z7Kmz9xYV0#4C#ToBHkR15YY226&o}O*(~bocl1v%Im|n>GK3Fu_W-3~BmBg^-X97A zwIpyqlg^?b8wj~FwtkvF5uOcA<8?n1RswBXLxsf$%9tPo>t>)Vd4Fwy1==r=fGs}j zF$glD(PWyM72e7ON;(<#X0pc;@GvThkQvL!5J-ObJwG?l70AmwK3kUZA*p-3@p3Ecr5jM! zxU{wF`9g&&UBSzYhW4>?V~*hOfpa@brzQo&!qfo9vVD+$mEtGfMXS>7^%gw4HrD8| zUD@ao2f1r|MPE2xw;I@~u@4)4mU?TaE!BceDzo7>RNW>D_d6U|x0&x3WPhZc}T;f=LX{M)7 zDBWb2P}2eqhyP{ASQ4j2t}mLIl3i-A-t_$*tS8f2<==&JAOU_{*!K4Ca*td1*384W zcC4QzY2JI2N1EPbCneq2zLt3GrV}>_I@La2!95*yi-(48i*~=6V0KVClqR)^0RJ;S zWf>?n9+iY;w^r{qlW2Q17J{7{tQTzU-4Wb=|7L6XPORoHPtZYj;-?o-G_*6ymbH!K zrrRZrh`rW{=4k&tb27tGCUN}a{Noq(K1x|rX zn9H~K%e~+)zsA?7cg0Ot(>n?7x6#fV&eV(;^V(#L!{J#v_iwev$YQMuwGIlk&I(TJ zfR3-1qxOf-cu2!yMfP8pn|XJjK+4>F&T!83RZ?~MVC)>C9=V>~^rnfw&Bn7ja+iO` z3=!wnj<Zm!%A;t5d=CId|OsBR+uv4&b-QfV40e`=o>l@2klVIdgvK> zf-i*IuhW-$u0x!Mx&~G*y&u=|ezlj`U45K;EZTHyj`dV-3w#Ixe1Dd(wTlTKo%76s zeiw^eUrpYc`oaF*xv|i}WzXeF5zX|^NV~qOT5yTI824Fy(~GwvczXQs`f*oYaTEg0 z4uW|1h%S!d?#NCENW{nF2GMb;Jr!y{NTvMt@wn>%{G4YPduU-3#D&wZVXhvjz8!qk zapzdgnLTs6&SA=#io*!QUkF=kz;mdLWpQy-DiMKjMxspl-5zs_hL6XT$zIJ7R_fC@ zPg!=2V!_T*=7nu0Dnd^t29G~vXXrz?MV}|FlQ39XUyhVVfi$PV~HvWWi|K#H9I{7rTjMj{Ch7 zqBxp_h(@x)87n|KAsR%JO`C<3IBxhe#YM)EjmX6eY#twThl;$v81WU>1BMV))vr|x z;*M$%pe40lEJ_nO-Pn*?`P5P$d3pn~zP4XnV&aPjE|-D_$aXua^%2LEre_dYJcaqn~#6WD@j1t2N#LS3eUErwsf=p#nF1uQE-`a#l0yG18bu?Q~uD$ z!81^UBQG}=xTfQ9@B|-^IM=WnPuKK^FaML>?`%#qm#}8z@G3r6x^LDf{w)Qvl+u13%P@qDLc!)vQQzB(?}d%5&|7w|sjXn0DfNyu z!g$tLI50_>4yR5l)Qs#a&K6E|ZJ60ivWkN^y`3yQFNG*Qi5Oy5=wU#Kir$7jf+Q>A z$Q4B@;JOQGqy|y)k|nh$AtHY+p2#GgwrBtwR6bl&PV*isSD)QHF>F?0I}URSGfwkS z8x}B7q-PO4Vo0!CiQ6a1n2qRwFv1gt^^7LA0S0QPA+*q9_jD$$ca3JJaM*_BKLfgx7!Fxl@*r zzFYk=dLHiKLO2*Dxp1A$J=UQ{xE*Za#oIWnY;4d%uG_lQK99=6sdzB|>A!veZseYv zg+j82a_d3{-wYj0Y-yu%3uk(Og(0eKPEXOge)?}9&RG77!QEIG{QGCfi4mkY1Gb#G zaNBmg>#Nc$)={7GTX-YiYq&d10ppOXX!yEVvg)W=TCvJX=nHaK@o;hQ@&Ewr01hhv zHx~z+6^A(w9}f>ZI}d={((K#+w<5*aiyVrLHzm=F<{yatuW_1rzC%e&6(jI~&_E?| zBnIJXzZU=Lf$A{$EsGvqMBLQ8xuO0Z)*)`rtfnRm-OMrMbZ*}7<&@@>##*9y0YO$m z%Y^X6gt*lNf06+aQ?B{LmKz;+J%pM!P@Oj%nK#6~U4wbUFbozI-w|b?P%0nf;1CoL zDN2IH1`#rkB%T=djUXH|QVhRY6svO}1m|9a2>6rKEiposAVeur1a5F1@<=7{Yet}K zMwo2|B>4}n#|tg|Pj?z)(%m@fhu<n%d?^OU>oZ?~>$K5+9HWLe&2U?da}d Y>gM6&W@&}=?*n*vkiLA8RF*>ef2iSfH~;_u delta 27444 zcmZs?W0Wr24mR4ht<|<|+qP}nZ`-zQyI0%RYTH_ETX&yx?svzx$GAUhRLx5Aq>}k0 zGc|n#Ty+bazz$&K=ZA4|bv84ygYn!5RqV0`V}iSUKz|Q(V{M|_L~7&w4YmNj6^eF8 z=b;w$2|%^-<3dmdBZ1%(XJPh3jkpSoQk=)IE?!JW*QcfbIVfB_WPu`saxU^GAI4xs z*Csvfw_Iv}p*VS*&~?=#9%|CeV97|WWyx@2uE8)?aRZ!em|weCxs+kClut}*Vk#Nf zhFY31=QR00YPg_5L(y3{NhpaZ|4A~gP`df#ywWh!NVwdo>s7txp$}!^IpscfU)`j) zau#eYuJ$9W!@;UX6WO-C$f)Q#k(=V!ey*NLVP~3EiTj#M@8kOfq7KnRfHAW-{eLYs zvrpy#rUfvubN$~a9BU24kx(G@oYK5Q%0^LB3gWyWQAMU~Qum5+#f)9_42Sa_zo@Y4 z!N<&ab33ai>&4dC3sh7=e&PSgJ9{vtND$xw&jF!8U3_##-qU#V?d<$^&G7#mQGg1= z{&MA1V8@c>ys9BXy>#XLx&sTC0|2=~G%x_|06Qk#P-?8*P5C(4K!NMb`MJ4iHCTLPhUZ zw?4^9>;|`SF~eL*g_>++V~|d?1L?2at2`KPeh*?n3PWrgGP`qn_iUnzUsY1q%83Q5 z`9Xm*o`4@-6coE&wb?5^U>fuRltVh$2~HL?*g*0f{gy^6Aqf8>r6SF}< z<1|e(OzZSDU`qEH?9r)f`j9=-!>l(J-LI~I>F(+L%V1o)O$?WS;^H5JF2F|L7{;|X z);%1G|51h1!_`kRaI~rJf2!CxOes)iBU1Y(*BGRF(JK_C>SBnaD>EEyHob4KSDfAy z6{^n?QFnQGyT3H~fpkb{2`}ntL%|8*ob$8;eE!lF{^1OfBi#*0v$Tv1(+br#f1%qq z6XmyS57{)2?45qGhEEQX~C~$2{TPd-eCl+3W3)0QMM}OEM)S7l4(GZT-RhfYUwMeg3YhWj?f)zh!r##kD|MpiZJvG8xQ z9swoyZmh>Wl1`6nzDb^SWm2?Bqf*^6Kr&CGG-qSkcyb^$M@KK8@EHFDk8b^w9qL!` zuU@)#>uE;0D!)) zEP!@y;E^Q*F&~AMX8^m=Y1`fr!v=1)B81hCvr*HCskm0M6Glk$6gQOi>_E#Ti;TCd z+7kq9|MmcbzjkBL;^OQV5DpDO@+=dHq#=E9r#+Y+Jmp@@asQ1NWhRdk^4?Ny=XjvF zzA-3O#c%pG$gP4F-$^&`G5|Uzi}S zCdOY^<3^7gp4<{I-)SM{dvL9Yy;J{aTxH#D%}+uk-)RWhwwqStL=KGZQqr4ts-lB3 zktI-~^;iqRnYrPS8+{ZP8ZLt7SylqJHQM8xP^cXGwZPRVer?ZVgWM zxAQv?ZR=p}7iU8VTLNDZ8a}c)8}LWAvB8(65qBWtzrR3ePc;D;N(Lja)dgx3Mf{U4 zhH8VLU2)8_AhTOxO)J@o_I!4tZ)|DDbl`?1s2k<&c!ys%YLj_46g@iYU|j>S z7e)*l6I+qdB~YVo>ukUClgkEj|D#Wf#(%u*Wbq#_+e#L+xTXX9#8*5r$a3V8s| zMn}!lhCK&lIpbHA0avt4-9w)#mow`_Us zF~oFSCC|At$xcCO;5&2*(7Tmm{LMk>l-Z7En55}nXPCh}53MOh5VBe}dCt6k8t>B9 z|9tedzmsr@x*!0iWjF9XL_XM_X}N)@tH z!zwhfi(xRTGQO1mZJ-mY-F?X=t_A!1L8a~Gucor}IwG_eH(TzSJ8(a}OuN3Og{tL{ zA9-@f1+hFGAC*O!lIhk|;At@zjJd9fzSym+8yAU)(9)-zl}ivF{cvNfqC@6r1TaE2 zJ2nO^*6|Jx)b^~L+P_Y4b()s%ElsBMJziQLMSCncIt@8y*%*+Fdunn=Yq$x>&?VB{ zQlg;0Q7Lyeku8t{$XOLO_X*SM_6SSA9x#E@tl)oFC17M5P2N@H$<&sW8%Zq2oloaHVObPQA0@GknX9?(perVtG+7rSyTD(AA>V=lr@%7 z@~I@AI@x~<@OqFP&i*4juKs%B3KYS@%RZ`+-Yv)H2r}80O>`C5PTEQt}?v zEU0|6!7sx3H1)GTXENbNmEW(hn#|(4;3&*NL>W8`R%rZ!!JA z?x+c0we-sQXi}r6JTjpfXLvoy6Xe!)wVXW2Numa$_Jx9{AiF+2bCc{yi?O|v^+t`& z4$8n=;Y4hh8pf!aY9}NDi#am2L11?<7I;PU&QucW$#ZnbUZmsKC9My_WZrehP78$v zOfgC#_*SuWtlk9zE;=)JCyMTIRrfu-H%4xb&dB>*LRLH)f8A&EiOe#^O2c_l@yqb5 zK;Xk_*Lw0L`q*gCeacVNPf*^iyM82lTkeykUhc8YPb%xR#LT9igO(@jL(q#`ceVjJ z*~v&04Q20ZiM7!vI)z)!$cizRx~yB5qgaBXr1qqvp?SmtFf1KO*PPZiv-DN@TW0hM z3Zcas@k+ByEh(Yo%+b%8yXc@1N`gJbP- z&Y-8K?d%V?r131`4NEvVz)9YEUJ04GQDTm~RBRj(wj~-p>lYF|3Sba8_$2EOiq05V zBl9DY)=W{edJGdqw1bH}{1C!M&~PBKgxJ$IV0+HoVuiGhRX z&DG&;Je3R^#mjuCQcTxqSK46Z0XM9$Hw|EyJkYM(TXg2Z-~9rv8hbhWSIubZU~CP; z!jzndL<-8v%9)%Givv(bBQtCq0hS7I4R^sTS<@S`avo88`6#4)b3-K5#L`w8%Dhty z!z6_ICSin-0e1=fXvXw^eK_5IXY60Sfx%-WQ^z7F6rqQsAQmFQ8Z|gYdc_HnCHlh$ z7E4re;PcF;D{p)r;o9|y@6X;8k!Evogi`(&Ly}ven?3Gtj}t)G+wI);3HytbBXpSM zw0+-lwZKp+=h;3JEmS65s$;#jM0(l$gTR44)2!`+BCcscy>|SwPsV7dCvg_8I3D4#g6d)V@$oM~|Y4NZ0dNHv+7C zX=qD#75gjb9?^@#5~JkrD;i5v34UryyA!Yf8|3Pr_uyn9Lo{Hvf4oQrU}F8hv#{QR zl1(rp640IpKn$Npd|tDfCc@AysG+X7O@L5N9CiCv|V0fD2BJg#YO28oQ#-Kd(A@{nrOrwYq8-!A51-)ZrpG>K6w<3+OKx?Jd@yI_jCGZ4>s)wq+cuqB3q+$P z!QNiv#4=+#4eG5(0^LpPvZ>UKzX}2|#Hm@veY;?Yk1bX0Wr|OE=it|yEz{NhnZ8bz zgW=+dG|Z}lhOfj^t{1UUjG}spR%-*P8ZxOwPyr&D$|FW*&1a+*`R=-*q8d8Lm)uW< zph$Ec5S5dJ73v{%`$*~muG!~GHL@_I0sCfprK`AVxms0Pr95z9z_>xHb^QiOENuTmG->xgh>q=k(cG^wMTzs|5(<~op{{&Y&~4h_C{Qe674bjz@ z(<1FB`}TR9>TT7G!!E~7f3fz^8kxFPQ-g{KU_)Pm$W`NAH&>+=lYLIgTaL{j2=_%J zWPCime>KzK?;?!#qDFmOkgx(4)iR#mT26_o3&@|&$^zfgqPx4{NnAs#e9}k}Os;Kh z!soZvtaY9+JvC?fWx>nT;B|7FQ4}VnE@)f}#80@aqV_pcDL!Bz=t!{&aU4+`^r>W? zAEbXNF8BH1CtoQ~85m)30Wy#C+V`oH!_ZLPTrnX;xsvjUz;k>RMEUip==ey$(~OJY z6JxQ7>}nXuHvD z_{CUDU4fadtr2#8HAIPG(Ydm52dcDOWzhs!PRTti>uTCehllp~Y5n=!>FK>fuv4)X z$f(-{=&>7~kh$;;9;&~DV_7XBSB^tO{-o>5cvEX#1X-Bmfh z^iEA)-qOG^QhZ^*lyDt-N*bB^pp;Hb|UEE;2b0pC_{r%OEK!s|k69=wJ1s zmkemN@XN?5krmNpCUbJGt`;;G36y5+ywqI>-#sU~pEhN_80?kd>pH!DCk<;kz{Pee z^fs1RpFzUWaQ%Pt3Fm+F2^-VDeWDQk&(}Y4;~$0BMLY7d5d>AM-eB7T zDeCjL-Czcm&sK0hJ(I&LIVSVSYIZX*Q$Sf2JhsNli_Qv3K?}KSzUMgXs-d%1T<+Y! z&CDTVqVTeBDlVgAH@|M|;&gSNv@>aQ#hC{G32^T`dl|62MELZ19?6yU(BcVC;>P6w z7EK(?^uVfyFaBm6Ek|en$aM3|Os?tJqwP0o=mu4u-%ml@>o_e*oEjJI4z<$apLFzz zq}_>#8mkf7$ue}@;R}G%Sn%bFYF}y2;+3g%drg0wg|mAUuR`Jl;YqNr*fmTG$k`fB ziJcp^>-eKOdcntTzZ3!3WBtvkI?QK&)1Qy>saGcCUTE9{zM&lzB^Y@fBs!vf)3-wB_s!tw#H+ zSKc5h*fqNU7k94z?8X3A#(xJxvV+YaBhu*Zi^@@{iR4cfXM(T>I*bdhx`3dZf<}W? zERS)MdG_eAgkFlfA zzIx~3L2ntLP6sV8H+ge-{bbU9voRSm(2WJCvMD|t8)8o>Dq~4PjL#Dt)~%Tuvnyz0 zJe99e&qMn5U+RT_CNkIB&i!k)@zKP#KB_x>nUQW^-u?2Gs?8h>)y?YWOw_rkC)eJ) zU`pdcC$yYAT@Vk=!J<7Dv8l8g(sB@?9t$>abAW|&$=LMp)92Fa#3upp@*-82$QB@8S75JvWQ@D`_b zfp8OeXav(hB-4n}fh1F*{xEe#!CpZ~Sx_)a7Az;F6XXb3DmX7L!-=u%UzGu&k*r(U zMi^d|Eo@$uTkQd|P#9{^yY1sevDP=r&57;X+Z0(7*4Q7H_owX*C#-E;Clh`-QLyo}+zeV$sNz3rs z$Ysoo@HC-=?jUm3R7iyGgkpz*^}p5)Hfv<`^fMW)i;aPuYPxf!ywZ0rXZ)7&7q@bQYPh2ua&+%LE(tcPT zgJ+o^aLuC{GX4krf2k{gnd4uzr(WV_)IV7&?8Yyu!&WP5%#AAIk6k;VZCB|z=&-3P zC>yjAgYU<()Y%9E>Fo>^3*ghli8=*upigT?2CpzxS`+WlluI}`S5+S?Fu~UsWxLyA z^dTP8ysk##7V-34dv~Xo!DE{R9iofJeKB}l51^Mjga+0|-<1U~{CISrIy)5MSEvoI zbpre~gVQ|bB>JJ#Aiz!;ZSiO@r< zNgICIt$AID@^e5?S7r6a&}`$LL%%MRP{K8zM=2kX6hXPo!_DgTq!pW+#l5Re&C9A) zt;>2qTBsj=-|{ZdP`E%4#0yC=L4vSehH$^MTNp$*EF2NPmA@gVwpO{ijsLd7Y}3ug z=0dx@(*XXVuW=pfW1 z7(Mr@4P3n`Fs3`@`O1GvZq!#nIbO=N}tpwJct3at&*i*3f9- z!9o2ffa)X~YhFH7m-_%e=kq57FK8$+04Bz7i_biJ~L(v}|GTw1yH5wmo8%EWRC zyNJ9PnVoFON>z$BHM>i>Ze^m%zyMll;#4IZpqAak%d$ef97?GYz3^-cPtNlBP%2CD z#$&){b&LXHOkAQDzwhn|$u2NWTBDLGQ#U&+vljY|zzP68T)o6qxen#AFNxFy1T8+8 zC^k+r&TI;f5;#ogG>$+DKOx$bfLDTK^qLd1g&qOs4gMr1?M19lT|ae-ozM4a_G!Hf zFy6fg(j5>f1o4BB6B0lUjp8k;Ujszm0O4F0WX^c+s17c&;;2A{MN6r3k)d6(Y2l4{ zHjZ>}N;ch}IYce0dR^4aQO`Trfy_Z0o)KHIwn|^!OaAIN-<7}%o`WgS^UQ+BT$2eH zp`BTWTM9vGb=v~M-*Um$u2yc`W#pMKBTpMxU!!Ys}z{BCp? zf76)o>5R1u8dao)ES>?25gqGSoFtr2Z|tE0H^9h7D|W^3aBXXIN1zczesdp-Y$N(y zgS>ZirkJ#6srU9OMbr5@*Enw`Ao#_-Ps%vAlBGX_yyaGQMn2K&D}8S~tizK8SVYJT zXx^Xf3AYW&NKNe^`dZJ(_HYET&p%>$D9kVE1<9DIJwah<6i-h{4jE%02!-9hp9@z& z$e~YiOCUQVlw0hqZXQ|}HSqizc7Bdb*lh&1-D_tM2F}?A{ko94W1Xy<4VQZHWNgYs z=>Bc%dQ$;z&@V!5GQyd`d5-7AC6#SldQNUQM0mF|c}7`)*Kr*r zD_w_;V6?<|-n8B&+G`em4d3Bd$IOyyXGF9HTO68n-#YC!^&>2mIGIn3PXG8v!2j?bhiA6nhxj4jche2N@bhmxC zRdtCI+!lOvU5B?f^ed4AFzk~B`_NzV6(p6a@1cI9j^qhO#pAWGA1FF{HC2up*OM|4 zfMp1FME z-Zuvl$w&?v*o@^PujhdYe=>xIN|??G_8x`6A%A{oYe6f7!Sr5MA&YHV~C zg9Y`=i8azGYHD(BfHU*+#N91Nkvch^tOF%Qql2_e6ih1fSy=EnH%X)29Qz3Q*+v)i zt<+x+z~jbu6ynMYieC0En9S`f%pNW26wYKWy;XH_YhmO#KR+1G9Rq`I_l_Ob_&G^9 zL_8>uz6oR+4vJ1w=d>v;O)3UQO3PB~`Zics(o-T@P>Ws%Af$<~oR+`<4&SvUaDT-< z$^Du2x1(+MBYQ?Q84)v|$bGq*jtHh`Ot*mrF5X|_tbb0sQGHQh`ek-@fLKY2Qbmw@ zFdaX3s+?>EY93L>O$kV`4bXh@;i=In=i|?5lBL`QI(yKDJ*@@{!$)!FfTn;^vU?J} z2+!s@*{Xc?0QPx0tILO%m!!iD7=Khi>Ws$a&4-q&sy{31^S|RyVj%f+w;eMr%hweP zXRYZN9b2-$Gt`(d!DeA-{v6o;Ww28UJqfCX?WuN;_1?zylkExJ^W>Pos}wdmj%NWY zWm^t|=-x4Ra8LNdN`|2-XMp;>C7*M}(cyZQZ;Ls12skgx$3K0>14?{wJoUPSSsb-{ zlVkhan8b+jh2z=cH(cOcO@f-w01$H^tlfoe^obAst*J2pJ^vPsq-UZl{kV3RvXUB5 zOd2CWpyz$F)loKc2c~ncgF0f%l0Fn#$nJoEI3~yOZf_WPO8`fHHt}?+Sp`Q|L0Xf* zFl?#*4$!gjmJi17{#eY9!WyA|6s9E~T=0wt+5g*9$g_H3+pjHxCEG>gQaTy8koNrS zw~eQdi}SEw#J;vQdLaM<8-Kq~5+OCZb52uFf!5RUPe-i?PeODtd_jM;k%4FqImwO$ zPOY^7#{uk_{hnw8;?gV(M9&MnQGjPNF|?Tl9WWnRN@zkDe5vxQf>YhU(>33#Pk%|h zMWHO!R?n)nCt_j;RnVUl_n|Sa8?=@$HM`z3W-2nxMmtYP`0YF1Sdu zF0o^DXhKMf!;tM?76RwzXhs5#0Ic&Km6uW^_^#O~O{Jx7vg}>p<+{2PeuY34HG5!n z7N>bG_eb>G0SeL&%XmsxO(WyH(x->(A8>M4cpAt7*+vv13D zl&)vbY}M)5@$o3Pa{_&tKqq3PJOr_zQF-kV-Lv~i9(ODJf&_$TacRJW@Dd}00BYem z+`IrcR9|vr{X|(D2P*Q2i55u@=3b-N`&3tDbRCQ_;)S4|+YiPVmie|OgMFNaP(}a@HD6KyR6~cKkiMmN(+7-zvsmwd z^o1-yqqw9mi5Td9v~lQ1E>h+v9mV*@$_*p_6lZCojR2+)y+fYbjCni7R0WkvPt2_2l-`ggL~ zJVvpVS_>7`a!wZ0ssN*-e}kEhc$1fnZ51O2BfxQoc9mb!bHG5;&XaD(ST2$SHmtG z@RK4NMK%mgr6nN^%}yFa*+gzI>S-TYID(8yP1DAICMCrf#e5DU1T9%ALQZbGjgpX% z4PaN@N9JWC2tO7_U15922o^h{EvpFVzvm2odRl4ge(&@-7`%C&x z{gonRCaw0M8onL8-FKgHn8+oJrNmmK&?D~WgXDGK*AZvuwjdg=0XjYa#XQ4R*{ZFR z8td+21FI+&i-3}mhgoNm?|7Nm-tWj=T-R7w)yjN2JWHZmd5BhJ+QlO)^l1Z^2Z%nk z8@Lx#)Y|=7#Lcx(xX-Gz@cSmbDe!TTT z4lEjj0qtChJed$;X?z4thI0n*4sk`h^l+-Em_9o(2ss z&*&9j4V4&cT$k(KjS&x=!T9g2k-)ykA$`qPb|mw`X_xr;2Vh41=;pJ*xS%%b@^jbY zOzT8H<)~#`7*7RafTVT`yN($>OG=O|{jygyOTaa{h2&I*_Q${x9PZ@S)c(#udWyH@ z0BhP==3tn__yoIva2t1?><2lWI4j|+qLe3zLk&__xEBd|@_@PUmPqBQ4qPD2N#Py* zCHrwICaQ;v`)k-Ya%iwac!J03mhhA9mz`<#z7#AA=+am^z@bI8ly={7TjAOVL3!vw z0DE+zv~h=6Jz+vMBF64Q)zlDPMQLAMA2Dh`zlKmQ*RLY^>QaQA!U{(sK^pAHV(;RK z>eWcCuM9)pC%SM!R{VkIvm17$wJ`I`uwwH?>6Z=wbY1=~%L%vSrsdZOc`_3}{l;3( zpADyt`B5(zzz@bD=UV`bbqfSHsRgD~RBDZ&VJxN} zXB+K;SVp#fmaG?m{7g8Q$ac7hNO;=*PMN#Z*RZa_RJRyG>hRw zNv@K*S+Wa8wp2RD8Eco{2k>l~QL9BmrFUn;$s9d5KmezRCw1LiM2yOJLC8m_RlZZX zU+`)V^|)7LL~CsQaKuak;qDLTUKy>UP&w?yyAsRh){Sx?1sD?d1)h^}cE+VA`;AWC z*C=Dwb-DkXc^}0)in{E23$Z`uOS&FST&D8XN&FsO*ZuVL5PYIYD$N06L zcX=r{!0v9Y^;VYV=j)rrYUK+kUnad&V8P7M@=}?FBjm*4hhXOFr&Kn{mpgp=_|RDq zRU=Rg*0!I77m^`E0NdxVk+0bZf%f$i+0#i=uS_pO^0!qZ2gu6@DK2%cuFq2kD)9%; zDf^Vu_mMhUhmyn=HF_jRgqBCJGQC#h7KQW+AOiw7>U4#6$T?;7`j5tf1wAH#-6>=> zQ@zFBv2Z%o-4yXF7ip@cllN0{A!e{Pi}pL1a!dakAacEd(&p1Gq;KKC0;OE2k5q}R^|M1#!R3Fbx#G)ONTz&Awfurtg7Tr&*^~RUHz+Qi+sicDcXOTF?1LH&eS0 zYs03^>o!G5t97;a_TvChHSxC#v@+Cgspr;lca{&JlrEMFgrh$&?n0?NyHH$Kj8B#o zf2!h#Gw~?SHYNoHEihk?CoU8NT3f3$c6t-QzKM%TxKY>};vSZdWsMK=ZFC@Ztdi05^5i;oK>5gAfamq%86aCJIFPv#Dyp+8b z{O--^_EifdEAynuj<6uSw4i4D3I*NGF~-pbl16z*+O(>VD}TFC+l^>V z%4gBKh5vx`UiJ(y+{*I7M}{U?sziB~J&ugQz2fT!Y)emA_7Rbri$b+~e}S5Y$z!co zo~7~{wmdfxC26H*q}-waI<UZ{e zU)tJ%A@wczLz!~r>*;R??DyQEd^h@I@!l+N`Olzg{`4k(B0(-W87zJ6ze{v>4cr*w z(*zA-*ja8qZHBR=p4v2Jailu_%H6KW_(BOKCCB$<+ZlJ@aA?m2*!o9Qa+(&Eh)_m_E<|Hru0Vwa79uI zlqk$s59_nb#rVpJXGKfq1`>cn1HsXu7LtR?aOW9Hi^4mf$qIHJI zwOZ$1&AfhsNM@in@G;9t-h@P0R~B>(MT4qIQOk6e27LK|c3fNt6Q`h*($8$k%>xT! zR9pdgbn=IHNI2F{myiW*ZR>hNnn^`9DnyEsn-qy?#I$Xrd^$1(v9Hq2f@f3#_YqLh z7n>@*Wuu6rxji#4>6s1Cwf1;mGS8G&0w-b{lJtaD3bQVG7Va|o(#%Cyo^u=RdRu=V zn954?%sWYI|4HVrU!RW@7rYZ&v%#lRi0El)Xy|G9s_`lQ z0_J-u&jx=pDaQU+^|1V(4m*k>qq?K)R?__I9t|ig5b-xS+W($l`)|*ko&8@^8-D80 zs%RP*wQXnAF>4@Z9j-!Zl~5H%N>VX0AoKx|5y-lVI)$y-Vkr=v>*&aKq4bt$TCDc8 zQKD&S=80&(#pQIHIFl%gM~ml44=q{Eb2Q#FSybq-=Z;L}tK`3`-k&ahUaq@ddKiZA z@E9{?*#V@s{vrN7E^Y`Ib@Fpkvydz9W6afBwF(F77YA$?#$0~1?UI-yrP!{O5cKqF`DwOTr&DxM3XG1}?@OZc zo#p2%XRHvpX)-bk=gM3r-EpvbcpVY2^Ay+}4Iyluq``3ycl(^d@?#^ou@j4*pD|WW zy@2;6&OS}6m;nd9AHv}LFM<37@cn4t!JYhHc=*_tHq)%mjqj@R)hyO1E7-n(__GTR zS?(=H16ve!Y#+$%C~)KE21Q$Zb^_Qj3}a+XG>l*?re7HGWQI14qO`D^l<9;iafxe^ zJQ)a@$j`yF((W#T?*R|ah+a)w=ZqtTs(}5P2o+Z9y1m2O_y{LacBdVt`MdpoaL_ry zV&%^zQ$2?Mp!k8Yb8SdaAz02z4230Swhmu6>Lu)O0q`td_wp+QvpTHnZigzI%-_Sb%`$ z#A=fz84}t$=Kuo-o3-47Q@`Ot9x8_T8_Fs8T`wUhgClBqaQf$nm#3f*GY%q}_Uz+~ zGU$p2fswTnJHnJ9FI-?N?LBo-g6(3`u$t`Os0prp)_b&@V2bY%kIaE>TbHFeMT1o3 z8n#wpO%mDWNgPAVD-lO;O3Vi%LO`oP@@|^mZ@RJJ8p(Lc&j9h_X~ug}Sc|)J=icjz zN{e;q6`U?p08}gp2yX(cG9Nag!$3*g>Bky}kXRv|XJc(ePt|Vi{QxJlF1p3YQ5|$-d6w6J5UZTv+i7=G;GxeW7Z|gOTRQs1hxRt zO$ixzq&0*%(q^108vFd-8-RooAr(X2mYVTl^I@$ef~*XS+i@bW32i0Gfu6d6=bxUpk=L>M%YqSU8J zOlj2GRe2eGJJKsC57EZTzRFW{!G?ewgw1yF3&#UH6c zu&!2x(vBaP@4EH@0ss{-31Xn>gYSGa;as8C^BeuzsR-tk02LjK^YH3{N)<^j7dbgU zKY1BfZ*g%)N3c?F#z)p+@ji>tw=w6Ek~OcX40~3HuoYrtS4#k!~l;M@m!`#>C)hG{62`qUEZk79`!ChPQpf zJ^+>$$fL{MUd7;EF_OJ_erGWOhDiW&Ai=!w(Hb^ce0uW7Q3RxTCQb`o*kS~oKzB}E zJMQXCl?^-I63`lkruTOODq)B*!xM56>*$*WJ&oCYGW)Y#0sn#H$E(nM;smA4nXZp< zfF4JsTC!IfRS`yn%v=}+oVu^v62^NBK#LQZ)Atf|#(21+f;CuBh^`70&nQZq1bL}X z0dO`zb-5JuQRCR&$wM`mQ75~N*0)lE>5}?Qd*_D=2S{?BV+3|GMpT+fFF!)R*Llc{ zc;S6@36u#w8Z>rHjJ7a{DNuy77uDyHW^XzpJ82qpmSDq=mqrKC_xF3b zPBI?LMQ?xgW9^Q%C^ajyDCLqDL}*5i?N%Gezvp>@;psKxC+eitD+N(`Hd_uoVZROT zAep3jJvjM(1W)hxifV<;LEO~s3J7#`B;tyM1>nGN&f&9W5S^BZ-3Q`40|9%gNt{W< zDEf@PbIIjx?W!8q7#+5mk=1LEE&a7?+Zdw5WJ?z(;$VHEYcUaDe{4e{SNv`NTN?D^ zWwXFIQHSYxV(w8l%XYIXbi!)S=efH7IL7grh~S6}x?L{Hu%6Hc)3BO!n=Z)}b_9v~ z7eF=&&=Xotl6=HQIXUSN2t7M;-3KX6d@#ttlN{#RhK|6jD+|S{&t23ecGcURESVTHLpM3*#VDpQU-G< z=FaI#e@?&1J@wAeP-F{GD1aZ`tPAvs2FyH>H}Ln12lF6alcJIev8QuqyJE)jP5SCB zyIj|ui|>iC!oYib>^x=^PtfIt+Cv4RE8zi`yI|1B%J{ zwSmw?oUuZldEW-~QM{yPP7PI~373h@DHt(s_X3Dsq>d@oq=Ue*-yYcQ-B^#o@3>g+ z2f;Th<7UMr?#cE%=wT7n1Y_RBnY|n4J|hX-?JDdnYx$j|n>|FJRdjZhjY@C)QE=+Zo6T2cArWMVQkJO#W0rCh9!KUc#nhaWIxk+s-R~!6rs}&OFYeBN(rs8jh z-O-8&8HP4YrUHpAdQxKd-#Y2cy|_c{b>)Y|)jrPapDLgA7HX@nG+pvcFEsUOs|#Zr z%*BWeAI5J=Dr#R|cbT{F36M3+QlUt&8M?l-Wa3UBfhQT$o9N>gO#Y|UfHZ=O>bBz* z#`UtJOEzjdzo;k8ufjH!`Sf|9qZr;6OTt6+l5Y&Y<|&s5@UZU5j5$MkrLN?7i+PQ& zFPKt4o@?3#`MiZZ9G}hJJ`CLl>S4qwLp3!o@Y(MD2FV-N1P>h2Zs6Af@#xZuir*y_ zEiGp(6ck1lAJ@6)X?kQMFz6WN13$pwB#}k`W2GGbA8$1@Wag}(O#AcaA#ea32yYwg ze}g2tIovvRQfi@4TmL2Ig5bn-LhMMyV}l&Q>Co{HM(m4R2f*VJCctSIZ$90VP( zk7E#mB_V-8hX@Kke@cxDqd?h&G=zw;BP-3X9PqcwV_KZ6+Lh;)=bk<8SXrD1Oz+S3 zP#EfLmb0v8`Xp0qN`0UD?!NTyegOJ*p zzCD9F8XcjWY!CSm6TlO^svVg~4%3E&PK#g=3JBv1eFyxhS+DWh&2cbE;{*i%NMjg~ zqK->zjE#&5v`W!ZrNTHnn{_YW-Pzox((UIyb70o9LH*`uck# z3q)(sP9Dg3HR)tQ`583GlX<(WQ)@UWDbakXRrG<{`d0B&<%yu&si9%)EbKRJVA(}x3^9XaqudjdCcZWO; zqvVui8s6f(3C#;HQtTi>ZQR=#2M+lCk&mbZ{ugA ztcdS0lSA2QsjLU};b@nRhm&a@b^&kylh1nME@Flqiq4ydibn8i4BvkUE~pZsWwAlj z_r+isWO4@$zPBqi`8hxjDdxW>&WkNA|1D*Rl7izsUz5&*e)p;f)=9-MFYpp znonvs@15|%~9=j)KtTJT98qh_& z#=0sH{jqn8poUc=+C`)u^++{HH&V-LhhR^2a5v26pL1?Q7ehKTgjhuiM$HK1&<6d8 zMO$zDFR&iltGkewI6NCJF460k=k&+@FFHFSfpyM39z;g(<{+9Sdp~w;feOA=H)^m` zc6>61mR|yFF$4e`87WANTrCCh`Oh;;!)GOooCk=M?ujyl0ikPyWO?#Ca57~zVoUHVxe8#NbxrxGETS2n>xQr`Y{+~k5DLNBiY1grxiEZ1OaAMoG z?c|GX+Y?NTFScz?Y}-Eb|NG|bb92_Jt6p7K-K$qs_4_^r9sm%c$BQ4OGAFM^3~Zo% zfzJ})^xWsTvOQC!&OLj)P5RYy#&edDtFe`_W-s=qCxe+!g3t;H8gV&ictc&qM+ky# z3dr*yr4O{oEiF(`@}-Xsh1X?m4`|+NQ7*L~m_I%51wX`oe0q3`!ft$GVTzGtBbu3P z5UMF=&`e>#A_Hu+v(CGgkcvLa-kb3!W6DhpS&S(=rk7x_df#_^NzX)4vP?rYlbNvy8D&>;2dlg&@3X2%l6u;CbIwJ2!U(zzBKoJo4{36=)cEr1-}Xc z)0C~j+p))*ld?%i=X>tS=q3cDBqLuimTj82B_$Nd7Xth^7;TWhc#gTQ%jN}1i@PD= zjLH{2kt_B+nv)!9+#U&y)`c|+3Z12V-n#0~4$ zX}-VXd;sPPvO6;Tp$KkQZWfbdndd6F4a{wSH(>&(XwF4Vm3Ddt^n-qoKb2;VXdp1dGRw^&@yQ0OO?TI zjVqMfkpOuvIB&Cr9@vW9>Gvx_UoyWaL#4#EQ!G9Ga)Ir0oO06-LJNq}s6q8T_ONv& zEjvRxw$|4NB3F{byD_QCZzO?n)P)v>wIQ%n76A{*SUgO!Q`H-P#%9w8VVW>#cv{7c zo&l9(j1qb_Y?#!K)W4Oz?9U{nzBLAz-y@=}tZ+XA7Ir{mW3bZ_XI$EMwVSpt1zaFJ zS~60Brh&q0l;%I7pindKg>$=aq{iv(fJm-o}>K)_N(@K{haWJ@6>|!e2K{QS?Ib2 z9+U4nB1W&SJvq7d*f@b_mZ-w17Sz7K7i#B z)tW_T5kzGrg$uaI>3KN_vvC5$t%Dz!kwvDiW8xv^aXq^i-cJ% z)i9jbS>E?AyasOuntqs+g%*(r72Z}5bSq~Wn__GztoSSqejAP|wp8O*0ka{7{j6lK zseCf{%S8UQ$1$gZ{^1Jt?2Xt!3Y07(hF>X=rGL9YIv;0 z{SqFMUG8~VcexnDi}9HS1-v5d)PVNtT~ZOtBNlAhx4ffmDZ7+qpFr~rQ7ZnSJXI)T zyeguc4Ol~na^yV_p5Ci4pa6I+m_V^B-|G9Tg$ zm_nJtbwpXg&6W?lAx5c4rGz9)!8>6q*K%OVUFa~#|L*EqUDb20)A1>1HZ?M0E=FonIRRYAr;xrv_EF>C6!fCzT>6hz->e=#B4TC zd{(|Ilt1dZx!Y=DAvJtOZXFt__$n@STd(S8PAz$Jr%O0oc|Kn(_+Mc7VH%BC7SV0u zomUQKS$y_jvvOO#-=X;ZSD+ogZh1#Lpo&Llra!K7<8KUl0J&l&9{7VzwRd_ZD)QKS zU;ghp3VwD;gk4RKl$}J*yJ*8e3IykcC?X6>)Ul$jiuc>9i`n(EpoGm&T(81!u@z$f zhW%N0)<0ouuFyd@X!{X_Zwx-lVs0)DcHOd#FmICr*hS0&&|#Osq64LUR^I-bdb^v= zah)L5)Vf1~fH{e|@WICeT!dG`({Nc1YLxE(tcf zcBf4#LGz)?pTNpSPT|y7k|lOnnrO0UA!Guv;2F-=SiV1N(rT=ui_bhj~ulX&h@%CiGdDZO&R zj;uyV(7Gi~M}uhltIFgaFf0;1ttqRiYRQc`+{>YgUS?#z+RIbP zVt8wbfEnE$CAk^eo%vX#7RMIRkTH^z(whehd&&;^;J+`mG*C9NSsFGEQ#-Dc6Fel? z z6RRBwrNTF%jTh9NxQ`QDJL|$msPKA{}F7(*B71kDXqR~q#f zEwh#0ZCz}dX*V9)aM6j>8X<(5cQ7a$KzST)kqu^#wK4evocrn}g$7w-+SbWKm61Gjbp)c)soAHqacU=nEKw1QrDJCb%mvapcn*Vu>7Y+`ub7x@ao1TpaAsy ztj?NlAuj8(M2i5afOL{HyK8Rx<{Djm(^!Q0*R(6~K1zA*F_|IF5*oBL8`s4kMM1T{ zd6Pd@o`}QDOH$pK!OUqm-BlLwcNQ8{J-s(#yF2AU9bQ}Cniw*Rcwf1y(YrUR!uRn@ zOry_BTvbi`j^IQo<=3g?Hz&S0z)rq$AkGWu?-eLt!hy~-TO6irSo0?Wl}-#Y{ATfw zi2#=OPpb~;b{%{-xz&nJMQvTiE|Kr*MEJIK01>BiX+LSKSn4lK${+T!eR)|ZUGAkV zm6fTho7_bXZ_^u3j|DS9w^(P>{cS{zG>8~umz4;SrplRB{l8t#B9=uu0Cf=PL?xA{ zJRM7A-jwZv)_`osMZVAHAHTk|z2=4KzZy>PeXqDbYKc+JT3x28m=^Q8{6OvBG6dQl ziE=npT1)7IC226tKk&E9@PBHX*gX=G#rGd8TJ*B13g|H<%J(nYP*n@L8Oub%sT|j? zCxdKN`!T%OpMdu-9kjM^1D@yN14Ljc9pQt1g|zxCE(Ul!FU5Hzu6>b=@qB#D?Hafz z>S;h5ZQzvJpPmVQ*6uEWoKG@%MkzJlIe@C;M&wIAnf=~(j=XlQ^cdWfdFuala@zj1 zGUDiir?`}yiQ5ak4YTxuluym$&?6$6!?bmswm0FiAebZv4OjJu1h^Y`S_l^Pv`D6J zEO!Q|aneLfpr=xtCp)U3meY}SY;f55(`)WkB}mKMHN=g_<)7f3SQEQ*=Bq;AGL4Wd zPg;(o-BdM`=suq?O@oCc!wZ%zXS4!JU>47s{NlY#$|ch?n?ApX+x82W|7r*MhxOdf z{`?5A?gg#lOixAN0r*}%YDUlNNYlHjnxA_7Mu6AKH(IMsfkcBu{pmy2TBwyL-do&Y0n#R7^Ki5 zpnMUX@17Pxx>I!@mUi@QykS7Z*F?LjbKK1Ry^1qG7@?JK9q@L0BwkG^l=kcyNW{cc zsZ5vp!25O@?mCP0V5j{NY^{};^n2gi#d9nMg8-pqEU zde(0)-ZH8Og_->B&+7V*-R>TwZ5WMhNak9k6x61)g%_H)@T0#n%y8G(Y*Oo^qH4r0 zVbp5oudR=DD@)Kt~o4rEhk+){u6z zv_@+mY#0iqX_|V?AKneLSb8scfBSDW|2E*l)T&yh?*JaWhn(LaNnUeh(N4an%diSx z7c>|UhL*#|ul0c3+<#6!J%2EU%KVLtz9IO5sbJA?Lp6#_b&rjIH18aDo%CG_;5P2O zb=_3j5PAtNXbOs zumsIL*vYaswl~^F?Cfv2we||iw~v_dZYT<5V|6YF^tx_X(jt&kl{xTBdG8yeYWoJi zx9>yv-|^Oecn9RH|K)S~9|0>0iUy``>)~(+w1hek6ok?pD!C6E9h`;je{E9$79LKv z|Jw}frjF={K7!G`a1Gipuc;9&4f!eYb)#GKIXLjP22{5YSgxD9Ve7lQHNzlQZBt<2o-t ze{t2d?)CoU<1=$WxQY$4zFdPWtRcdr5sK{1inw2&IA;7vN!{DU|F}p)L1R z-`UWhCq5tzBF`hwBV`{{7_%6|F#Y0sG)vWtLiD15YU~1RT>Z7K`#a8H&a0RH+Bk_X zlRBZTZ{D;ZgIUHTB{$@Xqi0<|&z80jFINUh-(J9+&gee3#`{L`X`eh~#g@uc#C3Ku z<$kU&dU(~vh+fT=4wDmm=zTxQ`-#7-V#|C+Cu1c;qi4A)&S$GBpl1%`{$ne+JQq6b zjCa|jDaQ`@(m_mx>Y7p%;hWTCu;ao#0qSsK&9`AT=1wzh+cB>rxLVWNv0+;lZ|Vd2 z8K$nN7qqI(tbS__rm4Sb4yRGt%1kk=DrRKmr{C{|O);Ha)c&=YRx_?UpP;jAzmAw} ziIdx*BsE8Ej3mFP&hG4M}25u$Y<7ELH)0kXwnxfCuQXCenw9h;#}KMoO^; z%O)WIQlE306SxI)(kx10m--_2)22*TyGc*|Q1k5loRIpu48+Ee|NRHL@^58jr7lKR z;wiy=0-x#%*c6JnsFQVwLDf~uW7ZUB_S%Nc`StbXP^&eB`3Bu?%dbB|#5>S}hHmuC zy&)MWXmYY}>eZ#@(=tV!_AGxflnv_QQdGGC)oFjG&xGaRo5Zt1sdDokBcN>C~;gk<M0K(ZX@m==H{CTc6&g4&Rtj%eg-`j5S0Dw;R~&kqFS;~H0XcvI(!!Z_-d8>hQ07xD~5VQu*j-X>iD zNIyf7cldQJanFTZYQ&I1Ibg7K31&DP!j=*gXt4T0JZuBR)Y6AG?iCO-4o<&TSs0$X zJF&1k%s<KQm)!Y+MR>SqeDFoxb{OR z#hvkOJt>uSlR?4Y*4BR=jZN9!_#3P24v)w7QukJvtufxCUX0uGYNNP8~aTBzuA#p4Tj_wY6dcR|i|6Yk<1a4lwk0JZp9=B3O(Aa(fn5;bB>y3nlU{_mytF5OgBGC_IN_n-nE!sEqI6U~? z^E}MMvRE8YKWe&VPgqyFTN(-eZ-j1MzB~ZrQ(#h0t;>p4jH&V-B@q+ zp(n&NEm3NYfzXy$!6S!&h-Ckcog4kJZyFJox;2~H@-l@&OeDbk*6Nl~Wq4Ni@UztO zav+1ggj4@V0@Y93XeE}P?@q(A3Lh(m_IrX}^9Y+NGPz^dNIp!<+rPjE{`9ywK!2f!tk>9`ma8-4?|U;&#%dZxUu~+rm}D%sd!aCaS~0X@MLFa!m@h3(~Gm)2f7m10r}8Qy=TlZ-ex#Nz>B?e1yc$i5H>Ml&y#@%Crei*x#3^(sZ(Sk9;cDqX=S3M$qr>&L;9N-TGa*0E@FH zBFWeW-%Nd-Bx^DmXqu?aIcUv;jpdEqJyK%Dv{#`*Nm;1oZoEV6BE)cUamk{{6{)`w zMfg$Y|5F6~FD{4qzw9VF3Cg{Ly}i9d%!&npb!eEhn#DpU4lp~(rbW&BKR~n|z&!qw z`#(-;Ucf)c^naBQW+}+F=xX>Q*Uej-0gZdps10!)BScCeZUg`}_B~DBD0JyKbw-yF16i5gMAIf@MKt3F0z`oCkP^&Yvs|+Xq+xCfc-E0i=AI z2ik|pcxw4rtsfkQi3BO@!l4_MfAnu+E}-dt#moGGbY^gjstpRDrKNSGb1o3hHHMat z*MN*|*aJVRiAXw89>PVrS&4v~F!Q4&@tp0C~<7pR4)ltR|ViIxp+}5eF-+jhrnr7 zcu0ldG)96IMNm`GM)LNj+wZZG?UQiB&x!d;93^#(8q6=3Z3@3v0b;{>c}t6ny(!1r z+Rl!E+0tNgvW{K!TFOlvD7{Qy{6MB`}DF? zL82HHQ<(`7?dW{|@I;3E>eKQ%No!#y*EFIJ4Xht4o0-mNZQ_aMHmv8U`w2P1BkUV) zDf7k_*@mJ1d}9m%C04`}!t59CBFk@?a1<}D`w<@(CTCcPkrUa|j%;KY?%dsOR-uHX z40xi>`*y>@Os-%@5+)XE262ky-BJHQyz{}9Mt2*%NB#S7JolQdjvg0b^D6nU72-P9o@b<+45B4QD#(E3}10_ZPyePtoLySVEo_Eg>`}*x@ zOccq#P9!r_*i%f%3}MCZ`0n(6yP2u_Ahz^dRSB7TSO2pUwqp0)mER)f%H&S;vJ33z zz(tT!ETGL7>S2w%^q&5LmjnSY*eZ&5=anBx>jh5OM9>K;I`-qDH*bO(T<&kA_|_Mt zFzLI(tgZrp^#zfg$)@1qY>?oi_lhmO#teCqTfptEbLjqT&!*#X+VlDL&{5z!)Za-b zzWRDX=qv0dX=zF1lhr{o(o`&K$uYW`XC7@WgJ1)U?`7sRa0^l;CI=1h7=^_*?HzJJ zDe$G`t{_@w@W`RY=g;_yya5U6tFMgE{cssWmDLrXGsFM$VI2kk;A;POIkik7*HVkB zgKqxZhB6#DrwNJQvjQ9s3gBw-dM#r5yRQyc)oAPC&pz{V;zwPrjb3^g4+0s z7f-U285aUHBqk&j6gUW+F(}u+^&iQjX4r@g!pC^@688d@(v2I4^pe8_s zLqJx9$Xksfh$)KtRA~#~vZNS5U>$*=n(fa~G!rGLSvY~}WQ3b!5pJ5q9+Um~Y7x<9 zIsr}@#{nySwJJe8FHRtr2-*+}C(p`kvHlKqmJa|Qhd#IrF#XWm06d`t&<7l$oefr5 zHC>+BFwDMK3HYA~+!$!Sj!mtgl?BiYN^y^Up-BZPt?ByAAGL-crE_2i3`(Hnx^#&8 zbw6Ceu|BNm)lIsQc2Gs3oIuoY25&PQA{1VL%FMd7@Ux)z3^`;RP~lR>oE#6tMsoIT6&+tkM)xoxdQYqpV@`NP)fRiROvwk*{%vP6<$hK_NJG>Vll2 zhg6Ps#bG2#5*Q1GV^*ZU7w-iiuPtJTQsdlg8_R&L($?Ws}? zEH%A@YkB$mi8Gzt{7t0V%5=H=BCF}~;$nd72e!7b>j8{&CtL`NJ_(o5k}hrkEjS?Y z?W4Bndr}g)>NIlmJ0!G|a69hY%gK?oi?_2pypfl$^^Lc)vT{wx)a=XLQ>Qw1Pf<8! z8Xv>R&Qk|r;$jD>Zue^_S_En{_GE- z0u^{*KrSBeZYj4g8(7nBTKXuC)ep$Z6C&VU8Tjzw&%&b3nk|mTWyl`Bf~aZ?ezW1o zRci^U&d#~QC-7R&s1S`mUiu+rTD9q(Q>(ycJRrd9Wq#n!bo3{@Xgs!#7FFGR*j7R@ zvmW`^EFP*YY0z}ccAOzAdb5w6`RhL05>%`e*Ie9q;;LAm3ddb9=|-4fz9t}KqUvwh zIa?)BL|r2E=Cy(OvVEIIrkhSKZ{t^Bg1LYxDHElO??lJchG>c%Gv-@Y$E4l;AzN7s zujtWao)%nm$+~&%zv%cEo8xNde9CS!Gml#KD$VRGq0pU`Zr7#T9pjy=cQtHGExd9^ z9uDqZ-NXVXn`i734p**#SV*sqC0NI+z=T{sYG_~LH&J6@qlu2O{`MPOXkq@JcF_q+ z5Z!C9|KcZQ>=vH-)*kyNA#Al|R!3b)GYX6U*Xhi6!M{&*w^3@rUi*xV?Tr+H0r`8- zR-15)ZJtiE>T2AA0y!j^0~xCD)Rjf@aE|hAqp8G@CXVrwKpB9JjL^N6&F)kHQ}yqy zBFK>dDQ!F(XlnJOrUEC#vm4hiWGw@o*=hj50(6X-AIY zv4J3>teyjjmM4ws&+<*D>E?p4xfsroK$;TT?>%V}i1n&&iQ zuR~Vu{fVfIGZfrr`U^6GRj^ike>eKHC5S&Wz!=b1Z2N=SLc5m9VyP}~8c83SsZ!yh zXa9}vJxZui>ye^ZL9qC}(%SvT?&0~x{^9Tm@BLiJxuWgps+QiSs@_B)%+1a5Zif4y zEpVs0ex~&;^xmL>a(2DL+8Mva{r%0HzwfU6{_)1ejV*jL z`yH_E)mL1u5EnPN2X>Qvm)(7w)Dilqygj&>v?RGTVI1hdF+t?6}Yb2HHszYO6a^rm>r1 z&YfVQX(laqYg!>{bn3(D9mBv(c$^`WjtW2+5_{P(wyZW`j?W;BwKLvRcf^u|Kz2$? zAl;I=ERJVoT({Jq_1q62foJ+bORM|0e_x7YTy&Nu_K?l6Y?5Aa$a8nlLDwTDi# zoZ_p|Xf>ly3;S0$!=l2>37QT$085UB)5F8Z%jG-PjDG$<+$R!MKS6hG&9y@qTbBQ= zpT0(mMKaUE3qmX5%=y}L@c!I`OX{J6MX@z!o-R>NtYbp_`85vd=H{kqi))PwE$j}_ z((#h5Z+Ii;m$7L0{Fp>1`^`Tr*$0W`6Ysaq6E{Pe1CQF{XesY!4$~K#?`2Q1yPYda*=sRQ*?xAE|FL!clp&z0pG+Ym&x~o| zVe|u^(Nge(;oHrbgMb9XtE`s9mK`F3Mj$@hnYbs%KO=^v!}y{290~i=`t`FVKHpzJ zrzlaO0<)t6^IHids37c z|L(SSTDPu$uRNS0asc>$-**Nd4Lz7YKqy=JH=RrV8YfDG%fq0l*2L!}s4gH5PzOT~ z`|1=f4^elVgda!_y5)mdP%x5UP_C-@?bYL1@{f3aO_zG)sIwBaZa`P7-}U|Qw15T= zV68rpt6n9VkD8ULre0f$qN*;i#(L18osD`s)jln&tHfxm!2q;`tN+WdPR%Pz*fyYJ zif7vLx~ld&kOK7;Hp>PF6I80ApuPwspi7;V|amFy-JfX5(aL=V0YAGBq}5 z=3(bH<>WLnH)j1e2jTz!?MNPWB!XvWVbaiHA!a3J)%#C}!TMi#QHD7Q`5+^dfL#Y$ z>Y@N*+NU7BKK**Es#QE{O#0PTFL*3_+0G~~=3A8E!D?v7;_qyy`-9ve^5htnqi3#x z)hSBbUNn3Wgt%SFm<8-{$uk)noar41Mq*f+))1Z6F!qf|gwvYdsDoD5$pAH{Retv8Rb+~PL010*&K6ao|oiG`@Fx!C$VN(Fng(9roEYj;NXzoq`aYz9?TmedZ zA#{!+|0Cr3;GNmC}X#s?EAwsDUDk(E~ zBQx}U9mshdrTsZ@kEiA4OY=pa!BZL?^Q-RHYuOhWV`{Os4%!RA@*m4qdmZg#nKxBY z)kdP<+iImvg9H({~ZZB{gq1)!e8dh`FB f;6J#xi>r~dtEaP>IUE}^D=Q})1;sA~ak&2jHfzKu diff --git a/blueprint/print/print.synctex.gz b/blueprint/print/print.synctex.gz index 9c8e33b51aa27b63229597e106a4d15f44917b4a..1371aed044316f937b84b85dd4241060e4602708 100644 GIT binary patch literal 6179 zcmYjUbyU=Cw;j4uYG{z|6h=Uhkd_=u8W9+Jq`QU~T4|IT zxbVIA{qFt!bJlO2wVt*2K4(AYJS_3}fd710?G``X9)jKk&l!7RomgX3i|x^Nl8SUa zA$}G9$6};t!ejvP8GWE)sb2l@$FtijY;o}cHOrEboF1>jVKE&MI*v&02o14q`HptC z(5;)(sZj5jwY8g*jGCK2Cx5QJhTYwLt}=HwN@e6aaCc5N{?y(EHpwx$-?YiMx#Wdz zb>!`yUX^w3$oqcl+-bR9`8m3H6nN(27bLgHNcJ;VN9uZ0r)+n-9K3*PV9ZsV?bg&v+)ZpoQjAsvOWnD*wEd7U57B-|6zabt;4mvC55bEvzBS zQSi}B7dVF6PVRnxk6J3Po=;+q;VtjYH=J@Y7MAF);YK(WHa*a;g_jq>cArx%GVy+l zML$V`pSn-8*Nyl3E}>d_3tN*}%Bx|_H^(?!EU~*;PxM^tuNkv{ZxN*cuuJspFJX}P zfA-2x{u~ASF1Vpuj^lpk{<$pQyEyi~I=qOLuc-dQNJi6L)82BN3Nar$tvS1G0(Fgi z&@o)cHB%NXwYyoiRQw!-Ib%TF&-PNHm+=tJr_e5pz+cbH`lnv| z%07L3lya>hDQwAj)%1YFqW?G!@`4V#MWM;}>NxzjSsO?6n0L+kgPA4~`o4VN7(-Tib{uy8 zWbW<@zRWZArHzR=o9n*~-U}f8O**wyj)DOxe$DqZZric!ZwVW2_RNe=gI+BuAFaOc zW>`PSjoI}(I&pm+cEA*(n;tJkplAQxH%JC96jJb_9_CrB^J}Ta^{;}rp!p+MwJqbx znM+J$BQJ0p#$UFxetLu99sCV~4E=lQsd*+GVB`0z;a!rcdD>vd z8NpPfcp~@XhHmCno-X>_hA1}3LnS#HP6Iow142P=PZmR;NiJQXDa(;Wkeka8!T{^d zrpw`tm6L-T&sNaM(v;X&quYy1zZP_5=k@X2Rp0=<`~2_DsebvB@KvwYOH&3e4Y8Zd~IMBg=h^9&^Q(gWm!9Ytq+$@Kq4$jnW0xs!u*HE{Xjrg;r$o$yCvo zFY+|=WCMwk@&Sus0up9}(#BI0%32yabd;QSzvXlZPvhmgmg4H2Vja-S4Io4eJEcJuKbF6KuE9+M#tm|cW zZx+1?oFZ|}p@F(hfb1m}R^HH22=%Kf@uau7v8FP_M4k4FLKSTss1~iP%>7LVw~toW z;bh_;&)Enrd}7NvXqyiEc~GvX=eja3QHmKr`g7oh{Yk6IHKdztVI;2<$@GTRiR#obuNR0!K6m0g2v+?2p`P;G6;T2Up)+zX2k zLmeb+5*5R%TieE3qUmNJN2gbT^x>hPHRG)la+!GwY@mKaBvkmR={ePhqT^{pI>oWX zWD(2=(OrQGS_}f-GIA~q$Hz@Q;>+vbDW&N>tV-PtFn;=yL`%>AwkarJqpxR^Tb_IF zKamDoAHqCgAT>Jgh?hjxeSbPV`KEMLG7A{?(%x_+5p&d}o}6wJ4=;X!w0Nk5^_2gc zw+H^i_qOfL!lj;q1}T9xB}ZbfOd{WZ&~I(}w$KBg$=JeA_+pJ$h0$Avej?3}&9@7O z?i1m<(xS8eR!rAG^iVN7g=1S$ z$HbS9!^-4FqS*pICjBx4xG`N&%M~WXKX}@!=|pAki4|zdic6r~^3>e0kFDJkWj{&g zy%mq{et>h|(ZVj?iLoT}{B~6HB)usQMZHeTsThYM$yBkZ&e%@qCGZHGsn4BW1>iK# zEX#;B*Qe0TT?uqMCPZF%auF!*R-OMAQI-qqmUA*@b%@jwMqEfD2G@JsR8vkv;`zGm zaQmIhm4_!kxY*9qI~1@_;(jeqFrof{(MZ3`SP8X)bDNd&c;QFn5BjC&Y6L5@PQ8Ky zZDa91fbk=>QAf4Zij0_20`nMTTHA^G8WTwhst<&0Ou_|nn|%~GKK02vi$%Ggt7G8%P;$7BWsEDH@UyCm9t@m;Xm^m$Z&gw^tt#39lm7nDc!aZ1ox86Q2d zBbqR|5RyqfbZTGIg}&;U2(d*?5kPUFprrRPoY)d{r}4Bh z!pJ)7w{D3Kb#czg^Go@3OKnO!hqm-e^+%W(h;Nx@y%mlbWtG{pLQS3+W3KPngO zb4O?3GOTJ~6n~#2-O<#mzQUev*_qwd+Dk8YV@l(D8Uy7r$qp5DYqTqlJCX5Oa4BoX z+L&-gvW&c@RzeFXMl|Xx3q7SBw{<36?(12MQRM4wErhF|kQ z%8waQ&-2E9LE)}%rE+NtqU6u8ni-~TYG4);F(>DhhFW|=84%i9`@R9xGRqgi|i*xKV-12%qsurS}x-AOkeMT6rY1=!3ZiH za}~YW(5)@;YW+6-&L%z1YDMhfhsN3%Jz$(Lb1-1w|Alm{)Jj4C5&=m0C$vS&rLjup zMGqz%F~-mu2D<+J2Ys^!p*_@>?}(RgrTIS2z{g>EP@09Z_F?(b%u(UBMK=6?~-5i2E;SBs@p7Gb1S65Hp*ZBZ8tf$Oo0MF+q<-2OcI}d5iv!!EkPP2@lptWzgo9 z-+g;&ZZWc(Fi#ns|SG2mOX z0g8M1u1wP3JpGX2u+9D)Y78%IXbP3$TgjUpAg=@es`hNTnw0rH*W?_uN<`4KxAlq7HFBD7F$Q;s4>u) zPd})RP#~KBI`6L9#`k4#!XN@(n+6+g9y-#vMm^JMhA7v{dd^@MnBN=u|GDAbDp-{N zwaR_6OB^qob8C4@B-<(P4!zAt?8=s%Hh?MIBmGeJow@w~c^kUUA@INBSM6m<)K0X` z07VZt4+@qDgQk~hiQiw-NJxgY1TK;ghryiMRS-EexBkilti)+Xv*-c=Lc!W4BvHA* zdBNl#GZe)F$O$neXd9}hebweYryeW$7aMmNJPD#j)U_mD9 zv3!{&q>ZQ#{o8lm$}BrrrZHu77qh{AYqon;Xk1bA)e=sQufbUaD+(va+gM6`f7PO3 z{dN5=Cb(}9hheUTXk7?}!+!IljYyf^9fk9zN8zcB3;L0+h|w8sV7;b1z@$J^$N~f4 zs(>$kA<0H7v`e^OMYvq3xe~Hi_>)0r|wW4>lOuA#7Ge z>a^d@5lI9rq=w0QvA-0>G{TVAGA#44Yq0i-o$&5c{@elQe zTbO96fRtGWl86GaUv`No+k;Y~SEG-&EAopa0;N6ZKY_Epc39%5ZgSw&Q|+_JpLsC$ zdGqFNWEQcxiag1;4yfmvRqcaSTG_yh*_Mxb*oYr>n;*v%sG9eLrnvoy{-F8JCTvr~ zQ|6cG3L(rlNS0mh^8@Ck{n$v=xSQXGSWN|EIgfUGd~>U&Zwtd!yYRR^V=E-Cz?DLc z+EGP-)d-~9san)pevsG~3LMNq4m)wwj{*TfM! zL6Sch6xA^}pU>>^3Ok$vSmfp(Z#ucK9s0R92XyRo$V(fNBxR zqjbIB9)AM4GCubESKZCBiHSJl@3rcO4otyNR0x$$H>@Z{;4za`endCS+)(EPj{!Wy z@(g>}05iPH&9Mq_=y6z#4v1u3OZj?Q=>l<*mLt6dP9pIYzH;}jbz|1%$n2j|dh~#5 zhUg>0mlQS3Fv%ljGfVl{>|X{h-|N=t|pV-E5hOv#P$!_QWt{UwR4wo%)3TfPlCi3TF@*-$Wl<(XaZx z6#}mMg2=Ch@QRku3dgO)Y9X0e6MInBOAAuv&S8u-poz-Hj*|yp0GS;fJDq}B)BScM z@|Z&|gH#=Me0+iO`xC2_hcE_8ps@?b9s55#Mbb8jGX zv$F}^d~sqklyKCR7~>9Vr_jE}4f^7-Shd$n?|de|pqXA<=em{2xPk2K`ca-g22~~F zeJ|PO{p><)jf}Pcugtf$A}WdQ0W5|_Ek)g|%h5!1O}|ntf##PNi;*IY{g(?7zhCZF!_j)Rc`Mv6hKa3);R|Tu&QeN2&6p(a44Y`H2ToYMW(C}_4J5w1e~{ya z!Mu5jcq-|0=Jm3iQy=tMDCRnW-4B$)4zg9GWu<*)%cFYzF!4y9Z1DSWdeQkXxE*1( zYD|(wnZEVd>Lr3rQ#FaL(r3xE4VS|hN?94iv}NB#8e}*$!~M>G=*r9?Sn`0s_N$6u zO8F{&zWPd?04|AZTbJp%lvkoZcS1v*qqR4jA~e;OE~UgIf9Mnz>&dr34pSygwN1pn zHYwpb!VB%Fn9U0O4W|{ARJAb$Ssh+|d`o{=`?|1q0Pgp;@BSUIcJQa}?xERHJ0r=y zweO?c0})3kKqqhK;(q1ePrk~}>U+2$O()TEOnDF{&GeN}H&N(*)E~rN@O+OInwS-9 zA%=({ffJ>73z=qr-*<2g2qBu>O}m<T7q#zG0aL^*j2+xi?fWC?3wmA z7R)I_h!Ppra_@^iSW=hCNUtw0`*CiDk|hBFh1MIMq4WqQs9(C1QFZUtyg9GCjdix9 z3TS7IjgdA0n<&mQtG9}=afGWaPE1(pdbpksJq8sF=DQu|VZo)D3}vuX#Cy`4uy2#D zg;JrmL@#zGLCA4CKSfJiPV0C%_1Y(Zibi|XfO-1OAXq=|sa=rm?0BqCDQ(g79kb-O zCU>pAeIU5G*~>AXBt*%qc!~Us*ZSn)HbIQ9Q7F$yzzEsRW^_pO>`ic}tgGd2UhB`9 k{2uve8q4s#0yM_ORZY;CbKY zy}tQ#&)GlDS$o}Ut-bd-GzkENe}2fdK`YLTqVIM-_k5t(N5>dZ`W-yFfQXhI^Oduq zHGy2<23(n_Vh?FggS6(XRD{rc6t@>(NuoYpnu~fJ<(o{A)NWalV0Cvwqt@O_{qR%m z@$c!4_v78UqRHI~Z0r`Ee&-qV_s;iIutffG5y7SB{hymV)0h?5%0;hKuhhE4o&Qzv z&D~w#-Qii*z(BoE%-#acLJ`e69#8#WwerLEg_XmU1=wCn`M_T%?V!%!kbv%B-=1#2 zPtn^kw;Q+%O04O@es?!xS-0(PZhY@u(;w~w&%8ecOLj^07D}y4by+jquq1Y^Jw8Sd znQe*j&{Sy+zoMp#AVV~H%vA{ zRD0J#?s0;F;t#e*oZlmZcKoM?2M%GIn>VNTJ77X_xB7xf;r8JHSk?_Z>m+7-Ics2H zMtn#rPdLTJw5SMr*dNnQlTsAtqxsNP2}f>iZ4QaR*q?_F!;jOJmzIWTTweQ>@7aQ) ziYi(Qf`ZymRt+7jY+}fK$Dm%$D%h1{!vvKb$+SNndvxV;9Xp1NPfR=;@`Ku$X;h1;pr&0CO zg%$~z+BABD)!Nz7OIpoi+C#nW>|%m@LD<^faY!0~SANo-V!HlK&B3w#Ys9P5L#w*r z5|Y2w_ppUWpEFD@LuriwarFMRl$E`wR{cpgSQaH{*pOV4pnkvh`h*he^!(^dTt)WV z)6>sfS&1)?T*cOksBv9bvL^x^gG=B0;3e;65vp{qAFw#QwFQbWcHG|?Nvj)vju|xi zG(dPQcXX79w%EdBYSpC0(6KHJ_Y*5!)C$(D_kJ01Fcp0Dq{m296FORfD| zUjG*_X65t1QR8){|0j>jbmiNX&5KvLenLZQRG8~U$B(!7Ap5CJuWO3d&mJ#Pyq(RL zF2;yX;XJdu6VsrU9NUe-KgXGUSmQrkdZ^axdV5#9Aoml}6{BkjC;~b2RMP9Sh|*J~ zOB0`XRrgJC+pofwmqne#42>n1i}Z0>9F=+7#9zHO9a*X0h_5Xo=Q2I%eRNk|;PJNg z&92E`&z&-RtN{NWgYTXVgmpzXJmC3#{_X2=dxOnUx;H$$$KoJ$m$tj&!z%QUK0n$^ z=bN{aJ^}KPEk+?ij5Qt|KmfjlDFB8&+mmi7q!2pCoV3pVF3nogF}ygozg+?NFRTf zhdka8+awhY4u#C8Jo2H&!^#t+4Oz~Iq_>AQw$b%IkkuDpJ|N$ngI^(XNI8aMZ$@ZL zu(F+_ySXiC!Y0+Wkneol<|ydx&PrNz{L>p567K1vvP>vIcYh_NCbTHJa3T0r!kQxW z(qvq31@iS#88-TPsBdPJ zDo_+9QkWsNtf-G)je0d-m8uYBQb%HNM>^FG?{)S3-e2;hD7II)VJb@Qwza~;KkSAX zw288zdQsIL&lJC?jad(edq~>VhV!mpUbxQ9S0jE#lOsDM7Rzb+k=On$SF>J-9q+zn z#vEus)%s0!kBEuPOWSbV;zZD&L$;&fNO`4!E`~(+wGkyz@@3u;M(g_II~yWMI)(;DWHA#nLU<>l_UVOah0fbj zoTxC_I$I;Jo@J}V8%!8><>uyo#DNjluhMGu7|qUDSHuh;pYI<^q!-LZN*$O)3#Gam zp<hRF?AM*L}Bfs6229AvWKu<(u$$~4+Y$CEe@p})ESvMAo48r=|QTAw^YH~HtPU=)d zUA$rcE_k#&Bp#>_Jx)}db}V$6P{HG1CcP!_zg|S#m(Qo_Q>BX?zFgU7x+RxP^hkS1B-Qtg7g=%P` z5O`CkHv<#2`o*#}6%kP+nBpzuys@?Lz>d%NC}ftgsDs>?%e<*k zpCnKk;Gcv`B-j_dZ$(I*VOCi5GphoTo`I?RWh^R`PEHQ*kb4ffVbyIpni^!{x0%gi zRsb}E%p>>RwDcSzlI5^5f@Jtg{NF&^5p_~~&@)sy^fkZyToq`YQ?iz4+qA6Xi&oE_ zOV6a5MLmz6v+=?XVztJ;b@Ipm_S~_P@rx>2)^y^Iyy{~4*ia+`R3a)Uk{ECN9hZ?U zf{u(Z{&WsKG)ja(-Ls8!YU%aB3Oy7#Z>YU<+vG|ICF5gaSVww45s9GyEBc$tKgZ&l{=}2S%?LR7s=6vn^U{KgSq zo@uA&rL@K#FPPPeo2LKb|E=Cz)6(BRGaHpX3cD7S9%R*-DccHGZZq(u=umIhpJ+Uc`&?BW)aOfoWg-ocB}%HP;Q zB8%jgOXr+S+5d7auK;it)|E{F#_`HoR3U3wVB^P@9%6q{8fT^#OJ_ohLyoJQxFoPd z8d#y_Wyl*6{$;1U5kKgf!3*-yRAzixE~a1PU1b zc?vR2WvJ@^VEk`EtQu@VP*TAX+27H)!KBG%Y^cV_ z{3LLtaU>`K42hMOEA)Q_LHj@06Nw3!eTYRSxYQ}iXXDcQ@+fIVAoh~)G}ZTuk7mV(99 zl8J?pnXe(EjalS1C4_eVHTE{#46t)NfzokPT2MRGgh z*M)!Y!VMCg5uyST!I0Mh94Kr*+?<=2^GiwI#6+;o+%d|s9vMHrbBt67_%Xk-!hc>Y z0s7Sp*AE2Uzf;@DIn)Nnp92}=-r-RpNzN^5>H9gN&l1V94dAQK)*dj-)yAc1+v>-VNQIBMw5Ql$w_SY=H ze~v32^J=@(X9UbUsV0S_=~+$7MCIj(u~=nDrS4gc9PjKUGhK_z+Bt_P-)?~5^}mr* z5Z9Yr3Ag-}8X*=T0~Ny;f6}q(+I?z5WCXsUn$@)XnC;7=nlIYI5~MQEm8F7g>vU1U z@Ja=OQlNOr99IQfv}QB|RJ(oZRh1#(#|m67D)ffV*0|USqBZuxH0R>xZs+gbFV;!c zUMzCVp1XXH{c4s>MQ-gJDs3?!%9^g(^vQA(e8y+Z2W+kLx()3LPOBlB7Hm~#28 z`^M4tUDe}^uAb4LOnsq_BBp7Ax2xNQ{(1$E8HDzZ0g_QC``hD)-~v>YWo7~;^P4>n zU12gz{%|-MW>#o@aRagv>#tA(OmS#rKQ8M(mrjV-QB>*>bMy@LMZ}5HW?8`$OJ{z{ z;8Kz#kcM7n(Ju@pf_DWCeTw9({sHMnhYB<&O-D<6Fpoiw|E2_xt+9@A@8X1Pyq`F74r>b*!H53aoA-@r<5@wQl)l%WGE3= zKGcOkN1-TNDwbr?y-gmyrZNZ)OzozR)=+1}I~Q4YHuaDLam zuZ+?MOv#P@nbtyyI3;L_)2I6OB62(opdCX_oQoqkh{Gqq7r(xVQCsT6Do1IH$`)gN zutmK*M^-%lSz2@@K9K$;(ff6O3UNWrw8m7bB-U4`5QGc6xRUff`BeWBR?QS5#e=jD zijtagm9jJ4XhN8O#(5XGL~pVa4n9uNZ6kSLJLQN`WP((nct!T)W2eJ^zDx-t$cJG5 z7dNo#Wz_CZmAVMAY5g4q%aTcn$=?TQG)?WjBzArx@lM}e*dxGb!ynr~)w1&Wm>!I; z_dz}~-}nc)wgf=&>*g#b{<&wX--8jm3Qdptu`fcq2&M z;ehTV5}o>xeViTrYpU?ASvuB#3)crt#VBuL(cMla+bjpJWeu^kg?^P&;)*ZuBqf`Sn1^T*VY4tJNcy%}hKj6uAU`w{Bdg6CJ^jiuYsF}(Qn_xOh} zr|{c>%`I#|sgtxlZ7fEE2Ma@hD~xM1@GAkn{tM1!yUj|O9rW!;Lw zNohr&?A|G}^cbkYdY=n<%6cv5nse#Y;M&s9Y@Z_ZgEZ-RV_H)y&*-BWMYYLLjxs*7gg%)wT^$+r`C**EV$laPK-4aBeGvQ(;DawcS z^|Mx9jlm^fyhI7I*_81HFcifShM98?K#xol#E0~*LY0i1J<^DC2YeKfxSI6BPa(Irp30;z1nVPDBL_NPgpm6Nm2&;b#l_#7ko_JUvtn`<8 z*hbJ3Kg5P^(|D4_Lf#y8XXbvzwVoVnX}YthR0g2cXh5GFtDQpB_|%4KT<|}Iq|#!J zj#Y=s!g{$3QYgB6S@Bl8YS_RwW3-tkS;K%o)$-4j%@0`4d?I!TCpmTyvbsPeLKd=_ z%Y-hVct*>PpqN&yA}f|{?heu=P&UShQ%LKR@~g78#>dmtiw6?b<%fXnfVnTM{;%rVir0(P-SUY`Jl_&jh5z|h zpbr|HI*U`+Sd7rDd?@v6NsRhcQQH1f1&E|w@m_%zGRGkQFY0IT@>S|yfG6-|hzvG8 z$F?t%J0$l7MLaGsq|htt1^u^2^#E29iCarw_)l&T$yl2_aIiZZ;gN1L0HT? zBZh1n{Tmzq%wXa0X$E@51LHU* zkf+qK5PV9VG-dY+AKw_#C&{?~WzO4Z0Zflvphgfh?xo|jVv&Isx)pT$c}bc+Ca*X1 zg8@)IL4_KNAzJ+!|3NXm2>D4`byq!M*GZH#T)8;vFfIMMbNe*1Zv|2~NSIm9_O?KV z{8Na#!qki_lWJA~o7$Mic&&2%UJl2~C%>YLc6{VpwC+ii1Cg4^PsB?UPX+{X5PYr5ne`-)aM+lz> zZNQxQ%gg6wKjK%?v&FXxpDZ5mWbsksJR@t&d!z%V^M!C_AW1XC)C57ixff>C zKT=h(FEYp}mkKF&(IV4mkl4<}%rgnU9V!^pfH#m;ZO3bD6Ox;LK?)W;(%w`e{|fP* z4U8A7f=32N0~G>B?`K!ukF=0)uuqwwDOzx;*m50p#;CvNZav1wlN=YrjiUuX=OsU6 z6nY=>$D&24p&O7fE&~{H!TC+h_r#=Wmd=&S@uge&ASFO%ku_OqfgnbqNm+G`&dI#a z@_FFQ1d+FaS~uAVn}2w*`bPPoQ>;k$VHgLnLIis4Z^2)0=hSC_-9Qin_d< z_o^XXnn3ADTi{*+QU(3+D#5l`a(?YBSf8gE*EM4%^<1pqY-Y6PB3htoFFm@X!3XZ1 z+C#@+NhkioQPu_!X3+khyRW2%u)4WBEO%-zyKNq~cvZJp#+ZqdY-dx18#Sjj8@DmM zVmnfB@r)Q{=CoOeT8J-HTTbhrGE^Zl7N1cDOg}NT;5`mRYIPT!Ou?3X{oUV=F}Bpa}vC+ zx%LbJ++^|xN7;t$Z4yE}DxBurX-|AD3Xg!r*f=HHrM`~h5^lqK!1W3maH$`4E~!B( zb4ZXr@SL3?U9Fi?1%8aVCG6S*;@bC0GDYo>98x{fT$y^KrQ|)Bp|BC7fkASvF3QX7 zi|ofC$S8Bsr>Qd!t~AXzr*cWWTD`7wZcO>lCT3KZCt28kxPe3qsx?plvRcd$EK+Viv@pR65 z>B-Ng$c>Hi`NX{Q6u6?PA;-QVqN%-U2FZ;@qNzp7y*n~eD#hnRC;n2YF3>{Q?E@Ff zk39^dNmI&E)9~+cfh112+m9K-j>I`B+s${aZ>|pquY;!jaM_5&{EiiR=vVN}UCH%& zVJ>YLCI&YS5tdoP6iRZjZ}r^*=*zOQUNA{czTB@9YvG#ttFRb5*_KGZwf&+$m3u0| zL3?1d>;r`54NJIxwze|Mat`6rPR!(_)Q$fyMuzNUQY_A}b7CQ>pyr|jL}ZUw1t*RhF6g;?mX)VIbd1z zqjy$nU*;L|N~0Py$N0bRkv)h2`Oa}n(W}+l&+-m( zpnclux-xVHL4@$JD27Ia_&RMSz2c9CR%w7-;EeFu45tCssdA!b3YXme($~mhRK2YM zzKL3(S!R_drFiAI=avsLOp_fPIWs=eAe&kSC<0`oICP z>;-{J%Y{1E{<#Hu_`)JY(lR+H4!#U333s!ZZ7nx{*VfqAFKmx0B?F`x2=x9eZ$=MY z^L*JQZ`O~Nj$(0?eNVqv-)sq2rE-fZHftO)XL#$RvT~yHs>b%pveEV_$R*+m{#|4b zmh2SuSknor;ugFAbbFtcp=_uS>JOpe)M9%y)|U| zPpo&NhZGTxllNHJS7B`V=NvbkWEv5~{rZ_~$bXnQU?Nowf*<9jQf{b45kDfB@$B`o zUK`OZY=Kzb*a%AyZ(OcmWLSU~pf=rv>P2}HogX;Ey@`O6(>CdnBa#dS zC6kx#n*IWlPDIbBiWjUH8_%5>l-(1lYcI@PQr{WwEBTZO_`^wui1e5WwG_7q_)KNe zhe;TqVpo^~4Sqw&Ja^x@x+9m>&v|;Krd^mu6j@qP*!iwf9{e(yB-E4q4ThnNQd&=A zygV)Qi#|G_Bq9;^yW|N7;||acNwQ$gB@NiBvT?gg$HpG;J@bwIQRxS2N)PRK9uFPd zbb6S!e@L(0u$=$|%f_w^uc?Fv$Az&&?rQy?_A;U95B&e0og~Xrri|;7Nj{juSvV#8 zO!M^u%QxiuV1E;kK!C^E;HOZaljtkTiMWb>;4?iGUa^m**jo9*e50fGgC}s{=~~Q4C6@8W)S>SL&a^`rQ(mz+MZ+ zM7%MJ-1N(8KEZGbOoz8IA`<-I9L0K%+NXnL=h~U$9`yru!huo_p2?sfG#kq7iSt!Z z|4~ZJo`@kuEJ(?*n`04!T+)YUwLWa?2kW_KgwK%w&nGjjbTkb-PDC zCIunHEzH;Gf1x%JCtet4uoFH1*b2ayH%gtU{Pv1=jh3O@h~!JlAUdL|@(MMEgFnt9 z!!kNuz9o=i#)e~n7F^1YI~ZZf%}^O;q_BTV-(5L^$4^v4@7_jNEA;V&&h)qsb_gZ- z`Hb|d_T}8X4{;Z+(Lzp^|kLg3t?UF(msZ-ug7f~?ZwA7ku zbxU2YPD;!<04s8sca#L({r>Uf!q5-g|2r>TKp}4!9Ol5Q zxZNS|+f&Q64WmAa;wCGpP6Ew$I2l!7XVMArJ3y2EXCun@V|vh<@AEL28}JX}5C}EI z^=!K8-9!_7eLCv-t@JPTLetk9QwkopdOLlJXTL<(Vu3&V{{Gx?)n13!!pWb6I%2xx4W_J3ZXIg`b_B{jQ%h#l`Dgrz$iJF$xLx zmG0_VmoBK=Fmb7uHrZHT>&pKDKOD}xEr0$(-@@B(bT?pf#}#CH^0gk#uF_L&kigJ6 z&a81KIkwxxX%TB$Q@0IVb5<4>T&OwL=!Q4=AwA5q-#xaFJEg&H%Ki+zyte2(Aai3h zwBb&Z(HEI5)Mow3vzy3;eth`ALp^61(ghc@o&0nV*g8sfq5bWgfXDdGs^BP)>%6qS zKL>7zgqhfr+X8xhqB`aQzHK>#`m{1Js(nXSTi}OalHXQf1nx1n9WGgyHKCNMknZv9 zvh7CL6h;#;(?V$CzR{Yg^PY;z@x~Ml?lIKgv^2I~wlbL?Z=WG| zWGR*pAjG()qhT3+DRItmqEI$mSqzWoYHuN#KIp(9lkmZJ&ljMISK+bz%Fl5|$M>u6 zS2RPBV%=e@==D3*^{k)TXd}y22tFRyhA8Engi55wqPJp}qluj+Rlyzz{H99^a<&KI zj?BAD-%8p%$uo`LvTzJ34Os57H_JCITX2!|j=0C&cx6@>J-sZnFLdYrlsO8w*`f?w zU}h;Dq1a^xh7S#$w2iC&k`@)FdkpUKixI`xzU(dBcrBb#M1xzz{jhU=4;NTt!W5kx ZDOz_nJu!WKlJYc+?q56ZchHJ}@P9wu$YKBh diff --git a/blueprint/src/chapters/basics.tex b/blueprint/src/chapters/basics.tex index a2f8fc7..a075b18 100644 --- a/blueprint/src/chapters/basics.tex +++ b/blueprint/src/chapters/basics.tex @@ -3,259 +3,95 @@ \section{Vectors} %%% Really trivial stuff about numbers, vectors, etc. \begin{lemma} - \label{lem:two-vector-notation} + \label{lem:vector-notation} \lean{Matrix.Vector_eq_VecNotation₂} \leanok - For any vector $v : \Fin 2 \to \bbn$, we have $v = ![v(0), v(1)]$. + For any vector $v : \Fin 2 \to X$, we have $v = ![v(0), v(1)]$. \end{lemma} \begin{proof} \leanok \end{proof} -%%% - -\section{Theories} -%%% Really trivial stuff about theories - -\begin{lemma} - \label{lem:linear-order-theory-in-dlo} - \lean{FirstOrder.Language.Order.linearOrderTheory_subset_dlo} - \leanok - The theory of linear orders is a subset of DLO. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -%%%% LinearOrder -\begin{lemma} - \label{lem:reflexive-in-linear-order-theory} - \lean{FirstOrder.Language.Order.reflexive_in_linearOrderTheory} - \leanok - The theory of linear orders contains the reflexivity sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:transitive-in-linear-order-theory} - \lean{FirstOrder.Language.Order.transitive_in_linearOrderTheory} - \leanok - The theory of linear orders contains the transitivity sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:antisymmetric-in-linear-order-theory} - \lean{FirstOrder.Language.Order.antisymmetric_in_linearOrderTheory} - \leanok - The theory of linear orders contains the antisymmetry sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:total-in-linear-order-theory} - \lean{FirstOrder.Language.Order.total_in_linearOrderTheory} - \leanok - The theory of linear orders contains the totality sentence. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-reflexive} - \lean{FirstOrder.Language.Order.realize_reflexive_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the reflexivity sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:reflexive-in-linearOrderTheory} -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-transitive} - \lean{FirstOrder.Language.Order.realize_transitive_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the transitivity sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:transitive-in-linearOrderTheory} -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-antisymmetric} - \lean{FirstOrder.Language.Order.realize_antisymmetric_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the antisymmetry sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:antisymmetric-in-linearOrderTheory} -\end{proof} - -\begin{lemma} - \label{lem:models-of-linearOrderTheory-realize-total} - \lean{FirstOrder.Language.Order.realize_total_of_model_linearOrderTheory} - \leanok - Models of the theory of linear orders realize the totality sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:total-in-linearOrderTheory} -\end{proof} - -%%%% -%%%% DLO \begin{lemma} - \label{lem:reflexive-in-dlo} - \lean{FirstOrder.Language.Order.reflexive_in_dlo} + \label{lem:vector-notation-under-composition} + \lean{Matrix.comp_VecNotation₂} \leanok - The theory DLO contains the reflexivity sentence. + For any function $f : X \to Y$ and elements $x_1, x_2 \in X$, we have $f \circ ![x_1, x_2] = ![f(x_1), f(x_2)]$. \end{lemma} \begin{proof} \leanok - \uses{lem:linear-order-theory-in-dlo, lem:reflexive-in-linear-order-theory} \end{proof} -\begin{lemma} - \label{lem:transitive-in-dlo} - \lean{FirstOrder.Language.Order.transitive_in_dlo} - \leanok - The theory DLO contains the transitivity sentence -\end{lemma} -\begin{proof} - \leanok - \uses{lem:linear-order-theory-in-dlo, lem:transitive-in-linear-order-theory} -\end{proof} +%%% -\begin{lemma} - \label{lem:antisymmetric-in-dlo} - \lean{FirstOrder.Language.Order.antisymmetric_in_dlo} - \leanok - The theory DLO contains the antisymmetry sentence. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:linear-order-theory-in-dlo, lem:antisymmetric-in-linear-order-theory} -\end{proof} +\section{Theories} +%%% Really trivial stuff about theories \begin{lemma} - \label{lem:total-in-dlo} - \lean{FirstOrder.Language.Order.total_in_dlo} + \label{lem:realize-reflexivity} + \lean{FirstOrder.Language.Order.DLO.realize_reflexive} \leanok - The theory DLO contains the totality sentence. + Models of the theory of dense linear orders realize the reflexivity sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:linear-order-theory-in-dlo, lem:total-in-linear-order-theory} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-reflexivity} - \lean{FirstOrder.Language.Order.realize_reflexive_of_model_dlo} + \label{lem:realize-transitivity} + \lean{FirstOrder.Language.Order.DLO.realize_transitive} \leanok - Models of the theory DLO realize the reflexivity sentence. + Models of the theory of dense linear orders realize the transitivity sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:reflexive-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-transitivity} - \lean{FirstOrder.Language.Order.realize_transitive_of_model_dlo} + \label{lem:realize-antisymmetric} + \lean{FirstOrder.Language.Order.DLO.realize_antisymmetric} \leanok - Models of the theory DLO realize the transitivity sentence. + Models of the theory of dense linear orders realize the antisymmetry sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:transitive-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-antisymmetric} - \lean{FirstOrder.Language.Order.realize_antisymmetric_of_model_dlo} + \label{lem:realize-total} + \lean{FirstOrder.Language.Order.DLO.realize_total} \leanok - Models of the theory DLO realize the antisymmetry sentence. + Models of the theory of dense linear orders realize the totality sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:antisymmetric-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-realize-total} - \lean{FirstOrder.Language.Order.realize_total_of_model_dlo} + \label{lem:realize-densely-ordered} + \lean{FirstOrder.Language.Order.DLO.realize_denselyOrderedSentence} \leanok - Models of the theory DLO realize the totality sentence. + Models of the theory of dense linear orders realize the densely ordered sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:total-in-dlo} \end{proof} \begin{lemma} - \label{lem:models-of-dlo-models-of-linear-order-theory} - \lean{FirstOrder.Language.Order.model_linearOrderTheory_of_model_dlo} + \label{lem:realize-no-min} + \lean{FirstOrder.Language.Order.DLO.realize_noBotOrderSentence} \leanok - Models of DLO are also models of the theory of linear orders. + Models of the theory of dense linear orders realize no minimum sentence. \end{lemma} \begin{proof} \leanok - \uses{lem:linear-order-theory-in-dlo} \end{proof} -%%%% - -%%% - -\section{Instances} -%%% Simple instances and instance chains - -\begin{definition} - \label{def:le-instance-ordered-language} - \lean{FirstOrder.Language.Order.inst_LE_of_IsOrdered} - \leanok - Any structure of an ordered language is an ordered set. -\end{definition} - -\begin{definition} - \label{def:preorder-instance-models-of-dlo} - \lean{FirstOrder.Language.Order.inst_Preorder_of_dlo} - \leanok - \uses{def:le-instance-ordered-language, lem:models-of-dlo-realize-reflexivity, lem:models-of-dlo-realize-transitivity} - statement of your definition -\end{definition} - -\begin{definition} - \label{def:linear-order-instance-models-of-dlo} - \lean{FirstOrder.Language.Order.inst_LinearOrder_of_dlo} - \leanok - \uses{def:preorder-instance-models-of-dlo, lem:models-of-dlo-realize-antisymmetric, lem:models-of-dlo-realize-total} - statement of your definition -\end{definition} - -\begin{definition} - \label{def:binary-relational-language} - \lean{FirstOrder.Language.IsRelational₂} - \leanok - A language is binary relational if it has onyl binary relation symbols. -\end{definition} - \begin{lemma} - \label{lem:canonical-ordered-language-binary-relational} - \lean{FirstOrder.Language.Order.instIsRelational₂} + \label{lem:realize-no-max} + \lean{FirstOrder.Language.Order.DLO.realize_noTopOrderSentence} \leanok - \uses{def:binary-relational-language} - The canonical ordered language consisting of a single binary relation $\leq$ is a binary relational language. + Models of the theory of dense linear orders realize no maximum sentence. \end{lemma} \begin{proof} \leanok @@ -263,74 +99,4 @@ \section{Instances} %%% -\section{Structures} -%%% Equality of structures for relational languages - -\begin{lemma} - \label{lem:structure-funmap-relational-language} - \lean{FirstOrder.Language.Structure.funMap_eq_funMap_of_relational} - \leanok - Structures of a relational language have equal function maps. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:equality-of-structures-relational-language} - \lean{FirstOrder.Language.Structure.structure_eq_structure_of_relational_iff} - \leanok - Two structures of a relational language are equal if and only if they agree on the - interpretation of all relation symbols. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:structure-funmap-relational-language} -\end{proof} - -%%% - -%%% Equality of structures for binary relational languages - -\begin{lemma} - \label{lem:structure-relmap-binary-relational-language} - \lean{FirstOrder.Language.Structure.RelMap_eq_RelMap_of_relational₂} - \leanok - \uses{def:binary-relational-language} - Two structures of a binary relational language have equal relation maps if and only - if they agree on the interpretation of all binary relation symbols. -\end{lemma} -\begin{proof} - \leanok -\end{proof} - -\begin{lemma} - \label{lem:equality-of-structures-binary-relational-language} - \lean{FirstOrder.Language.Structure.structure_eq_of_structure_of_relational₂_iff} - \leanok - \uses{def:binary-relational-language} - Two structures of a binary relational language are equal if and only if they agree on the - interpretation of all binary relation symbols. -\end{lemma} -\begin{proof} - \leanok - \uses{lem:structure-relmap-binary-relational-language, lem:equality-of-structures-relational-language} -\end{proof} - -\begin{lemma} - \label{lem:orders-coincide-for-ordered-structures} - \lean{FirstOrder.Language.Order.orderStructure_of_LE_of_structure} - \leanok - \uses{def:le-instance-ordered-language} - statement of your lemma -\end{lemma} -\begin{proof} - \leanok - \uses{def:le-instance-ordered-language, - lem:canonical-ordered-language-binary-relational, - lem:equality-of-structures-binary-relational-language, - lem:two-vector-notation} -\end{proof} - -%%% diff --git a/blueprint/src/chapters/main.tex b/blueprint/src/chapters/main.tex index d49a292..a7ff0ae 100644 --- a/blueprint/src/chapters/main.tex +++ b/blueprint/src/chapters/main.tex @@ -1,10 +1,11 @@ \begin{theorem} \label{thm:dlo-aleph0-categorical} - \lean{FirstOrder.Language.Order.aleph0_categorical_of_dlo} - \notready + \lean{FirstOrder.Language.Order.DLO.aleph0_categorical_of_dlo} + \leanok The theory of dense linear orders without endpoints is $\aleph_0$-categorical. \end{theorem} \begin{proof} - \notready + \leanok + \uses{def:linearorder-dlo, lem:to-isomorphism} \end{proof} diff --git a/blueprint/src/chapters/model_theory.tex b/blueprint/src/chapters/model_theory.tex new file mode 100644 index 0000000..89fd629 --- /dev/null +++ b/blueprint/src/chapters/model_theory.tex @@ -0,0 +1,67 @@ +\section{Instances} +%%% Simple instances + +\begin{definition} + \label{def:le-instance-language-order} + \lean{FirstOrder.Language.Order.instLE} + \leanok + Any structure of the language of orders is an ordered set. +\end{definition} + +\begin{lemma} + \label{lem:order-structure-of-le} + \lean{FirstOrder.Language.Order.orderStructure_of_LE} + \leanok + \uses{def:le-instance-language-order} + The structure induced from $\le$ which is induced from another structure is equal to the original structure. +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-language-order, lem:vector-notation} +\end{proof} + +\begin{definition} + \label{def:preorder-dlo} + \lean{FirstOrder.Language.Order.DLO.instPreorder} + \leanok + \uses{def:le-instance-language-order, lem:realize-reflexivity, lem:realize-transitivity} + Models of the theory of dense linear orders are preorders. +\end{definition} + +\begin{definition} + \label{def:linearorder-dlo} + \lean{FirstOrder.Language.Order.DLO.instLinearOrder} + \leanok + \uses{def:le-instance-language-order, def:preorder-dlo, lem:realize-antisymmetric, lem:realize-total} + Models of the theory of dense linear orders are linear orders. +\end{definition} + +%%% + +\section{Homomorphisms} + +\begin{lemma} + \label{lem:to-embedding} + \lean{FirstOrder.Language.Order.toLEmbedding} + \leanok + \uses{def:le-instance-language-order} + A function which is an order embedding is also an embedding in the model theoretic sense. +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-language-order, lem:vector-notation, lem:vector-notation-under-composition} +\end{proof} + +\begin{lemma} + \label{lem:to-isomorphism} + \lean{FirstOrder.Language.Order.toLIso} + \leanok + \uses{def:le-instance-language-order} + A function which is an order isomorphism is also an isomorphism in the model theoretic sense. +\end{lemma} +\begin{proof} + \leanok + \uses{def:le-instance-language-order, lem:vector-notation, lem:vector-notation-under-composition, lem:to-embedding} +\end{proof} + + diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 523fdd8..befd653 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -16,15 +16,19 @@ % \end{theorem} % \begin{proof} -% \leanokcd +% \leanok % \uses{thm:open_ample, lem:open_ample_immersion} % This obviously follows from what we did so far. -% \end +% \end{proof} \chapter{Basic Definitions and Lemmas} \input{chapters/basics.tex} -\chapter{Main Results} +\chapter{Model Theory and The Rest of Mathlib} + +\input{chapters/model_theory.tex} + +\chapter{Main Result} \input{chapters/main.tex} \ No newline at end of file diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux index f1545044bcb85eb469da341f071384dc84e45519..76313b9c63390822cc431019dae2be053c62cda8 100644 GIT binary patch literal 9130 zcmbW6TaOh*5XX&(#*i2gjfxS_1$I$qJeOTA2T&4Ud_YVH8e@#>a8B>eBy%~;%t6+K zs3iI{J~=-7CHzEw61%GA(zluES$z=P>H7bwx~jUm_t%&H{%7k2{O4I&oc!Y9m-qI{ zXXQ@uUhYQ=FJxZy-i;|K_VxXSqdST)Ba%k=O|p9VM}8$SSR&!5H!AX4(+KU?5Vh!bH14a z`bD3q25l$feoiKndAnsD>csaBMJN9$aTFg!Jjk^nydFyp-6bt>CgEz|R_tIAWX_`? z_R=FKWg#Y!7ph%AA8u9C>R2!wJ3kaN`{^%;|Yu zkp7;K)7OhJcKn+>xAwFUSuqgx1gRbNc;kgZe&i$vPO~~2VxN}^`*>^U!7bH;F+AkQ zdA>XP#!C?wD|ffQa*H8zO@fHcWdMOdrxfre$Pi;l6D?^acE8G&JtgA)3Iljs3*Z?0 z1ojpOTbPOq4wqeb(|@6oGx9$+JPUp-V78~RGgf;yPVNagra&} z*jw>4UQ*X|LMsG9b~*Bx42Bc#JL(3!qP`cvfAD|tf8;zj<^3IFoRB^Nq}BzyoU534 z&dE%FAk#u&8e^TH_IlzpP!1K^H5KhoM7yh?b#%8Ljdmj!9gEx3MK07T17~UmLQ;&e zg?V^e&%+ToqR(j3M?N z8GEdaHif%()h6br%~3>iBEMW zMj0Vj-T>$MB{*bHgC~$BPIWcrDe>~uow?JA8gBCvWcom7(rlCNo1mMgUYrGahp?86 z9cxf|OIOydlk{bfj*=A%GZ^aON|!P|Cs^yoh5ro~fg_ZP)b_?o$o$^N$-v8Q$BRMNpf;I_Q89>abjAXw&Bz!D@zjyYG?q%;zWwK zGcV4A>?n#@&fhN~Q3rymbt`)-$ZNRcSs@VeMc9a(KMjT!s9LicUX6&#z%eLEXz;=y zbbbosSJ18SsTUr`8*B8j&_apG#OqLO!Q*3VsS zFSl)tm;!0LmUz!XAPv92@wedx6<&G$tHML%M}={L@9@XT_w{(GhDj5r3FSx527ZCa zFUHY2flE>nV}vRSUTHFgr3vIR3?#$iM2c_N>M>bgL68jxXPK>Y5z-hQy-fn7j}4{% zadUzw09tUmS0RC+4H+c}0e(5hhg_Nz^kz^6fv2z>gq~#xv8^YIS%fIgh!kywSL%EO zl+_KNqw0ljRk4WQ71dTO&REEQBS!CBZCcLYaYNSaU5Er%y9rbw^89s?CFU2CK&T8H z(_{qG_o#faTe&jZA?Q67edf({K#+fLBgj7^L3~^m-|XsNk5b5Mab9V9HyT=tAoV46 zM!#pm1}QudDslvc`Ab*(=3NfnPeK}!dEx<&R(d_l5T#E03I+DoEJ75gfwg&KsAqsm zT&p?#Yt*bq0Kt99BuSlZ&kZ6{)U+BiE5s#cCMBH delta 1211 zcmZXTPiWI%7{+O5lhw9a(luSuv@7kvcCJa6wADG42_C#v4X`%Q5BmJ@4~8@7w2R-p+(J4m>QU zUxy;WfB_+Rjx{v1yJAh?dq8=!75p=V<+O|iMh==P-ZPiR3U)}>s+zuIPTK5wv)S%6 zS9Z)PoMcM@6?HL*4faOhHh!}RY{DLX%-%N}CTE|*U-l5rMsw(ftDcHMtGo*vMCE7r zO2(a2(W(?-k1sZtW}!#YgnM+*lK1^oXs(P#WZE%Zk8F96PppRBu!0}MiUa1OF9Wae zIoj#FtN1f!ViOLy5o>t?YSh?mP9wg`+$~Ro25^df+q&LVTdV4#)!rc!g8aq71Ufj%d=Y9!LPJQR z$4BvnHwLiJa#lF(+Nt6hd3IcgVM{1`0evg{AQVUidqSg6kbHE!QatBW@E~ptX3o&e zZrpH~dL&6aa#$X%dvd;kA4iL>J!8ME2)>ObP)g|NjY}{R1vjb0bC41#d`)PGWhLar zDPprOF5@ow>WO)0+@84BzZF9}LOHT^=yEaIX)amKo1|%{;upzH4?jxd2EiwzgT*-b zow0kw5*w$(+BHWSJ&9vXXYHp+&uPrbDe}`9VwQ~`qt#XNLUSBv<;9eD9CR}_*{>)L zk$b?2aT%XvUG-4k--UPYsNG$#{yU*k>cT+W*GB<5pTb&d-*nAA4)VFJObs6STFD|O oC}=2*yD`;$Gp{h1ml-@!)P9>4&1bKGT)ODw9ZAm(U0c`w0Unln4gdfE diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html index eade282..ac32b62 100644 --- a/blueprint/web/dep_graph_document.html +++ b/blueprint/web/dep_graph_document.html @@ -61,25 +61,25 @@

Dependencies

-
+
-