text:
------------------------------------------------------------------------
-- Code related to the paper "Higher Lenses"
--
-- Nils Anders Danielsson
--
-- The paper is coauthored with Paolo Capriotti and Andrea Vezzosi.
------------------------------------------------------------------------

-- Most of the code referenced below can be found in modules that are
-- parametrised by a notion of equality. One can use them both with
-- Cubical Agda paths and with the Cubical Agda identity type family.

-- Note that the code does not follow the paper exactly. For instance,
-- some definitions use bijections (functions with quasi-inverses)
-- instead of equivalences.

-- An attempt has also been made to track uses of univalence by
-- passing around explicit proofs of the univalence axiom (except in
-- certain README modules). However, univalence is provable in Cubical
-- Agda, and some library code that is used does not adhere to this
-- convention, so perhaps some use of univalence is not tracked in
-- this way. On the other hand some library code that is not defined
-- in Cubical Agda passes around explicit proofs of function
-- extensionality.

-- Some other differences are mentioned below.

-- Note that there is a known problem with guarded corecursion in
-- Agda. Due to "quantifier inversion" (see "Termination Checking in
-- the Presence of Nested Inductive and Coinductive Types" by Thorsten
-- Altenkirch and myself) certain types may not have the expected
-- semantics when the option --guardedness is used. I expect that the
-- results would still hold if this bug were fixed, but because I do
-- not know what the rules of a fixed version of Agda would be I do
-- not know if any changes to the code would be required.

