text:
open import Prelude hiding (lift; id)

module Implicits.Syntax.LNMetaType where

open import Implicits.Syntax.Type
open import Data.Nat as Nat

mutual
  data MetaSType (m : ℕ) : Set where
    tvar : ℕ → MetaSType m
    mvar : Fin m → MetaSType m
    _→'_ : (a b : MetaType m) → MetaSType m
    tc   : ℕ → MetaSType m

  data MetaType (m : ℕ) : Set where
    _⇒_ : (a b : MetaType m) → MetaType m
    ∀'  : MetaType m → MetaType m
    simpl : MetaSType m → MetaType m

mutual

  open-meta : ∀ {m} → ℕ → MetaType m → MetaType (suc m)
  open-meta k (a ⇒ b) = open-meta k a ⇒ open-meta k b
  open-meta k (∀' a) = ∀' (open-meta (suc k) a )
  open-meta k (simpl x) = simpl (open-st k x)
    where
      open-st : ∀ {m} → ℕ → MetaSType m → MetaSType (suc m)
      open-st k (tvar x) with Nat.compare x k
      open-st .(suc (x N+ k)) (tvar x) | less .x k = tvar x
      open-st k (tvar .k) | equal .k = mvar zero
      open-st k (tvar .(suc (k N+ x))) | greater .k x = tvar (k N+ x)
      open-st k (mvar x) = mvar (suc x)
      open-st k (a →' b) = open-meta k a →' open-meta k b
      open-st k (tc x) = tc x

mutual

  data TClosedS {m} (n : ℕ) : MetaSType m → Set where
    tvar : ∀ {x} → (x N< n) → TClosedS n (tvar x)
    mvar : ∀ {x} → TClosedS n (mvar x)
    _→'_ : ∀ {a b} → TClosed n a → TClosed n b → TClosedS n (a →' b)
    tc   : ∀ {c} → TClosedS n (tc c)

  data TClosed {m} (n : ℕ) : MetaType m → Set where
    _⇒_ : ∀ {a b} → TClosed n a → TClosed n b → TClosed n (a ⇒ b)
    ∀'  : ∀ {a} → TClosed (suc n) a → TClosed n (∀' a)
    simpl : ∀ {τ} → TClosedS n τ → TClosed n (simpl τ)

