text:
{-# OPTIONS --no-universe-polymorphism #-}
open import Induction.WellFounded as WF
open import Data.Product
open import Relation.Binary.Core
open import Relation.Unary as U using (Decidable)
open import Relation.Nullary
import Level as L using (zero)

module DivideEtImpera where
{-- This module implements a quite general version of Divide and Conquer as desribed by Douglas R. Smith in his paper
   "The Design of Divide and Conquer Algorithms" 1984. the function makeD&C requires a well founded relation, a decidable proposition
   of whether a given input is primitive, a composition and a decomposition function, a special function g and a function dirSolve.
   All of these functions have to fullfill certain conditions and lastly you also need an "induction principle" that describes that these
   functions work well together. After putting in all this work, you can finally reap your reward: an algorithm that does what you want:
   takes inputs that satisfy the input condition and returns results that satisfy the output condition.
 --}

{-- these 2 functions should be somewhere in the agda standard libraries but i couln't find them so i just wrote them again --}

foldAcc : {A : Set} → {_<_ : Rel A L.zero} → {R : A → Set} →
          (step : (x : A) → ((y : A) → _<_ y x → R y) → R x) →
          (z : A) → Acc _<_ z → R z
foldAcc step z (acc a) = step z (λ y y<z → foldAcc step y (a y y<z))

wfInd : {A : Set} {_<_ : Rel A _} → (WellFounded _<_) →
        {R : A → Set} →
        (step : (x : A) → ((y : A) → _<_ y x → R y) → R x) →
        (z : A) → R z
wfInd wf step z = foldAcc step z (wf z)

{- the algorithm itself as one huge function:
 instead of requiring all the functions and then five axioms describing their behaiviour, i use
 dependent types to embedd four of the axions in therespective function they describe and
 only the last one (called "lemma" here) as an extra. See the paper for details -}

makeD&C1 : {D₁ R₁ D₂ R₂ : Set} {I₁ : D₁ → Set} {O₁ : D₁ → R₁ → Set} {I₂ : D₂ → Set}
           {O₂ : D₂ → R₂ → Set} {O₃ : D₁ → (D₂ × D₁) → Set} {O₄ : (R₂ × R₁) → R₁ → Set}
           {_<_ : Rel D₁ _} → (wf : Well-founded _<_) → {Prim : D₁ → Set} → (pDec : U.Decidable Prim) →
           (decomp : (x : D₁) → I₁ x → ¬ Prim x → Σ (D₂ × D₁)
                   λ y → I₂ (proj₁ y) × (I₁ (proj₂ y)) × (_<_ (proj₂ y) x) × (O₃ x y) ) →
           (comp : (u : (R₂ × R₁)) → Σ R₁ (O₄ u)) →
           (g : (x : D₂) → I₂ x → Σ R₂ (O₂ x)) →
           (dirSolve : (x : D₁) → I₁ x → Prim x → Σ R₁ (O₁ x)) →
           (lemma : ∀{x₀ x₁ x₂ z₀ z₁ z₂} → O₃ x₀ (x₁ , x₂) → O₂ x₁ z₁ → O₁ x₂ z₂ → O₄ (z₁ , z₂) z₀ → O₁ x₀ z₀) →
           (x : D₁) → I₁ x → Σ R₁ (O₁ x)

makeD&C1 {D₁ = D₁} {R₁ = R₁} {I₁ = I₁} {O₁ = O₁} {_<_ = _<_} wf {Prim} pDec decomp comp g dirSolve lemma x = wfInd wf step x where
                                                step : (x : D₁) → ((y : D₁) → _<_ y x → I₁ y → Σ R₁ (O₁ y)) → I₁ x → Σ R₁ (O₁ x)
                                                step x rec ix with (pDec x)
                                                step x rec ix | (yes pfY) = dirSolve x ix pfY
                                                step x rec ix | (no  pfN) = let dec = decomp x ix pfN
                                                                                decV  = proj₁ dec
                                                                                decV1 = proj₁ decV
                                                                                decV2 = proj₂ decV
                                                                                decP  = proj₂ dec
                                                                                decP1 = proj₁ decP
                                                                                decP2 = proj₁ (proj₂ decP)
                                                                                decP3 = proj₁ (proj₂ (proj₂ decP))
                                                                                decP4 = proj₂ (proj₂ (proj₂ decP))
                                                                                gRes  = g decV1 decP1
                                                                                gV    = proj₁ gRes
                                                                                gP    = proj₂ gRes
                                                                                fRes  = rec decV2 decP3 decP2
                                                                                fV    = proj₁ fRes
                                                                                fP    = proj₂ fRes
                                                                                com   = comp (gV , fV)
                                                                                comV  = proj₁ com
                                                                                comP  = proj₂ com
                                                                                proof = lemma decP4 gP fP comP
                                                                             in (comV , proof)

{- it occurred to me, that a proper Divide and conquer algorithm should make (at least) two recursive calls,
   the algorithm describen inthe pape, however, only makes one! So slightly modified it to fit in that extra
   recursive calls but left the basic principle exactly the same in this second version -}

makeD&C2 : {D₁ R₁ D₂ R₂ : Set} {I₁ : D₁ → Set} {O₁ : D₁ → R₁ → Set} {I₂ : D₂ → Set}
                 {O₂ : D₂ → R₂ → Set} {O₃ : D₁ → (D₂ × (D₁ × D₁)) → Set} {O₄ : (R₂ × (R₁ × R₁)) → R₁ → Set}
                 {_<_ : Rel D₁ _} → (wf : Well-founded _<_) → {Prim : D₁ → Set} → (pDec : U.Decidable Prim) →
                 (decomp : (x : D₁) → I₁ x → ¬ Prim x → Σ (D₂ × (D₁ × D₁))
                           λ y → (I₂ (proj₁ y)) × (I₁ (proj₁ (proj₂ y))) × (I₁ (proj₂ (proj₂ y))) ×
                                 (_<_ (proj₁ (proj₂ y)) x) × (_<_ (proj₂ (proj₂ y)) x) × (O₃ x y) ) →
                 (comp : (u : (R₂ × (R₁ × R₁)) ) → Σ R₁ (O₄ u)) →
                 (g : (x : D₂) → I₂ x → Σ R₂ (O₂ x)) →
                 (dirSolve : (x : D₁) → I₁ x → Prim x → Σ R₁ (O₁ x)) →
                 (lemma : ∀{x₀ x₁ x₂ x₃ z₀ z₁ z₂ z₃} → O₃ x₀ (x₁ , (x₂ , x₃ )) → O₂ x₁ z₁ → O₁ x₂ z₂
                             → O₁ x₃ z₃ → O₄ (z₁ , (z₂ , z₃)) z₀ → O₁ x₀ z₀) →
                 (x : D₁) → I₁ x → Σ R₁ (O₁ x)

makeD&C2 {D₁ = D₁} {R₁ = R₁} {I₁ = I₁} {O₁ = O₁} {_<_ = _<_} wf {Prim} pDec decomp comp g dirSolve lemma x = wfInd wf step x where
                                                step : (x : D₁) → ((y : D₁) → _<_ y x → I₁ y → Σ R₁ (O₁ y)) → I₁ x → Σ R₁ (O₁ x)
                                                step x rec ix with (pDec x)
                                                step x rec ix | (yes pfY) = dirSolve x ix pfY
                                                step x rec ix | (no  pfN) = let dec = decomp x ix pfN
                                                                                decV = proj₁ dec
                                                                                decV1 = proj₁ decV
                                                                                decV2 = proj₁ (proj₂ decV)
                                                                                decV3 = proj₂ (proj₂ decV)
                                                                                decP  = proj₂ dec
                                                                                decP1 = proj₁ decP
                                                                                decP2 = proj₁ (proj₂ decP)
                                                                                decP3 = proj₁ (proj₂ (proj₂ decP))
                                                                                decP4 = proj₁ (proj₂ (proj₂ (proj₂ decP)))
                                                                                decP5 = proj₁ (proj₂ (proj₂ (proj₂ (proj₂ decP))))
                                                                                decP6 = proj₂ (proj₂ (proj₂ (proj₂ (proj₂ decP))))
                                                                                gRes  = g decV1 decP1
                                                                                gV    = proj₁ gRes
                                                                                gP    = proj₂ gRes
                                                                                f1Res = rec decV2 decP4 decP2
                                                                                f1V   = proj₁ f1Res
                                                                                f1P   = proj₂ f1Res
                                                                                f2Res = rec decV3 decP5 decP3
                                                                                f2V   = proj₁ f2Res
                                                                                f2P   = proj₂ f2Res
                                                                                com   = comp (gV , (f1V , f2V))
                                                                                comV  = proj₁ com
                                                                                comP  = proj₂ com
                                                                                proof = lemma decP6 gP f1P f2P comP
                                                                            in (comV , proof)

max_stars_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_issues_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda

max_forks_repo_name: NAMEhzj/Divide-and-Conquer-in-Agda


text:
------------------------------------------------------------------------------
-- Totality properties for Tree
------------------------------------------------------------------------------

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

module FOTC.Program.Mirror.Tree.TotalityI where

open import FOTC.Base
open import FOTC.Base.List
open import FOTC.Data.List
open import FOTC.Program.Mirror.Forest.TotalityI
open import FOTC.Program.Mirror.Mirror
open import FOTC.Program.Mirror.Type

------------------------------------------------------------------------------

mirror-Tree : ∀ {t} → Tree t → Tree (mirror · t)
mirror-Tree = Tree-mutual-ind {A} {B} hA B[] hB
  where
  A : D → Set
  A t = Tree (mirror · t)

  B : D → Set
  B ts = Forest (map mirror ts)

  hA : ∀ d {ts} → Forest ts → B ts → A (node d ts)
  hA d {ts} Fts Bts = subst Tree
                            (sym (mirror-eq d ts))
                            (tree d (reverse-Forest Bts))

  B[] : B []
  B[] = subst Forest (sym (map-[] mirror)) fnil

  hB : ∀ {t ts} → Tree t → A t → Forest ts → B ts → B (t ∷ ts)
  hB {t} {ts} Tt At Fts Bts =
    subst Forest (sym (map-∷ mirror t ts)) (fcons At Bts)

ext: agda

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
{-# OPTIONS --cubical --safe #-}

module Data.Binary.Testers where

open import Prelude
open import Data.Binary.Conversion.Fast.Strict
open import Data.Binary.Definition
open import Data.List using (List; _⋯_)
open import Data.List.Sugar using (liftA2)

test : (𝔹 → 𝔹 → 𝔹) →
       (ℕ → ℕ → ℕ) →
       ℕ → Type
test bf nf n = let ns = 0 ⋯ n in
  liftA2 (λ n m → bf ⟦ n ⇑⟧ ⟦ m ⇑⟧) ns ns ≡
  liftA2 (λ n m → ⟦ nf n m ⇑⟧) ns ns

import Data.Nat as ℕ
open import Data.Binary.Addition using (_+_)
open import Data.Binary.Multiplication using (_*_)

_ : test _+_ ℕ._+_ 15
_ = refl

_ : test _*_ ℕ._*_ 15
_ = refl

max_stars_repo_name: oisdk/agda-playground

max_issues_repo_name: oisdk/agda-playground

max_forks_repo_name: oisdk/agda-playground


text:
module FFI.Data.Either where

{-# FOREIGN GHC import qualified Data.Either #-}

data Either (A B : Set) : Set where
  Left : A → Either A B
  Right : B → Either A B
{-# COMPILE GHC Either = data Data.Either.Either (Data.Either.Left|Data.Either.Right) #-}

mapLeft : ∀ {A B C} → (A → B) → (Either A C) → (Either B C)
mapLeft f (Left x) = Left (f x)
mapLeft f (Right x) = Right x

mapRight : ∀ {A B C} → (B → C) → (Either A B) → (Either A C)
mapRight f (Left x) = Left x
mapRight f (Right x) = Right (f x)

max_issues_repo_name: XanderYZZ/luau

max_forks_repo_name: XanderYZZ/luau


text:
module Prelude.Data.Natural where

open import Prelude.Core
open import Prelude.Classes
open import Prelude.Orders

----------------
-- Conversion --
----------------

record ToNatural {ℓ} (A : Set ℓ) : Set ℓ where
  constructor mk[ToNatural]
  field
    𝕟 : A → ℕ
open ToNatural {{…}}

-----------
-- Order --
-----------

data _≤ⁿ_ : ℕ → ℕ → Set where
  Zero : ∀ {n} → Zero ≤ⁿ n
  Succ : ∀ {n₁ n₂} → n₁ ≤ⁿ n₂ → Succ n₁ ≤ⁿ Succ n₂

xRx⸢≤ⁿ⸣ : reflexive _≤ⁿ_
xRx⸢≤ⁿ⸣ {Zero} = Zero
xRx⸢≤ⁿ⸣ {Succ n} = Succ xRx⸢≤ⁿ⸣

⋈⸢≤ⁿ⸣ : antisymmetric _≤ⁿ_
⋈⸢≤ⁿ⸣ Zero Zero = ↯
⋈⸢≤ⁿ⸣ (Succ n₁≤n₂) (Succ n₂≤n₁) = res[•x] $ ⋈⸢≤ⁿ⸣ n₁≤n₂ n₂≤n₁

_⊚⸢≤ⁿ⸣_ : transitive _≤ⁿ_
n₁≤n₂ ⊚⸢≤ⁿ⸣ Zero = Zero
Succ n₂≤n₃ ⊚⸢≤ⁿ⸣ Succ n₁≤n₂ = Succ (n₂≤n₃ ⊚⸢≤ⁿ⸣ n₁≤n₂)

data _<ⁿ_ : ℕ → ℕ → Set where
  Zero : ∀ {n} → Zero <ⁿ Succ n
  Succ : ∀ {n₁ n₂} → n₁ <ⁿ n₂ → Succ n₁ <ⁿ Succ n₂

weaken[<]ⁿ : ∀ {n₁ n₂} → n₁ <ⁿ n₂ → n₁ ≤ⁿ n₂
weaken[<]ⁿ Zero = Zero
weaken[<]ⁿ (Succ <₁) = Succ (weaken[<]ⁿ <₁)

strict[<]ⁿ : ∀ {n₁ n₂} → n₁ <ⁿ n₂ → ¬ (n₂ ≤ⁿ n₁)
strict[<]ⁿ Zero ()
strict[<]ⁿ (Succ <₁) (Succ ≤₁) = strict[<]ⁿ <₁ ≤₁

complete[<]ⁿ : ∀ {n₁ n₂} → n₁ ≤ⁿ n₂ → ¬ (n₂ ≤ⁿ n₁) → n₁ <ⁿ n₂
complete[<]ⁿ {n₂ = Zero} Zero ¬≤ = exfalso (¬≤ Zero)
complete[<]ⁿ {n₂ = Succ n₂} Zero ¬≤ = Zero
complete[<]ⁿ (Succ ≤₁) ¬≤ = Succ (complete[<]ⁿ ≤₁ (λ ≤₂ → ¬≤ (Succ ≤₂)))

_⋚ⁿ_ : ℕ → ℕ → ⪥!
Zero ⋚ⁿ Zero = [≡]
Zero ⋚ⁿ Succ n₂ = [<]
Succ n₁ ⋚ⁿ Zero = [>]
Succ n₁ ⋚ⁿ Succ n₂ = n₁ ⋚ⁿ n₂

_⋚ⁿᴾ_ : ∀ n₁ n₂ → n₁ ⪥!ᴾ[ _<ⁿ_ ] n₂
Zero ⋚ⁿᴾ Zero = [≡] ↯
Zero ⋚ⁿᴾ Succ n₂ = [<] Zero
Succ n₁ ⋚ⁿᴾ Zero = [>] Zero
Succ n₁ ⋚ⁿᴾ Succ n₂ with n₁ ⋚ⁿᴾ n₂
… | [<] <₀ = [<] (Succ <₀)
… | [≡] ≡₀ rewrite ≡₀ = [≡] ↯
… | [>] >₀ = [>] (Succ >₀)

_⋚ⁿᴸ_ : ∀ n₁ n₂ → n₁ ⪥!ᴸ[ _<ⁿ_ ] n₂ ‖[ n₁ ⋚ⁿ n₂ , n₁ ⋚ⁿᴾ n₂ ]
Zero ⋚ⁿᴸ Zero = [≡]
Zero ⋚ⁿᴸ Succ n₂ = [<]
Succ n₁ ⋚ⁿᴸ Zero = [>]
Succ n₁ ⋚ⁿᴸ Succ n₂ with n₁ ⋚ⁿ n₂ | n₁ ⋚ⁿᴾ n₂ | n₁ ⋚ⁿᴸ n₂
… | [<] | [<] <₀ | [<] = [<]
… | [≡] | [≡] ≡₀ | [≡] rewrite ≡₀ = [≡]
… | [>] | [>] >₀ | [>] = [>]

instance
  Reflexive[≤]ⁿ : Reflexive _≤ⁿ_
  Reflexive[≤]ⁿ = record { xRx = xRx⸢≤ⁿ⸣ }
  Antisymmetric[≤]ⁿ : Antisymmetric _≤ⁿ_
  Antisymmetric[≤]ⁿ = record { ⋈ = ⋈⸢≤ⁿ⸣ }
  Transitive[≤]ⁿ : Transitive _≤ⁿ_
  Transitive[≤]ⁿ = record { _⊚_ = _⊚⸢≤ⁿ⸣_ }
  Strict[<]ⁿ : Strict _≤ⁿ_ _<ⁿ_
  Strict[<]ⁿ = record
    { weaken[≺] = weaken[<]ⁿ
    ; strict[≺] = strict[<]ⁿ
    ; complete[≺] = complete[<]ⁿ
    }
  Irreflexive[<]ⁿ : Irreflexive _<ⁿ_
  Irreflexive[<]ⁿ = Irreflexive[<]/≤ _≤ⁿ_ _<ⁿ_
  Asymmetric[<]ⁿ : Asymmetric _<ⁿ_
  Asymmetric[<]ⁿ = Asymmetric[<]/≤ _≤ⁿ_ _<ⁿ_
  Transitive[<]ⁿ : Transitive _<ⁿ_
  Transitive[<]ⁿ = Transitive[<]/≤ _≤ⁿ_ _<ⁿ_
  Totally[<]ⁿ : Totally _<ⁿ_
  Totally[<]ⁿ = record
    { _⪥_ = _⋚ⁿ_
    ; _⪥ᴾ_ = _⋚ⁿᴾ_
    ; _⪥ᴸ_ = _⋚ⁿᴸ_
    }
  Order[ℕ] : Order 0ᴸ ℕ
  Order[ℕ] = mk[Order] _≤ⁿ_ _<ⁿ_

weaken[≤]ⁿ : ∀ {n₁ n₂} → n₁ ≤ⁿ n₂ → n₁ ≤ⁿ Succ n₂
weaken[≤]ⁿ Zero = Zero
weaken[≤]ⁿ (Succ n₁≤n₂) = Succ (weaken[≤]ⁿ n₁≤n₂)

pred[≤]ⁿ : ∀ {n₁ n₂} → Succ n₁ ≤ⁿ n₂ → n₁ ≤ⁿ n₂
pred[≤]ⁿ (Succ x) = weaken[≤]ⁿ x

n≤succ : ∀ {n : ℕ} → n ≤ⁿ Succ n
n≤succ = weaken[≤]ⁿ xRx

rel[</≤]ⁿ : ∀ {n₁ n₂} → n₁ <ⁿ n₂ ↔ Succ n₁ ≤ⁿ n₂
rel[</≤]ⁿ = ⟨ LHS , RHS ⟩
  where
    LHS : ∀ {n₁ n₂} → n₁ <ⁿ n₂ → Succ n₁ ≤ⁿ n₂
    LHS Zero = Succ Zero
    LHS (Succ <₁) = Succ (LHS <₁)
    RHS : ∀ {n₁ n₂} → Succ n₁ ≤ⁿ n₂ → n₁ <ⁿ n₂
    RHS {Zero} (Succ ≤₁) = Zero
    RHS {Succ n₃} (Succ ≤₁) = Succ (RHS ≤₁)

------------------
-- ≤ⁿ Decidable --
------------------

instance
  DecRel[≡]ⁿ : DecRel (_≡_ {A = ℕ})
  DecRel[≡]ⁿ = record
    { _⁇_ = ⁇[≡]/⪥[] _≤_ _<_
    ; _⁇ᴾ_ = ⁇ᴾ[≡]/⪥[] _≤_ _<_
    ; _⁇ᴸ_ = ⁇ᴸ[≡]/⪥[] _≤_ _<_
    }
  DecRel[≤]ⁿ : DecRel _≤ⁿ_
  DecRel[≤]ⁿ = record
    { _⁇_ = ⁇[≤]/⪥[] _≤_ _<_
    ; _⁇ᴾ_ = ⁇ᴾ[≤]/⪥[] _≤_ _<_
    ; _⁇ᴸ_ = ⁇ᴸ[≤]/⪥[] _≤_ _<_
    }
  DecRel[<]ⁿ : DecRel _<ⁿ_
  DecRel[<]ⁿ = record
    { _⁇_ = ⁇[<]/⪥[] _≤_ _<_
    ; _⁇ᴾ_ = ⁇ᴾ[<]/⪥[] _≤_ _<_
    ; _⁇ᴸ_ = ⁇ᴸ[<]/⪥[] _≤_ _<_
    }

--------------
-- Addition --
--------------

_+ⁿ_ : ℕ → ℕ → ℕ
Zero +ⁿ n₂ = n₂
Succ n₁ +ⁿ n₂ = Succ (n₁ +ⁿ n₂)

left-unit[+]ⁿ : ∀ (n : ℕ) → 0 +ⁿ n ≡ n
left-unit[+]ⁿ n = ↯

right-unit[+]ⁿ : ∀ (n : ℕ) → n +ⁿ 0 ≡ n
right-unit[+]ⁿ Zero = ↯
right-unit[+]ⁿ (Succ n) rewrite right-unit[+]ⁿ n = ↯

associative[+]ⁿ : ∀ (n₁ n₂ n₃ : ℕ) → (n₁ +ⁿ n₂) +ⁿ n₃ ≡ n₁ +ⁿ (n₂ +ⁿ n₃)
associative[+]ⁿ Zero n₂ n₃ = ↯
associative[+]ⁿ (Succ n₁) n₂ n₃ rewrite associative[+]ⁿ n₁ n₂ n₃ = ↯

m+suc[n]=suc[m+n] : ∀ (n₁ n₂ : ℕ) → n₁ +ⁿ Succ n₂ ≡ Succ (n₁ +ⁿ n₂)
m+suc[n]=suc[m+n] Zero n₂ = ↯
m+suc[n]=suc[m+n] (Succ n₁) n₂ rewrite m+suc[n]=suc[m+n] n₁ n₂ = ↯

suc[m+n]=m+suc[n] : ∀ (n₁ n₂ : ℕ) → Succ (n₁ +ⁿ n₂) ≡ n₁ +ⁿ Succ n₂
suc[m+n]=m+suc[n] n₁ n₂ = ◇ $ m+suc[n]=suc[m+n] n₁ n₂

commutative[+]ⁿ : ∀ (n₁ n₂ : ℕ) → n₁ +ⁿ n₂ ≡ n₂ +ⁿ n₁
commutative[+]ⁿ Zero n₂ rewrite right-unit[+]ⁿ n₂ = ↯
commutative[+]ⁿ (Succ n₁) n₂ rewrite commutative[+]ⁿ n₁ n₂ | suc[m+n]=m+suc[n] n₂ n₁ = ↯

instance
  Additive[ℕ] : Additive ℕ
  Additive[ℕ] = record
    { zero = Zero
    ; _+_ = _+ⁿ_
    ; left-unit[+] = left-unit[+]ⁿ
    ; right-unit[+] = right-unit[+]ⁿ
    ; associative[+] = associative[+]ⁿ
    ; commutative[+] = commutative[+]ⁿ
    }

--------------------
-- Multiplication --
--------------------

oneⁿ : ℕ
oneⁿ = Succ Zero

_×ⁿ_ : ℕ → ℕ → ℕ
Zero ×ⁿ n₂ = Zero
Succ n₁ ×ⁿ n₂ = n₂ +ⁿ (n₁ ×ⁿ n₂)

left-zero[×]ⁿ : ∀ n → zero ×ⁿ n ≡ zero
left-zero[×]ⁿ n = ↯

right-zero[×]ⁿ : ∀ n → n ×ⁿ zero ≡ zero
right-zero[×]ⁿ Zero = ↯
right-zero[×]ⁿ (Succ n) rewrite right-zero[×]ⁿ n = ↯

left-unit[×]ⁿ : ∀ n → oneⁿ ×ⁿ n ≡ n
left-unit[×]ⁿ n = right-unit[+]ⁿ n

right-unit[×]ⁿ : ∀ n → n ×ⁿ oneⁿ ≡ n
right-unit[×]ⁿ Zero = ↯
right-unit[×]ⁿ (Succ n) rewrite right-unit[×]ⁿ n = ↯

distributive[×]ⁿ : ∀ n₁ n₂ n₃ → (n₁ +ⁿ n₂) ×ⁿ n₃ ≡ (n₁ ×ⁿ n₃) +ⁿ (n₂ ×ⁿ n₃)
distributive[×]ⁿ Zero n₂ n₃ = ↯
distributive[×]ⁿ (Succ n₁) n₂ n₃ rewrite distributive[×]ⁿ n₁ n₂ n₃ | associative[+]ⁿ n₃ (n₁ ×ⁿ n₃) (n₂ ×ⁿ n₃) = ↯

associative[×]ⁿ : ∀ n₁ n₂ n₃ → (n₁ ×ⁿ n₂) ×ⁿ n₃ ≡ n₁ ×ⁿ (n₂ ×ⁿ n₃)
associative[×]ⁿ Zero n₂ n₃ = ↯
associative[×]ⁿ (Succ n₁) n₂ n₃ rewrite distributive[×]ⁿ n₂ (n₁ ×ⁿ n₂) n₃ | associative[×]ⁿ n₁ n₂ n₃ = ↯

commutative[×]ⁿ : ∀ n₁ n₂ → n₁ ×ⁿ n₂ ≡ n₂ ×ⁿ n₁
commutative[×]ⁿ Zero n₂ rewrite right-zero[×]ⁿ n₂ = ↯
commutative[×]ⁿ n₁ Zero rewrite right-zero[×]ⁿ n₁ = ↯
commutative[×]ⁿ (Succ n₁) (Succ n₂)
  rewrite commutative[×]ⁿ n₁ (Succ n₂)
        | commutative[×]ⁿ n₂ (Succ n₁)
        | commutative[×]ⁿ n₁ n₂
        | ◇ $ associative[+]ⁿ n₁ n₂ (n₂ ×ⁿ n₁)
        | commutative[+]ⁿ n₁ n₂
        | associative[+]ⁿ n₂ n₁ (n₂ ×ⁿ n₁)
        = ↯

instance
  Multiplicative[ℕ] : Multiplicative ℕ
  Multiplicative[ℕ] = record
    { one = oneⁿ
    ; _×_ = _×ⁿ_
    ; left-zero[×] = left-zero[×]ⁿ
    ; right-zero[×] = right-zero[×]ⁿ
    ; left-unit[×] = left-unit[×]ⁿ
    ; right-unit[×] = right-unit[×]ⁿ
    ; associative[×] = associative[×]ⁿ
    ; commutative[×] = commutative[×]ⁿ
    ; distributive[×] = distributive[×]ⁿ
    }

-----------------
-- Subtraction --
-----------------

_-ⁿ_‖_ : ∀ (n₁ n₂ : ℕ) → n₂ ≤ n₁ → ℕ
n₁ -ⁿ Zero ‖ Zero = n₁
Succ n₁ -ⁿ Succ n₂ ‖ Succ n₁≤n₂ = n₁ -ⁿ n₂ ‖ n₁≤n₂

correct[-ⁿ‖] : ∀ n₁ n₂ (n₂≤n₁ : n₂ ≤ n₁) → n₂ + (n₁ -ⁿ n₂ ‖ n₂≤n₁) ≡ n₁
correct[-ⁿ‖] n₁ Zero Zero = ↯
correct[-ⁿ‖] (Succ n₁) (Succ n₂) (Succ n₂≤n₁) rewrite correct[-ⁿ‖] n₁ n₂ n₂≤n₁ = ↯

n-n=0 : ∀ n → n -ⁿ n ‖ xRx ≡ Zero
n-n=0 Zero = ↯
n-n=0 (Succ n) rewrite n-n=0 n = ↯

n-0=n : ∀ n → n -ⁿ 0 ‖ Zero ≡ n
n-0=n n = ↯

suc[m-n]=suc[m]-n : ∀ n₁ n₂ (n₂≤n₁ : n₂ ≤ n₁) → Succ (n₁ -ⁿ n₂ ‖ n₂≤n₁) ≡ Succ n₁ -ⁿ n₂ ‖ weaken[≤]ⁿ n₂≤n₁
suc[m-n]=suc[m]-n n₁ Zero Zero = ↯
suc[m-n]=suc[m]-n (Succ n₁) (Succ n₂) (Succ n₂≤n₁) rewrite suc[m-n]=suc[m]-n n₁ n₂ n₂≤n₁ = ↯

instance
  Subtractive/OK[ℕ] : Subtractive/OK ℕ
  Subtractive/OK[ℕ] = record { ok[_-_] = _≥_ }
  Subtractive[ℕ] : Subtractive/P ℕ
  Subtractive[ℕ] = record
    { _-_‖_ = _-ⁿ_‖_
    ; correct[-‖] = correct[-ⁿ‖]
    }

_-%ⁿ_ : ∀ (n₁ n₂ : ℕ) → ℕ ∨ ℕ
Zero -%ⁿ n₂ = Inr n₂
n₁ -%ⁿ Zero = Inl n₁
Succ n₁ -%ⁿ Succ n₂ = n₁ -%ⁿ n₂

correct[-%ⁿ]/spec : ℕ → ℕ → Set
correct[-%ⁿ]/spec n₁ n₂ with n₁ -%ⁿ n₂
… | Inl n = n₂ + n ≡ n₁
… | Inr n = n₁ + n ≡ n₂

correct[-%ⁿ] : ∀ n₁ n₂ → correct[-%ⁿ]/spec n₁ n₂
correct[-%ⁿ] Zero Zero = ↯
correct[-%ⁿ] Zero (Succ n₂) = ↯
correct[-%ⁿ] (Succ n₁) Zero = ↯
correct[-%ⁿ] (Succ n₁) (Succ n₂) with n₁ -%ⁿ n₂ | correct[-%ⁿ] n₁ n₂
… | Inl x | IH rewrite IH = ↯
… | Inr x | IH rewrite IH = ↯

--------------------------
-- Division and Modulus --
--------------------------

divmod-loop : ∀ (n₁ n₂ quo n₂-rem : ℕ) → n₂-rem ≤ n₂ → ∃ quo,n₂-rem ⦂ ℕ ∧ ℕ 𝑠𝑡 let ⟨ quo' , n₂-rem' ⟩ = quo,n₂-rem in n₂-rem' ≤ n₂
divmod-loop Zero n₂ quo n₂-rem n₂-rem≤n₂ = ⟨∃ ⟨ quo , n₂-rem ⟩ , n₂-rem≤n₂ ⟩
divmod-loop (Succ n₁) n₂ quo Zero n₂-rem≤n₂ = divmod-loop n₁ n₂ (Succ quo) n₂ xRx
divmod-loop (Succ n₁) n₂ quo (Succ n₂-rem) n₂-rem≤n₂ = divmod-loop n₁ n₂ quo n₂-rem (pred[≤]ⁿ n₂-rem≤n₂)

correct[divmod-loop] :
  ∀ (n₁ n₂ quo n₂-rem : ℕ) (n₂-rem≤n₂ : n₂-rem ≤ n₂)
  → let ⟨∃ ⟨ quo' , n₂-rem' ⟩ , n₂-rem'≤n₂ ⟩ = divmod-loop n₁ n₂ quo n₂-rem n₂-rem≤n₂ in
    quo' × Succ n₂ + (n₂ - n₂-rem' ‖ n₂-rem'≤n₂) ≡ n₁ + (quo × Succ n₂) + (n₂ - n₂-rem ‖ n₂-rem≤n₂)
correct[divmod-loop] Zero n₂ quo n₂-rem n₂-rem≤n₂ = ↯
correct[divmod-loop] (Succ n₁) n₂ quo Zero Zero
  with divmod-loop n₁ n₂ (Succ quo) n₂ xRx
     | correct[divmod-loop] n₁ n₂ (Succ quo) n₂ xRx
… | ⟨∃ ⟨ quo' , n₂-rem' ⟩ , n₂-rem'≤n₂ ⟩ | IH
  rewrite suc[m+n]=m+suc[n] n₁ (quo × Succ n₂ + n₂ - Zero ‖ Zero)
        | n-n=0 n₂
        | commutative[+] (quo × Succ n₂) n₂
        | right-unit[+] (n₂ + quo × Succ n₂)
        = IH
correct[divmod-loop] (Succ n₁) (Succ n₂) quo (Succ n₂-rem) (Succ n₂-rem≤n₂)
  with divmod-loop n₁ (Succ n₂) quo n₂-rem (weaken[≤]ⁿ n₂-rem≤n₂)
     | correct[divmod-loop] n₁ (Succ n₂) quo n₂-rem (weaken[≤]ⁿ n₂-rem≤n₂)
… | ⟨∃ ⟨ quo' , n₂-rem' ⟩ , n₂-rem'≤n₂ ⟩ | IH
  rewrite suc[m+n]=m+suc[n] n₁ (quo × Succ (Succ n₂) + n₂ - n₂-rem ‖ n₂-rem≤n₂)
        | suc[m+n]=m+suc[n] (quo × Succ (Succ n₂)) (n₂ - n₂-rem ‖ n₂-rem≤n₂)
        | suc[m-n]=suc[m]-n n₂ n₂-rem n₂-rem≤n₂
        = IH

_/%ⁿ_‖_ : ∀ (n₁ n₂ : ℕ) (0<n₂ : 0 < n₂) → ℕ ∧ ℕ
n₁ /%ⁿ Succ n₂ ‖ Zero with divmod-loop n₁ n₂ 0 n₂ xRx⸢≤ⁿ⸣
… | ⟨∃ ⟨ quo , n₂-rem ⟩ , n₂-rem≤n₂ ⟩ = ⟨ quo , n₂ - n₂-rem ‖ n₂-rem≤n₂ ⟩

correct[/%‖]ⁿ : ∀ n₁ n₂ (0<n₂ : 0 < n₂) → let ⟨ quo , rem ⟩ = n₁ /%ⁿ n₂ ‖ 0<n₂ in n₂ × quo + rem ≡ n₁
correct[/%‖]ⁿ n₁ (Succ n₂) Zero with divmod-loop n₁ n₂ 0 n₂ xRx | correct[divmod-loop] n₁ n₂ 0 n₂ xRx
… | ⟨∃ ⟨ quo , n₂-rem ⟩ , n₂-rem≤n₂ ⟩ | H rewrite n-n=0 n₂ | right-unit[+] n₁ | commutative[×] quo (Succ n₂) = H

instance
  DivMod/OK[ℕ] : DivMod/OK ℕ
  DivMod/OK[ℕ] = record
    { ok[_/%_] = (λ n₁ n₂ → 0 < n₂) }
  DivMod[ℕ] : DivMod/P ℕ
  DivMod[ℕ] = record
    { _/%_‖_ = _/%ⁿ_‖_
    ; correct[/%‖] = correct[/%‖]ⁿ
    }

-------------
-- Bounded --
-------------

record ℕ≤[_] (nᵇ : ℕ) : Set where
  constructor mk[ℕ≤]
  field
    n : ℕ
    n≤nᵇ : n ≤ nᵇ

-- mk↯[ℕ≤] : ∀ {nᵇ} n → {{_ : ✓‼ (n ⁇[ _≤_ ] nᵇ)}} → ℕ≤[ nᵇ ]
-- mk↯[ℕ≤] {nᵇ} n {{_}} with n ⁇[ _≤_ ] nᵇ |
-- mk↯[ℕ≤] {nᵇ} n {{↯Rel}} | Rel n≤nᵇ = mk[ℕ≤] n n≤nᵇ

weaken[ℕ≤] : ∀ {nᵇ₁ nᵇ₂} → nᵇ₁ ≤ nᵇ₂ → ℕ≤[ nᵇ₁ ] → ℕ≤[ nᵇ₂ ]
weaken[ℕ≤] nᵇ₁≤nᵇ₂ (mk[ℕ≤] n n≤nᵇ₁) = mk[ℕ≤] n (nᵇ₁≤nᵇ₂ ⊚ n≤nᵇ₁)

instance
  ToNatural[ℕ≤] : ∀ {nᵇ} → ToNatural ℕ≤[ nᵇ ]
  ToNatural[ℕ≤] = mk[ToNatural] ℕ≤[_].n

record ℕ<[_] (nᵇ : ℕ) : Set where
  constructor mk[ℕ<]
  field
    n : ℕ
    n<nᵇ : n < nᵇ

-- mk↯[ℕ<] : ∀ {nᵇ} n → {{_ : rel (dec-rel[ _<_ ] n nᵇ)}} → ℕ<[ nᵇ ]
-- mk↯[ℕ<] {nᵇ} n {{_}} with dec-rel[ _<_ ] n nᵇ
-- mk↯[ℕ<] {nᵇ} n {{↯Rel}} | Rel n<nᵇ = mk[ℕ<] n n<nᵇ

weaken[ℕ<] : ∀ {nᵇ₁ nᵇ₂} → nᵇ₁ ≤ nᵇ₂ → ℕ<[ nᵇ₁ ] → ℕ<[ nᵇ₂ ]
weaken[ℕ<] nᵇ₁≤nᵇ₂ (mk[ℕ<] n n<nᵇ₁) = mk[ℕ<] n $ π₂ rel[</≤]ⁿ $ nᵇ₁≤nᵇ₂ ⊚ π₁ rel[</≤]ⁿ n<nᵇ₁

instance
  ToNatural[ℕ<] : ∀ {nᵇ} → ToNatural ℕ<[ nᵇ ]
  ToNatural[ℕ<] = mk[ToNatural] ℕ<[_].n

data fin : ℕ → Set where
  Zero : ∀ {n} → fin (Succ n)
  Succ : ∀ {n} → fin n → fin (Succ n)

mk[fin/<] : ∀ {nᵇ} n → n < nᵇ → fin nᵇ
mk[fin/<] Zero Zero = Zero
mk[fin/<] (Succ n) (Succ <₁) = Succ (mk[fin/<] n <₁)

mk[fin/ℕ<] : ∀ {nᵇ} → ℕ<[ nᵇ ] → fin nᵇ
mk[fin/ℕ<] (mk[ℕ<] n n<nᵇ) = mk[fin/<] n n<nᵇ

record ℕ⁺ : Set where
  constructor mk[ℕ⁺]
  field
    n : ℕ
    0<n : 0 < n

-- mk↯[ℕ⁺] : ∀ n {{_ : rel (dec-rel[ _<_ ] 0 n)}} → ℕ⁺
-- mk↯[ℕ⁺] n {{_}} with dec-rel[ _<_ ] 0 n
-- mk↯[ℕ⁺] n {{↯Rel}} | Rel 0<n = mk[ℕ⁺] n 0<n

instance
  ToNatural[ℕ⁺] : ToNatural ℕ⁺
  ToNatural[ℕ⁺] = mk[ToNatural] ℕ⁺.n

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text: module Issue591.M where

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


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

module Experiment.TTG where

{-
data Phase : Set where
  parse : Phase
  scopecheck : Phase
  typecheck : Phase

xVar : Phase → Set
xVar p = ?

idP : Phase → Set
idP p = ?

xNew : Phase → Set

data Exp (p : Phase) : Set where
  var : xVar p → idP p → Exp p
  new : xNew p → Exp p
-}


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- This module is DEPRECATED. Please use
-- Data.List.Relation.Binary.Permutation.Inductive.Properties directly.
------------------------------------------------------------------------

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

module Data.List.Relation.Permutation.Inductive.Properties where

open import Data.List.Relation.Binary.Permutation.Inductive.Properties
  public

{-# WARNING_ON_IMPORT
"Data.List.Relation.Permutation.Inductive.Properties was deprecated in v1.0.
Use Data.List.Relation.Binary.Permutation.Inductive.Properties instead."
#-}


text:
module _ where

open import Agda.Builtin.Float
open import Common.Prelude hiding (_+_; _*_)

print : Float → IO Unit
print x = putStrLn (primShowFloat x)

printB : Bool → IO Unit
printB true  = putStrLn "true"
printB false = putStrLn "false"

_+_ = primFloatPlus
_*_ = primFloatTimes
_/_ = primFloatDiv
_==_ = primFloatEquality
_<_ = primFloatLess

NaN : Float
NaN = 0.0 / 0.0

Inf : Float
Inf = 1.0 / 0.0

-Inf : Float
-Inf = -1.0 / 0.0

pi : Float
pi = 3.141592653589793

main : IO Unit
main =
  putStr "123.0 = " ,, print 123.0 ,,
  putStr "NaN   = " ,, print NaN   ,,
  putStr "Inf   = " ,, print Inf   ,,
  putStr "-Inf  = " ,, print -Inf  ,,
  putStr "-0.0  = " ,, print -0.0  ,,
  -- Disabled due to #1856 and #1857
  -- putStr "√2    = " ,, print (primFloatTimes 2.0 (primSin (primFloatDiv pi 4.0))) ,,
  -- putStr "e     = " ,, print (primExp 1.0) ,,
  putStr "NaN == NaN = " ,, printB (NaN == NaN) ,,
  putStr "Inf == Inf = " ,, printB (Inf == Inf) ,,
  putStr "NaN < -Inf = " ,, printB (NaN < -Inf) ,,
  putStr "NaN < -5.0 = " ,, printB (NaN < -5.0) ,,
  return unit


text:
-- Andreas, 2015-07-01 polarity of the size argument to data
-- needs to be considered for polarity of later definitions.

-- {-# OPTIONS -v tc.pos:10 -v tc.polarity:20 #-}

open import Common.Size
open import Common.Prelude

data D : (i : Size) → Set where
  c : ∀ i → D (↑ i)

E : Bool → Size → Set
E true  i = D i
E false i = D i

cast : ∀{i b} → E b i → E b (↑ i)
cast x = x

-- should succeed

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- issue 685
module ShadowedLetBoundVar where

import Common.Level

record Wrap {a}(A : Set a) : Set a where
  constructor wrap
  field wrapped : A

-- let is not recursive
works : Set → Set
works x = let x = x in x

fails : Set → Set
fails A = let wrap A = wrap A in A
-- works now


text:
module hott.topology where

open import hott.topology.loopspace public

max_stars_repo_name: piyush-kurur/hott

max_issues_repo_name: piyush-kurur/hott

max_forks_repo_name: piyush-kurur/hott


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

module Codiscrete where

open import Level using (Level; 0ℓ; lift; lower)
open import Data.Nat using (ℕ; suc)
open import Data.Fin hiding (lift)
open import Data.Unit
open import Function renaming (id to idf)
open import Relation.Binary.PropositionalEquality
  using (_≡_; refl; sym; trans)

open import Categories.Category.Groupoid
open import Categories.Category.Instance.One
open import Categories.Category.Equivalence using (StrongEquivalence; WeakInverse)
open import Categories.Functor using (Functor; _∘F_) renaming (id to idF)
open import Categories.Category using (Category)
open import Categories.NaturalTransformation using (NaturalTransformation)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_)

-- Codiscrete Groupoid on (n+1) points
CodiscreteGroupoid : (n : ℕ) → Groupoid 0ℓ 0ℓ 0ℓ
CodiscreteGroupoid n = record
  { category = record
    { Obj = Fin (suc n)
    ; _⇒_ = λ _ _ → ⊤
    ; _≈_ = _≡_
    ; assoc = refl
    ; sym-assoc = refl
    ; identityˡ = refl
    ; identityʳ = refl
    ; equiv = record { refl = refl ; sym = sym ; trans = trans }
    ; ∘-resp-≈ = λ _ _ → refl
    }
  ; isGroupoid = record
    { _⁻¹ = idf
    ; iso = record { isoˡ = refl ; isoʳ = refl }
    }
  }

open Groupoid

Contractible : (n : ℕ) → (k : Fin (suc n)) →
  StrongEquivalence (category (CodiscreteGroupoid n)) (One {0ℓ} {0ℓ} {0ℓ})
Contractible n k = record
  { F = F
  ; G = G
  ; weak-inverse = record
    { F∘G≈id = F∘G≃id
    ; G∘F≈id = G∘F≃id
    }
  }
  where
  C : Category _ _ _
  C = category (CodiscreteGroupoid n)
  O : Category 0ℓ 0ℓ 0ℓ
  O = One
  F : Functor C O
  F = record
    { F₀ = λ _ → lift tt -- This is our 'GC' function
    ; F₁ = lift
    ; identity = lift tt
    ; homomorphism = lift tt
    ; F-resp-≈ = λ _ → lift tt
    }
  -- This is where 'k' is used:
  G : Functor O C
  G = record
    { F₀ = λ _ → k
    ; F₁ = lower
    ; identity = refl
    ; homomorphism = refl
    ; F-resp-≈ = λ _ → refl
    }
  F∘G≃id : F ∘F G ≃ idF
  F∘G≃id = record
    { F⇒G = record { η = idf ; commute = idf }
    ; F⇐G = record { η = idf ; commute = idf }
    }
  G∘F≃id : G ∘F F ≃ idF
  G∘F≃id = record
    { F⇒G = record { η = λ _ → tt ; commute = λ _ → refl }
    ; F⇐G = record { η = λ _ → tt ; commute = λ _ → refl }
    ; iso = λ X → record { isoˡ = refl ; isoʳ = refl }
    }

max_stars_repo_name: JacquesCarette/pi-dual

max_issues_repo_name: JacquesCarette/pi-dual

max_forks_repo_name: JacquesCarette/pi-dual


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic types related to coinduction
------------------------------------------------------------------------

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

module Codata.Musical.Notation where

open import Agda.Builtin.Coinduction public


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for Strings
------------------------------------------------------------------------

module Data.String.Core where

open import Data.List using (List)
open import Data.Bool using (Bool; true; false)
open import Data.Char.Core using (Char)

------------------------------------------------------------------------
-- The type

postulate
  String : Set

{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}

------------------------------------------------------------------------
-- Primitive operations

primitive
  primStringAppend   : String → String → String
  primStringToList   : String → List Char
  primStringFromList : List Char → String
  primStringEquality : String → String → Bool
  primShowString     : String → String

  -- Here instead of Data.Char.Core to avoid an import cycle
  primShowChar       : Char → String


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Some basic properties of Rings
------------------------------------------------------------------------

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

open import Algebra

module Algebra.Properties.Ring {r₁ r₂} (R : Ring r₁ r₂) where

open Ring R

import Algebra.Properties.AbelianGroup as AbelianGroupProperties
open import Function using (_$_)
open import Relation.Binary.Reasoning.Setoid setoid

------------------------------------------------------------------------
-- Export properties of abelian groups

open AbelianGroupProperties +-abelianGroup public
  renaming
  ( ε⁻¹≈ε            to -0#≈0#
  ; ∙-cancelˡ        to +-cancelˡ
  ; ∙-cancelʳ        to +-cancelʳ
  ; ∙-cancel         to +-cancel
  ; ⁻¹-involutive    to -‿involutive
  ; ⁻¹-injective     to -‿injective
  ; ⁻¹-anti-homo-∙   to -‿anti-homo-+
  ; identityˡ-unique to +-identityˡ-unique
  ; identityʳ-unique to +-identityʳ-unique
  ; identity-unique  to +-identity-unique
  ; inverseˡ-unique  to +-inverseˡ-unique
  ; inverseʳ-unique  to +-inverseʳ-unique
  ; ⁻¹-∙-comm        to -‿+-comm
  -- DEPRECATED
  ; left-identity-unique  to +-left-identity-unique
  ; right-identity-unique to +-right-identity-unique
  ; left-inverse-unique   to +-left-inverse-unique
  ; right-inverse-unique  to +-right-inverse-unique
  )

------------------------------------------------------------------------
-- Properties of -_

-‿distribˡ-* : ∀ x y → - (x * y) ≈ - x * y
-‿distribˡ-* x y = sym $ begin
  - x * y                        ≈⟨ sym $ +-identityʳ _ ⟩
  - x * y + 0#                   ≈⟨ +-congˡ $ sym (-‿inverseʳ _) ⟩
  - x * y + (x * y + - (x * y))  ≈⟨ sym $ +-assoc _ _ _  ⟩
  - x * y + x * y + - (x * y)    ≈⟨ +-congʳ $ sym (distribʳ _ _ _) ⟩
  (- x + x) * y + - (x * y)      ≈⟨ +-congʳ $ *-congʳ $ -‿inverseˡ _ ⟩
  0# * y + - (x * y)             ≈⟨ +-congʳ $ zeroˡ _ ⟩
  0# + - (x * y)                 ≈⟨ +-identityˡ _ ⟩
  - (x * y)                      ∎

-‿distribʳ-* : ∀ x y → - (x * y) ≈ x * - y
-‿distribʳ-* x y = sym $ begin
  x * - y                        ≈⟨ sym $ +-identityˡ _ ⟩
  0# + x * - y                   ≈⟨ +-congʳ $ sym (-‿inverseˡ _) ⟩
  - (x * y) + x * y + x * - y    ≈⟨ +-assoc _ _ _  ⟩
  - (x * y) + (x * y + x * - y)  ≈⟨ +-congˡ $ sym (distribˡ _ _ _)  ⟩
  - (x * y) + x * (y + - y)      ≈⟨ +-congˡ $ *-congˡ $ -‿inverseʳ _ ⟩
  - (x * y) + x * 0#             ≈⟨ +-congˡ $ zeroʳ _ ⟩
  - (x * y) + 0#                 ≈⟨ +-identityʳ _ ⟩
  - (x * y)                      ∎

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.1

-‿*-distribˡ : ∀ x y → - x * y ≈ - (x * y)
-‿*-distribˡ x y = sym (-‿distribˡ-* x y)
{-# WARNING_ON_USAGE -‿*-distribˡ
"Warning: -‿*-distribˡ was deprecated in v1.1.
Please use -‿distribˡ-* instead.
NOTE: the equality is flipped so you will need sym (-‿distribˡ-* ...)."
#-}
-‿*-distribʳ : ∀ x y → x * - y ≈ - (x * y)
-‿*-distribʳ x y = sym (-‿distribʳ-* x y)
{-# WARNING_ON_USAGE -‿*-distribʳ
"Warning: -‿*-distribʳ was deprecated in v1.1.
Please use -‿distribʳ-* instead.
NOTE: the equality is flipped so you will need sym (-‿distribʳ-* ...)."
#-}


text:
module Generic.Lib.Decidable where

open import Relation.Nullary public
open import Relation.Nullary.Decidable hiding (map) public
open import Relation.Binary using (Decidable) public

open import Generic.Lib.Intro
open import Generic.Lib.Equality.Propositional
open import Generic.Lib.Equality.Heteroindexed
open import Generic.Lib.Data.Sum
open import Generic.Lib.Data.Product

open import Relation.Nullary
import Data.String as String

infix 3 _#_

IsSet : ∀ {α} -> Set α -> Set α
IsSet A = Decidable {A = A} _≡_

record Eq {α} (A : Set α) : Set α where
  infixl 5 _≟_ _==_

  field _≟_ : IsSet A

  _==_ : A -> A -> Bool
  x == y = ⌊ x ≟ y ⌋
open Eq {{...}} public

record _↦_ {α} (A B : Set α) : Set α where
  constructor packInj
  field
    to      : A -> B
    from    : B -> A
    from-to : from ∘ to ≗ id

-- Can't make it an instance, because otherwise it unreasonably breaks instance search.
viaInj : ∀ {α} {A B : Set α} {{bEq : Eq B}} -> A ↦ B -> Eq A
viaInj {A = A} {B} inj = record
  { _≟_ = flip (via-injection {A = ≡-Setoid A} {B = ≡-Setoid B}) _≟_ $ record
      { to        = record
          { _⟨$⟩_ = to
          ; cong  = cong to
          }
      ; injective = λ q -> right (from-to _) (trans (cong from q) (from-to _))
      }
  } where open _↦_ inj

_#_ : ∀ {α} {A : Set α} -> A -> A -> Set
x # y = Dec (x ≡ y)

delim : ∀ {α π} {A : Set α} {P : Dec A -> Set π}
      -> (∀ x -> P (yes x)) -> (∀ c -> P (no c)) -> (d : Dec A) -> P d
delim f g (yes x) = f x
delim f g (no  c) = g c

drec : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> (¬ A -> B) -> Dec A -> B
drec = delim

dmap : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> (¬ A -> ¬ B) -> Dec A -> Dec B
dmap f g = drec (yes ∘ f) (no ∘ g)

sumM2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
      -> (A -> Dec C) -> (B -> Dec C) -> (¬ A -> ¬ B -> Dec C) -> Dec A -> Dec B -> Dec C
sumM2 f g h d e = drec f (λ c -> drec g (h c) e) d

prodM2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
       -> (A -> B -> Dec C) -> (¬ A -> Dec C) -> (¬ B -> Dec C) -> Dec A -> Dec B -> Dec C
prodM2 h f g d e = drec (λ x -> drec (h x) g e) f d

sumF2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
      -> (A -> C) -> (B -> C) -> (¬ A -> ¬ B -> ¬ C) -> Dec A -> Dec B -> Dec C
sumF2 f g h = sumM2 (yes ∘ f) (yes ∘ g) (no % ∘ h)

prodF2 : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ}
       -> (A -> B -> C) -> (¬ A -> ¬ C) -> (¬ B -> ¬ C) -> Dec A -> Dec B -> Dec C
prodF2 h f g = prodM2 (yes % ∘ h) (no ∘ f) (no ∘ g)

dcong : ∀ {α β} {A : Set α} {B : Set β} {x y}
      -> (f : A -> B) -> (f x ≡ f y -> x ≡ y) -> x # y -> f x # f y
dcong f inj = dmap (cong f) (_∘ inj)

dcong₂ : ∀ {α β γ} {A : Set α} {B : Set β} {C : Set γ} {x₁ x₂ y₁ y₂}
       -> (f : A -> B -> C)
       -> (f x₁ y₁ ≡ f x₂ y₂ -> x₁ ≡ x₂ × y₁ ≡ y₂)
       -> x₁ # x₂
       -> y₁ # y₂
       -> f x₁ y₁ # f x₂ y₂
dcong₂ f inj = prodF2 (cong₂ f) (λ c -> c ∘ proj₁ ∘ inj) (λ c -> c ∘ proj₂ ∘ inj)

dhcong₂ : ∀ {α β γ} {A : Set α} {B : A -> Set β} {C : Set γ} {x₁ x₂ y₁ y₂}
        -> (f : ∀ x -> B x -> C)
        -> (f x₁ y₁ ≡ f x₂ y₂ -> [ B ] y₁ ≅ y₂)
        -> x₁ # x₂
        -> (∀ y₂ -> y₁ # y₂)
        -> f x₁ y₁ # f x₂ y₂
dhcong₂ f inj (yes refl) q = dcong (f _) (homo ∘ inj) (q _)
dhcong₂ f inj (no  c)    q = no (c ∘ inds ∘ inj)

dsubst : ∀ {α β γ} {A : Set α} {x y}
       -> (B : A -> Set β)
       -> (C : ∀ {x} -> B x -> Set γ)
       -> x # y
       -> (z : B x)
       -> ((z : B y) -> C z)
       -> (x ≢ y -> C z)
       -> C z
dsubst B C (yes refl) z g h = g z
dsubst B C (no  c)    z g h = h c

dsubst′ : ∀ {α β γ} {A : Set α} {C : Set γ} {x y}
        -> (B : A -> Set β) -> x # y -> B x -> (B y -> C) -> (x ≢ y -> C) -> C
dsubst′ B = dsubst B _

,-inj : ∀ {α β} {A : Set α} {B : A -> Set β} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
      -> (x₁ , y₁) ≡ (x₂ , y₂) -> [ B ] y₁ ≅ y₂
,-inj refl = irefl

inj₁-inj : ∀ {α β} {A : Set α} {B : Set β} {x₁ x₂ : A}
         -> inj₁ {B = B} x₁ ≡ inj₁ x₂ -> x₁ ≡ x₂
inj₁-inj refl = refl

inj₂-inj : ∀ {α β} {A : Set α} {B : Set β} {y₁ y₂ : B}
         -> inj₂ {A = A} y₁ ≡ inj₂ y₂ -> y₁ ≡ y₂
inj₂-inj refl = refl

-- _<,>ᵈ_ : ∀ {α β} {A : Set α} {B : Set β} {x₁ x₂ : A} {y₁ y₂ : B}
--        -> x₁ # x₂ -> y₁ # y₂ -> x₁ , y₁ # x₂ , y₂
-- _<,>ᵈ_ = dcong₂ _,_ (inds-homo ∘ ,-inj)

-- _<,>ᵈᵒ_ : ∀ {α β} {A : Set α} {B : A -> Set β} {x₁ x₂} {y₁ : B x₁} {y₂ : B x₂}
--         -> x₁ # x₂ -> (∀ y₂ -> y₁ # y₂) -> x₁ , y₁ # x₂ , y₂
-- _<,>ᵈᵒ_ = dhcong₂ _,_ ,-inj

decSum : ∀ {α β} {A : Set α} {B : Set β}
       -> IsSet A -> IsSet B -> IsSet (A ⊎ B)
decSum f g (inj₁ x₁) (inj₁ x₂) = dcong inj₁ inj₁-inj (f x₁ x₂)
decSum f g (inj₂ y₁) (inj₂ y₂) = dcong inj₂ inj₂-inj (g y₁ y₂)
decSum f g (inj₁ x₁) (inj₂ y₂) = no λ()
decSum f g (inj₂ y₁) (inj₁ x₂) = no λ()

decProd : ∀ {α β} {A : Set α} {B : A -> Set β}
        -> IsSet A -> (∀ {x} -> IsSet (B x)) -> IsSet (Σ A B)
decProd f g (x₁ , y₁) (x₂ , y₂) = dhcong₂ _,_ ,-inj (f x₁ x₂) (g y₁)

module _ where
  import Relation.Binary.PropositionalEquality as B

  liftBase : ∀ {α} {A : Set α} {x y : A} -> x B.≡ y -> x ≡ y
  liftBase B.refl = refl

  lowerBase : ∀ {α} {A : Set α} {x y : A} -> x ≡ y -> x B.≡ y
  lowerBase refl = B.refl

  viaBase : ∀ {α} {A : Set α} -> Decidable (B._≡_ {A = A}) -> Eq A
  viaBase d = record
    { _≟_ = flip (via-injection {A = ≡-Setoid _} {B = B.setoid _}) d $ record
        { to = record
            { _⟨$⟩_ = id
            ; cong  = lowerBase
            }
        ; injective = liftBase
        }
    }

max_stars_repo_name: turion/Generic

max_issues_repo_name: turion/Generic

max_forks_repo_name: turion/Generic


text:
-- The following deeply left-nested expression illustrates a problem
-- in a previous implementation of the occurrence machinery.

postulate A : Set

data List : Set where
  nil  : List
  snoc : List → A → List

f : A → List
f x = snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc (snoc nil x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x) x