{-# OPTIONS --cubical --guardedness #-}

module README.Higher-Lenses where

import Circle
import Coherently-constant
import Equality
import Equality.Decidable-UIP
import Equivalence
import Equivalence.Half-adjoint
import Function-universe
import H-level
import H-level.Truncation.Propositional
import H-level.Truncation.Propositional.Non-recursive
import H-level.Truncation.Propositional.One-step
import Preimage
import Surjection

import Lens.Non-dependent.Bijection as B
import Lens.Non-dependent.Equivalent-preimages as EP
import Lens.Non-dependent.Higher as E
import Lens.Non-dependent.Higher.Capriotti as F
import Lens.Non-dependent.Higher.Coinductive as C
import Lens.Non-dependent.Higher.Coherently.Coinductive as Coh
import Lens.Non-dependent.Higher.Coherently.Not-coinductive as NC
import Lens.Non-dependent.Higher.Coinductive.Small as S
import Lens.Non-dependent.Higher.Combinators as EC
import Lens.Non-dependent.Traditional as T
import Lens.Non-dependent.Traditional.Combinators as TC

import README.Not-a-set

------------------------------------------------------------------------
-- I: Introduction

-- Traditional lenses.

Lensᵀ = T.Lens

-- The function modify.

modify = T.Lens.modify

-- The two variants of Tm, and proofs showing that Tm A is not a set
-- if A is inhabited.

Tm₁       = README.Not-a-set.Tm
¬-Tm₁-set = README.Not-a-set.¬-Tm-set
Tm₂       = README.Not-a-set.Tmˢ
¬-Tm₂-set = README.Not-a-set.¬-Tmˢ-set

------------------------------------------------------------------------
-- II: Homotopy type theory

-- The cong function.
--
-- The axiomatisation of equality that is used makes it possible to
-- choose the implementation of cong. However, the implementation is
-- required to satisfy a property which implies that the definition is
-- unique.

cong        = Equality.Equality-with-J.cong
cong-refl   = Equality.Equality-with-J.cong-refl
cong-unique =
  Equality.Derived-definitions-and-properties.monomorphic-cong-canonical

-- Is-equivalence and _≃_.
--
-- Note that the syntax used for Σ-types in the paper is not valid
-- Agda syntax. Furthermore the code defines _≃_ as a record type
-- instead of using a Σ-type.

Is-equivalence = Equivalence.Half-adjoint.Is-equivalence
_≃_            = Equivalence._≃_

-- Lemma 6.

lemma-6 = Equivalence._≃_.left-right-lemma

-- H-level, Contractible, Is-proposition and Is-set.
--
-- Some of the definitions are slightly different from the ones given
-- in the paper.

H-level        = H-level.H-level
Contractible   = Equality.Reflexive-relation′.Contractible
Is-proposition = Equality.Reflexive-relation′.Is-proposition
Is-set         = Equality.Reflexive-relation′.Is-set

-- The circle.

𝕊¹ = Circle.𝕊¹

-- A function that is distinct from refl.

not-refl      = Circle.not-refl
not-refl≢refl = Circle.not-refl≢refl

-- The type base ≡ base is equivalent to ℤ.

base≡base≃ℤ = Circle.base≡base≃ℤ

-- The circle is not a set.

circle-not-set = Circle.¬-𝕊¹-set

-- The propositional truncation operator.

∥_∥ = H-level.Truncation.Propositional.∥_∥

------------------------------------------------------------------------
-- III: Traditional lenses

-- Lenses with equal setters have equal getters.

getters-equal-if-setters-equal = T.getters-equal-if-setters-equal

-- The identity lens.

id-traditional = TC.id

-- The lens used for the counterexamples.
--
-- This lens is a little different from the one in the text: the
-- source and view types are liftings of the circle instead of the
-- circle. This change also affects the proof of Lemma 12.

l = T.bad

-- Lemmas 12 and 13.

lemmas-12-and-13 = T.getter-equivalence-but-not-coherent

-- There are lenses with equal setters that are not equal.

equal-setters-but-not-equal =
  TC.equal-setters-and-equivalences-as-getters-but-not-equal

-- Lemma 14.

lemma-14 = T.lens-to-proposition↔

-- Lensᵀ A ⊤ is not necessarily a proposition (and thus not
-- necessarily equivalent to the unit type).

Traditional-lens-𝕊¹-⊤-not-propositional = T.¬-lens-to-⊤-propositional

-- Fibres.

_⁻¹_ = Preimage._⁻¹_

-- Lemmas 16 and 17, and a variant of Lemma 16 for lenses which
-- satisfy certain coherence laws.

lemma-16          = T.≃get⁻¹×
lemma-16-coherent = T.≃get⁻¹×-coherent
lemma-17          = T.≃Σ∥set⁻¹∥×

-- A variant of Lemma 17 without the requirement that the source type
-- is a set does not hold in general.

not-lemma-17-without-Is-set = TC.≄Σ∥set⁻¹∥×

------------------------------------------------------------------------
-- IV: Lenses based on bijections

-- Lenses based on bijections.

Lensᴮ = B.Lens

-- Lensᴮ ⊥ ⊥ is equivalent to Type.
--
-- Note that the definition of ⊥ that is used in the code can target
-- different universes, not just Type.

Lensᴮ-⊥-⊥≃Type = B.Lens-⊥-⊥≃Type

-- Lensᵀ ⊥ ⊥ is equivalent to ⊤.

Lensᵀ-⊥-⊥≃Type = T.lens-from-⊥≃⊤

------------------------------------------------------------------------
-- V: Higher lenses

-- Lensᴱ.
--
-- For performance reasons η-equality has been turned off for this
-- definition.

Lensᴱ = E.Lens

-- Lemma 20.

lemma-20 = E.isomorphism-to-lens

-- The functions get, remainder and set.

get       = E.Lens.get
remainder = E.Lens.remainder
set       = E.Lens.set

-- The inhabited field is equivalent to stating that the remainder
-- function is surjective.

inhabited≃remainder-surjective = E.inhabited≃remainder-surjective

-- Lemmas 24-27.

lemma-24 = E.Lens.get-set
lemma-25 = E.Lens.remainder-set
lemma-26 = E.Lens.set-get
lemma-27 = E.Lens.set-set

-- Traditional lenses that have stable view types and that satisfy two
-- coherence laws can be translated to higher lenses with the same
-- getters and setters.

coherent-to-higher                       = EP.coherent↠higher
coherent-to-higher-preserves-get-and-set =
  EP.coherent↠higher-preserves-getters-and-setters

------------------------------------------------------------------------
-- VI: Coherence laws

-- Lemmas 28-29.

lemma-28 = E.Lens.get-set-get
lemma-29 = E.Lens.get-set-set

------------------------------------------------------------------------
-- VII: Some equivalences

-- Lemmas 30-37.
--
-- Lemmas 31 and 33 are formulated slightly differently.

lemma-30 = E.lens-to-proposition↔get
lemma-31 = E.lens-to-contractible↔⊤
lemma-32 = E.lens-to-⊥↔¬
lemma-33 = E.lens-from-contractible↔codomain-contractible
lemma-34 = E.lens-from-⊥↔⊤
lemma-35 = E.get-equivalence≃inhabited-equivalence
lemma-36 = E.≃-≃-Σ-Lens-Is-equivalence-get
lemma-37 = E.remainder≃get⁻¹

-- Lemmas 32-34 hold for traditional lenses.

lemma-32-for-traditional = T.lens-to-⊥↔
lemma-33-for-traditional = T.lens-from-⊤≃codomain-contractible
lemma-34-for-traditional = T.lens-from-⊥≃⊤

-- The right-to-left direction of Lemma 36 returns the lens's getter
-- (and some proof).

lemma-36-right-to-left = E.to-from-≃-≃-Σ-Lens-Is-equivalence-get≡get

-- Lemma 36 does not in general hold for traditional lenses.

¬-lemma-36-traditional = TC.¬Π≃-≃-Σ-Lens-Is-equivalence-get

------------------------------------------------------------------------
-- VIII: Equality of lenses with equal setters

-- Lemmas 38-44.

lemma-38 = E.equality-characterisation₁
lemma-39 = E.equality-characterisation₄
lemma-40 = E.lenses-with-inhabited-codomains-equal-if-setters-equal
lemma-41 = E.lenses-equal-if-setters-equal
lemma-42 = E.lenses-equal-if-setters-equal-and-remainder-set
lemma-43 = E.¬-lenses-equal-if-setters-equal
lemma-44 = E.lenses-equal-if-setters-equal→constant→coherently-constant

-- Constant and CC.

Constant = Equality.Decidable-UIP.Constant
CC       = Coherently-constant.Coherently-constant

-- Lemma 47.

lemma-47 = Coherently-constant.¬-Constant→Coherently-constant

------------------------------------------------------------------------
-- IX: Homotopy levels

-- Lemmas 48-54.

lemma-48 = E.h-level-respects-lens-from-inhabited
lemma-49 = E.contractible-to-contractible
lemma-50 = E.no-first-projection-lens
lemma-51 = E.remainder-has-same-h-level-as-domain
lemma-52 = E.get-equivalence→remainder-propositional
lemma-53 = E.Contractible-closed-codomain
lemma-54 = E.Is-proposition-closed-codomain

-- Lemmas 48-50 for traditional lenses.

lemma-48-for-traditional = T.h-level-respects-lens-from-inhabited
lemma-49-for-traditional = T.contractible-to-contractible
lemma-50-for-traditional = T.no-first-projection-lens

------------------------------------------------------------------------
-- X: Higher and traditional lenses are equivalent for sets

-- Split surjections.

_↠_ = Surjection._↠_

-- Lemmas 55 and 56.
--
-- Lemma 55 takes an extra argument of type Unit, written as
-- Block "conversion". Some other definitions below also take such
-- arguments.

lemma-55 = E.¬Lens↠Traditional-lens
lemma-56 = E.Lens↔Traditional-lens

-- Lemma 56 preserves getters and setters in both directions.

lemma-56-preserves-get-and-set =
  E.Lens↔Traditional-lens-preserves-getters-and-setters

------------------------------------------------------------------------
-- XI: Identity and composition

-- The identity lens.

id = EC.id

-- Lemma 58.

lemma-58 = EC.id-unique

-- A composition operator for types in the same universe.

∘-same-universe = EC._∘_

-- A more general composition operator.

∘-more-general = EC.⟨_,_⟩_∘_

-- A lens from a type in a smaller universe to a type in a (possibly)
-- larger universe.

smaller-to-larger = E.↑-lens

-- Composition laws.

associativity  = EC.associativity
left-identity  = EC.left-identity
right-identity = EC.right-identity

-- Composition laws for traditional lenses.

associativity-traditional  = TC.associativity
left-identity-traditional  = TC.left-identity
right-identity-traditional = TC.right-identity

-- Lemma 60.
--
-- The lemma is formulated slightly differently.

lemma-60 = EC.∘-unique

-- The composition operator produces lenses for which the setter
-- satisfies certain equations.

setter-correct = EC.∘-set

-- Is-bi-invertible.

Is-bi-invertible = EC.Is-bi-invertible

-- Lemmas 62 and 63.

lemma-62 = EC.≃≃≊
lemma-63 = EC.Is-bi-invertible≃Is-equivalence-get

-- Lemma 62 maps bi-invertible lenses to their getter functions.

lemma-62-right-to-left = EC.to-from-≃≃≊≡get

-- Lemma 62 does not in general hold for traditional lenses.

not-lemma-62-for-traditional = TC.¬Π≃≃≊

-- A variant of Lemma 62 for traditional lenses (a split surjection in
-- the other direction).

lemma-62-for-traditional = TC.≊↠≃

-- Lemma 63 for traditional lenses.

lemma-63-for-traditional = TC.Is-bi-invertible≃Is-equivalence-get

-- A category of higher lenses between sets with the same universe
-- level.

category-higher = EC.category

-- A category of traditional lenses between sets with the same
-- universe level.

category-traditional = TC.category

-- The category of higher lenses is equal to the one for traditional
-- lenses (lifted, so that the two categories have the same type).

category≡category = EC.category≡category

-- Naive categories.

Naive-category = TC.Naive-category

-- A notion of univalence for naive categories.

Univalent = TC.Univalent

-- A naive category of higher lenses between types with the same
-- universe level.

naive-category-higher = EC.naive-category

-- This category is univalent.

naive-category-higher-univalent = EC.univalent

-- A naive category of traditional lenses between types with the same
-- universe level.

naive-category-traditional = TC.naive-category

-- This category is not univalent.

naive-category-traditional-not-univalent = TC.¬-univalent

------------------------------------------------------------------------
-- XII: Coherently constant families of fibres

-- Lens^F.

Lens^F = F.Lens

-- Lemma 65.

lemma-65 = F.Lens.get⁻¹-constant

-- A setter.

set^F = F.Lens.set

-- Lemma 67.
--
-- Unlike in the paper this lemma is defined in two steps, using a
-- minor variant of Lens^F "in the middle".

lemma-67 = F.Lens≃Higher-lens

-- Lemma 67 preserves getters and setters in both directions.

lemma-67-preserves-get-and-set =
  F.Lens≃Higher-lens-preserves-getters-and-setters

------------------------------------------------------------------------
-- XIII: Coinductive lenses

-- The one-step truncation operator, and its non-dependent eliminator.

∥_∥¹ = H-level.Truncation.Propositional.One-step.∥_∥¹
rec  = H-level.Truncation.Propositional.One-step.rec′

-- Lemma 70.

lemma-70 = H-level.Truncation.Propositional.Non-recursive.∥∥→≃

-- ∥_∥¹-out, ∥_∥¹-in and ∣_,_∣-in.

∥_∥¹-out = H-level.Truncation.Propositional.One-step.∥_∥¹-out-^
∥_∥¹-in  = H-level.Truncation.Propositional.One-step.∥_∥¹-in-^
∣_,_∣-in = H-level.Truncation.Propositional.One-step.∣_,_∣-in-^

-- Lemmas 74 and 75.

lemma-74 = H-level.Truncation.Propositional.One-step.∥∥¹-out-^≃∥∥¹-in-^
lemma-75 = H-level.Truncation.Propositional.One-step.∣∣≡∣,∣-in-^

-- Coherently and CC^C.

Coherently = Coh.Coherently
CC^C       = C.Coherently-constant

-- Coherently can be defined without using coinduction.

Coherently-without-coinduction            = NC.Coherently
Coherently≃Coherently-without-coinduction =
 Coh.Coherently≃Not-coinductive-coherently

-- But then Lens^C would not be small (at least with the definition we
-- came up with).

Lens^C-without-coinduction        = S.Not-coinductive-lens
Lens^C-without-coinduction≃Lens^C = S.Not-coinductive-lens≃Lens

-- Constant¹ and CC^C1.

Constant¹ = C.Constant′
CC^C1     = C.Coherently-constant′

-- Lemmas 80-86.
--
-- Lemma 84 is more general than in the paper.

lemma-80 = C.Constant≃Constant′
lemma-81 = C.Coherently-constant≃Coherently-constant′
lemma-82 = C.∥∥→≃
lemma-83 = Equivalence.Σ-preserves
lemma-84 = Function-universe.Π-cong-contra
lemma-85 = C.Coherently-constant′≃
lemma-86 = C.Coherently-constant≃Coherently-constant

-- Constant^S and CC^S.

Constant^S = S.Constant-≃
CC^S       = S.Coherently-constant

-- Lemma 89.

lemma-89 = S.Coinductive-coherently-constant≃Coherently-constant

-- Lens^C.

Lens^C = S.Lens

-- Lemmas 91-92.

lemma-91 = S.Higher-lens≃Lens
lemma-92 = S.Lens.get⁻¹-constant

-- Lemma 91 preserves getters and setters.

lemma-91-preserves-get-and-set =
  S.Higher-lens≃Lens-preserves-getters-and-setters

------------------------------------------------------------------------
-- XIV: Unrestricted composition

-- Lemmas 93 and 94.

lemma-93 = S.Coherently-constant-map
lemma-94 = S.Coherently-constant-Σ

-- Composition.

∘-most-general = S.⟨_,_⟩_∘_

-- Lemma 96.

lemma-96 = S.set-∘

-- Composition laws.

associativity-stable  = S.associativity
left-identity-stable  = S.left-identity
right-identity-stable = S.right-identity

-- An unrestricted composition operator for Lensᴱ.

∘-most-general′ = S.⟨_,_,_,_,_,_,_,_⟩_⊚_

-- This operator matches "∘-more-general" when all types have the same
-- universe level and the view type of the resulting lens is stable.

∘-more-general-matches-∘-most-general′ = S.⊚≡∘

------------------------------------------------------------------------
-- XV: Homotopy levels, continued

-- Coherently′.

Coherently′ = Coh.Coherently-with-restriction

-- Lemma 98.

lemma-98 = Coh.Coherently≃Coherently-with-restriction

-- Coherently′ can be expressed as an indexed M-type for a certain
-- indexed container.

Coherently′-as-M-type =
  Coh.Coherently-with-restriction≃Coherently-with-restriction′

-- Lemmas 99-103.

lemma-99  = Coh.H-level-Coherently-with-restriction
lemma-100 = Coh.H-level-Coherently-→Type
lemma-101 = S.H-level-Coherently-constant
lemma-102 = S.lens-preserves-h-level
lemma-103 = S.h-level-respects-lens-from-inhabited

-- Lemma 103 and a variant of Lemma 102 hold for traditional lenses.

lemma-102-for-traditional = T.lens-preserves-h-level
lemma-103-for-traditional = T.lens-from-⊤≃codomain-contractible

------------------------------------------------------------------------
-- XVI: Related work

-- Lemmas 104-106.

lemma-104 = E.grenrus-example
lemma-105 = E.grenrus-example₁-true
lemma-106 = E.grenrus-example₂-false

-- The lenses used in Lemmas 105 and 106 are equal.

lenses-equal = E.grenrus-example₁≡grenrus-example₂

max_stars_repo_name: nad/dependent-lenses

max_issues_repo_name: nad/dependent-lenses

max_forks_repo_name: nad/dependent-lenses


text:
module Formalization.Polynomial where

import      Lvl
open import Data.ListSized
open import Numeral.Natural as ℕ using (ℕ)
open import Type

private variable ℓ ℓₑ : Lvl.Level
private variable T : Type{ℓ}
private variable n n₁ n₂ : ℕ

-- TODO: Some of the operations should work with arbitrary Rg structures, not just ℕ, and some other stuff should work with more assumptions. Currently, one of the function that needs to be modified is 𝐷 and normalize for this to work because their implementations depend on ℕ.
-- TODO: Composition of polynomials, power operation

module _ where
  -- A polynomial of a finite degree represented as a list of its coefficients.
  -- Examples:
  --   (a₀⋅x⁰ + a₁⋅x¹ + a₂⋅x² + a₃⋅x³ + a₄⋅x⁴) of degree 4 is [a₀,a₁,a₂,a₃,a₄]
  --   (5 + 7⋅x + x³) of maximal degree 3 is [5,7,0,1]
  Polynomial : ℕ → Type
  Polynomial(n) = List(ℕ)(ℕ.𝐒(n))

  open import Data.ListSized.Functions
  import      Functional as Fn
  open import Logic.Propositional
  open import Logic.Predicate
  import      Numeral.Natural.Function as ℕ
  open import Numeral.Natural.Function.Proofs
  import      Numeral.Natural.Oper as ℕ
  open import Numeral.Natural.Relation.Order
  open import Numeral.Natural.Relation.Order.Proofs
  open import Relator.Equals
  open import Relator.Equals.Proofs.Equiv{T = ℕ}

  -- Constant polynomial.
  -- Semantically, this corresponds to a constant.
  const : ℕ → Polynomial(n)
  const {n} a = a ⊰ repeat ℕ.𝟎 n

  -- Zero polynomial.
  -- Semantically, this corresponds to zero.
  𝟎 : Polynomial(n)
  𝟎 {n} = const{n} ℕ.𝟎

  -- Unit polynomial.
  -- Semantically, this corresponds to one.
  𝟏 : Polynomial(n)
  𝟏 {n} = const{n}(ℕ.𝐒(ℕ.𝟎))

  -- Increases the degree of the polynomial by adding a zero term at the beginning.
  -- Semantically, this corresponds to multiplying the whole polynomial by the variable.
  -- Example: (var⋅ [a₀,a₁,a₂] = [0,a₀,a₁,a₂])
  --   x ⋅ (a₀⋅x⁰ + a₁⋅x¹ + a₂⋅x²)
  --   = a₀⋅x¹ + a₁⋅x² + a₂⋅x³
  var⋅_ : Polynomial(n) → Polynomial(ℕ.𝐒(n))
  var⋅_ = ℕ.𝟎 ⊰_

  -- Single variable polynomial.
  var : Polynomial(ℕ.𝐒(n))
  var = var⋅ 𝟏

  -- Polynomial addition.
  -- Adds the powers component-wise.
  -- Examples: ([a₀,a₁,a₂] + [b₀,b₁,b₂] = [a₀b₀ , a₁+b₁ , a₂+b₂])
  --   (a₀⋅x⁰ + a₁⋅x¹ + a₂⋅x²) + (b₀⋅x⁰ + b₁⋅x¹ + b₂⋅x²)
  --   = (a₀+b₀)⋅x⁰ + (a₁+b₁)⋅x¹ + (a₂+b₂)⋅x²
  --   of maximal degree 2 is [a₀+b₀ , a₁+b₁ , a₂+b₂]
  _+_ : Polynomial(n₁) → Polynomial(n₂) → Polynomial(ℕ.max n₁ n₂)
  _+_ = map₂(ℕ._+_) Fn.id Fn.id

  -- Polymonial scalar multiplication.
  -- Multiplies every component by a factor.
  -- Example: (n ⋅ [a₀,a₁,a₂] = [n⋅a₀ , n⋅a₁ , n⋅a₂])
  --   n ⋅ (a₀⋅x⁰ + a₁⋅x¹ + a₂⋅x²)
  --   = (n⋅a₀)⋅x⁰ + (n⋅a₁)⋅x¹ + (n⋅a₂)⋅x²
  _⋅_ : ℕ → Polynomial(n) → Polynomial(n)
  n ⋅ as = map (n ℕ.⋅_) as

  -- Increases the degree of the polynomial by adding zero terms at the end.
  -- Semantically, this corresponds to adding terms multiplied by zero.
  -- Example: (pad [a₀,a₁,a₂] = [a₀,a₁,a₂,0,0])
  --   a₀⋅x⁰ + a₁⋅x¹ + a₂⋅x²
  --   = a₀⋅x⁰ + a₁⋅x¹ + a₂⋅x² + 0⋅x³ + 0⋅x⁴
  pad : ⦃ _ : (n₁ ≤ n₂)⦄ → Polynomial(n₁) → Polynomial(n₂)
  pad {n₁ = ℕ.𝟎}     {n₂ = ℕ.𝟎}     ⦃ min ⦄  (a ⊰ ∅)  = singleton a
  pad {n₁ = ℕ.𝟎}     {n₂ = ℕ.𝐒(n₂)} ⦃ min ⦄  (a ⊰ ∅)  = a ⊰ 𝟎
  pad {n₁ = ℕ.𝐒(n₁)} {n₂ = ℕ.𝐒(n₂)} ⦃ succ p ⦄ (a ⊰ as) = a ⊰ pad ⦃ p ⦄ as

  -- Polynomial multiplication.
  -- Proof of step:
  --   ∑(0‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ) ⋅ ∑(0‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ)
  --   = (a + ∑(1‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ)) ⋅ (b + ∑(1‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ))
  --   = (a ⋅ b) + (a ⋅ ∑(1‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ)) + (∑(1‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ) ⋅ b) + (∑(1‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ) ⋅ ∑(1‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ))
  --   = (a⋅b) + (a ⋅ ∑(1‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ)) + (∑(1‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ) ⋅ b⋅x) + (∑(1‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ) ⋅ ∑(1‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ))
  --   = (a⋅b) + (a ⋅ ∑(0‥n₂)(i ↦ bᵢ⋅xⁱ)⋅x) + (∑(0‥n₁)(i ↦ aᵢ⋅xⁱ)⋅x ⋅ b) + (∑(1‥𝐒(n₁))(i ↦ aᵢ⋅xⁱ) ⋅ ∑(1‥𝐒(n₂))(i ↦ bᵢ⋅xⁱ))
  --   = (a⋅b) + (a ⋅ ∑(0‥n₂)(i ↦ bᵢ⋅xⁱ))⋅x + (∑(0‥n₁)(i ↦ aᵢ⋅xⁱ) ⋅ b)⋅x + (∑(0‥n₁)(i ↦ aᵢ⋅xⁱ) ⋅ ∑(0‥n₂)(i ↦ bᵢ⋅xⁱ))⋅x²
  --   = (a⋅b) + ((a ⋅ ∑(0‥n₂)(i ↦ bᵢ⋅xⁱ)) + (∑(0‥n₁)(i ↦ aᵢ⋅xⁱ) ⋅ b) + (∑(0‥n₁)(i ↦ aᵢ⋅xⁱ) ⋅ ∑(0‥n₂)(i ↦ bᵢ⋅xⁱ))⋅x)⋅x
  --   Also see `eval-preserves-multiplication`.
  _⨯_ : Polynomial(n₁) → Polynomial(n₂) → Polynomial(n₁ ℕ.+ n₂)
  _⨯_                  as@(_ ⊰ _)       (b ⊰ ∅)          = b ⋅ as
  _⨯_                  (a ⊰ ∅)          bs@(_ ⊰ _ ⊰ _)   = a ⋅ bs
  _⨯_ {ℕ.𝐒 n₁}{ℕ.𝐒 n₂} (a ⊰ as@(_ ⊰ _)) (b ⊰ bs@(_ ⊰ _)) = (a ℕ.⋅ b) ⊰ lr where
    l : Polynomial(n₁ ℕ.+ n₂)
    l = pad ⦃ max-order-[+] ⦄ ((b ⋅ as) + (a ⋅ bs))

    r : Polynomial(ℕ.𝐒(n₁ ℕ.+ n₂))
    r = var⋅ (as ⨯ bs)

    lr : Polynomial(ℕ.𝐒(n₁ ℕ.+ n₂))
    lr = [≡]-substitutionᵣ ([↔]-to-[→] max-defᵣ [≤]-of-[𝐒]) {Polynomial} (l + r)

  normalize : Polynomial(n) → ∃(Polynomial)
  normalize {ℕ.𝟎}   (x ⊰ ∅)      = [∃]-intro ℕ.𝟎 ⦃ x ⊰ ∅ ⦄
  normalize {ℕ.𝐒 n} (ℕ.𝟎 ⊰ p) with normalize{n} p
  ... | [∃]-intro ℕ.𝟎 ⦃ singleton ℕ.𝟎 ⦄ = [∃]-intro ℕ.𝟎      ⦃ singleton ℕ.𝟎 ⦄
  {-# CATCHALL #-}
  ... | [∃]-intro m   ⦃ a ⦄             = [∃]-intro (ℕ.𝐒(m)) ⦃ ℕ.𝟎 ⊰ a ⦄
  normalize {ℕ.𝐒 n} (ℕ.𝐒(x) ⊰ p) = [∃]-map ℕ.𝐒 (ℕ.𝐒(x) ⊰_) (normalize{n} p)

  degree : Polynomial(n) → ℕ
  degree = [∃]-witness Fn.∘ normalize

  𝐷 : Polynomial(n) → Polynomial(ℕ.𝐏(n))
  𝐷 {ℕ.𝟎}   = Fn.id
  𝐷 {ℕ.𝐒 n} = map₂₌(ℕ._⋅_) (accumulateIterate n ℕ.𝐒(ℕ.𝐒(ℕ.𝟎))) Fn.∘ tail

  import Numeral.Natural.Oper.FlooredDivision as ℕ
  ∫ : Polynomial(n) → Polynomial(ℕ.𝐒(n))
  ∫ {n} p = var⋅(map₂₌(ℕ._⌊/⌋₀_) p (accumulateIterate n ℕ.𝐒(ℕ.𝐒(ℕ.𝟎))))

module Semantics where
  open import Data.ListSized.Functions
  open import Logic.Propositional
  open import Numeral.Finite as 𝕟 using (𝕟)
  import      Numeral.Natural.Oper as ℕ
  open import Numeral.Natural.Oper.Proofs
  open import Numeral.Natural.Relation.Order
  open import Relator.Equals.Proofs.Equiv{T = ℕ}
  open import Structure.Function.Multi
  open import Structure.Operator
  open import Structure.Operator.Proofs.Util
  open import Structure.Operator.Properties
  open import Structure.Relator.Properties
  open import Structure.Setoid
  open import Syntax.Function
  open import Syntax.Transitivity

  eval : Polynomial(n) → (ℕ → ℕ)
  eval (singleton a)    _ = a
  eval (a ⊰ al@(_ ⊰ _)) x = a ℕ.+ (x ℕ.⋅ (eval al x))

  module Proofs where
    eval-of-[⊰] : ∀{x}{a}{al : Polynomial(n)} → (eval (a ⊰ al) x ≡ a ℕ.+ (x ℕ.⋅ (eval al x)))
    eval-of-[⊰] {ℕ.𝟎}   {x} {a} {b ⊰ ∅}      = reflexivity(_≡_)
    eval-of-[⊰] {ℕ.𝐒 n} {x} {a} {b ⊰ c ⊰ al} = reflexivity(_≡_)

    eval-preserves-var⋅ : ∀{x}{a : Polynomial(n)} → (eval (var⋅ a) x ≡ x ℕ.⋅ (eval a x))
    eval-preserves-var⋅ {n}{x}{a} = eval-of-[⊰] {n}{x}{ℕ.𝟎}{a}

    eval-preserves-zero : ∀{x} → (eval{n} 𝟎 x ≡ ℕ.𝟎)
    eval-preserves-zero {ℕ.𝟎}   {x} = reflexivity(_≡_)
    eval-preserves-zero {ℕ.𝐒 n} {x} =
      eval(𝟎 {ℕ.𝐒 n}) x              🝖[ _≡_ ]-[]
      eval(ℕ.𝟎 ⊰ 𝟎 {n}) x            🝖[ _≡_ ]-[]
      ℕ.𝟎 ℕ.+ (x ℕ.⋅ eval (𝟎 {n}) x) 🝖[ _≡_ ]-[]
      x ℕ.⋅ eval (𝟎 {n}) x           🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-zero{n}{x}) ]
      x ℕ.⋅ ℕ.𝟎                      🝖[ _≡_ ]-[ absorberᵣ(ℕ._⋅_)(ℕ.𝟎) {x} ]
      ℕ.𝟎                            🝖-end

    eval-preserves-const : ∀{x}{a} → (eval{n} (const a) x ≡ a)
    eval-preserves-const {ℕ.𝟎}   {x}{a} = reflexivity(_≡_)
    eval-preserves-const {ℕ.𝐒 n} {x}{a} =
      eval{ℕ.𝐒 n} (const a) x                  🝖[ _≡_ ]-[]
      eval(a ⊰ repeat ℕ.𝟎 (ℕ.𝐒 n)) x           🝖[ _≡_ ]-[ eval-of-[⊰] {x = x}{a}{repeat ℕ.𝟎 (ℕ.𝐒 n)} ]
      a ℕ.+ (x ℕ.⋅ eval(repeat ℕ.𝟎 (ℕ.𝐒 n)) x) 🝖[ _≡_ ]-[]
      a ℕ.+ (x ℕ.⋅ eval{n} 𝟎 x)                🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a) (eval-preserves-zero{ℕ.𝐒 n}{x = x}) ]
      a ℕ.+ (x ℕ.⋅ ℕ.𝟎)                        🝖[ _≡_ ]-[]
      a ℕ.+ ℕ.𝟎                                🝖[ _≡_ ]-[ identityᵣ(ℕ._+_)(ℕ.𝟎) ]
      a                                        🝖-end

    eval-preserves-one : ∀{x} → (eval{n} 𝟏 x ≡ ℕ.𝐒(ℕ.𝟎))
    eval-preserves-one {n}{x} = eval-preserves-const {n}{x}{ℕ.𝐒(ℕ.𝟎)}

    eval-preserves-var : ∀{x}{a : Polynomial(n)} → (eval (var{n}) x ≡ x)
    eval-preserves-var {n}{x}{a} =
      eval (var{n}) x      🝖[ _≡_ ]-[ eval-preserves-var⋅{n}{x}{𝟏} ]
      x ℕ.⋅ eval (𝟏 {n}) x 🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-one {n}{x}) ]
      x ℕ.⋅ ℕ.𝐒(ℕ.𝟎)       🝖[ _≡_ ]-[ identityᵣ(ℕ._⋅_)(ℕ.𝐒(ℕ.𝟎)) {x} ]
      x                    🝖-end

    eval-preserves-addition : ∀{x}{a : Polynomial(n₁)}{b : Polynomial(n₂)} → (eval (a + b) x ≡ (eval a x) ℕ.+ (eval b x))
    eval-preserves-addition {x = x} {singleton a}    {singleton b}    = reflexivity(_≡_)
    eval-preserves-addition {x = x} {singleton a}    {b ⊰ bs@(_ ⊰ _)} = associativity(ℕ._+_) {a}{b}
    eval-preserves-addition {x = x} {a ⊰ as@(_ ⊰ _)} {singleton b}    =
      eval ((a ⊰ as) + (singleton b)) x            🝖[ _≡_ ]-[]
      (a ℕ.+ b) ℕ.+ (x ℕ.⋅ (eval as x))            🝖[ _≡_ ]-[ associativity(ℕ._+_) {a}{b} ]
      a ℕ.+ (b ℕ.+ (x ℕ.⋅ (eval as x)))            🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a) (commutativity(ℕ._+_) {x = b}) ]
      a ℕ.+ ((x ℕ.⋅ (eval as x)) ℕ.+ b)            🝖[ _≡_ ]-[ associativity(ℕ._+_) {a}{x ℕ.⋅ eval as x} ]-sym
      (a ℕ.+ (x ℕ.⋅ (eval as x))) ℕ.+ b            🝖[ _≡_ ]-[]
      (eval (a ⊰ as) x) ℕ.+ (eval (singleton b) x) 🝖-end
    eval-preserves-addition {x = x} {a ⊰ as@(_ ⊰ _)} {b ⊰ bs@(_ ⊰ _)} =
      eval ((a ⊰ as) + (b ⊰ bs)) x                                  🝖[ _≡_ ]-[]
      eval ((a ℕ.+ b) ⊰ (as + bs)) x                                🝖[ _≡_ ]-[]
      (a ℕ.+ b) ℕ.+ (x ℕ.⋅ (eval (as + bs) x))                      🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.+ b) (congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-addition {x = x}{as}{bs})) ]
      (a ℕ.+ b) ℕ.+ (x ℕ.⋅ ((eval as x) ℕ.+ (eval bs x)))           🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.+ b) (distributivityₗ(ℕ._⋅_)(ℕ._+_) {x}{eval as x}{eval bs x}) ]
      (a ℕ.+ b) ℕ.+ ((x ℕ.⋅ (eval as x)) ℕ.+ (x ℕ.⋅ (eval bs x)))   🝖[ _≡_ ]-[ One.associate-commute4 {a = a}{b = b}{c = x ℕ.⋅ (eval as x)}{d = x ℕ.⋅ (eval bs x)} (commutativity(ℕ._+_) {b}) ]
      (a ℕ.+ (x ℕ.⋅ (eval as x))) ℕ.+ (b ℕ.+ (x ℕ.⋅ (eval bs x)))   🝖[ _≡_ ]-[]
      (eval (a ⊰ as) x) ℕ.+ (eval (b ⊰ bs) x)                       🝖-end

    eval-preserves-scalar-multiplication : ∀{x}{a}{b : Polynomial(n)} → (eval (a ⋅ b) x ≡ a ℕ.⋅ (eval b x))
    eval-preserves-scalar-multiplication {ℕ.𝟎}   {x} {a} {b ⊰ ∅} = reflexivity(_≡_)
    eval-preserves-scalar-multiplication {ℕ.𝐒 n} {x} {a} {b ⊰ bs@(_ ⊰ _)} =
      eval (a ⋅ (b ⊰ bs)) x                     🝖[ _≡_ ]-[]
      eval ((a ℕ.⋅ b) ⊰ (a ⋅ bs)) x             🝖[ _≡_ ]-[]
      (a ℕ.⋅ b) ℕ.+ (x ℕ.⋅ (eval (a ⋅ bs) x))   🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.⋅ b) (congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-scalar-multiplication {n} {x}{a}{bs})) ]
      (a ℕ.⋅ b) ℕ.+ (x ℕ.⋅ (a ℕ.⋅ (eval bs x))) 🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.⋅ b) (One.commuteₗ-assocᵣ {a = x}{b = a}{c = eval bs x}) ]
      (a ℕ.⋅ b) ℕ.+ (a ℕ.⋅ (x ℕ.⋅ (eval bs x))) 🝖[ _≡_ ]-[ distributivityₗ(ℕ._⋅_)(ℕ._+_) {x = a}{y = b}{z = x ℕ.⋅ (eval bs x)} ]-sym
      a ℕ.⋅ (b ℕ.+ (x ℕ.⋅ (eval bs x)))         🝖[ _≡_ ]-[]
      a ℕ.⋅ eval (b ⊰ bs) x                     🝖-end

    eval-preserves-pad : ∀{x}{a : Polynomial(n₁)} ⦃ ord : (n₁ ≤ n₂) ⦄ → (eval (pad ⦃ ord ⦄ a) x ≡ eval a x)
    eval-preserves-pad {ℕ.𝟎}    {ℕ.𝟎}    {x} {a ⊰ ∅}          ⦃ ord@min ⦄  = reflexivity(_≡_)
    eval-preserves-pad {ℕ.𝟎}    {ℕ.𝐒 n₂} {x} {a ⊰ ∅}          ⦃ ord@min ⦄  =
      eval (pad ⦃ ord ⦄ (a ⊰ ∅)) x  🝖[ _≡_ ]-[]
      a ℕ.+ (x ℕ.⋅ eval (𝟎 {n₂}) x) 🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a) (congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-zero{n₂}{x})) ]
      a ℕ.+ (x ℕ.⋅ ℕ.𝟎)             🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a) (absorberᵣ(ℕ._⋅_)(ℕ.𝟎) {x}) ]
      a ℕ.+ ℕ.𝟎                     🝖[ _≡_ ]-[ identityᵣ(ℕ._+_)(ℕ.𝟎) ]
      a                             🝖[ _≡_ ]-[]
      eval (a ⊰ ∅) x                🝖-end
    eval-preserves-pad {ℕ.𝐒 n₁} {ℕ.𝐒 n₂} {x} {a ⊰ as@(_ ⊰ _)} ⦃ ord@(succ p) ⦄ =
      eval (pad ⦃ ord ⦄ (a ⊰ as)) x       🝖[ _≡_ ]-[]
      eval (a ⊰ pad ⦃ _ ⦄ as) x           🝖[ _≡_ ]-[ eval-of-[⊰] {n₂}{x}{a}{pad ⦃ p ⦄ as} ]
      a ℕ.+ (x ℕ.⋅ eval (pad ⦃ _ ⦄ as) x) 🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a) (congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-pad {n₁}{n₂}{x}{as} ⦃ p ⦄)) ]
      a ℕ.+ (x ℕ.⋅ eval as x)       🝖[ _≡_ ]-[ eval-of-[⊰] {n₁}{x}{a}{as} ]-sym
      eval (a ⊰ as) x               🝖-end

    eval-preserves-multiplication : ∀{x}{a : Polynomial(n₁)}{b : Polynomial(n₂)} → (eval (a ⨯ b) x ≡ (eval a x) ℕ.⋅ (eval b x))
    eval-preserves-multiplication {n₁}    {ℕ.𝟎}   {x} {a ⊰ as}         {b ⊰ ∅}          =
      eval ((a ⊰ as) ⨯ (b ⊰ ∅)) x          🝖[ _≡_ ]-[]
      eval (b ⋅ (a ⊰ as)) x                🝖[ _≡_ ]-[ eval-preserves-scalar-multiplication {x = x}{b}{a ⊰ as} ]
      b ℕ.⋅ eval (a ⊰ as) x                🝖[ _≡_ ]-[ commutativity(ℕ._⋅_) {b}{eval(a ⊰ as) x} ]
      eval (a ⊰ as) x ℕ.⋅ b                🝖[ _≡_ ]-[]
      (eval (a ⊰ as) x ℕ.⋅ eval (b ⊰ ∅) x) 🝖-end
    eval-preserves-multiplication {ℕ.𝟎}   {ℕ.𝐒 n₂}{x} {a ⊰ ∅}          {b ⊰ bs@(_ ⊰ _)} =
      eval ((a ⊰ ∅) ⨯ (b ⊰ bs)) x        🝖[ _≡_ ]-[]
      eval (a ⋅ (b ⊰ bs)) x              🝖[ _≡_ ]-[ eval-preserves-scalar-multiplication {x = x}{a}{b ⊰ bs} ]
      a ℕ.⋅ (b ℕ.+ (x ℕ.⋅ eval bs x))    🝖[ _≡_ ]-[]
      eval (a ⊰ ∅) x ℕ.⋅ eval (b ⊰ bs) x 🝖-end
    eval-preserves-multiplication {ℕ.𝐒 n₁}{ℕ.𝐒 n₂}{x} {a ⊰ as@(_ ⊰ _)} {b ⊰ bs@(_ ⊰ _)} =
      eval((a ℕ.⋅ b) ⊰ lr) x                                                                                🝖[ _≡_ ]-[ eval-of-[⊰] {x = x}{a = a ℕ.⋅ b}{al = lr} ]
      (a ℕ.⋅ b) ℕ.+ (x ℕ.⋅ eval lr x)                                                                                🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.⋅ b) (congruence₂ᵣ(ℕ._⋅_)(x) eval-lr) ]
      (a ℕ.⋅ b) ℕ.+ (x ℕ.⋅ (((b ℕ.⋅ eval as x) ℕ.+ (a ℕ.⋅ eval bs x)) ℕ.+ (x ℕ.⋅ (eval as x ℕ.⋅ eval bs x))))                   🝖[ _≡_ ]-[ alg{a}{b}{x}{eval as x}{eval bs x} ]
      (a ℕ.+ (x ℕ.⋅ eval as x)) ℕ.⋅ (b ℕ.+ (x ℕ.⋅ eval bs x))                                                                   🝖[ _≡_ ]-[ congruence₂(ℕ._⋅_) (eval-of-[⊰] {x = x}{a = a}{al = as}) (eval-of-[⊰] {x = x}{a = b}{al = bs}) ]
      (eval(a ⊰ as) x ℕ.⋅ eval(b ⊰ bs) x)                                                                                🝖-end
      where
        open import Numeral.Natural.Function
        open import Numeral.Natural.Function.Proofs
        open import Numeral.Natural.Relation.Order.Proofs
        open import Relator.Equals using ([≡]-intro)

        l : Polynomial(n₁ ℕ.+ n₂)
        l = pad ⦃ max-order-[+] ⦄ ((b ⋅ as) + (a ⋅ bs))

        r : Polynomial(ℕ.𝐒(n₁ ℕ.+ n₂))
        r = var⋅ (as ⨯ bs)

        lr : Polynomial(ℕ.𝐒(n₁ ℕ.+ n₂))
        lr = [≡]-substitutionᵣ ([↔]-to-[→] max-defᵣ [≤]-of-[𝐒]) {Polynomial} (l + r)

        eval-l : (eval l x ≡ (b ℕ.⋅ eval as x) ℕ.+ (a ℕ.⋅ eval bs x))
        eval-l =
          eval l x                                             🝖[ _≡_ ]-[]
          eval (pad ⦃ max-order-[+] ⦄ ((b ⋅ as) + (a ⋅ bs))) x 🝖[ _≡_ ]-[ eval-preserves-pad {x = x}{(b ⋅ as) + (a ⋅ bs)} ⦃ max-order-[+] ⦄ ]
          eval ((b ⋅ as) + (a ⋅ bs)) x                         🝖[ _≡_ ]-[ eval-preserves-addition {x = x}{b ⋅ as}{a ⋅ bs} ]
          eval (b ⋅ as) x ℕ.+ eval (a ⋅ bs) x                  🝖[ _≡_ ]-[ congruence₂(ℕ._+_) (eval-preserves-scalar-multiplication {x = x}{b}{as}) (eval-preserves-scalar-multiplication {x = x}{a}{bs}) ]
          (b ℕ.⋅ eval as x) ℕ.+ (a ℕ.⋅ eval bs x)              🝖-end

        eval-r : (eval r x ≡ x ℕ.⋅ (eval as x ℕ.⋅ eval bs x))
        eval-r =
          eval r x                        🝖[ _≡_ ]-[]
          eval (var⋅ (as ⨯ bs)) x         🝖[ _≡_ ]-[ eval-preserves-var⋅ {x = x}{as ⨯ bs} ]
          x ℕ.⋅ eval (as ⨯ bs) x          🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._⋅_)(x) (eval-preserves-multiplication {x = x}{as}{bs}) ]
          x ℕ.⋅ (eval as x ℕ.⋅ eval bs x) 🝖-end

        eval-substitution : ∀{m n}{a : Polynomial(m)}{eq : (m ≡ n)}{x} → (eval ([≡]-substitutionᵣ eq {Polynomial} a) x ≡ eval a x)
        eval-substitution {eq = [≡]-intro} = [≡]-intro

        eval-lr : (eval lr x ≡ ((b ℕ.⋅ eval as x) ℕ.+ (a ℕ.⋅ eval bs x)) ℕ.+ (x ℕ.⋅ (eval as x ℕ.⋅ eval bs x)))
        eval-lr =
          eval lr x                                                                       🝖[ _≡_ ]-[ eval-substitution{a = l + r}{[↔]-to-[→] max-defᵣ [≤]-of-[𝐒]}{x = x} ]
          eval (l + r) x                                                                  🝖[ _≡_ ]-[ eval-preserves-addition{x = x}{l}{r} ]
          eval l x ℕ.+ eval r x                                                           🝖[ _≡_ ]-[ congruence₂(ℕ._+_) eval-l eval-r ]
          ((b ℕ.⋅ eval as x) ℕ.+ (a ℕ.⋅ eval bs x)) ℕ.+ (x ℕ.⋅ (eval as x ℕ.⋅ eval bs x)) 🝖-end

        alg : ∀{a b x q r} → ((a ℕ.⋅ b) ℕ.+ (x ℕ.⋅ (((b ℕ.⋅ q) ℕ.+ (a ℕ.⋅ r)) ℕ.+ (x ℕ.⋅ (q ℕ.⋅ r)))) ≡ (a ℕ.+ (x ℕ.⋅ q)) ℕ.⋅ (b ℕ.+ (x ℕ.⋅ r)))
        alg {a}{b}{x}{q}{r} =
          (a ℕ.⋅ b) ℕ.+ (x ℕ.⋅ (((b ℕ.⋅ q) ℕ.+ (a ℕ.⋅ r)) ℕ.+ (x ℕ.⋅ (q ℕ.⋅ r))))                   🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.⋅ b) (distributivityₗ(ℕ._⋅_)(ℕ._+_) {x}{(b ℕ.⋅ q) ℕ.+ (a ℕ.⋅ r)}{x ℕ.⋅ (q ℕ.⋅ r)}) ]
          (a ℕ.⋅ b) ℕ.+ ((x ℕ.⋅ ((b ℕ.⋅ q) ℕ.+ (a ℕ.⋅ r))) ℕ.+ (x ℕ.⋅ (x ℕ.⋅ (q ℕ.⋅ r))))           🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.⋅ b) (congruence₂(ℕ._+_) (distributivityₗ(ℕ._⋅_)(ℕ._+_) {x}{b ℕ.⋅ q}{a ℕ.⋅ r}) (symmetry(_≡_) (associativity(ℕ._⋅_) {x}{x}{q ℕ.⋅ r}))) ]
          (a ℕ.⋅ b) ℕ.+ (((x ℕ.⋅ (b ℕ.⋅ q)) ℕ.+ (x ℕ.⋅ (a ℕ.⋅ r))) ℕ.+ ((x ℕ.⋅ x) ℕ.⋅ (q ℕ.⋅ r)))   🝖[ _≡_ ]-[ congruence₂ᵣ(ℕ._+_)(a ℕ.⋅ b) (congruence₂(ℕ._+_) (congruence₂(ℕ._+_) (One.commuteᵣ-assocᵣ {_▫_ = ℕ._⋅_}{a = x}{b}{q}) (One.commuteₗ-assocᵣ {_▫_ = ℕ._⋅_}{a = x}{a}{r})) (One.associate-commute4-c {_▫_ = ℕ._⋅_}{a = x}{x}{q}{r})) ]
          (a ℕ.⋅ b) ℕ.+ ((((x ℕ.⋅ q) ℕ.⋅ b) ℕ.+ (a ℕ.⋅ (x ℕ.⋅ r))) ℕ.+ ((x ℕ.⋅ q) ℕ.⋅ (x ℕ.⋅ r)))   🝖[ _≡_ ]-[ One.associate4-231-222 {_▫_ = ℕ._+_} {a = a ℕ.⋅ b}{(x ℕ.⋅ q) ℕ.⋅ b}{a ℕ.⋅ (x ℕ.⋅ r)}{(x ℕ.⋅ q) ℕ.⋅ (x ℕ.⋅ r)} ]
          ((a ℕ.⋅ b) ℕ.+ ((x ℕ.⋅ q) ℕ.⋅ b)) ℕ.+ ((a ℕ.⋅ (x ℕ.⋅ r)) ℕ.+ ((x ℕ.⋅ q) ℕ.⋅ (x ℕ.⋅ r)))   🝖[ _≡_ ]-[ OneTypeTwoOp.cross-distribute{a = a}{x ℕ.⋅ q}{b}{x ℕ.⋅ r} ]-sym
          (a ℕ.+ (x ℕ.⋅ q)) ℕ.⋅ (b ℕ.+ (x ℕ.⋅ r))                                                   🝖-end

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Text.Greek.SBLGNT.Titus where