to-meta : ∀ {ν} → Type ν → MetaType zero
to-meta (simpl (tc x)) = simpl (tc x)
to-meta (simpl (tvar n)) = simpl (tvar (toℕ n))
to-meta (simpl (a →' b)) = simpl (to-meta a →' to-meta b)
to-meta (a ⇒ b) = to-meta a ⇒ to-meta b
to-meta (∀' a) = ∀' (to-meta a)

from-meta : ∀ {ν} {a : MetaType zero} → TClosed ν a → Type ν
from-meta (a ⇒ b) = from-meta a ⇒ from-meta b
from-meta (∀' a) = ∀' (from-meta a)
from-meta (simpl (tvar x)) = simpl (tvar (fromℕ≤ x))
from-meta (simpl (mvar {()}))
from-meta (simpl (a →' b)) = simpl (from-meta a →' from-meta b)
from-meta (simpl (tc {c})) = simpl (tc c)


text:
{-# OPTIONS --safe #-}
module Cubical.Experiments.HAEquivInt where

open import Cubical.Experiments.HAEquivInt.Base public

ext: agda

max_stars_repo_name: marcinjangrzybowski/cubical

max_issues_repo_name: marcinjangrzybowski/cubical

max_forks_repo_name: marcinjangrzybowski/cubical


text:
-----------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of the heterogeneous sublist relation
------------------------------------------------------------------------

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

module Data.List.Relation.Binary.Sublist.Heterogeneous.Properties where

open import Data.Empty
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Base as List hiding (map; _∷ʳ_)
import Data.List.Properties as Lₚ
open import Data.List.Relation.Unary.Any.Properties
  using (here-injective; there-injective)
open import Data.List.Relation.Binary.Pointwise as Pw using (Pointwise; []; _∷_)
open import Data.List.Relation.Binary.Sublist.Heterogeneous

open import Data.Maybe.Relation.Unary.All as MAll using (nothing; just)
open import Data.Nat using (ℕ; _≤_; _≥_); open ℕ; open _≤_
import Data.Nat.Properties as ℕₚ
open import Data.Product using (_×_; uncurry)

open import Function
open import Function.Bijection   using (_⤖_; bijection)
open import Function.Equivalence using (_⇔_ ; equivalence)

open import Relation.Nullary using (yes; no; ¬_)
open import Relation.Nullary.Negation using (¬?)
import Relation.Nullary.Decidable as Dec
open import Relation.Unary as U using (Pred; _⊆_)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)

------------------------------------------------------------------------
-- Injectivity of constructors

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  ∷-injectiveˡ : ∀ {x y xs ys} {px qx : R x y} {pxs qxs : Sublist R xs ys} →
                 (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → px ≡ qx
  ∷-injectiveˡ P.refl = P.refl

  ∷-injectiveʳ : ∀ {x y xs ys} {px qx : R x y} {pxs qxs : Sublist R xs ys} →
                 (Sublist R (x ∷ xs) (y ∷ ys) ∋ px ∷ pxs) ≡ (qx ∷ qxs) → pxs ≡ qxs
  ∷-injectiveʳ P.refl = P.refl

  ∷ʳ-injective : ∀ {y xs ys} {pxs qxs : Sublist R xs ys} →
                 (Sublist R xs (y ∷ ys) ∋ y ∷ʳ pxs) ≡ (y ∷ʳ qxs) → pxs ≡ qxs
  ∷ʳ-injective P.refl = P.refl

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  length-mono-≤ : ∀ {as bs} → Sublist R as bs → length as ≤ length bs
  length-mono-≤ []        = z≤n
  length-mono-≤ (y ∷ʳ rs) = ℕₚ.≤-step (length-mono-≤ rs)
  length-mono-≤ (r ∷ rs)  = s≤s (length-mono-≤ rs)

------------------------------------------------------------------------
-- Conversion to and from Pointwise (proto-reflexivity)

  fromPointwise : Pointwise R ⇒ Sublist R
  fromPointwise []       = []
  fromPointwise (p ∷ ps) = p ∷ fromPointwise ps

  toPointwise : ∀ {as bs} → length as ≡ length bs →
                Sublist R as bs → Pointwise R as bs
  toPointwise {bs = []}     eq []         = []
  toPointwise {bs = b ∷ bs} eq (r ∷ rs)   = r ∷ toPointwise (ℕₚ.suc-injective eq) rs
  toPointwise {bs = b ∷ bs} eq (b ∷ʳ rs) =
    ⊥-elim $ ℕₚ.<-irrefl eq (s≤s (length-mono-≤ rs))

------------------------------------------------------------------------
-- Various functions' outputs are sublists

-- These lemmas are generalisations of results of the form `f xs ⊆ xs`.
-- (where _⊆_ stands for Sublist R). If R is reflexive then we can indeed
-- obtain `f xs ⊆ xs` from `xs ⊆ ys → f xs ⊆ ys`. The other direction is
-- only true if R is both reflexive and transitive.

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  tail-Sublist : ∀ {as bs} → Sublist R as bs →
                 MAll.All (λ as → Sublist R as bs) (tail as)
  tail-Sublist []        = nothing
  tail-Sublist (b ∷ʳ ps) = MAll.map (b ∷ʳ_) (tail-Sublist ps)
  tail-Sublist (p ∷ ps)  = just (_ ∷ʳ ps)

  take-Sublist : ∀ {as bs} n → Sublist R as bs → Sublist R (take n as) bs
  take-Sublist n       (y ∷ʳ rs) = y ∷ʳ take-Sublist n rs
  take-Sublist zero    rs        = minimum _
  take-Sublist (suc n) []        = []
  take-Sublist (suc n) (r ∷ rs)  = r ∷ take-Sublist n rs

  drop-Sublist : ∀ n → Sublist R ⇒ (Sublist R ∘′ drop n)
  drop-Sublist n       (y ∷ʳ rs) = y ∷ʳ drop-Sublist n rs
  drop-Sublist zero    rs        = rs
  drop-Sublist (suc n) []        = []
  drop-Sublist (suc n) (r ∷ rs)  = _ ∷ʳ drop-Sublist n rs

module _ {a b r p} {A : Set a} {B : Set b}
         {R : REL A B r} {P : Pred A p} (P? : U.Decidable P) where

  takeWhile-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (takeWhile P? as) bs
  takeWhile-Sublist []        = []
  takeWhile-Sublist (y ∷ʳ rs) = y ∷ʳ takeWhile-Sublist rs
  takeWhile-Sublist {a ∷ as} (r ∷ rs) with P? a
  ... | yes pa = r ∷ takeWhile-Sublist rs
  ... | no ¬pa = minimum _

  dropWhile-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (dropWhile P? as) bs
  dropWhile-Sublist []        = []
  dropWhile-Sublist (y ∷ʳ rs) = y ∷ʳ dropWhile-Sublist rs
  dropWhile-Sublist {a ∷ as} (r ∷ rs) with P? a
  ... | yes pa = _ ∷ʳ dropWhile-Sublist rs
  ... | no ¬pa = r ∷ rs

  filter-Sublist : ∀ {as bs} → Sublist R as bs → Sublist R (filter P? as) bs
  filter-Sublist []        = []
  filter-Sublist (y ∷ʳ rs) = y ∷ʳ filter-Sublist rs
  filter-Sublist {a ∷ as} (r ∷ rs) with P? a
  ... | yes pa = r ∷ filter-Sublist rs
  ... | no ¬pa = _ ∷ʳ filter-Sublist rs

------------------------------------------------------------------------
-- Various functions are increasing wrt _⊆_

-- We write f⁺ for the proof that `xs ⊆ ys → f xs ⊆ f ys`
-- and f⁻ for the one that `f xs ⊆ f ys → xs ⊆ ys`.

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

------------------------------------------------------------------------
-- _∷_

  ∷ˡ⁻ : ∀ {a as bs} → Sublist R (a ∷ as) bs → Sublist R as bs
  ∷ˡ⁻ (y ∷ʳ rs) = y ∷ʳ ∷ˡ⁻ rs
  ∷ˡ⁻ (r ∷  rs) = _ ∷ʳ rs

  ∷ʳ⁻ : ∀ {a as b bs} → ¬ R a b → Sublist R (a ∷ as) (b ∷ bs) →
        Sublist R (a ∷ as) bs
  ∷ʳ⁻ ¬r (y ∷ʳ rs) = rs
  ∷ʳ⁻ ¬r (r ∷  rs) = ⊥-elim (¬r r)

  ∷⁻ : ∀ {a as b bs} → Sublist R (a ∷ as) (b ∷ bs) → Sublist R as bs
  ∷⁻ (y ∷ʳ rs) = ∷ˡ⁻ rs
  ∷⁻ (x ∷  rs) = rs

module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
         {R : REL C D r} where

------------------------------------------------------------------------
-- map

  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
         Sublist (λ a b → R (f a) (g b)) as bs →
         Sublist R (List.map f as) (List.map g bs)
  map⁺ f g []        = []
  map⁺ f g (y ∷ʳ rs) = g y ∷ʳ map⁺ f g rs
  map⁺ f g (r ∷ rs)  = r ∷ map⁺ f g rs

  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
         Sublist R (List.map f as) (List.map g bs) →
         Sublist (λ a b → R (f a) (g b)) as bs
  map⁻ {[]}     {bs}     f g rs        = minimum _
  map⁻ {a ∷ as} {[]}     f g ()
  map⁻ {a ∷ as} {b ∷ bs} f g (_ ∷ʳ rs) = b ∷ʳ map⁻ f g rs
  map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs)  = r ∷ map⁻ f g rs

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

------------------------------------------------------------------------
-- _++_

  ++⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds →
        Sublist R (as ++ cs) (bs ++ ds)
  ++⁺ []         cds = cds
  ++⁺ (y ∷ʳ abs) cds = y ∷ʳ ++⁺ abs cds
  ++⁺ (ab ∷ abs) cds = ab ∷ ++⁺ abs cds

  ++⁻ : ∀ {as bs cs ds} → length as ≡ length bs →
        Sublist R (as ++ cs) (bs ++ ds) → Sublist R cs ds
  ++⁻ {[]}     {[]}     eq rs = rs
  ++⁻ {a ∷ as} {b ∷ bs} eq rs = ++⁻ (ℕₚ.suc-injective eq) (∷⁻ rs)
  ++⁻ {[]} {_ ∷ _} ()
  ++⁻ {_ ∷ _} {[]} ()

  ++ˡ : ∀ {as bs} (cs : List B) → Sublist R as bs → Sublist R as (cs ++ bs)
  ++ˡ zs = ++⁺ (minimum zs)

  ++ʳ : ∀ {as bs} (cs : List B) → Sublist R as bs → Sublist R as (bs ++ cs)
  ++ʳ cs []        = minimum cs
  ++ʳ cs (y ∷ʳ rs) = y ∷ʳ ++ʳ cs rs
  ++ʳ cs (r ∷ rs)  = r ∷ ++ʳ cs rs

------------------------------------------------------------------------
-- take / drop

  take⁺ : ∀ {m n as bs} → m ≤ n → Pointwise R as bs →
          Sublist R (take m as) (take n bs)
  take⁺ z≤n       ps        = minimum _
  take⁺ (s≤s m≤n) []        = []
  take⁺ (s≤s m≤n) (p ∷  ps) = p ∷ take⁺ m≤n ps

  drop⁺ : ∀ {m n as bs} → m ≥ n → Sublist R as bs →
          Sublist R (drop m as) (drop n bs)
  drop⁺ {m} z≤n       rs        = drop-Sublist m rs
  drop⁺     (s≤s m≥n) []        = []
  drop⁺     (s≤s m≥n) (y ∷ʳ rs) = drop⁺ (ℕₚ.≤-step m≥n) rs
  drop⁺     (s≤s m≥n) (r ∷ rs)  = drop⁺ m≥n rs

  drop⁺-≥ : ∀ {m n as bs} → m ≥ n → Pointwise R as bs →
            Sublist R (drop m as) (drop n bs)
  drop⁺-≥ m≥n pw = drop⁺ m≥n (fromPointwise pw)

  drop⁺-⊆ : ∀ {as bs} m → Sublist R as bs →
            Sublist R (drop m as) (drop m bs)
  drop⁺-⊆ m = drop⁺ (ℕₚ.≤-refl {m})

module _ {a b r p q} {A : Set a} {B : Set b}
         {R : REL A B r} {P : Pred A p} {Q : Pred B q}
         (P? : U.Decidable P) (Q? : U.Decidable Q) where

  ⊆-takeWhile-Sublist : ∀ {as bs} →
    (∀ {a b} → R a b → P a → Q b) →
    Pointwise R as bs → Sublist R (takeWhile P? as) (takeWhile Q? bs)
  ⊆-takeWhile-Sublist rp⇒q [] = []
  ⊆-takeWhile-Sublist {a ∷ as} {b ∷ bs} rp⇒q (p ∷ ps) with P? a | Q? b
  ... | yes pa | yes qb = p ∷ ⊆-takeWhile-Sublist rp⇒q ps
  ... | yes pa | no ¬qb = ⊥-elim $ ¬qb $ rp⇒q p pa
  ... | no ¬pa | yes qb = minimum _
  ... | no ¬pa | no ¬qb = []

  ⊇-dropWhile-Sublist : ∀ {as bs} →
    (∀ {a b} → R a b → Q b → P a) →
    Pointwise R as bs → Sublist R (dropWhile P? as) (dropWhile Q? bs)
  ⊇-dropWhile-Sublist rq⇒p [] = []
  ⊇-dropWhile-Sublist {a ∷ as} {b ∷ bs} rq⇒p (p ∷ ps) with P? a | Q? b
  ... | yes pa | yes qb = ⊇-dropWhile-Sublist rq⇒p ps
  ... | yes pa | no ¬qb = b ∷ʳ dropWhile-Sublist P? (fromPointwise ps)
  ... | no ¬pa | yes qb = ⊥-elim $ ¬pa $ rq⇒p p qb
  ... | no ¬pa | no ¬qb = p ∷ fromPointwise ps

  ⊆-filter-Sublist : ∀ {as bs} → (∀ {a b} → R a b → P a → Q b) →
                     Sublist R as bs → Sublist R (filter P? as) (filter Q? bs)
  ⊆-filter-Sublist rp⇒q [] = []
  ⊆-filter-Sublist rp⇒q (y ∷ʳ rs) with Q? y
  ... | yes qb = y ∷ʳ ⊆-filter-Sublist rp⇒q rs
  ... | no ¬qb = ⊆-filter-Sublist rp⇒q rs
  ⊆-filter-Sublist {a ∷ as} {b ∷ bs} rp⇒q (r ∷ rs) with P? a | Q? b
  ... | yes pa | yes qb = r ∷ ⊆-filter-Sublist rp⇒q rs
  ... | yes pa | no ¬qb = ⊥-elim $ ¬qb $ rp⇒q r pa
  ... | no ¬pa | yes qb = _ ∷ʳ ⊆-filter-Sublist rp⇒q rs
  ... | no ¬pa | no ¬qb = ⊆-filter-Sublist rp⇒q rs

module _ {a r p} {A : Set a} {R : Rel A r} {P : Pred A p} (P? : U.Decidable P) where

  takeWhile-filter : ∀ {as} → Pointwise R as as →
                     Sublist R (takeWhile P? as) (filter P? as)
  takeWhile-filter [] = []
  takeWhile-filter {a ∷ as} (p ∷ ps) with P? a
  ... | yes pa = p ∷ takeWhile-filter ps
  ... | no ¬pa = minimum _

  filter-dropWhile : ∀ {as} → Pointwise R as as →
                     Sublist R (filter P? as) (dropWhile (¬? ∘ P?) as)
  filter-dropWhile [] = []
  filter-dropWhile {a ∷ as} (p ∷ ps) with P? a
  ... | yes pa = p ∷ filter-Sublist P? (fromPointwise ps)
  ... | no ¬pa = filter-dropWhile ps

------------------------------------------------------------------------
-- reverse

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  reverseAcc⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds →
                Sublist R (reverseAcc cs as) (reverseAcc ds bs)
  reverseAcc⁺ []         cds = cds
  reverseAcc⁺ (y ∷ʳ abs) cds = reverseAcc⁺ abs (y ∷ʳ cds)
  reverseAcc⁺ (r ∷ abs)  cds = reverseAcc⁺ abs (r ∷ cds)

  reverse⁺ : ∀ {as bs} → Sublist R as bs → Sublist R (reverse as) (reverse bs)
  reverse⁺ rs = reverseAcc⁺ rs []

  reverse⁻ : ∀ {as bs} → Sublist R (reverse as) (reverse bs) → Sublist R as bs
  reverse⁻ {as} {bs} p = cast (reverse⁺ p) where
    cast = P.subst₂ (Sublist R) (Lₚ.reverse-involutive as) (Lₚ.reverse-involutive bs)

------------------------------------------------------------------------
-- Inversion lemmas

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} {a as b bs} where

  ∷⁻¹ : R a b → Sublist R as bs ⇔ Sublist R (a ∷ as) (b ∷ bs)
  ∷⁻¹ r = equivalence (r ∷_) ∷⁻

  ∷ʳ⁻¹ : ¬ R a b → Sublist R (a ∷ as) bs ⇔ Sublist R (a ∷ as) (b ∷ bs)
  ∷ʳ⁻¹ ¬r = equivalence (_ ∷ʳ_) (∷ʳ⁻ ¬r)

------------------------------------------------------------------------
-- Irrelevant special case

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

  Sublist-[]-irrelevant : U.Irrelevant (Sublist R [])
  Sublist-[]-irrelevant []       []        = P.refl
  Sublist-[]-irrelevant (y ∷ʳ p) (.y ∷ʳ q) = P.cong (y ∷ʳ_) (Sublist-[]-irrelevant p q)

------------------------------------------------------------------------
-- (to/from)Any is a bijection

  toAny-injective : ∀ {xs x} {p q : Sublist R [ x ] xs} → toAny p ≡ toAny q → p ≡ q
  toAny-injective {p = y ∷ʳ p} {y ∷ʳ q} =
    P.cong (y ∷ʳ_) ∘′ toAny-injective ∘′ there-injective
  toAny-injective {p = _ ∷ p}  {_ ∷ q}  =
    P.cong₂ (flip _∷_) (Sublist-[]-irrelevant p q) ∘′ here-injective
  toAny-injective {p = _ ∷ʳ _} {_ ∷ _}  = λ ()
  toAny-injective {p = _ ∷ _}  {_ ∷ʳ _} = λ ()

  fromAny-injective : ∀ {xs x} {p q : Any (R x) xs} →
                      fromAny {R = R} p ≡ fromAny q → p ≡ q
  fromAny-injective {p = here px} {here qx} = P.cong here ∘′ ∷-injectiveˡ
  fromAny-injective {p = there p} {there q} =
    P.cong there ∘′ fromAny-injective ∘′ ∷ʳ-injective
  fromAny-injective {p = here _}  {there _} = λ ()
  fromAny-injective {p = there _} {here _}  = λ ()

  toAny∘fromAny≗id : ∀ {xs x} (p : Any (R x) xs) → toAny (fromAny {R = R} p) ≡ p
  toAny∘fromAny≗id (here px) = P.refl
  toAny∘fromAny≗id (there p) = P.cong there (toAny∘fromAny≗id p)

  Sublist-[x]-bijection : ∀ {x xs} → (Sublist R [ x ] xs) ⤖ (Any (R x) xs)
  Sublist-[x]-bijection = bijection toAny fromAny toAny-injective toAny∘fromAny≗id

------------------------------------------------------------------------
-- Relational properties

module _ {a r} {A : Set a} {R : Rel A r} where

  reflexive : Reflexive R → _≡_ ⇒ Sublist R
  reflexive R-refl P.refl = fromPointwise (Pw.refl R-refl)

  refl : Reflexive R → Reflexive (Sublist R)
  refl R-refl = reflexive R-refl P.refl

module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
         {R : REL A B r} {S : REL B C s} {T : REL A C t} where

  trans : Trans R S T → Trans (Sublist R) (Sublist S) (Sublist T)
  trans rs⇒t []        []        = []
  trans rs⇒t rs        (y ∷ʳ ss) = y ∷ʳ trans rs⇒t rs ss
  trans rs⇒t (y ∷ʳ rs) (s ∷ ss)  = _ ∷ʳ trans rs⇒t rs ss
  trans rs⇒t (r ∷ rs)  (s ∷ ss)  = rs⇒t r s ∷ trans rs⇒t rs ss

module _ {a b r s e} {A : Set a} {B : Set b}
         {R : REL A B r} {S : REL B A s} {E : REL A B e} where

  open ℕₚ.≤-Reasoning

  antisym : Antisym R S E → Antisym (Sublist R) (Sublist S) (Pointwise E)
  antisym rs⇒e []        []        = []
  antisym rs⇒e (r ∷ rs)  (s ∷ ss)  = rs⇒e r s ∷ antisym rs⇒e rs ss
  -- impossible cases
  antisym rs⇒e (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) =
    ⊥-elim $ ℕₚ.<-irrefl P.refl $ begin
    length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
    length zs        ≤⟨ ℕₚ.n≤1+n (length zs) ⟩
    length (z ∷ zs)  ≤⟨ length-mono-≤ rs ⟩
    length ys₁       ∎
  antisym rs⇒e (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss)  =
    ⊥-elim $ ℕₚ.<-irrefl P.refl $ begin
    length (z ∷ zs) ≤⟨ length-mono-≤ rs ⟩
    length ys₁      ≤⟨ length-mono-≤ ss ⟩
    length zs       ∎
  antisym rs⇒e (_∷_ {x} {xs} {y} {ys₁} r rs)  (_∷ʳ_ {ys₂} {zs} z ss) =
    ⊥-elim $ ℕₚ.<-irrefl P.refl $ begin
    length (y ∷ ys₁) ≤⟨ length-mono-≤ ss ⟩
    length xs        ≤⟨ length-mono-≤ rs ⟩
    length ys₁       ∎

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} (R? : Decidable R) where

  sublist? : Decidable (Sublist R)
  sublist? []       ys       = yes (minimum ys)
  sublist? (x ∷ xs) []       = no λ ()
  sublist? (x ∷ xs) (y ∷ ys) with R? x y
  ... | yes r = Dec.map (∷⁻¹   r) (sublist? xs ys)
  ... | no ¬r = Dec.map (∷ʳ⁻¹ ¬r) (sublist? (x ∷ xs) ys)

module _ {a e r} {A : Set a} {E : Rel A e} {R : Rel A r} where

  isPreorder : IsPreorder E R → IsPreorder (Pointwise E) (Sublist R)
  isPreorder ER-isPreorder = record
    { isEquivalence = Pw.isEquivalence       ER.isEquivalence
    ; reflexive     = fromPointwise ∘ Pw.map ER.reflexive
    ; trans         = trans                  ER.trans
    } where module ER = IsPreorder ER-isPreorder

  isPartialOrder : IsPartialOrder E R → IsPartialOrder (Pointwise E) (Sublist R)
  isPartialOrder ER-isPartialOrder = record
    { isPreorder = isPreorder ER.isPreorder
    ; antisym    = antisym    ER.antisym
    } where module ER = IsPartialOrder ER-isPartialOrder

  isDecPartialOrder : IsDecPartialOrder E R →
                      IsDecPartialOrder (Pointwise E) (Sublist R)
  isDecPartialOrder ER-isDecPartialOrder = record
    { isPartialOrder = isPartialOrder ER.isPartialOrder
    ; _≟_            = Pw.decidable   ER._≟_
    ; _≤?_           = sublist?       ER._≤?_
    } where module ER = IsDecPartialOrder ER-isDecPartialOrder

module _ {a e r} where

  preorder : Preorder a e r → Preorder _ _ _
  preorder ER-preorder = record
    { isPreorder = isPreorder ER.isPreorder
    } where module ER = Preorder ER-preorder

  poset : Poset a e r → Poset _ _ _
  poset ER-poset = record
    { isPartialOrder = isPartialOrder ER.isPartialOrder
    } where module ER = Poset ER-poset

  decPoset : DecPoset a e r → DecPoset _ _ _
  decPoset ER-poset = record
    { isDecPartialOrder = isDecPartialOrder ER.isDecPartialOrder
    } where module ER = DecPoset ER-poset


text:
module Tactic.Nat.Subtract.Exp where

open import Prelude
open import Tactic.Nat.Exp
open import Tactic.Nat.NF
open import Container.Bag
open import Data.TreeRep

infixl 6 _⟨+⟩_ _⟨-⟩_
infixl 7 _⟨*⟩_

data SubExp : Set where
  var : (x : Var) → SubExp
  lit : (n : Nat) → SubExp
  _⟨+⟩_ _⟨-⟩_ _⟨*⟩_ : (a b : SubExp) → SubExp

infix 4 _:≡_ _:<_
data Eqn : Set where
  _:≡_ : (a b : SubExp) → Eqn
  _:<_ : (a b : SubExp) → Eqn

⟦_⟧se : SubExp → Env Var → Nat
⟦ var x ⟧se    ρ = ρ x
⟦ lit n ⟧se    ρ = n
⟦ e₁ ⟨+⟩ e₂ ⟧se ρ = ⟦ e₁ ⟧se ρ + ⟦ e₂ ⟧se ρ
⟦ e₁ ⟨-⟩ e₂ ⟧se ρ = ⟦ e₁ ⟧se ρ - ⟦ e₂ ⟧se ρ
⟦ e₁ ⟨*⟩ e₂ ⟧se ρ = ⟦ e₁ ⟧se ρ * ⟦ e₂ ⟧se ρ

⟦_⟧eqn : Eqn → Env Var → Set
⟦ e₁ :≡ e₂ ⟧eqn ρ = ⟦ e₁ ⟧se ρ ≡ ⟦ e₂ ⟧se ρ
⟦ e₁ :< e₂ ⟧eqn ρ = ⟦ e₁ ⟧se ρ < ⟦ e₂ ⟧se ρ

data SubAtom : Set

SubNF : Set
SubNF = NF SubAtom

data SubAtom where
  var   : Var → SubAtom
  _⟨-⟩_  : (a b : SubNF) → SubAtom

⟦_⟧sn : SubNF → Env Var → Nat
⟦_⟧st : Tm SubAtom → Env Var → Nat
⟦_⟧sa : SubAtom → Env Var → Nat

⟦ var x ⟧sa ρ = ρ x
⟦ a ⟨-⟩ b ⟧sa ρ = ⟦ a ⟧sn ρ - ⟦ b ⟧sn ρ

⟦ []     ⟧st ρ = 1
⟦ t ∷ ts ⟧st ρ = ⟦ t ⟧sa ρ * ⟦ ts ⟧st ρ

⟦ []           ⟧sn ρ = 0
⟦ (k , ts) ∷ n ⟧sn ρ = k * ⟦ ts ⟧st ρ + ⟦ n ⟧sn ρ

⟦_⟧sns : SubNF → Env Var → Nat
⟦_⟧sts : Tm SubAtom → Env Var → Nat
⟦_⟧sas : SubAtom → Env Var → Nat

⟦ var x ⟧sas ρ = ρ x
⟦ a ⟨-⟩ b ⟧sas ρ = ⟦ a ⟧sns ρ - ⟦ b ⟧sns ρ

⟦ []     ⟧sts ρ = 1
⟦ t ∷ [] ⟧sts ρ = ⟦ t ⟧sas ρ
⟦ t ∷ ts ⟧sts ρ = ⟦ t ⟧sas ρ * ⟦ ts ⟧sts ρ

⟦ []            ⟧sns ρ = 0
⟦ (k , ts) ∷ [] ⟧sns ρ = k * ⟦ ts ⟧sts ρ
⟦ (k , ts) ∷ n  ⟧sns ρ = k * ⟦ ts ⟧sts ρ + ⟦ n ⟧sns ρ

atomEnv : Env Var → Env SubAtom
atomEnv ρ x = ⟦ x ⟧sa ρ

atomEnvS : Env Var → Env SubAtom
atomEnvS ρ x = ⟦ x ⟧sas ρ

instance
  EncodeSubAtom : TreeEncoding SubAtom
  EncodeSubAtom = treeEncoding enc dec emb
    where
      enc    : SubAtom    → TreeRep
      encNF  : SubNF      → TreeRep
      encNFs : SubNF      → List TreeRep
      encTm  : Tm SubAtom → List TreeRep

      enc (var x)  = node x []
      enc (a ⟨-⟩ b) = node 0 (encNF a ∷ encNF b ∷ [])

      encNF n = node 0 (encNFs n)

      encNFs [] = []
      encNFs ((n , t) ∷ ns) = node n (encTm t) ∷ encNFs ns

      encTm []       = []
      encTm (x ∷ xs) = enc x ∷ encTm xs

      dec   : TreeRep → Maybe SubAtom
      decNF : TreeRep → Maybe SubNF
      decNFs : List TreeRep → Maybe SubNF
      decTm  : List TreeRep → Maybe (Tm SubAtom)

      dec (node x []) = just (var x)
      dec (node _ (t ∷ t₁ ∷ [])) = _⟨-⟩_ <$> decNF t <*> decNF t₁
      dec _ = nothing

      decNF (leaf _)    = nothing
      decNF (node _ ts) = decNFs ts

      decNFs (node n ts ∷ ts₁) = _∷_ <$> (_,_ n <$> decTm ts) <*> decNFs ts₁
      decNFs _                 = just []

      decTm []       = just []
      decTm (x ∷ ts) = _∷_ <$> dec x <*> decTm ts

      emb    : ∀ a → dec    (enc    a) ≡ just a
      embNFs : ∀ n → decNFs (encNFs n) ≡ just n
      embTm  : ∀ t → decTm  (encTm  t) ≡ just t

      emb (var x) = refl
      emb (a ⟨-⟩ b) = _⟨-⟩_ =$= embNFs a =*= embNFs b

      embNFs [] = refl
      embNFs ((n , t) ∷ ns) = _∷_ =$= (_,_ n =$= embTm t) =*= embNFs ns

      embTm []       = refl
      embTm (x ∷ xs) = _∷_ =$= emb x =*= embTm xs

  EqSubAtom : Eq SubAtom
  EqSubAtom = EqByTreeEncoding

  OrdSubAtom : Ord SubAtom
  OrdSubAtom = OrdByTreeEncoding

_-nf′_ : SubNF → SubNF → SubNF
a -nf′ b =
  case cancel a b of λ where
    (x  , []) → x
    ([] ,  _) → []
    (a′  , b′) → [ 1 , [ a′ ⟨-⟩ b′ ] ]

data IsSubtraction : SubNF → Set where
  _⟨-⟩_ : ∀ a b → IsSubtraction [ 1 , [ a ⟨-⟩ b ] ]
  no   : ∀ {a} → IsSubtraction a

is-subtraction : ∀ a → IsSubtraction a
is-subtraction [ 1 , [ a ⟨-⟩ b ] ] = a ⟨-⟩ b
is-subtraction a = no

infixl 6 _-nf_
infixl 7 _*nf₁_ _*tm_ _*ktm_ _*ktm′_
_-nf_ : SubNF → SubNF → SubNF
a  -nf b with is-subtraction a
_  -nf c | a ⟨-⟩ b = a -nf′ (b +nf c)
a  -nf b | no     = a -nf′ b

data IsSubtractionTm : Nat × Tm SubAtom → Set where
  _⟨-⟩_ : ∀ a b → IsSubtractionTm (1 , [ a ⟨-⟩ b ])
  no   : ∀ {a} → IsSubtractionTm a

is-subtraction-tm : ∀ a → IsSubtractionTm a
is-subtraction-tm (1 , [ a ⟨-⟩ b ]) = a ⟨-⟩ b
is-subtraction-tm a = no

_*nf₁_ : SubNF → SubNF → SubNF
_*ktm′_ : Nat × Tm SubAtom → SubNF → SubNF

_*tm_ : Nat × Tm SubAtom → Nat × Tm SubAtom → SubNF
s *tm t with is-subtraction-tm t
s       *tm _       | b ⟨-⟩ c = s *ktm′ b -nf s *ktm′ c
(a , x) *tm (b , y) | no     = [ a * b , merge x y ]

t *ktm′ [] = []
t *ktm′ (x ∷ a) = t *tm x +nf t *ktm′ a

_*ktm_ : Nat × Tm SubAtom → SubNF → SubNF
t *ktm a with is-subtraction-tm t
_ *ktm c | a ⟨-⟩ b = a *nf₁ c -nf b *nf₁ c
t *ktm a | no     = t *ktm′ a

[]      *nf₁ b = []
(t ∷ a) *nf₁ b = t *ktm b +nf (a *nf₁ b)

normSub : SubExp → SubNF
normSub (var x) = [ 1 , [ var x ] ]
normSub (lit 0) = []
normSub (lit n) = [ n , [] ]
normSub (e ⟨+⟩ e₁) = normSub e +nf normSub e₁
normSub (e ⟨-⟩ e₁) = normSub e -nf normSub e₁
normSub (e ⟨*⟩ e₁) = normSub e *nf₁ normSub e₁

max_stars_repo_name: L-TChen/agda-prelude

max_issues_repo_name: L-TChen/agda-prelude

max_forks_repo_name: L-TChen/agda-prelude


text:
postulate
  @0 A : Set

_ : @0 Set → (Set → Set) → Set
_ = λ @0 where
  A G → G A

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
-- New NO_POSITIVITY_CHECK pragma for data definitions and mutual
-- blocks

-- Skipping a single data definition.
{-# NO_POSITIVITY_CHECK #-}
data D : Set where
  lam : (D → D) → D


text:
import Agda.Builtin.Nat as Nat public

f : let open Nat public in Nat → Nat
f x = x


text:
{-# OPTIONS --without-K #-}
module sets.nat.properties where

open import equality.core
open import equality.calculus
open import equality.reasoning
open import function.isomorphism.core
open import sets.nat.core
open import sets.empty

+-left-unit : ∀ n → 0 + n ≡ n
+-left-unit n = refl

+-right-unit : ∀ n → n + 0 ≡ n
+-right-unit zero = refl
+-right-unit (suc n) = ap suc (+-right-unit n)

+-associativity : ∀ n m p → n + m + p ≡ n + (m + p)
+-associativity 0 m p = refl
+-associativity (suc n) m p = ap suc (+-associativity n m p)

+-left-cancel : ∀ n → injective (_+_ n)
+-left-cancel 0 p = p
+-left-cancel (suc n) p = +-left-cancel n (ap pred p)

right-distr : ∀ n m p → (n + m) * p ≡ n * p + m * p
right-distr 0 m p = refl
right-distr (suc n) m p = begin
    p + (n + m) * p
  ≡⟨ ap (_+_ p) (right-distr n m p) ⟩
    p + (n * p + m * p)
  ≡⟨ sym (+-associativity p (n * p) (m * p)) ⟩
    p + n * p + m * p
  ∎
  where open ≡-Reasoning

*-left-unit : ∀ n → 1 * n ≡ n
*-left-unit n = +-right-unit n

*-right-unit : ∀ n → n * 1 ≡ n
*-right-unit zero = refl
*-right-unit (suc n) = ap suc (*-right-unit n)

*-associativity : ∀ n m p → n * m * p ≡ n * (m * p)
*-associativity 0 m p = refl
*-associativity (suc n) m p =
    right-distr m (n * m) p
  · ap (λ z → (m * p) + z)
         (*-associativity n m p)

+-commutativity : ∀ n m → n + m ≡ m + n
+-commutativity 0 m = sym (+-right-unit m)
+-commutativity (suc n) m = begin
    suc (n + m)
  ≡⟨ ap suc (+-commutativity n m) ⟩
    suc (m + n)
  ≡⟨ lem m n ⟩
    m + suc n
  ∎
  where
    open ≡-Reasoning
    lem : ∀ n m → suc n + m ≡ n + suc m
    lem 0 m = refl
    lem (suc n) m = ap suc (lem n m)

left-distr : ∀ n m p → n * (m + p) ≡ n * m + n * p
left-distr 0 m p = refl
left-distr (suc n) m p = begin
    m + p + n * (m + p)
  ≡⟨ +-associativity m p _ ⟩
    m + (p + n * (m + p))
  ≡⟨ ap (λ z → m + (p + z))
          (left-distr n m p) ⟩
    m + (p + (n * m + n * p))
  ≡⟨ ap (_+_ m)
          (sym (+-associativity p (n * m) _)) ⟩
    m + (p + n * m + n * p)
  ≡⟨ ap (λ z → m + (z + n * p))
          (+-commutativity p (n * m)) ⟩
    m + (n * m + p + n * p)
  ≡⟨ ap (_+_ m) (+-associativity (n * m) p _) ⟩
    m + (n * m + (p + n * p))
  ≡⟨ sym (+-associativity m (n * m) _) ⟩
    m + n * m + (p + n * p)
  ∎
  where open ≡-Reasoning

left-zero : ∀ n → 0 * n ≡ 0
left-zero n = refl

right-zero : ∀ n → n * 0 ≡ 0
right-zero 0 = refl
right-zero (suc n) = right-zero n

*-commutativity : ∀ n m → n * m ≡ m * n
*-commutativity 0 m = sym (right-zero m)
*-commutativity (suc n) m = begin
    m + n * m
  ≡⟨ ap₂ _+_ (sym (*-right-unit m))
               (*-commutativity n m) ⟩
    m * 1 + m * n
  ≡⟨ sym (left-distr m 1 n) ⟩
    m * suc n
  ∎
  where open ≡-Reasoning

suc-fixpoint : ∀ {n} → ¬ (suc n ≡ n)
suc-fixpoint {zero} ()
suc-fixpoint {suc n} p = suc-fixpoint (suc-inj p)

max_stars_repo_name: pcapriotti/agda-base

max_issues_repo_name: pcapriotti/agda-base

max_forks_repo_name: pcapriotti/agda-base


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

module Categories.Category.Monoidal.Structure where

open import Level

open import Categories.Category
open import Categories.Category.Monoidal.Core

record MonoidalCategory o ℓ e : Set (suc (o ⊔ ℓ ⊔ e)) where
  field
    U        : Category o ℓ e
    monoidal : Monoidal U

  module U = Category U
  module monoidal = Monoidal monoidal

  open U public
  open monoidal public

max_stars_repo_name: bblfish/agda-categories

max_issues_repo_name: bblfish/agda-categories

max_forks_repo_name: bblfish/agda-categories


text:
-- Andreas, 2019-07-23, issue #3932
--
-- Mutual blocks are not supported in mutual blocks

module _ where

module M where

  mutual
    A : Set1
    A = Set

    mutual
      B : Set1
      B = A

module N where

  mutual
    A : Set1
    A = Set

    mutual
      A = Set

module O where

  mutual
    A : Set1

    mutual
      A = Set

-- WAS: internal errors

-- EXPECTED ERRORS:
--
-- * mutual blocks in mutual blocks are not supported
--
-- * The following names are declared but not accompanied by a definition: A
--   when scope checking the declaration
--     module O where


text:
-- Andreas, 2021-11-19, issue #5657 reported by J Barrett
-- Regression in 2.6.2: internal error instead of error message

record R : Set₁ where
  field A : Set

postulate r : R
open R r

fail : Set
fail = r .A

-- WAS:
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Rules/Application.hs:968

-- Expected:
-- Set should be a function type, but it isn't
-- when checking that r is a valid argument to a function of type Set

max_stars_repo_name: cagix/agda

max_issues_repo_name: cagix/agda

max_forks_repo_name: cagix/agda


text:
{-
  Day 3 input
-}
module a3-input where

open import Data.Nat
open import Data.List hiding (lookup;allFin)
                      renaming (map to mapList)
open import Data.Vec

input : List (Vec ℕ 12)
input =
  (0 ∷ 0 ∷ 0 ∷ 1 ∷ 1 ∷ 1 ∷ 1 ∷ 1 ∷ 1 ∷ 0 ∷ 0 ∷ 1 ∷ []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  (0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  0 ∷  0 ∷  []) ∷
  (1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  0 ∷  1 ∷  0 ∷  []) ∷
  (0 ∷  1 ∷  1 ∷  0 ∷  0 ∷  1 ∷  1 ∷  1 ∷  0 ∷  1 ∷  0 ∷  1 ∷  []) ∷
  []

max_stars_repo_name: felixwellen/adventOfCode

max_issues_repo_name: felixwellen/adventOfCode

max_forks_repo_name: felixwellen/adventOfCode