open import Data.List
open import Text.Greek.Bible
open import Text.Greek.Script
open import Text.Greek.Script.Unicode

ΠΡΟΣ-ΤΙΤΟΝ : List (Word)
ΠΡΟΣ-ΤΙΤΟΝ =
    word (Π ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "Titus.1.1"
  ∷ word (δ ∷ ο ∷ ῦ ∷ ∙λ ∷ ο ∷ ς ∷ []) "Titus.1.1"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.1.1"
  ∷ word (ἀ ∷ π ∷ ό ∷ σ ∷ τ ∷ ο ∷ ∙λ ∷ ο ∷ ς ∷ []) "Titus.1.1"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.1.1"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Titus.1.1"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.1.1"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Titus.1.1"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Titus.1.1"
  ∷ word (ἐ ∷ κ ∷ ∙λ ∷ ε ∷ κ ∷ τ ∷ ῶ ∷ ν ∷ []) "Titus.1.1"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.1.1"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.1"
  ∷ word (ἐ ∷ π ∷ ί ∷ γ ∷ ν ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "Titus.1.1"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "Titus.1.1"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Titus.1.1"
  ∷ word (κ ∷ α ∷ τ ∷ []) "Titus.1.1"
  ∷ word (ε ∷ ὐ ∷ σ ∷ έ ∷ β ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "Titus.1.1"
  ∷ word (ἐ ∷ π ∷ []) "Titus.1.2"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ δ ∷ ι ∷ []) "Titus.1.2"
  ∷ word (ζ ∷ ω ∷ ῆ ∷ ς ∷ []) "Titus.1.2"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ ο ∷ υ ∷ []) "Titus.1.2"
  ∷ word (ἣ ∷ ν ∷ []) "Titus.1.2"
  ∷ word (ἐ ∷ π ∷ η ∷ γ ∷ γ ∷ ε ∷ ί ∷ ∙λ ∷ α ∷ τ ∷ ο ∷ []) "Titus.1.2"
  ∷ word (ὁ ∷ []) "Titus.1.2"
  ∷ word (ἀ ∷ ψ ∷ ε ∷ υ ∷ δ ∷ ὴ ∷ ς ∷ []) "Titus.1.2"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ς ∷ []) "Titus.1.2"
  ∷ word (π ∷ ρ ∷ ὸ ∷ []) "Titus.1.2"
  ∷ word (χ ∷ ρ ∷ ό ∷ ν ∷ ω ∷ ν ∷ []) "Titus.1.2"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ ω ∷ ν ∷ []) "Titus.1.2"
  ∷ word (ἐ ∷ φ ∷ α ∷ ν ∷ έ ∷ ρ ∷ ω ∷ σ ∷ ε ∷ ν ∷ []) "Titus.1.3"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.1.3"
  ∷ word (κ ∷ α ∷ ι ∷ ρ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.1.3"
  ∷ word (ἰ ∷ δ ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "Titus.1.3"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Titus.1.3"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ν ∷ []) "Titus.1.3"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.1.3"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.1.3"
  ∷ word (κ ∷ η ∷ ρ ∷ ύ ∷ γ ∷ μ ∷ α ∷ τ ∷ ι ∷ []) "Titus.1.3"
  ∷ word (ὃ ∷ []) "Titus.1.3"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ε ∷ ύ ∷ θ ∷ η ∷ ν ∷ []) "Titus.1.3"
  ∷ word (ἐ ∷ γ ∷ ὼ ∷ []) "Titus.1.3"
  ∷ word (κ ∷ α ∷ τ ∷ []) "Titus.1.3"
  ∷ word (ἐ ∷ π ∷ ι ∷ τ ∷ α ∷ γ ∷ ὴ ∷ ν ∷ []) "Titus.1.3"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.1.3"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "Titus.1.3"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.1.3"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.1.3"
  ∷ word (Τ ∷ ί ∷ τ ∷ ῳ ∷ []) "Titus.1.4"
  ∷ word (γ ∷ ν ∷ η ∷ σ ∷ ί ∷ ῳ ∷ []) "Titus.1.4"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ ῳ ∷ []) "Titus.1.4"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Titus.1.4"
  ∷ word (κ ∷ ο ∷ ι ∷ ν ∷ ὴ ∷ ν ∷ []) "Titus.1.4"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Titus.1.4"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "Titus.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.4"
  ∷ word (ε ∷ ἰ ∷ ρ ∷ ή ∷ ν ∷ η ∷ []) "Titus.1.4"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "Titus.1.4"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.1.4"
  ∷ word (π ∷ α ∷ τ ∷ ρ ∷ ὸ ∷ ς ∷ []) "Titus.1.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.4"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.1.4"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Titus.1.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.1.4"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "Titus.1.4"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.1.4"
  ∷ word (Τ ∷ ο ∷ ύ ∷ τ ∷ ο ∷ υ ∷ []) "Titus.1.5"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ν ∷ []) "Titus.1.5"
  ∷ word (ἀ ∷ π ∷ έ ∷ ∙λ ∷ ι ∷ π ∷ ό ∷ ν ∷ []) "Titus.1.5"
  ∷ word (σ ∷ ε ∷ []) "Titus.1.5"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.1.5"
  ∷ word (Κ ∷ ρ ∷ ή ∷ τ ∷ ῃ ∷ []) "Titus.1.5"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.1.5"
  ∷ word (τ ∷ ὰ ∷ []) "Titus.1.5"
  ∷ word (∙λ ∷ ε ∷ ί ∷ π ∷ ο ∷ ν ∷ τ ∷ α ∷ []) "Titus.1.5"
  ∷ word (ἐ ∷ π ∷ ι ∷ δ ∷ ι ∷ ο ∷ ρ ∷ θ ∷ ώ ∷ σ ∷ ῃ ∷ []) "Titus.1.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.5"
  ∷ word (κ ∷ α ∷ τ ∷ α ∷ σ ∷ τ ∷ ή ∷ σ ∷ ῃ ∷ ς ∷ []) "Titus.1.5"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Titus.1.5"
  ∷ word (π ∷ ό ∷ ∙λ ∷ ι ∷ ν ∷ []) "Titus.1.5"
  ∷ word (π ∷ ρ ∷ ε ∷ σ ∷ β ∷ υ ∷ τ ∷ έ ∷ ρ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.1.5"
  ∷ word (ὡ ∷ ς ∷ []) "Titus.1.5"
  ∷ word (ἐ ∷ γ ∷ ώ ∷ []) "Titus.1.5"
  ∷ word (σ ∷ ο ∷ ι ∷ []) "Titus.1.5"
  ∷ word (δ ∷ ι ∷ ε ∷ τ ∷ α ∷ ξ ∷ ά ∷ μ ∷ η ∷ ν ∷ []) "Titus.1.5"
  ∷ word (ε ∷ ἴ ∷ []) "Titus.1.6"
  ∷ word (τ ∷ ί ∷ ς ∷ []) "Titus.1.6"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Titus.1.6"
  ∷ word (ἀ ∷ ν ∷ έ ∷ γ ∷ κ ∷ ∙λ ∷ η ∷ τ ∷ ο ∷ ς ∷ []) "Titus.1.6"
  ∷ word (μ ∷ ι ∷ ᾶ ∷ ς ∷ []) "Titus.1.6"
  ∷ word (γ ∷ υ ∷ ν ∷ α ∷ ι ∷ κ ∷ ὸ ∷ ς ∷ []) "Titus.1.6"
  ∷ word (ἀ ∷ ν ∷ ή ∷ ρ ∷ []) "Titus.1.6"
  ∷ word (τ ∷ έ ∷ κ ∷ ν ∷ α ∷ []) "Titus.1.6"
  ∷ word (ἔ ∷ χ ∷ ω ∷ ν ∷ []) "Titus.1.6"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ά ∷ []) "Titus.1.6"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.6"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.1.6"
  ∷ word (κ ∷ α ∷ τ ∷ η ∷ γ ∷ ο ∷ ρ ∷ ί ∷ ᾳ ∷ []) "Titus.1.6"
  ∷ word (ἀ ∷ σ ∷ ω ∷ τ ∷ ί ∷ α ∷ ς ∷ []) "Titus.1.6"
  ∷ word (ἢ ∷ []) "Titus.1.6"
  ∷ word (ἀ ∷ ν ∷ υ ∷ π ∷ ό ∷ τ ∷ α ∷ κ ∷ τ ∷ α ∷ []) "Titus.1.6"
  ∷ word (δ ∷ ε ∷ ῖ ∷ []) "Titus.1.7"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Titus.1.7"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Titus.1.7"
  ∷ word (ἐ ∷ π ∷ ί ∷ σ ∷ κ ∷ ο ∷ π ∷ ο ∷ ν ∷ []) "Titus.1.7"
  ∷ word (ἀ ∷ ν ∷ έ ∷ γ ∷ κ ∷ ∙λ ∷ η ∷ τ ∷ ο ∷ ν ∷ []) "Titus.1.7"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "Titus.1.7"
  ∷ word (ὡ ∷ ς ∷ []) "Titus.1.7"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.1.7"
  ∷ word (ο ∷ ἰ ∷ κ ∷ ο ∷ ν ∷ ό ∷ μ ∷ ο ∷ ν ∷ []) "Titus.1.7"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.7"
  ∷ word (α ∷ ὐ ∷ θ ∷ ά ∷ δ ∷ η ∷ []) "Titus.1.7"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.7"
  ∷ word (ὀ ∷ ρ ∷ γ ∷ ί ∷ ∙λ ∷ ο ∷ ν ∷ []) "Titus.1.7"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.7"
  ∷ word (π ∷ ά ∷ ρ ∷ ο ∷ ι ∷ ν ∷ ο ∷ ν ∷ []) "Titus.1.7"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.7"
  ∷ word (π ∷ ∙λ ∷ ή ∷ κ ∷ τ ∷ η ∷ ν ∷ []) "Titus.1.7"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.7"
  ∷ word (α ∷ ἰ ∷ σ ∷ χ ∷ ρ ∷ ο ∷ κ ∷ ε ∷ ρ ∷ δ ∷ ῆ ∷ []) "Titus.1.7"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Titus.1.8"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ό ∷ ξ ∷ ε ∷ ν ∷ ο ∷ ν ∷ []) "Titus.1.8"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ά ∷ γ ∷ α ∷ θ ∷ ο ∷ ν ∷ []) "Titus.1.8"
  ∷ word (σ ∷ ώ ∷ φ ∷ ρ ∷ ο ∷ ν ∷ α ∷ []) "Titus.1.8"
  ∷ word (δ ∷ ί ∷ κ ∷ α ∷ ι ∷ ο ∷ ν ∷ []) "Titus.1.8"
  ∷ word (ὅ ∷ σ ∷ ι ∷ ο ∷ ν ∷ []) "Titus.1.8"
  ∷ word (ἐ ∷ γ ∷ κ ∷ ρ ∷ α ∷ τ ∷ ῆ ∷ []) "Titus.1.8"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ε ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ν ∷ []) "Titus.1.9"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.1.9"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Titus.1.9"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Titus.1.9"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ χ ∷ ὴ ∷ ν ∷ []) "Titus.1.9"
  ∷ word (π ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.1.9"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ υ ∷ []) "Titus.1.9"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.1.9"
  ∷ word (δ ∷ υ ∷ ν ∷ α ∷ τ ∷ ὸ ∷ ς ∷ []) "Titus.1.9"
  ∷ word (ᾖ ∷ []) "Titus.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.9"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ α ∷ ∙λ ∷ ε ∷ ῖ ∷ ν ∷ []) "Titus.1.9"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.1.9"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.1.9"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ ᾳ ∷ []) "Titus.1.9"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.1.9"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ι ∷ ν ∷ ο ∷ ύ ∷ σ ∷ ῃ ∷ []) "Titus.1.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.9"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Titus.1.9"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ι ∷ ∙λ ∷ έ ∷ γ ∷ ο ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Titus.1.9"
  ∷ word (ἐ ∷ ∙λ ∷ έ ∷ γ ∷ χ ∷ ε ∷ ι ∷ ν ∷ []) "Titus.1.9"
  ∷ word (Ε ∷ ἰ ∷ σ ∷ ὶ ∷ ν ∷ []) "Titus.1.10"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Titus.1.10"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ο ∷ ὶ ∷ []) "Titus.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.10"
  ∷ word (ἀ ∷ ν ∷ υ ∷ π ∷ ό ∷ τ ∷ α ∷ κ ∷ τ ∷ ο ∷ ι ∷ []) "Titus.1.10"
  ∷ word (μ ∷ α ∷ τ ∷ α ∷ ι ∷ ο ∷ ∙λ ∷ ό ∷ γ ∷ ο ∷ ι ∷ []) "Titus.1.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.10"
  ∷ word (φ ∷ ρ ∷ ε ∷ ν ∷ α ∷ π ∷ ά ∷ τ ∷ α ∷ ι ∷ []) "Titus.1.10"
  ∷ word (μ ∷ ά ∷ ∙λ ∷ ι ∷ σ ∷ τ ∷ α ∷ []) "Titus.1.10"
  ∷ word (ο ∷ ἱ ∷ []) "Titus.1.10"
  ∷ word (ἐ ∷ κ ∷ []) "Titus.1.10"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Titus.1.10"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ τ ∷ ο ∷ μ ∷ ῆ ∷ ς ∷ []) "Titus.1.10"
  ∷ word (ο ∷ ὓ ∷ ς ∷ []) "Titus.1.11"
  ∷ word (δ ∷ ε ∷ ῖ ∷ []) "Titus.1.11"
  ∷ word (ἐ ∷ π ∷ ι ∷ σ ∷ τ ∷ ο ∷ μ ∷ ί ∷ ζ ∷ ε ∷ ι ∷ ν ∷ []) "Titus.1.11"
  ∷ word (ο ∷ ἵ ∷ τ ∷ ι ∷ ν ∷ ε ∷ ς ∷ []) "Titus.1.11"
  ∷ word (ὅ ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.1.11"
  ∷ word (ο ∷ ἴ ∷ κ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.1.11"
  ∷ word (ἀ ∷ ν ∷ α ∷ τ ∷ ρ ∷ έ ∷ π ∷ ο ∷ υ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.1.11"
  ∷ word (δ ∷ ι ∷ δ ∷ ά ∷ σ ∷ κ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.1.11"
  ∷ word (ἃ ∷ []) "Titus.1.11"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.11"
  ∷ word (δ ∷ ε ∷ ῖ ∷ []) "Titus.1.11"
  ∷ word (α ∷ ἰ ∷ σ ∷ χ ∷ ρ ∷ ο ∷ ῦ ∷ []) "Titus.1.11"
  ∷ word (κ ∷ έ ∷ ρ ∷ δ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.1.11"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ν ∷ []) "Titus.1.11"
  ∷ word (ε ∷ ἶ ∷ π ∷ έ ∷ ν ∷ []) "Titus.1.12"
  ∷ word (τ ∷ ι ∷ ς ∷ []) "Titus.1.12"
  ∷ word (ἐ ∷ ξ ∷ []) "Titus.1.12"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "Titus.1.12"
  ∷ word (ἴ ∷ δ ∷ ι ∷ ο ∷ ς ∷ []) "Titus.1.12"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "Titus.1.12"
  ∷ word (π ∷ ρ ∷ ο ∷ φ ∷ ή ∷ τ ∷ η ∷ ς ∷ []) "Titus.1.12"
  ∷ word (Κ ∷ ρ ∷ ῆ ∷ τ ∷ ε ∷ ς ∷ []) "Titus.1.12"
  ∷ word (ἀ ∷ ε ∷ ὶ ∷ []) "Titus.1.12"
  ∷ word (ψ ∷ ε ∷ ῦ ∷ σ ∷ τ ∷ α ∷ ι ∷ []) "Titus.1.12"
  ∷ word (κ ∷ α ∷ κ ∷ ὰ ∷ []) "Titus.1.12"
  ∷ word (θ ∷ η ∷ ρ ∷ ί ∷ α ∷ []) "Titus.1.12"
  ∷ word (γ ∷ α ∷ σ ∷ τ ∷ έ ∷ ρ ∷ ε ∷ ς ∷ []) "Titus.1.12"
  ∷ word (ἀ ∷ ρ ∷ γ ∷ α ∷ ί ∷ []) "Titus.1.12"
  ∷ word (ἡ ∷ []) "Titus.1.13"
  ∷ word (μ ∷ α ∷ ρ ∷ τ ∷ υ ∷ ρ ∷ ί ∷ α ∷ []) "Titus.1.13"
  ∷ word (α ∷ ὕ ∷ τ ∷ η ∷ []) "Titus.1.13"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ὶ ∷ ν ∷ []) "Titus.1.13"
  ∷ word (ἀ ∷ ∙λ ∷ η ∷ θ ∷ ή ∷ ς ∷ []) "Titus.1.13"
  ∷ word (δ ∷ ι ∷ []) "Titus.1.13"
  ∷ word (ἣ ∷ ν ∷ []) "Titus.1.13"
  ∷ word (α ∷ ἰ ∷ τ ∷ ί ∷ α ∷ ν ∷ []) "Titus.1.13"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ γ ∷ χ ∷ ε ∷ []) "Titus.1.13"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Titus.1.13"
  ∷ word (ἀ ∷ π ∷ ο ∷ τ ∷ ό ∷ μ ∷ ω ∷ ς ∷ []) "Titus.1.13"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.1.13"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ί ∷ ν ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "Titus.1.13"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.1.13"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.1.13"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "Titus.1.13"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.1.14"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ έ ∷ χ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.1.14"
  ∷ word (Ἰ ∷ ο ∷ υ ∷ δ ∷ α ∷ ϊ ∷ κ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.1.14"
  ∷ word (μ ∷ ύ ∷ θ ∷ ο ∷ ι ∷ ς ∷ []) "Titus.1.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.14"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ο ∷ ∙λ ∷ α ∷ ῖ ∷ ς ∷ []) "Titus.1.14"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ρ ∷ ώ ∷ π ∷ ω ∷ ν ∷ []) "Titus.1.14"
  ∷ word (ἀ ∷ π ∷ ο ∷ σ ∷ τ ∷ ρ ∷ ε ∷ φ ∷ ο ∷ μ ∷ έ ∷ ν ∷ ω ∷ ν ∷ []) "Titus.1.14"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Titus.1.14"
  ∷ word (ἀ ∷ ∙λ ∷ ή ∷ θ ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "Titus.1.14"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ []) "Titus.1.15"
  ∷ word (κ ∷ α ∷ θ ∷ α ∷ ρ ∷ ὰ ∷ []) "Titus.1.15"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.1.15"
  ∷ word (κ ∷ α ∷ θ ∷ α ∷ ρ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.1.15"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.1.15"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.1.15"
  ∷ word (μ ∷ ε ∷ μ ∷ ι ∷ α ∷ μ ∷ μ ∷ έ ∷ ν ∷ ο ∷ ι ∷ ς ∷ []) "Titus.1.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.15"
  ∷ word (ἀ ∷ π ∷ ί ∷ σ ∷ τ ∷ ο ∷ ι ∷ ς ∷ []) "Titus.1.15"
  ∷ word (ο ∷ ὐ ∷ δ ∷ ὲ ∷ ν ∷ []) "Titus.1.15"
  ∷ word (κ ∷ α ∷ θ ∷ α ∷ ρ ∷ ό ∷ ν ∷ []) "Titus.1.15"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Titus.1.15"
  ∷ word (μ ∷ ε ∷ μ ∷ ί ∷ α ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "Titus.1.15"
  ∷ word (α ∷ ὐ ∷ τ ∷ ῶ ∷ ν ∷ []) "Titus.1.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.15"
  ∷ word (ὁ ∷ []) "Titus.1.15"
  ∷ word (ν ∷ ο ∷ ῦ ∷ ς ∷ []) "Titus.1.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.15"
  ∷ word (ἡ ∷ []) "Titus.1.15"
  ∷ word (σ ∷ υ ∷ ν ∷ ε ∷ ί ∷ δ ∷ η ∷ σ ∷ ι ∷ ς ∷ []) "Titus.1.15"
  ∷ word (θ ∷ ε ∷ ὸ ∷ ν ∷ []) "Titus.1.16"
  ∷ word (ὁ ∷ μ ∷ ο ∷ ∙λ ∷ ο ∷ γ ∷ ο ∷ ῦ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.1.16"
  ∷ word (ε ∷ ἰ ∷ δ ∷ έ ∷ ν ∷ α ∷ ι ∷ []) "Titus.1.16"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.1.16"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.1.16"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ι ∷ ς ∷ []) "Titus.1.16"
  ∷ word (ἀ ∷ ρ ∷ ν ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ ι ∷ []) "Titus.1.16"
  ∷ word (β ∷ δ ∷ ε ∷ ∙λ ∷ υ ∷ κ ∷ τ ∷ ο ∷ ὶ ∷ []) "Titus.1.16"
  ∷ word (ὄ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.1.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.16"
  ∷ word (ἀ ∷ π ∷ ε ∷ ι ∷ θ ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.1.16"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.1.16"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Titus.1.16"
  ∷ word (π ∷ ᾶ ∷ ν ∷ []) "Titus.1.16"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ν ∷ []) "Titus.1.16"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ὸ ∷ ν ∷ []) "Titus.1.16"
  ∷ word (ἀ ∷ δ ∷ ό ∷ κ ∷ ι ∷ μ ∷ ο ∷ ι ∷ []) "Titus.1.16"
  ∷ word (Σ ∷ ὺ ∷ []) "Titus.2.1"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.2.1"
  ∷ word (∙λ ∷ ά ∷ ∙λ ∷ ε ∷ ι ∷ []) "Titus.2.1"
  ∷ word (ἃ ∷ []) "Titus.2.1"
  ∷ word (π ∷ ρ ∷ έ ∷ π ∷ ε ∷ ι ∷ []) "Titus.2.1"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.2.1"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ι ∷ ν ∷ ο ∷ ύ ∷ σ ∷ ῃ ∷ []) "Titus.2.1"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ ᾳ ∷ []) "Titus.2.1"
  ∷ word (π ∷ ρ ∷ ε ∷ σ ∷ β ∷ ύ ∷ τ ∷ α ∷ ς ∷ []) "Titus.2.2"
  ∷ word (ν ∷ η ∷ φ ∷ α ∷ ∙λ ∷ ί ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.2"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "Titus.2.2"
  ∷ word (σ ∷ ε ∷ μ ∷ ν ∷ ο ∷ ύ ∷ ς ∷ []) "Titus.2.2"
  ∷ word (σ ∷ ώ ∷ φ ∷ ρ ∷ ο ∷ ν ∷ α ∷ ς ∷ []) "Titus.2.2"
  ∷ word (ὑ ∷ γ ∷ ι ∷ α ∷ ί ∷ ν ∷ ο ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Titus.2.2"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.2.2"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "Titus.2.2"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.2.2"
  ∷ word (ἀ ∷ γ ∷ ά ∷ π ∷ ῃ ∷ []) "Titus.2.2"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.2.2"
  ∷ word (ὑ ∷ π ∷ ο ∷ μ ∷ ο ∷ ν ∷ ῇ ∷ []) "Titus.2.2"
  ∷ word (Π ∷ ρ ∷ ε ∷ σ ∷ β ∷ ύ ∷ τ ∷ ι ∷ δ ∷ α ∷ ς ∷ []) "Titus.2.3"
  ∷ word (ὡ ∷ σ ∷ α ∷ ύ ∷ τ ∷ ω ∷ ς ∷ []) "Titus.2.3"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.2.3"
  ∷ word (κ ∷ α ∷ τ ∷ α ∷ σ ∷ τ ∷ ή ∷ μ ∷ α ∷ τ ∷ ι ∷ []) "Titus.2.3"
  ∷ word (ἱ ∷ ε ∷ ρ ∷ ο ∷ π ∷ ρ ∷ ε ∷ π ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.2.3"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.2.3"
  ∷ word (δ ∷ ι ∷ α ∷ β ∷ ό ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.3"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ []) "Titus.2.3"
  ∷ word (ο ∷ ἴ ∷ ν ∷ ῳ ∷ []) "Titus.2.3"
  ∷ word (π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ῷ ∷ []) "Titus.2.3"
  ∷ word (δ ∷ ε ∷ δ ∷ ο ∷ υ ∷ ∙λ ∷ ω ∷ μ ∷ έ ∷ ν ∷ α ∷ ς ∷ []) "Titus.2.3"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ο ∷ δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ ά ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.3"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.2.4"
  ∷ word (σ ∷ ω ∷ φ ∷ ρ ∷ ο ∷ ν ∷ ί ∷ ζ ∷ ω ∷ σ ∷ ι ∷ []) "Titus.2.4"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "Titus.2.4"
  ∷ word (ν ∷ έ ∷ α ∷ ς ∷ []) "Titus.2.4"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ά ∷ ν ∷ δ ∷ ρ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.4"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "Titus.2.4"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ο ∷ τ ∷ έ ∷ κ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.4"
  ∷ word (σ ∷ ώ ∷ φ ∷ ρ ∷ ο ∷ ν ∷ α ∷ ς ∷ []) "Titus.2.5"
  ∷ word (ἁ ∷ γ ∷ ν ∷ ά ∷ ς ∷ []) "Titus.2.5"
  ∷ word (ο ∷ ἰ ∷ κ ∷ ο ∷ υ ∷ ρ ∷ γ ∷ ο ∷ ύ ∷ ς ∷ []) "Titus.2.5"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ά ∷ ς ∷ []) "Titus.2.5"
  ∷ word (ὑ ∷ π ∷ ο ∷ τ ∷ α ∷ σ ∷ σ ∷ ο ∷ μ ∷ έ ∷ ν ∷ α ∷ ς ∷ []) "Titus.2.5"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.2.5"
  ∷ word (ἰ ∷ δ ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "Titus.2.5"
  ∷ word (ἀ ∷ ν ∷ δ ∷ ρ ∷ ά ∷ σ ∷ ι ∷ ν ∷ []) "Titus.2.5"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.2.5"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.2.5"
  ∷ word (ὁ ∷ []) "Titus.2.5"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ς ∷ []) "Titus.2.5"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.2.5"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.2.5"
  ∷ word (β ∷ ∙λ ∷ α ∷ σ ∷ φ ∷ η ∷ μ ∷ ῆ ∷ τ ∷ α ∷ ι ∷ []) "Titus.2.5"
  ∷ word (Τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Titus.2.6"
  ∷ word (ν ∷ ε ∷ ω ∷ τ ∷ έ ∷ ρ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.6"
  ∷ word (ὡ ∷ σ ∷ α ∷ ύ ∷ τ ∷ ω ∷ ς ∷ []) "Titus.2.6"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ ά ∷ ∙λ ∷ ε ∷ ι ∷ []) "Titus.2.6"
  ∷ word (σ ∷ ω ∷ φ ∷ ρ ∷ ο ∷ ν ∷ ε ∷ ῖ ∷ ν ∷ []) "Titus.2.6"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Titus.2.7"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ []) "Titus.2.7"
  ∷ word (σ ∷ ε ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "Titus.2.7"
  ∷ word (π ∷ α ∷ ρ ∷ ε ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ς ∷ []) "Titus.2.7"
  ∷ word (τ ∷ ύ ∷ π ∷ ο ∷ ν ∷ []) "Titus.2.7"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "Titus.2.7"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ω ∷ ν ∷ []) "Titus.2.7"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.2.7"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.2.7"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ ᾳ ∷ []) "Titus.2.7"
  ∷ word (ἀ ∷ φ ∷ θ ∷ ο ∷ ρ ∷ ί ∷ α ∷ ν ∷ []) "Titus.2.7"
  ∷ word (σ ∷ ε ∷ μ ∷ ν ∷ ό ∷ τ ∷ η ∷ τ ∷ α ∷ []) "Titus.2.7"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ν ∷ []) "Titus.2.8"
  ∷ word (ὑ ∷ γ ∷ ι ∷ ῆ ∷ []) "Titus.2.8"
  ∷ word (ἀ ∷ κ ∷ α ∷ τ ∷ ά ∷ γ ∷ ν ∷ ω ∷ σ ∷ τ ∷ ο ∷ ν ∷ []) "Titus.2.8"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.2.8"
  ∷ word (ὁ ∷ []) "Titus.2.8"
  ∷ word (ἐ ∷ ξ ∷ []) "Titus.2.8"
  ∷ word (ἐ ∷ ν ∷ α ∷ ν ∷ τ ∷ ί ∷ α ∷ ς ∷ []) "Titus.2.8"
  ∷ word (ἐ ∷ ν ∷ τ ∷ ρ ∷ α ∷ π ∷ ῇ ∷ []) "Titus.2.8"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ ν ∷ []) "Titus.2.8"
  ∷ word (ἔ ∷ χ ∷ ω ∷ ν ∷ []) "Titus.2.8"
  ∷ word (∙λ ∷ έ ∷ γ ∷ ε ∷ ι ∷ ν ∷ []) "Titus.2.8"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Titus.2.8"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.2.8"
  ∷ word (φ ∷ α ∷ ῦ ∷ ∙λ ∷ ο ∷ ν ∷ []) "Titus.2.8"
  ∷ word (Δ ∷ ο ∷ ύ ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.9"
  ∷ word (ἰ ∷ δ ∷ ί ∷ ο ∷ ι ∷ ς ∷ []) "Titus.2.9"
  ∷ word (δ ∷ ε ∷ σ ∷ π ∷ ό ∷ τ ∷ α ∷ ι ∷ ς ∷ []) "Titus.2.9"
  ∷ word (ὑ ∷ π ∷ ο ∷ τ ∷ ά ∷ σ ∷ σ ∷ ε ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "Titus.2.9"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.2.9"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.2.9"
  ∷ word (ε ∷ ὐ ∷ α ∷ ρ ∷ έ ∷ σ ∷ τ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.9"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "Titus.2.9"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.2.9"
  ∷ word (ἀ ∷ ν ∷ τ ∷ ι ∷ ∙λ ∷ έ ∷ γ ∷ ο ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Titus.2.9"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.2.10"
  ∷ word (ν ∷ ο ∷ σ ∷ φ ∷ ι ∷ ζ ∷ ο ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.10"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Titus.2.10"
  ∷ word (π ∷ ᾶ ∷ σ ∷ α ∷ ν ∷ []) "Titus.2.10"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Titus.2.10"
  ∷ word (ἐ ∷ ν ∷ δ ∷ ε ∷ ι ∷ κ ∷ ν ∷ υ ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "Titus.2.10"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ή ∷ ν ∷ []) "Titus.2.10"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.2.10"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Titus.2.10"
  ∷ word (δ ∷ ι ∷ δ ∷ α ∷ σ ∷ κ ∷ α ∷ ∙λ ∷ ί ∷ α ∷ ν ∷ []) "Titus.2.10"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Titus.2.10"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.2.10"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "Titus.2.10"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.2.10"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.2.10"
  ∷ word (κ ∷ ο ∷ σ ∷ μ ∷ ῶ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.2.10"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.2.10"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.2.10"
  ∷ word (Ἐ ∷ π ∷ ε ∷ φ ∷ ά ∷ ν ∷ η ∷ []) "Titus.2.11"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Titus.2.11"
  ∷ word (ἡ ∷ []) "Titus.2.11"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "Titus.2.11"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.2.11"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.2.11"
  ∷ word (σ ∷ ω ∷ τ ∷ ή ∷ ρ ∷ ι ∷ ο ∷ ς ∷ []) "Titus.2.11"
  ∷ word (π ∷ ᾶ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.2.11"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ρ ∷ ώ ∷ π ∷ ο ∷ ι ∷ ς ∷ []) "Titus.2.11"
  ∷ word (π ∷ α ∷ ι ∷ δ ∷ ε ∷ ύ ∷ ο ∷ υ ∷ σ ∷ α ∷ []) "Titus.2.12"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Titus.2.12"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.2.12"
  ∷ word (ἀ ∷ ρ ∷ ν ∷ η ∷ σ ∷ ά ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Titus.2.12"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Titus.2.12"
  ∷ word (ἀ ∷ σ ∷ έ ∷ β ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "Titus.2.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.12"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "Titus.2.12"
  ∷ word (κ ∷ ο ∷ σ ∷ μ ∷ ι ∷ κ ∷ ὰ ∷ ς ∷ []) "Titus.2.12"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "Titus.2.12"
  ∷ word (σ ∷ ω ∷ φ ∷ ρ ∷ ό ∷ ν ∷ ω ∷ ς ∷ []) "Titus.2.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.12"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ί ∷ ω ∷ ς ∷ []) "Titus.2.12"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.12"
  ∷ word (ε ∷ ὐ ∷ σ ∷ ε ∷ β ∷ ῶ ∷ ς ∷ []) "Titus.2.12"
  ∷ word (ζ ∷ ή ∷ σ ∷ ω ∷ μ ∷ ε ∷ ν ∷ []) "Titus.2.12"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.2.12"
  ∷ word (τ ∷ ῷ ∷ []) "Titus.2.12"
  ∷ word (ν ∷ ῦ ∷ ν ∷ []) "Titus.2.12"
  ∷ word (α ∷ ἰ ∷ ῶ ∷ ν ∷ ι ∷ []) "Titus.2.12"
  ∷ word (π ∷ ρ ∷ ο ∷ σ ∷ δ ∷ ε ∷ χ ∷ ό ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Titus.2.13"
  ∷ word (τ ∷ ὴ ∷ ν ∷ []) "Titus.2.13"
  ∷ word (μ ∷ α ∷ κ ∷ α ∷ ρ ∷ ί ∷ α ∷ ν ∷ []) "Titus.2.13"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ δ ∷ α ∷ []) "Titus.2.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.13"
  ∷ word (ἐ ∷ π ∷ ι ∷ φ ∷ ά ∷ ν ∷ ε ∷ ι ∷ α ∷ ν ∷ []) "Titus.2.13"
  ∷ word (τ ∷ ῆ ∷ ς ∷ []) "Titus.2.13"
  ∷ word (δ ∷ ό ∷ ξ ∷ η ∷ ς ∷ []) "Titus.2.13"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.2.13"
  ∷ word (μ ∷ ε ∷ γ ∷ ά ∷ ∙λ ∷ ο ∷ υ ∷ []) "Titus.2.13"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.2.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.13"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "Titus.2.13"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.2.13"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Titus.2.13"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.2.13"
  ∷ word (ὃ ∷ ς ∷ []) "Titus.2.14"
  ∷ word (ἔ ∷ δ ∷ ω ∷ κ ∷ ε ∷ ν ∷ []) "Titus.2.14"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ὸ ∷ ν ∷ []) "Titus.2.14"
  ∷ word (ὑ ∷ π ∷ ὲ ∷ ρ ∷ []) "Titus.2.14"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.2.14"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.2.14"
  ∷ word (∙λ ∷ υ ∷ τ ∷ ρ ∷ ώ ∷ σ ∷ η ∷ τ ∷ α ∷ ι ∷ []) "Titus.2.14"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Titus.2.14"
  ∷ word (ἀ ∷ π ∷ ὸ ∷ []) "Titus.2.14"
  ∷ word (π ∷ ά ∷ σ ∷ η ∷ ς ∷ []) "Titus.2.14"
  ∷ word (ἀ ∷ ν ∷ ο ∷ μ ∷ ί ∷ α ∷ ς ∷ []) "Titus.2.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.14"
  ∷ word (κ ∷ α ∷ θ ∷ α ∷ ρ ∷ ί ∷ σ ∷ ῃ ∷ []) "Titus.2.14"
  ∷ word (ἑ ∷ α ∷ υ ∷ τ ∷ ῷ ∷ []) "Titus.2.14"
  ∷ word (∙λ ∷ α ∷ ὸ ∷ ν ∷ []) "Titus.2.14"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ ο ∷ ύ ∷ σ ∷ ι ∷ ο ∷ ν ∷ []) "Titus.2.14"
  ∷ word (ζ ∷ η ∷ ∙λ ∷ ω ∷ τ ∷ ὴ ∷ ν ∷ []) "Titus.2.14"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "Titus.2.14"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ω ∷ ν ∷ []) "Titus.2.14"
  ∷ word (Τ ∷ α ∷ ῦ ∷ τ ∷ α ∷ []) "Titus.2.15"
  ∷ word (∙λ ∷ ά ∷ ∙λ ∷ ε ∷ ι ∷ []) "Titus.2.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.15"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ κ ∷ ά ∷ ∙λ ∷ ε ∷ ι ∷ []) "Titus.2.15"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.2.15"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ γ ∷ χ ∷ ε ∷ []) "Titus.2.15"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "Titus.2.15"
  ∷ word (π ∷ ά ∷ σ ∷ η ∷ ς ∷ []) "Titus.2.15"
  ∷ word (ἐ ∷ π ∷ ι ∷ τ ∷ α ∷ γ ∷ ῆ ∷ ς ∷ []) "Titus.2.15"
  ∷ word (μ ∷ η ∷ δ ∷ ε ∷ ί ∷ ς ∷ []) "Titus.2.15"
  ∷ word (σ ∷ ο ∷ υ ∷ []) "Titus.2.15"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ φ ∷ ρ ∷ ο ∷ ν ∷ ε ∷ ί ∷ τ ∷ ω ∷ []) "Titus.2.15"
  ∷ word (Ὑ ∷ π ∷ ο ∷ μ ∷ ί ∷ μ ∷ ν ∷ ῃ ∷ σ ∷ κ ∷ ε ∷ []) "Titus.3.1"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Titus.3.1"
  ∷ word (ἀ ∷ ρ ∷ χ ∷ α ∷ ῖ ∷ ς ∷ []) "Titus.3.1"
  ∷ word (ἐ ∷ ξ ∷ ο ∷ υ ∷ σ ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "Titus.3.1"
  ∷ word (ὑ ∷ π ∷ ο ∷ τ ∷ ά ∷ σ ∷ σ ∷ ε ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "Titus.3.1"
  ∷ word (π ∷ ε ∷ ι ∷ θ ∷ α ∷ ρ ∷ χ ∷ ε ∷ ῖ ∷ ν ∷ []) "Titus.3.1"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Titus.3.1"
  ∷ word (π ∷ ᾶ ∷ ν ∷ []) "Titus.3.1"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ο ∷ ν ∷ []) "Titus.3.1"
  ∷ word (ἀ ∷ γ ∷ α ∷ θ ∷ ὸ ∷ ν ∷ []) "Titus.3.1"
  ∷ word (ἑ ∷ τ ∷ ο ∷ ί ∷ μ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.3.1"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "Titus.3.1"
  ∷ word (μ ∷ η ∷ δ ∷ έ ∷ ν ∷ α ∷ []) "Titus.3.2"
  ∷ word (β ∷ ∙λ ∷ α ∷ σ ∷ φ ∷ η ∷ μ ∷ ε ∷ ῖ ∷ ν ∷ []) "Titus.3.2"
  ∷ word (ἀ ∷ μ ∷ ά ∷ χ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.3.2"
  ∷ word (ε ∷ ἶ ∷ ν ∷ α ∷ ι ∷ []) "Titus.3.2"
  ∷ word (ἐ ∷ π ∷ ι ∷ ε ∷ ι ∷ κ ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.3.2"
  ∷ word (π ∷ ᾶ ∷ σ ∷ α ∷ ν ∷ []) "Titus.3.2"
  ∷ word (ἐ ∷ ν ∷ δ ∷ ε ∷ ι ∷ κ ∷ ν ∷ υ ∷ μ ∷ έ ∷ ν ∷ ο ∷ υ ∷ ς ∷ []) "Titus.3.2"
  ∷ word (π ∷ ρ ∷ α ∷ ΰ ∷ τ ∷ η ∷ τ ∷ α ∷ []) "Titus.3.2"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Titus.3.2"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Titus.3.2"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ρ ∷ ώ ∷ π ∷ ο ∷ υ ∷ ς ∷ []) "Titus.3.2"
  ∷ word (ἦ ∷ μ ∷ ε ∷ ν ∷ []) "Titus.3.3"
  ∷ word (γ ∷ ά ∷ ρ ∷ []) "Titus.3.3"
  ∷ word (π ∷ ο ∷ τ ∷ ε ∷ []) "Titus.3.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.3"
  ∷ word (ἡ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.3.3"
  ∷ word (ἀ ∷ ν ∷ ό ∷ η ∷ τ ∷ ο ∷ ι ∷ []) "Titus.3.3"
  ∷ word (ἀ ∷ π ∷ ε ∷ ι ∷ θ ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.3.3"
  ∷ word (π ∷ ∙λ ∷ α ∷ ν ∷ ώ ∷ μ ∷ ε ∷ ν ∷ ο ∷ ι ∷ []) "Titus.3.3"
  ∷ word (δ ∷ ο ∷ υ ∷ ∙λ ∷ ε ∷ ύ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.3.3"
  ∷ word (ἐ ∷ π ∷ ι ∷ θ ∷ υ ∷ μ ∷ ί ∷ α ∷ ι ∷ ς ∷ []) "Titus.3.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.3"
  ∷ word (ἡ ∷ δ ∷ ο ∷ ν ∷ α ∷ ῖ ∷ ς ∷ []) "Titus.3.3"
  ∷ word (π ∷ ο ∷ ι ∷ κ ∷ ί ∷ ∙λ ∷ α ∷ ι ∷ ς ∷ []) "Titus.3.3"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.3.3"
  ∷ word (κ ∷ α ∷ κ ∷ ί ∷ ᾳ ∷ []) "Titus.3.3"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.3"
  ∷ word (φ ∷ θ ∷ ό ∷ ν ∷ ῳ ∷ []) "Titus.3.3"
  ∷ word (δ ∷ ι ∷ ά ∷ γ ∷ ο ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.3.3"
  ∷ word (σ ∷ τ ∷ υ ∷ γ ∷ η ∷ τ ∷ ο ∷ ί ∷ []) "Titus.3.3"
  ∷ word (μ ∷ ι ∷ σ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.3.3"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ή ∷ ∙λ ∷ ο ∷ υ ∷ ς ∷ []) "Titus.3.3"
  ∷ word (ὅ ∷ τ ∷ ε ∷ []) "Titus.3.4"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.3.4"
  ∷ word (ἡ ∷ []) "Titus.3.4"
  ∷ word (χ ∷ ρ ∷ η ∷ σ ∷ τ ∷ ό ∷ τ ∷ η ∷ ς ∷ []) "Titus.3.4"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.4"
  ∷ word (ἡ ∷ []) "Titus.3.4"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ α ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ί ∷ α ∷ []) "Titus.3.4"
  ∷ word (ἐ ∷ π ∷ ε ∷ φ ∷ ά ∷ ν ∷ η ∷ []) "Titus.3.4"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.3.4"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "Titus.3.4"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.3.4"
  ∷ word (θ ∷ ε ∷ ο ∷ ῦ ∷ []) "Titus.3.4"
  ∷ word (ο ∷ ὐ ∷ κ ∷ []) "Titus.3.5"
  ∷ word (ἐ ∷ ξ ∷ []) "Titus.3.5"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ω ∷ ν ∷ []) "Titus.3.5"
  ∷ word (τ ∷ ῶ ∷ ν ∷ []) "Titus.3.5"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.3.5"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ι ∷ ο ∷ σ ∷ ύ ∷ ν ∷ ῃ ∷ []) "Titus.3.5"
  ∷ word (ἃ ∷ []) "Titus.3.5"
  ∷ word (ἐ ∷ π ∷ ο ∷ ι ∷ ή ∷ σ ∷ α ∷ μ ∷ ε ∷ ν ∷ []) "Titus.3.5"
  ∷ word (ἡ ∷ μ ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.3.5"
  ∷ word (ἀ ∷ ∙λ ∷ ∙λ ∷ ὰ ∷ []) "Titus.3.5"
  ∷ word (κ ∷ α ∷ τ ∷ ὰ ∷ []) "Titus.3.5"
  ∷ word (τ ∷ ὸ ∷ []) "Titus.3.5"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.3.5"
  ∷ word (ἔ ∷ ∙λ ∷ ε ∷ ο ∷ ς ∷ []) "Titus.3.5"
  ∷ word (ἔ ∷ σ ∷ ω ∷ σ ∷ ε ∷ ν ∷ []) "Titus.3.5"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Titus.3.5"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Titus.3.5"
  ∷ word (∙λ ∷ ο ∷ υ ∷ τ ∷ ρ ∷ ο ∷ ῦ ∷ []) "Titus.3.5"
  ∷ word (π ∷ α ∷ ∙λ ∷ ι ∷ γ ∷ γ ∷ ε ∷ ν ∷ ε ∷ σ ∷ ί ∷ α ∷ ς ∷ []) "Titus.3.5"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.5"
  ∷ word (ἀ ∷ ν ∷ α ∷ κ ∷ α ∷ ι ∷ ν ∷ ώ ∷ σ ∷ ε ∷ ω ∷ ς ∷ []) "Titus.3.5"
  ∷ word (π ∷ ν ∷ ε ∷ ύ ∷ μ ∷ α ∷ τ ∷ ο ∷ ς ∷ []) "Titus.3.5"
  ∷ word (ἁ ∷ γ ∷ ί ∷ ο ∷ υ ∷ []) "Titus.3.5"
  ∷ word (ο ∷ ὗ ∷ []) "Titus.3.6"
  ∷ word (ἐ ∷ ξ ∷ έ ∷ χ ∷ ε ∷ ε ∷ ν ∷ []) "Titus.3.6"
  ∷ word (ἐ ∷ φ ∷ []) "Titus.3.6"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Titus.3.6"
  ∷ word (π ∷ ∙λ ∷ ο ∷ υ ∷ σ ∷ ί ∷ ω ∷ ς ∷ []) "Titus.3.6"
  ∷ word (δ ∷ ι ∷ ὰ ∷ []) "Titus.3.6"
  ∷ word (Ἰ ∷ η ∷ σ ∷ ο ∷ ῦ ∷ []) "Titus.3.6"
  ∷ word (Χ ∷ ρ ∷ ι ∷ σ ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.3.6"
  ∷ word (τ ∷ ο ∷ ῦ ∷ []) "Titus.3.6"
  ∷ word (σ ∷ ω ∷ τ ∷ ῆ ∷ ρ ∷ ο ∷ ς ∷ []) "Titus.3.6"
  ∷ word (ἡ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.3.6"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.3.7"
  ∷ word (δ ∷ ι ∷ κ ∷ α ∷ ι ∷ ω ∷ θ ∷ έ ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.3.7"
  ∷ word (τ ∷ ῇ ∷ []) "Titus.3.7"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ί ∷ ν ∷ ο ∷ υ ∷ []) "Titus.3.7"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ τ ∷ ι ∷ []) "Titus.3.7"
  ∷ word (κ ∷ ∙λ ∷ η ∷ ρ ∷ ο ∷ ν ∷ ό ∷ μ ∷ ο ∷ ι ∷ []) "Titus.3.7"
  ∷ word (γ ∷ ε ∷ ν ∷ η ∷ θ ∷ ῶ ∷ μ ∷ ε ∷ ν ∷ []) "Titus.3.7"
  ∷ word (κ ∷ α ∷ τ ∷ []) "Titus.3.7"
  ∷ word (ἐ ∷ ∙λ ∷ π ∷ ί ∷ δ ∷ α ∷ []) "Titus.3.7"
  ∷ word (ζ ∷ ω ∷ ῆ ∷ ς ∷ []) "Titus.3.7"
  ∷ word (α ∷ ἰ ∷ ω ∷ ν ∷ ί ∷ ο ∷ υ ∷ []) "Titus.3.7"
  ∷ word (Π ∷ ι ∷ σ ∷ τ ∷ ὸ ∷ ς ∷ []) "Titus.3.8"
  ∷ word (ὁ ∷ []) "Titus.3.8"
  ∷ word (∙λ ∷ ό ∷ γ ∷ ο ∷ ς ∷ []) "Titus.3.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.8"
  ∷ word (π ∷ ε ∷ ρ ∷ ὶ ∷ []) "Titus.3.8"
  ∷ word (τ ∷ ο ∷ ύ ∷ τ ∷ ω ∷ ν ∷ []) "Titus.3.8"
  ∷ word (β ∷ ο ∷ ύ ∷ ∙λ ∷ ο ∷ μ ∷ α ∷ ί ∷ []) "Titus.3.8"
  ∷ word (σ ∷ ε ∷ []) "Titus.3.8"
  ∷ word (δ ∷ ι ∷ α ∷ β ∷ ε ∷ β ∷ α ∷ ι ∷ ο ∷ ῦ ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "Titus.3.8"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.3.8"
  ∷ word (φ ∷ ρ ∷ ο ∷ ν ∷ τ ∷ ί ∷ ζ ∷ ω ∷ σ ∷ ι ∷ ν ∷ []) "Titus.3.8"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "Titus.3.8"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ω ∷ ν ∷ []) "Titus.3.8"
  ∷ word (π ∷ ρ ∷ ο ∷ ΐ ∷ σ ∷ τ ∷ α ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "Titus.3.8"
  ∷ word (ο ∷ ἱ ∷ []) "Titus.3.8"
  ∷ word (π ∷ ε ∷ π ∷ ι ∷ σ ∷ τ ∷ ε ∷ υ ∷ κ ∷ ό ∷ τ ∷ ε ∷ ς ∷ []) "Titus.3.8"
  ∷ word (θ ∷ ε ∷ ῷ ∷ []) "Titus.3.8"
  ∷ word (τ ∷ α ∷ ῦ ∷ τ ∷ ά ∷ []) "Titus.3.8"
  ∷ word (ἐ ∷ σ ∷ τ ∷ ι ∷ ν ∷ []) "Titus.3.8"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ὰ ∷ []) "Titus.3.8"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.8"
  ∷ word (ὠ ∷ φ ∷ έ ∷ ∙λ ∷ ι ∷ μ ∷ α ∷ []) "Titus.3.8"
  ∷ word (τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.3.8"
  ∷ word (ἀ ∷ ν ∷ θ ∷ ρ ∷ ώ ∷ π ∷ ο ∷ ι ∷ ς ∷ []) "Titus.3.8"
  ∷ word (μ ∷ ω ∷ ρ ∷ ὰ ∷ ς ∷ []) "Titus.3.9"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.3.9"
  ∷ word (ζ ∷ η ∷ τ ∷ ή ∷ σ ∷ ε ∷ ι ∷ ς ∷ []) "Titus.3.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.9"
  ∷ word (γ ∷ ε ∷ ν ∷ ε ∷ α ∷ ∙λ ∷ ο ∷ γ ∷ ί ∷ α ∷ ς ∷ []) "Titus.3.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.9"
  ∷ word (ἔ ∷ ρ ∷ ε ∷ ι ∷ ς ∷ []) "Titus.3.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.9"
  ∷ word (μ ∷ ά ∷ χ ∷ α ∷ ς ∷ []) "Titus.3.9"
  ∷ word (ν ∷ ο ∷ μ ∷ ι ∷ κ ∷ ὰ ∷ ς ∷ []) "Titus.3.9"
  ∷ word (π ∷ ε ∷ ρ ∷ ι ∷ ΐ ∷ σ ∷ τ ∷ α ∷ σ ∷ ο ∷ []) "Titus.3.9"
  ∷ word (ε ∷ ἰ ∷ σ ∷ ὶ ∷ ν ∷ []) "Titus.3.9"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Titus.3.9"
  ∷ word (ἀ ∷ ν ∷ ω ∷ φ ∷ ε ∷ ∙λ ∷ ε ∷ ῖ ∷ ς ∷ []) "Titus.3.9"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.9"
  ∷ word (μ ∷ ά ∷ τ ∷ α ∷ ι ∷ ο ∷ ι ∷ []) "Titus.3.9"
  ∷ word (α ∷ ἱ ∷ ρ ∷ ε ∷ τ ∷ ι ∷ κ ∷ ὸ ∷ ν ∷ []) "Titus.3.10"
  ∷ word (ἄ ∷ ν ∷ θ ∷ ρ ∷ ω ∷ π ∷ ο ∷ ν ∷ []) "Titus.3.10"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "Titus.3.10"
  ∷ word (μ ∷ ί ∷ α ∷ ν ∷ []) "Titus.3.10"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.10"
  ∷ word (δ ∷ ε ∷ υ ∷ τ ∷ έ ∷ ρ ∷ α ∷ ν ∷ []) "Titus.3.10"
  ∷ word (ν ∷ ο ∷ υ ∷ θ ∷ ε ∷ σ ∷ ί ∷ α ∷ ν ∷ []) "Titus.3.10"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ ι ∷ τ ∷ ο ∷ ῦ ∷ []) "Titus.3.10"
  ∷ word (ε ∷ ἰ ∷ δ ∷ ὼ ∷ ς ∷ []) "Titus.3.11"
  ∷ word (ὅ ∷ τ ∷ ι ∷ []) "Titus.3.11"
  ∷ word (ἐ ∷ ξ ∷ έ ∷ σ ∷ τ ∷ ρ ∷ α ∷ π ∷ τ ∷ α ∷ ι ∷ []) "Titus.3.11"
  ∷ word (ὁ ∷ []) "Titus.3.11"
  ∷ word (τ ∷ ο ∷ ι ∷ ο ∷ ῦ ∷ τ ∷ ο ∷ ς ∷ []) "Titus.3.11"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.11"
  ∷ word (ἁ ∷ μ ∷ α ∷ ρ ∷ τ ∷ ά ∷ ν ∷ ε ∷ ι ∷ []) "Titus.3.11"
  ∷ word (ὢ ∷ ν ∷ []) "Titus.3.11"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ κ ∷ α ∷ τ ∷ ά ∷ κ ∷ ρ ∷ ι ∷ τ ∷ ο ∷ ς ∷ []) "Titus.3.11"
  ∷ word (Ὅ ∷ τ ∷ α ∷ ν ∷ []) "Titus.3.12"
  ∷ word (π ∷ έ ∷ μ ∷ ψ ∷ ω ∷ []) "Titus.3.12"
  ∷ word (Ἀ ∷ ρ ∷ τ ∷ ε ∷ μ ∷ ᾶ ∷ ν ∷ []) "Titus.3.12"
  ∷ word (π ∷ ρ ∷ ὸ ∷ ς ∷ []) "Titus.3.12"
  ∷ word (σ ∷ ὲ ∷ []) "Titus.3.12"
  ∷ word (ἢ ∷ []) "Titus.3.12"
  ∷ word (Τ ∷ υ ∷ χ ∷ ι ∷ κ ∷ ό ∷ ν ∷ []) "Titus.3.12"
  ∷ word (σ ∷ π ∷ ο ∷ ύ ∷ δ ∷ α ∷ σ ∷ ο ∷ ν ∷ []) "Titus.3.12"
  ∷ word (ἐ ∷ ∙λ ∷ θ ∷ ε ∷ ῖ ∷ ν ∷ []) "Titus.3.12"
  ∷ word (π ∷ ρ ∷ ό ∷ ς ∷ []) "Titus.3.12"
  ∷ word (μ ∷ ε ∷ []) "Titus.3.12"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Titus.3.12"
  ∷ word (Ν ∷ ι ∷ κ ∷ ό ∷ π ∷ ο ∷ ∙λ ∷ ι ∷ ν ∷ []) "Titus.3.12"
  ∷ word (ἐ ∷ κ ∷ ε ∷ ῖ ∷ []) "Titus.3.12"
  ∷ word (γ ∷ ὰ ∷ ρ ∷ []) "Titus.3.12"
  ∷ word (κ ∷ έ ∷ κ ∷ ρ ∷ ι ∷ κ ∷ α ∷ []) "Titus.3.12"
  ∷ word (π ∷ α ∷ ρ ∷ α ∷ χ ∷ ε ∷ ι ∷ μ ∷ ά ∷ σ ∷ α ∷ ι ∷ []) "Titus.3.12"
  ∷ word (ζ ∷ η ∷ ν ∷ ᾶ ∷ ν ∷ []) "Titus.3.13"
  ∷ word (τ ∷ ὸ ∷ ν ∷ []) "Titus.3.13"
  ∷ word (ν ∷ ο ∷ μ ∷ ι ∷ κ ∷ ὸ ∷ ν ∷ []) "Titus.3.13"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.13"
  ∷ word (Ἀ ∷ π ∷ ο ∷ ∙λ ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "Titus.3.13"
  ∷ word (σ ∷ π ∷ ο ∷ υ ∷ δ ∷ α ∷ ί ∷ ω ∷ ς ∷ []) "Titus.3.13"
  ∷ word (π ∷ ρ ∷ ό ∷ π ∷ ε ∷ μ ∷ ψ ∷ ο ∷ ν ∷ []) "Titus.3.13"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.3.13"
  ∷ word (μ ∷ η ∷ δ ∷ ὲ ∷ ν ∷ []) "Titus.3.13"
  ∷ word (α ∷ ὐ ∷ τ ∷ ο ∷ ῖ ∷ ς ∷ []) "Titus.3.13"
  ∷ word (∙λ ∷ ε ∷ ί ∷ π ∷ ῃ ∷ []) "Titus.3.13"
  ∷ word (μ ∷ α ∷ ν ∷ θ ∷ α ∷ ν ∷ έ ∷ τ ∷ ω ∷ σ ∷ α ∷ ν ∷ []) "Titus.3.14"
  ∷ word (δ ∷ ὲ ∷ []) "Titus.3.14"
  ∷ word (κ ∷ α ∷ ὶ ∷ []) "Titus.3.14"
  ∷ word (ο ∷ ἱ ∷ []) "Titus.3.14"
  ∷ word (ἡ ∷ μ ∷ έ ∷ τ ∷ ε ∷ ρ ∷ ο ∷ ι ∷ []) "Titus.3.14"
  ∷ word (κ ∷ α ∷ ∙λ ∷ ῶ ∷ ν ∷ []) "Titus.3.14"
  ∷ word (ἔ ∷ ρ ∷ γ ∷ ω ∷ ν ∷ []) "Titus.3.14"
  ∷ word (π ∷ ρ ∷ ο ∷ ΐ ∷ σ ∷ τ ∷ α ∷ σ ∷ θ ∷ α ∷ ι ∷ []) "Titus.3.14"
  ∷ word (ε ∷ ἰ ∷ ς ∷ []) "Titus.3.14"
  ∷ word (τ ∷ ὰ ∷ ς ∷ []) "Titus.3.14"
  ∷ word (ἀ ∷ ν ∷ α ∷ γ ∷ κ ∷ α ∷ ί ∷ α ∷ ς ∷ []) "Titus.3.14"
  ∷ word (χ ∷ ρ ∷ ε ∷ ί ∷ α ∷ ς ∷ []) "Titus.3.14"
  ∷ word (ἵ ∷ ν ∷ α ∷ []) "Titus.3.14"
  ∷ word (μ ∷ ὴ ∷ []) "Titus.3.14"
  ∷ word (ὦ ∷ σ ∷ ι ∷ ν ∷ []) "Titus.3.14"
  ∷ word (ἄ ∷ κ ∷ α ∷ ρ ∷ π ∷ ο ∷ ι ∷ []) "Titus.3.14"
  ∷ word (Ἀ ∷ σ ∷ π ∷ ά ∷ ζ ∷ ο ∷ ν ∷ τ ∷ α ∷ ί ∷ []) "Titus.3.15"
  ∷ word (σ ∷ ε ∷ []) "Titus.3.15"
  ∷ word (ο ∷ ἱ ∷ []) "Titus.3.15"
  ∷ word (μ ∷ ε ∷ τ ∷ []) "Titus.3.15"
  ∷ word (ἐ ∷ μ ∷ ο ∷ ῦ ∷ []) "Titus.3.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ε ∷ ς ∷ []) "Titus.3.15"
  ∷ word (ἄ ∷ σ ∷ π ∷ α ∷ σ ∷ α ∷ ι ∷ []) "Titus.3.15"
  ∷ word (τ ∷ ο ∷ ὺ ∷ ς ∷ []) "Titus.3.15"
  ∷ word (φ ∷ ι ∷ ∙λ ∷ ο ∷ ῦ ∷ ν ∷ τ ∷ α ∷ ς ∷ []) "Titus.3.15"
  ∷ word (ἡ ∷ μ ∷ ᾶ ∷ ς ∷ []) "Titus.3.15"
  ∷ word (ἐ ∷ ν ∷ []) "Titus.3.15"
  ∷ word (π ∷ ί ∷ σ ∷ τ ∷ ε ∷ ι ∷ []) "Titus.3.15"
  ∷ word (ἡ ∷ []) "Titus.3.15"
  ∷ word (χ ∷ ά ∷ ρ ∷ ι ∷ ς ∷ []) "Titus.3.15"
  ∷ word (μ ∷ ε ∷ τ ∷ ὰ ∷ []) "Titus.3.15"
  ∷ word (π ∷ ά ∷ ν ∷ τ ∷ ω ∷ ν ∷ []) "Titus.3.15"
  ∷ word (ὑ ∷ μ ∷ ῶ ∷ ν ∷ []) "Titus.3.15"
  ∷ []

max_stars_repo_name: scott-fleischman/GreekGrammar

max_issues_repo_name: scott-fleischman/GreekGrammar

max_forks_repo_name: scott-fleischman/GreekGrammar


text:
------------------------------------------------------------------------------
-- From ListN as the least fixed-point to ListN using data
------------------------------------------------------------------------------

{-# OPTIONS --exact-split              #-}
{-# OPTIONS --no-sized-types           #-}
{-# OPTIONS --no-universe-polymorphism #-}
{-# OPTIONS --without-K                #-}

-- We want to represent the total lists of total natural numbers data
-- type
--
-- data ListN : D → Set where
--   lnnil  : ListN []
--   lncons : ∀ {n ns} → N n → ListN ns → ListN (n ∷ ns)
--
-- using the representation of ListN as the least fixed-point.

module LFPs.ListN where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.Nat.Type
open import FOTC.Data.Nat.UnaryNumbers

------------------------------------------------------------------------------
-- ListN is a least fixed-point of a functor

-- The functor.
-- ListNF : (D → Set) → D → Set
-- ListNF P ns = ns ≡ [] ∨ (∃[ n' ] ∃[ ns' ] N n' ∧ ns ≡ n' ∷ ns' ∧ P ns')

-- List is the least fixed-point of ListF.
postulate
  ListN : D → Set

  -- ListN is a pre-fixed point of ListNF.
  --
  -- Peter: It corresponds to the introduction rules.
  ListN-in : ∀ {ns} →
             ns ≡ [] ∨ (∃[ n' ] ∃[ ns' ] N n' ∧ ns ≡ n' ∷ ns' ∧ ListN ns') →
             ListN ns

  -- ListN is the least pre-fixed point of ListFN.
  --
  -- Peter: It corresponds to the elimination rule of an inductively
  -- defined predicate.
  ListN-ind :
    (A : D → Set) →
    (∀ {ns} → ns ≡ [] ∨ (∃[ n' ] ∃[ ns' ] N n' ∧ ns ≡ n' ∷ ns' ∧ A ns') → A ns) →
    ∀ {ns} → ListN ns → A ns

------------------------------------------------------------------------------
-- The data constructors of List.
lnnil : ListN []
lnnil = ListN-in (inj₁ refl)

lncons : ∀ {n ns} → N n → ListN ns → ListN (n ∷ ns)
lncons {n} {ns} Nn LNns = ListN-in (inj₂ (n , ns , Nn , refl , LNns))

------------------------------------------------------------------------------
-- The induction principle for List.
ListN-ind' : (A : D → Set) →
             A [] →
             (∀ n {ns} → N n → A ns → A (n ∷ ns)) →
             ∀ {ns} → ListN ns → A ns
ListN-ind' A A[] is = ListN-ind A prf
  where
  prf : ∀ {ns} → ns ≡ [] ∨ (∃[ n' ] ∃[ ns' ] N n' ∧ ns ≡ n' ∷ ns'  ∧ A ns') →
        A ns
  prf (inj₁ ns≡[])                        = subst A (sym ns≡[]) A[]
  prf (inj₂ (n' , ns' , Nn' , h₁ , Ans')) = subst A (sym h₁) (is n' Nn' Ans')

------------------------------------------------------------------------------
-- Example

ys : D
ys = 0' ∷ 1' ∷ 2' ∷ []

ys-ListN : ListN ys
ys-ListN =
  lncons nzero (lncons (nsucc nzero) (lncons (nsucc (nsucc nzero)) lnnil))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --allow-unsolved-metas #-}
module TermNode where

open import OscarPrelude
open import TermCode

record TermNode : Set
 where
  inductive
  field
    children : List (TermCode × TermNode)
    number : Nat

open TermNode public

open import Membership

_child∈_ : TermCode → TermNode → Set
_child∈_ 𝔠 𝔫 = 𝔠 ∈ (fst <$> children 𝔫)

_child∉_ : TermCode → TermNode → Set
𝔠 child∉ 𝔫 = ¬ (𝔠 child∈ 𝔫)

open import DecidableMembership

_child∈?_ : (𝔠 : TermCode) → (𝔫 : TermNode) → Dec $ 𝔠 child∈ 𝔫
c child∈? record { children = cs } = c ∈? (fst <$> cs)

getChild : {𝔠 : TermCode} → (𝔫 : TermNode) → 𝔠 child∈ 𝔫 → TermNode
getChild {𝔠} (record { children = [] ; number = number₁ }) ()
getChild {._} (record { children = (fst₁ , snd₁) ∷ children₁ ; number = number₁ }) zero = snd₁
getChild {𝔠} (𝔫@record { children = x ∷ children₁ ; number = number₁ }) (suc x₁) = getChild record 𝔫 { children = children₁ } x₁

addChild : {𝔠 : TermCode} (𝔫 : TermNode) → 𝔠 child∉ 𝔫 → TermNode → TermNode
addChild {𝔠} 𝔫 𝔠∉𝔫 𝔫' =
  record 𝔫 { children = (𝔠 , 𝔫') ∷ children 𝔫 }

setChild : {𝔠 : TermCode} (𝔫 : TermNode) → 𝔠 child∈ 𝔫 → TermNode → TermNode
setChild {𝔠} record { children = [] ; number = number₁ } () 𝔫'
setChild 𝔫@record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } (zero) 𝔫' =
  record 𝔫 { children = ((fst₁ , 𝔫') ∷ children₁) }
setChild {𝔠} 𝔫@record { children = (x ∷ children₁) ; number = number₁ } (suc 𝔠∈𝔫) 𝔫' =
  record 𝔫 { children = (x ∷ children (setChild (record 𝔫 { children = children₁ }) 𝔠∈𝔫 𝔫')) }

setGet-ok : ∀ {𝔠} 𝔫 → (𝔠∈𝔫 : 𝔠 child∈ 𝔫) → setChild 𝔫 𝔠∈𝔫 (getChild 𝔫 𝔠∈𝔫) ≡ 𝔫
setGet-ok record { children = [] ; number = number₁ } ()
setGet-ok record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } (zero) = refl
setGet-ok record { children = ((fst₁ , snd₁) ∷ children₁) ; number = number₁ } (suc 𝔠∈𝔫) rewrite setGet-ok (record { children = children₁ ; number = number₁ }) 𝔠∈𝔫 = refl

storeTermCodes : List TermCode → Nat → StateT TermNode Identity Nat
storeTermCodes [] 𝔑 = return 𝔑
storeTermCodes (𝔠 ∷ 𝔠s) 𝔑 =
  𝔫 ← get -|
  case 𝔠 child∈? 𝔫 of λ
  { (no 𝔠∉tests) →
    let 𝔑' , 𝔫' = runIdentity $
                  runStateT
                    (storeTermCodes 𝔠s $ suc 𝔑)
                    (record
                      { children = []
                      ; number = suc 𝔑 }) in
    put ((addChild 𝔫 𝔠∉tests 𝔫')) ~|
    return 𝔑'
  ; (yes 𝔠∈tests) →
    let 𝔑' , 𝔫' = runIdentity $
                  runStateT
                    (storeTermCodes 𝔠s $ suc 𝔑)
                    ((getChild 𝔫 𝔠∈tests)) in
    put ((setChild 𝔫 𝔠∈tests 𝔫')) ~|
    return 𝔑' }

storeTermCodes[] : (𝔫 : TermNode) (𝔑 : Nat) → (runIdentity $ runStateT (storeTermCodes [] 𝔑) 𝔫) ≡ (𝔑 , 𝔫)
storeTermCodes[] 𝔫 𝔑 = refl

--{-# REWRITE storeTermCodes[] #-}

storeTermCodes' : List TermCode → StateT Nat (StateT TermNode Identity) ⊤
storeTermCodes' 𝔠s =
  𝔑 ← get -|
  tn ← lift get -|
  (let 𝔑' , tn' = runIdentity $ runStateT (storeTermCodes 𝔠s 𝔑) tn in
   put 𝔑' ~| lift (put tn') ~| return tt)

open import Term
open import Vector

mutual

  storeTerm : Term → StateT Nat (StateT TermNode Identity) ⊤
  storeTerm τ@(variable _) = storeTermCodes' (encodeTerm τ)
  storeTerm τ@(function _ τs) = storeTermCodes' (encodeTerm τ) ~| storeTerms τs

  storeTerms : Terms → StateT Nat (StateT TermNode Identity) ⊤
  storeTerms ⟨ ⟨ [] ⟩ ⟩ = return tt
  storeTerms ⟨ ⟨ τ ∷ τs ⟩ ⟩ = storeTerm τ ~| storeTerms ⟨ ⟨ τs ⟩ ⟩ ~| return tt

module ExampleStoreTerm where

  open import FunctionName
  open import VariableName

  example-Term₁ : Term
  example-Term₁ =
    (function ⟨ 2 ⟩
              ⟨ ⟨ variable ⟨ 0 ⟩
              ∷ function ⟨ 3 ⟩
                         ⟨ ⟨ variable ⟨ 2 ⟩ ∷ [] ⟩ ⟩
              ∷ variable ⟨ 5 ⟩
              ∷ []
              ⟩ ⟩
    )

  example-Term₂ : Term
  example-Term₂ =
    (function ⟨ 2 ⟩
              ⟨ ⟨ variable ⟨ 0 ⟩
              ∷ variable ⟨ 2 ⟩
              ∷ function ⟨ 3 ⟩
                         ⟨ ⟨ variable ⟨ 2 ⟩ ∷ [] ⟩ ⟩
              ∷ variable ⟨ 5 ⟩
              ∷ []
              ⟩ ⟩
    )

  topNode : TermNode
  topNode = record { children = [] ; number = 0 }

  example-storeTerm : (⊤ × Nat) × TermNode
  example-storeTerm = runIdentity $ runStateT (runStateT (storeTerm example-Term₁ >> storeTerm example-Term₂) 0) topNode

NodeStateT = StateT TermNode
TopNodeState = StateT Nat (NodeStateT Identity)

open import LiteralFormula
open import IsLiteralFormula

storeLiteralFormulaTerms : LiteralFormula → StateT Nat (StateT TermNode Identity) ⊤
storeLiteralFormulaTerms ⟨ atomic 𝑃 τs ⟩ = storeTerms τs
storeLiteralFormulaTerms ⟨ logical 𝑃 τs ⟩ = storeTerms τs

open import 𝓢equent

storeSequentLiteralFormulaTerms : 𝓢equent LiteralFormula → StateT Nat (StateT TermNode Identity) ⊤′
storeSequentLiteralFormulaTerms (φˢs ⊢ φᵗ) = sequence $ storeLiteralFormulaTerms <$> ({!φᵗ!} ∷ φˢs)


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Data.Unit where

open import Cubical.Data.Unit.Base       public
open import Cubical.Data.Unit.Properties public

max_stars_repo_name: dan-iel-lee/cubical

max_issues_repo_name: dan-iel-lee/cubical

max_forks_repo_name: dan-iel-lee/cubical


text:
-- Laws for weakenings and substitutions.

{-# OPTIONS --without-K --safe #-}

module Definition.Untyped.Properties where

open import Definition.Untyped

open import Tools.Fin
open import Tools.Nat
open import Tools.List
open import Tools.PropositionalEquality hiding (subst)

private
  variable
    ℓ m n : Nat
    ρ ρ′ : Wk m n
    η : Wk n ℓ
    σ σ′ : Subst m n

-- Weakening properties

-- Two weakenings ρ and ρ′ are extensionally equal if they agree on
-- all arguments when interpreted as functions mapping variables to
-- variables.  Formally, they are considered equal iff
--
--   (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
--
-- Intensional (propositional) equality would be too fine.  For
-- instance,
--
--   lift id : Γ∙A ≤ Γ∙A
--
-- is extensionally equal to
--
--   id : Γ∙A ≤ Γ∙A
--
-- but syntactically different.

-- "lift" preserves equality of weakenings.  Or:
-- If two weakenings are equal under wkVar, then they are equal when lifted.

wkVar-lift : (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
           → (∀ x → wkVar (lift ρ) x ≡ wkVar (lift ρ′) x)

wkVar-lift eq x0     = refl
wkVar-lift eq (x +1) = cong _+1 (eq x)

wkVar-lifts : (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
            → (∀ n x → wkVar (liftn ρ n) x ≡ wkVar (liftn ρ′ n) x)
wkVar-lifts eq 0 x      = eq x
wkVar-lifts eq (1+ n) x = wkVar-lift (wkVar-lifts eq n) x

-- Extensionally equal weakenings, if applied to a term,
-- yield the same weakened term.  Or:
-- If two weakenings are equal under wkVar, then they are equal under wk.

mutual
  wkVar-to-wk : (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
              → ∀ t → wk ρ t ≡ wk ρ′ t
  wkVar-to-wk eq (var x)   = cong var (eq x)
  wkVar-to-wk eq (gen k c) = cong (gen k) (wkVar-to-wkGen eq c)

  wkVar-to-wkGen : (∀ x → wkVar ρ x ≡ wkVar ρ′ x)
                 → ∀ {bs} c → wkGen {bs = bs} ρ c ≡ wkGen {bs = bs} ρ′ c
  wkVar-to-wkGen eq [] = refl
  wkVar-to-wkGen eq (_∷_ {b = b} t ts) =
    cong₂ _∷_ (wkVar-to-wk (wkVar-lifts eq b) t) (wkVar-to-wkGen eq ts)

-- lift id  is extensionally equal to  id.

wkVar-lift-id : (x : Fin (1+ n)) → wkVar (lift id) x ≡ wkVar id x
wkVar-lift-id x0     = refl
wkVar-lift-id (x +1) = refl

wkVar-lifts-id : (n : Nat) (x : Fin (n + m)) → wkVar (liftn id n) x ≡ wkVar id x
wkVar-lifts-id 0 x           = refl
wkVar-lifts-id (1+ n) x0     = refl
wkVar-lifts-id (1+ n) (x +1) = cong _+1 (wkVar-lifts-id n x)

-- id is the identity renaming.

wkVar-id : (x : Fin n) → wkVar id x ≡ x
wkVar-id x = refl

mutual
  wk-id : (t : Term n) → wk id t ≡ t
  wk-id (var x)   = refl
  wk-id (gen k ts) = cong (gen k) (wkGen-id ts)

  wkGen-id : ∀ {bs} x → wkGen {n} {n} {bs} id x ≡ x
  wkGen-id [] = refl
  wkGen-id (_∷_ {b = b} t ts) =
    cong₂ _∷_ (trans (wkVar-to-wk (wkVar-lifts-id b) t) ( wk-id t)) (wkGen-id ts)

-- lift id  is also the identity renaming.

wk-lift-id : (t : Term (1+ n)) → wk (lift id) t ≡ t
wk-lift-id t = trans (wkVar-to-wk wkVar-lift-id t) (wk-id t)

-- The composition of weakenings is correct...
--
-- ...as action on variables.

wkVar-comp : (ρ : Wk m ℓ) (ρ′ : Wk ℓ n) (x : Fin n) → wkVar ρ (wkVar ρ′ x) ≡ wkVar (ρ • ρ′) x
wkVar-comp id       ρ′        x      = refl
wkVar-comp (step ρ) ρ′        x      = cong _+1 (wkVar-comp ρ ρ′ x)
wkVar-comp (lift ρ) id        x      = refl
wkVar-comp (lift ρ) (step ρ′) x      = cong _+1 (wkVar-comp ρ ρ′ x)
wkVar-comp (lift ρ) (lift ρ′) x0     = refl
wkVar-comp (lift ρ) (lift ρ′) (x +1) = cong _+1 (wkVar-comp ρ ρ′ x)

wkVar-comps : ∀ k → (ρ : Wk m ℓ) (ρ′ : Wk ℓ n) (x : Fin (k + n))
            → wkVar (liftn ρ k • liftn ρ′ k) x
            ≡ wkVar (liftn (ρ • ρ′) k) x
wkVar-comps 0      ρ ρ′ x      = refl
wkVar-comps (1+ n) ρ ρ′ x0     = refl
wkVar-comps (1+ n) ρ ρ′ (x +1) = cong _+1 (wkVar-comps n ρ ρ′ x)

-- ... as action on terms.

mutual
  wk-comp : (ρ : Wk m ℓ) (ρ′ : Wk ℓ n) (t : Term n) → wk ρ (wk ρ′ t) ≡ wk (ρ • ρ′) t
  wk-comp ρ ρ′ (var x) = cong var (wkVar-comp ρ ρ′ x)
  wk-comp ρ ρ′ (gen k ts) = cong (gen k) (wkGen-comp ρ ρ′ ts)

  wkGen-comp : (ρ : Wk m ℓ) (ρ′ : Wk ℓ n) → ∀ {bs} g
             → wkGen ρ (wkGen ρ′ g) ≡ wkGen {bs = bs} (ρ • ρ′) g
  wkGen-comp ρ ρ′ [] = refl
  wkGen-comp ρ ρ′ (_∷_ {b = b} t ts) =
    cong₂ _∷_ (trans (wk-comp (liftn ρ b) (liftn ρ′ b) t)
                     (wkVar-to-wk (wkVar-comps b ρ ρ′) t))
      (wkGen-comp ρ ρ′ ts)

-- The following lemmata are variations on the equality
--
--   wk1 ∘ ρ = lift ρ ∘ wk1.
--
-- Typing:  Γ∙A ≤ Γ ≤ Δ  <==>  Γ∙A ≤ Δ∙A ≤ Δ.

lift-step-comp : (ρ : Wk m n) → step id • ρ ≡ lift ρ • step id
lift-step-comp id       = refl
lift-step-comp (step ρ) = cong step (lift-step-comp ρ)
lift-step-comp (lift ρ) = refl

wk1-wk : (ρ : Wk m n) (t : Term n) → wk1 (wk ρ t) ≡ wk (step ρ) t
wk1-wk ρ t = wk-comp (step id) ρ t

lift-wk1 : (ρ : Wk m n) (t : Term n) → wk (lift ρ) (wk1 t) ≡ wk (step ρ) t
lift-wk1 pr A = trans (wk-comp (lift pr) (step id) A)
                      (sym (cong (λ x → wk x A) (lift-step-comp pr)))

wk1-wk≡lift-wk1 : (ρ : Wk m n) (t : Term n) → wk1 (wk ρ t) ≡ wk (lift ρ) (wk1 t)
wk1-wk≡lift-wk1 ρ t = trans (wk1-wk ρ t) (sym (lift-wk1 ρ t))

-- Substitution properties.

-- Two substitutions σ and σ′ are equal if they are pointwise equal,
-- i.e., agree on all variables.
--
--   ∀ x →  σ x ≡ σ′ x

-- If  σ = σ′  then  lift σ = lift σ′.

substVar-lift : (∀ x → σ x ≡ σ′ x) → ∀ x → liftSubst σ x ≡ liftSubst σ′ x

substVar-lift eq x0     = refl
substVar-lift eq (x +1) = cong wk1 (eq x)

substVar-lifts : (∀ x → σ x ≡ σ′ x) → ∀ n x → liftSubstn σ n x ≡ liftSubstn σ′ n x

substVar-lifts eq 0 x           = eq x
substVar-lifts eq (1+ n) x0     = refl
substVar-lifts eq (1+ n) (x +1) = cong wk1 (substVar-lifts eq n x)

-- If  σ = σ′  then  subst σ t = subst σ′ t.

mutual
  substVar-to-subst : ((x : Fin n) → σ x ≡ σ′ x)
                    → (t : Term n) → subst σ t ≡ subst σ′ t
  substVar-to-subst eq (var x)    = eq x
  substVar-to-subst eq (gen k ts) = cong (gen k) (substVar-to-substGen eq ts)

  substVar-to-substGen : ∀ {bs} → ((x : Fin n) → σ x ≡ σ′ x)
                       → ∀ g → substGen {bs = bs} σ g ≡ substGen {bs = bs} σ′ g
  substVar-to-substGen eq [] = refl
  substVar-to-substGen eq (_∷_ {b = b} t ts) =
    cong₂ _∷_ (substVar-to-subst (substVar-lifts eq b) t)
              (substVar-to-substGen eq ts)

-- lift id = id  (as substitutions)

subst-lift-id : (x : Fin (1+ n)) → (liftSubst idSubst) x ≡ idSubst x
subst-lift-id x0     = refl
subst-lift-id (x +1) = refl

subst-lifts-id : (n : Nat) → (x : Fin (n + m)) → (liftSubstn idSubst n) x ≡ idSubst x
subst-lifts-id 0 x = refl
subst-lifts-id (1+ n) x0 = refl
subst-lifts-id (1+ n) (x +1) = cong wk1 (subst-lifts-id n x)

-- Identity substitution.

mutual
  subst-id : (t : Term n) → subst idSubst t ≡ t
  subst-id (var x) = refl
  subst-id (gen k ts) = cong (gen k) (substGen-id ts)

  substGen-id : ∀ {bs} g → substGen {n} {n} {bs} idSubst g ≡ g
  substGen-id [] = refl
  substGen-id (_∷_ {b = b} t ts) =
    cong₂ _∷_ (trans (substVar-to-subst (subst-lifts-id b) t )
                     (subst-id t))
              (substGen-id ts)

-- Correctness of composition of weakening and substitution.

-- Composition of liftings is lifting of the composition.
-- lift ρ •ₛ lift σ = lift (ρ •ₛ σ)

subst-lift-•ₛ : ∀ t
              → subst (lift ρ •ₛ liftSubst σ) t
              ≡ subst (liftSubst (ρ •ₛ σ)) t
subst-lift-•ₛ =
  substVar-to-subst (λ { x0 → refl ; (x +1) → sym (wk1-wk≡lift-wk1 _ _)})

helper1 : (n : Nat) (x : Fin (1+ n + m)) →
      (lift (liftn ρ n) •ₛ liftSubst (liftSubstn σ n)) x ≡
      liftSubst (liftSubstn (ρ •ₛ σ) n) x
helper1 0      x0     = refl
helper1 0      (x +1) = sym (wk1-wk≡lift-wk1 _ _)
helper1 (1+ n) x0     = refl
helper1 (1+ n) (x +1) = trans (sym (wk1-wk≡lift-wk1 _ _)) (cong wk1 (helper1 n x))

subst-lifts-•ₛ : ∀ n t
              → subst (liftn ρ n •ₛ liftSubstn σ n) t
              ≡ subst (liftSubstn (ρ •ₛ σ) n) t
subst-lifts-•ₛ 0 t = refl
subst-lifts-•ₛ (1+ n) t = substVar-to-subst (helper1 n) t

-- lift σ ₛ• lift ρ = lift (σ ₛ• ρ)

subst-lift-ₛ• : ∀ t
              → subst (liftSubst σ ₛ• lift ρ) t
              ≡ subst (liftSubst (σ ₛ• ρ)) t
subst-lift-ₛ• = substVar-to-subst (λ { x0 → refl ; (x +1) → refl})

helper2 : (n : Nat) → (x : Fin (1+ n + m))
        → liftSubst (liftSubstn σ n) (wkVar (lift (liftn ρ n)) x) ≡
          liftSubst (liftSubstn (λ x₁ → σ (wkVar ρ x₁)) n) x
helper2 0 x0          = refl
helper2 0 (x +1)      = refl
helper2 (1+ n) x0     = refl
helper2 (1+ n) (x +1) = cong wk1 (helper2 n x)

subst-lifts-ₛ• : ∀ n t
              → subst (liftSubstn σ n ₛ• liftn ρ n) t
              ≡ subst (liftSubstn (σ ₛ• ρ) n) t
subst-lifts-ₛ• 0 t = refl
subst-lifts-ₛ• (1+ n) t = substVar-to-subst (helper2 n) t

-- wk ρ ∘ subst σ = subst (ρ •ₛ σ)

mutual
  wk-subst : ∀ t → wk ρ (subst σ t) ≡ subst (ρ •ₛ σ) t
  wk-subst (var x) = refl
  wk-subst (gen k ts) = cong (gen k) (wkGen-substGen ts)

  wkGen-substGen : ∀ {bs} t → wkGen ρ (substGen σ t) ≡ substGen {bs = bs} (ρ •ₛ σ) t
  wkGen-substGen [] = refl
  wkGen-substGen (_∷_ {b = b} t ts) =
    cong₂ _∷_ (trans (wk-subst t) ( subst-lifts-•ₛ b t)) (wkGen-substGen ts)

-- subst σ ∘ wk ρ = subst (σ •ₛ ρ)

mutual
  subst-wk : ∀ t → subst σ (wk ρ t) ≡ subst (σ ₛ• ρ) t
  subst-wk (var x) = refl
  subst-wk (gen k ts) = cong (gen k) (substGen-wkGen ts)

  substGen-wkGen : ∀ {bs} t → substGen σ (wkGen ρ t) ≡ substGen {bs = bs} (σ ₛ• ρ) t
  substGen-wkGen [] = refl
  substGen-wkGen (_∷_ {b = b} t ts) =
    cong₂ _∷_ (trans (subst-wk t) (subst-lifts-ₛ• b t)) (substGen-wkGen ts)

-- Composition of liftings is lifting of the composition.

wk-subst-lift : (G : Term (1+ n))
              → wk (lift ρ) (subst (liftSubst σ) G)
              ≡ subst (liftSubst (ρ •ₛ σ)) G
wk-subst-lift G = trans (wk-subst G) (subst-lift-•ₛ G)

-- Renaming with ρ is the same as substituting with ρ turned into a substitution.

wk≡subst : (ρ : Wk m n) (t : Term n) → wk ρ t ≡ subst (toSubst ρ) t
wk≡subst ρ t = trans (cong (wk ρ) (sym (subst-id t))) (wk-subst t)

-- Composition of substitutions.

-- Composition of liftings is lifting of the composition.

substCompLift : ∀ x
              → (liftSubst σ ₛ•ₛ liftSubst σ′) x
              ≡ (liftSubst (σ ₛ•ₛ σ′)) x
substCompLift                    x0    = refl
substCompLift {σ = σ} {σ′ = σ′} (x +1) = trans (subst-wk (σ′ x)) (sym (wk-subst (σ′ x)))

substCompLifts : ∀ n x
              → (liftSubstn σ n ₛ•ₛ liftSubstn σ′ n) x
              ≡ (liftSubstn (σ ₛ•ₛ σ′) n) x
substCompLifts                   0       x     = refl
substCompLifts                   (1+ n)  x0    = refl
substCompLifts {σ = σ} {σ′ = σ′} (1+ n) (x +1) =
  trans (substCompLift {σ = liftSubstn σ n} {σ′ = liftSubstn σ′ n} (x +1))
        (cong wk1 (substCompLifts n x))
-- Soundness of the composition of substitutions.

mutual
  substCompEq : ∀ (t : Term n)
              → subst σ (subst σ′ t) ≡ subst (σ ₛ•ₛ σ′) t
  substCompEq (var x) = refl
  substCompEq (gen k ts) = cong (gen k) (substGenCompEq ts)

  substGenCompEq : ∀ {bs} t
              → substGen σ (substGen σ′ t) ≡ substGen {bs = bs} (σ ₛ•ₛ σ′) t
  substGenCompEq [] = refl
  substGenCompEq (_∷_ {b = b} t ts) =
    cong₂ _∷_ (trans (substCompEq t) (substVar-to-subst (substCompLifts b) t))
              (substGenCompEq ts)

-- Weakening single substitutions.

-- Pulling apart a weakening composition in specific context _[a].

wk-comp-subst : ∀ {a} (ρ : Wk m ℓ) (ρ′ : Wk ℓ n) G
  → wk (lift (ρ • ρ′)) G [ a ] ≡ wk (lift ρ) (wk (lift ρ′) G) [ a ]

wk-comp-subst {a = a} ρ ρ′ G =
  cong (λ x → x [ a ]) (sym (wk-comp (lift ρ) (lift ρ′) G))

-- Pushing a weakening into a single substitution.
-- ρ (t[a]) = ((lift ρ) t)[ρ a]

wk-β : ∀ {a} t → wk ρ (t [ a ]) ≡ wk (lift ρ) t [ wk ρ a ]
wk-β t = trans (wk-subst t) (sym (trans (subst-wk t)
               (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t)))

-- Pushing a weakening into a single shifting substitution.
-- If  ρ′ = lift ρ  then  ρ′(t[a]↑) = ρ′(t) [ρ′(a)]↑

wk-β↑ : ∀ {a} t → wk (lift ρ) (t [ a ]↑) ≡ wk (lift ρ) t [ wk (lift ρ) a ]↑
wk-β↑ t = trans (wk-subst t) (sym (trans (subst-wk t)
                (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t)))

-- A specific equation on weakenings used for the reduction of natrec.

wk-β-natrec : ∀ (ρ : Wk m n )G
  → Π ℕ ▹ (Π wk (lift ρ) G ▹ wk (lift (lift ρ)) (wk1 (G [ suc (var x0) ]↑)))
  ≡ Π ℕ ▹ (wk (lift ρ) G ▹▹ wk (lift ρ) G [ suc (var x0) ]↑)
wk-β-natrec ρ G =
  cong₂ Π_▹_ refl (cong₂ Π_▹_ refl
    (trans (wk-comp (lift (lift ρ)) (step id)
                    (subst (consSubst (wk1Subst var) (suc (var x0))) G))
       (trans (wk-subst G) (sym (trans (wk-subst (wk (lift ρ) G))
         (trans (subst-wk G)
                (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) G)))))))

-- Composing a singleton substitution and a lifted substitution.
-- sg u ∘ lift σ = cons id u ∘ lift σ = cons σ u

substVarSingletonComp : ∀ {u} (x : Fin (1+ n))
  → (sgSubst u ₛ•ₛ liftSubst σ) x ≡ (consSubst σ u) x
substVarSingletonComp x0 = refl
substVarSingletonComp {σ = σ} (x +1) = trans (subst-wk (σ x)) (subst-id (σ x))

-- The same again, as action on a term t.

substSingletonComp : ∀ {a} t
  → subst (sgSubst a ₛ•ₛ liftSubst σ) t ≡ subst (consSubst σ a) t
substSingletonComp = substVar-to-subst substVarSingletonComp

-- A single substitution after a lifted substitution.
-- ((lift σ) G)[t] = (cons σ t)(G)

singleSubstComp : ∀ t (σ : Subst m n) G
                 → (subst (liftSubst σ) G) [ t ]
                 ≡ subst (consSubst σ t) G
singleSubstComp t σ G = trans (substCompEq G) (substSingletonComp G)

-- A single substitution after a lifted substitution (with weakening).
-- ((lift (ρ ∘ σ)) G)[t] = (cons (ρ ∘ σ) t)(G)

singleSubstWkComp : ∀ t (σ : Subst m n) G
               → wk (lift ρ) (subst (liftSubst σ) G) [ t ]
               ≡ subst (consSubst (ρ •ₛ σ) t) G
singleSubstWkComp t σ G =
  trans (cong (subst (consSubst var t))
              (trans (wk-subst G) (subst-lift-•ₛ G)))
        (trans (substCompEq G) (substSingletonComp G))

-- Pushing a substitution into a single substitution.

singleSubstLift : ∀ G t
                → subst σ (G [ t ])
                ≡ subst (liftSubst σ) G [ subst σ t ]
singleSubstLift G t =
  trans (substCompEq G)
        (trans (trans (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) G)
                      (sym (substSingletonComp G)))
               (sym (substCompEq G)))

-- More specific laws.

idWkLiftSubstLemma : ∀ (σ : Subst m n) G
  → wk (lift (step id)) (subst (liftSubst σ) G) [ var x0 ]
  ≡ subst (liftSubst σ) G
idWkLiftSubstLemma σ G =
  trans (singleSubstWkComp (var x0) σ G)
        (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) G)

substVarComp↑ : ∀ {t} (σ : Subst m n) x
  → (consSubst (wk1Subst idSubst) (subst (liftSubst σ) t) ₛ•ₛ liftSubst σ) x
  ≡ (liftSubst σ ₛ•ₛ consSubst (wk1Subst idSubst) t) x
substVarComp↑ σ x0 = refl
substVarComp↑ σ (x +1) = trans (subst-wk (σ x)) (sym (wk≡subst (step id) (σ x)))

singleSubstLift↑ : ∀ (σ : Subst m n) G t
                 → subst (liftSubst σ) (G [ t ]↑)
                 ≡ subst (liftSubst σ) G [ subst (liftSubst σ) t ]↑
singleSubstLift↑ σ G t =
  trans (substCompEq G)
        (sym (trans (substCompEq G) (substVar-to-subst (substVarComp↑ σ) G)))

substConsComp : ∀ {t G}
       → subst (consSubst (λ x → σ (x +1)) (subst (tail σ) t)) G
       ≡ subst σ (subst (consSubst (λ x → var (x +1)) (wk1 t)) G)
substConsComp {t = t} {G = G} =
  trans (substVar-to-subst (λ { x0 → sym (subst-wk t) ; (x +1) → refl }) G)
        (sym (substCompEq G))

wkSingleSubstId : (F : Term (1+ n)) → (wk (lift (step id)) F) [ var x0 ] ≡ F
wkSingleSubstId F =
  trans (subst-wk F)
        (trans (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) F)
               (subst-id F))

cons-wk-subst : ∀ (ρ : Wk m n) (σ : Subst n ℓ) a t
       → subst (sgSubst a ₛ• lift ρ ₛ•ₛ liftSubst σ) t
       ≡ subst (consSubst (ρ •ₛ σ) a) t
cons-wk-subst ρ σ a = substVar-to-subst
  (λ { x0 → refl
     ; (x +1) → trans (subst-wk (σ x)) (sym (wk≡subst ρ (σ x))) })

natrecSucCaseLemma : (x : Fin (1+ n))
  → (step id •ₛ consSubst (wk1Subst idSubst) (suc (var x0)) ₛ•ₛ liftSubst σ) x
  ≡ (liftSubst (liftSubst σ) ₛ• step id ₛ•ₛ consSubst (wk1Subst idSubst) (suc (var x0))) x
natrecSucCaseLemma x0 = refl
natrecSucCaseLemma {σ = σ} (x +1) =
  trans (subst-wk (σ x))
           (sym (trans (wk1-wk (step id) _)
                             (wk≡subst (step (step id)) (σ x))))

natrecSucCase : ∀ (σ : Subst m n) F
  → Π ℕ ▹ (Π subst (liftSubst σ) F
                ▹ subst (liftSubst (liftSubst σ)) (wk1 (F [ suc (var x0) ]↑)))
  ≡ Π ℕ ▹ (subst (liftSubst σ) F ▹▹ subst (liftSubst σ) F [ suc (var x0) ]↑)
natrecSucCase σ F =
  cong₂ Π_▹_ refl
    (cong₂ Π_▹_ refl
       (trans (trans (subst-wk (F [ suc (var x0) ]↑))
                           (substCompEq F))
                 (sym (trans (wk-subst (subst (liftSubst σ) F))
                                   (trans (substCompEq F)
                                             (substVar-to-subst natrecSucCaseLemma F))))))

natrecIrrelevantSubstLemma : ∀ F z s m (σ : Subst ℓ n) (x : Fin (1+ n))
  → (sgSubst (natrec (subst (liftSubst σ) F) (subst σ z) (subst σ s) m)
     ₛ•ₛ liftSubst (sgSubst m)
     ₛ•ₛ liftSubst (liftSubst σ)
     ₛ•  step id
     ₛ•ₛ consSubst (tail idSubst) (suc (var x0))) x
  ≡ (consSubst σ (suc m)) x
natrecIrrelevantSubstLemma F z s m σ x0 =
  cong suc (trans (subst-wk m) (subst-id m))
natrecIrrelevantSubstLemma F z s m σ (x +1) =
  trans (subst-wk (wk (step id) (σ x)))
           (trans (subst-wk (σ x))
                     (subst-id (σ x)))

natrecIrrelevantSubst : ∀ F z s m (σ : Subst ℓ n)
  → subst (consSubst σ (suc m)) F
  ≡ subst (liftSubst (sgSubst m))
          (subst (liftSubst (liftSubst σ))
                 (wk1 (F [ suc (var x0) ]↑)))
                   [ natrec (subst (liftSubst σ) F) (subst σ z) (subst σ s) m ]
natrecIrrelevantSubst F z s m σ =
  sym (trans (substCompEq (subst (liftSubst (liftSubst σ))
        (wk (step id)
         (subst (consSubst (tail idSubst) (suc (var x0))) F))))
         (trans (substCompEq (wk (step id)
        (subst (consSubst (tail idSubst) (suc (var x0))) F)))
        (trans
           (subst-wk (subst (consSubst (tail idSubst) (suc (var x0))) F))
           (trans (substCompEq F)
                     (substVar-to-subst (natrecIrrelevantSubstLemma F z s m σ) F)))))

natrecIrrelevantSubstLemma′ : ∀ F z s n (x : Fin (1+ m))
  → (sgSubst (natrec F z s n)
     ₛ•ₛ liftSubst (sgSubst n)
     ₛ•  step id
     ₛ•ₛ consSubst (tail idSubst) (suc (var x0))) x
  ≡ (consSubst var (suc n)) x
natrecIrrelevantSubstLemma′ F z s n x0 =
  cong suc (trans (subst-wk n) (subst-id n))
natrecIrrelevantSubstLemma′ F z s n (x +1) = refl

natrecIrrelevantSubst′ : ∀ (F : Term (1+ m)) z s n
  → subst (liftSubst (sgSubst n))
      (wk1 (F [ suc (var x0) ]↑))
      [ natrec F z s n ]
  ≡ F [ suc n ]
natrecIrrelevantSubst′ F z s n =
  trans (substCompEq (wk (step id)
                         (subst (consSubst (tail idSubst) (suc (var x0))) F)))
        (trans (subst-wk (subst (consSubst (tail idSubst) (suc (var x0))) F))
               (trans (substCompEq F)
                      (substVar-to-subst (natrecIrrelevantSubstLemma′ F z s n) F)))

cons0wkLift1-id : ∀ (σ : Subst m n) G
    → subst (sgSubst (var x0))
            (wk (lift (step id)) (subst (liftSubst σ) G))
    ≡ subst (liftSubst σ) G
cons0wkLift1-id σ G =
  trans (subst-wk (subst (liftSubst σ) G))
        (trans (substVar-to-subst (λ { x0 → refl ; (x +1) → refl })
                                  (subst (liftSubst σ) G))
               (subst-id (subst (liftSubst σ) G)))

substConsId : ∀ {t} G
        → subst (consSubst σ (subst σ t)) G
        ≡ subst σ (subst (sgSubst t) G)
substConsId G =
  sym (trans (substCompEq G)
             (substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) G))

substConsTailId : ∀ {G t}
                → subst (consSubst (tail σ) (subst σ t)) G
                ≡ subst σ (subst (consSubst (tail idSubst) t) G)
substConsTailId {G = G} =
  trans (substVar-to-subst (λ { x0 → refl
                            ; (x +1) → refl }) G)
        (sym (substCompEq G))

substConcatSingleton′ : ∀ {a} t
                      → subst (σ ₛ•ₛ sgSubst a) t
                      ≡ subst (consSubst σ (subst σ a)) t
substConcatSingleton′ t = substVar-to-subst (λ { x0 → refl ; (x +1) → refl}) t

wk1-tailId : (t : Term n) → wk1 t ≡ subst (tail idSubst) t
wk1-tailId t = trans (sym (subst-id (wk1 t))) (subst-wk t)

wk1-sgSubst : ∀ (t : Term n) t' → (wk1 t) [ t' ] ≡ t
wk1-sgSubst t t' rewrite wk1-tailId t =
  let substVar-sgSubst-tail : ∀ a n → (sgSubst a ₛ•ₛ tail idSubst) n ≡ idSubst n
      substVar-sgSubst-tail a n = refl
  in  trans (trans
        (substCompEq t)
        (substVar-to-subst (substVar-sgSubst-tail t') t))
      (subst-id t)

max_stars_repo_name: fhlkfy/logrel-mltt

max_issues_repo_name: fhlkfy/logrel-mltt

max_forks_repo_name: fhlkfy/logrel-mltt


text:
{-# OPTIONS --without-K --safe #-}

open import Algebra
open import Relation.Unary
open import Relation.Binary hiding (Decidable)

module Data.FingerTree.Split.Point
  {r m}
  (ℳ : Monoid r m)
  {s}
  {ℙ : Pred (Monoid.Carrier ℳ) s}
  (ℙ-resp : ℙ Respects (Monoid._≈_ ℳ))
  (ℙ? : Decidable ℙ)
  where

open import Relation.Nullary using (¬_; yes; no; Dec)
open import Level using (_⊔_)
open import Data.Product
open import Function
open import Data.List as List using (List; _∷_; [])

open import Data.FingerTree.Measures ℳ
open import Data.FingerTree.Reasoning ℳ

open import Relation.Nullary using (Dec; yes; no)
open import Relation.Nullary.Decidable using (True; toWitness; False; toWitnessFalse)

open σ ⦃ ... ⦄

open Monoid ℳ renaming (Carrier to 𝓡)

open import Data.FingerTree.Relation.Binary.Reasoning.FasterInference.Setoid setoid

infixr 5 _∣_
record _∣_ (left focus : 𝓡) : Set s where
  constructor ¬[_]ℙ[_]
  field
    ¬ℙ : ¬ ℙ left
    !ℙ : ℙ (left ∙ focus)
open _∣_ public

_∣?_ : ∀ x y → Dec (x ∣ y)
x ∣? y with ℙ? x
... | yes p = no λ c → ¬ℙ c p
... | no ¬p with ℙ? (x ∙ y)
... | no ¬c = no (¬c ∘ !ℙ)
... | yes p = yes ¬[ ¬p ]ℙ[ p ]

infixl 2 _≈◄⟅_⟆ _≈▻⟅_⟆ _≈⟅_∣_⟆ _◄_ _▻_
_◄_ : ∀ {l f₁ f₂} → l ∣ f₁ ∙ f₂ → ¬ ℙ (l ∙ f₁) → (l ∙ f₁) ∣ f₂
!ℙ (p ◄ ¬ℙf) = ℙ-resp (sym (assoc _ _ _)) (!ℙ p)
¬ℙ (p ◄ ¬ℙf) = ¬ℙf

_▻_ : ∀ {l f₁ f₂} → l ∣ f₁ ∙ f₂ → ℙ (l ∙ f₁) → l ∣ f₁
!ℙ (p ▻ ℙf) = ℙf
¬ℙ (p ▻ ℙf) = ¬ℙ p

_≈◄⟅_⟆ : ∀ {x y z} → x ∣ y → x ≈ z → z ∣ y
¬ℙ (x⟅y⟆ ≈◄⟅ x≈z ⟆) = ¬ℙ x⟅y⟆ ∘ ℙ-resp (sym x≈z)
!ℙ (x⟅y⟆ ≈◄⟅ x≈z ⟆) = ℙ-resp (≪∙ x≈z) (!ℙ x⟅y⟆)

_≈▻⟅_⟆ : ∀ {x y z} → x ∣ y → y ≈ z → x ∣ z
¬ℙ (x⟅y⟆ ≈▻⟅ y≈z ⟆) = ¬ℙ x⟅y⟆
!ℙ (x⟅y⟆ ≈▻⟅ y≈z ⟆) = ℙ-resp (∙≫ y≈z) (!ℙ x⟅y⟆)

_≈⟅_∣_⟆ : ∀ {x₁ y₁ x₂ y₂} → x₁ ∣ y₁ → x₁ ≈ x₂ → y₁ ≈ y₂ → x₂ ∣ y₂
¬ℙ (x⟅y⟆ ≈⟅ x≈ ∣ y≈ ⟆) = ¬ℙ x⟅y⟆ ∘ ℙ-resp (sym x≈)
!ℙ (x⟅y⟆ ≈⟅ x≈ ∣ y≈ ⟆) = ℙ-resp (∙-cong x≈ y≈) (!ℙ x⟅y⟆)

¬∄ℙ : ∀ {i} → ¬ (i ∣ ε)
¬∄ℙ i⟅ε⟆ = ¬ℙ i⟅ε⟆ (ℙ-resp (identityʳ _) (!ℙ i⟅ε⟆))

max_stars_repo_name: oisdk/agda-indexed-fingertree

max_issues_repo_name: oisdk/agda-indexed-fingertree

max_forks_repo_name: oisdk/agda-indexed-fingertree