text:
module Haskell.RangedSets.RangedSet where
open import Agda.Builtin.Equality

open import Haskell.Prim
open import Haskell.Prim.Ord
open import Haskell.Prim.Bool
open import Haskell.Prim.Maybe
open import Haskell.Prim.Enum
open import Haskell.Prim.Num
open import Haskell.Prim.Eq
open import Haskell.Prim.Foldable
open import Haskell.Prim.Monoid
open import Haskell.Prim.Int
open import Haskell.Prim.List
open import Haskell.Prim.Integer
open import Haskell.Prim.Real

open import Haskell.RangedSets.Boundaries
open import Haskell.RangedSets.Ranges
open import Haskell.RangedSetsProp.library
open import Haskell.RangedSetsProp.BoundariesProperties

{-# FOREIGN AGDA2HS
import Haskell.RangedSets.Boundaries
#-}
{-# FOREIGN AGDA2HS
import Haskell.RangedSets.Ranges
#-}
{-# FOREIGN AGDA2HS
import Data.List
#-}

infixl 7 _-/\-_
infixl 6 _-\/-_ _-!-_
infixl 5 _-<=-_ _-<-_ _-?-_

okAdjacent : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Range a → Range a → Bool
okAdjacent r@(Rg lower1 upper1) r2@(Rg lower2 upper2) = rangeLower r <= rangeUpper r && rangeUpper r <= rangeLower r2 && rangeLower r2 <= rangeUpper r2
{-# COMPILE AGDA2HS okAdjacent #-}

validRangeList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Range a) → Bool
validRangeList [] = true
validRangeList (x ∷ []) = (rangeLower x) <= (rangeUpper x)
validRangeList (x ∷ rs@(r1 ∷ rss)) = (okAdjacent x r1) && (validRangeList rs)
{-# COMPILE AGDA2HS validRangeList #-}

validBoundaryList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Boundary a) → Bool
validBoundaryList [] = true
validBoundaryList (x ∷ []) = true
validBoundaryList (x ∷ rs@(r1 ∷ rss)) = (x <= r1) && (validBoundaryList rs)

data RSet (a : Set) ⦃ o : Ord a ⦄ ⦃ dio : DiscreteOrdered a ⦄ : Set where
    RS : (rg : List (Range a)) → {IsTrue (validRangeList rg)} → RSet a

{-# COMPILE AGDA2HS RSet #-}

rSetRanges : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → RSet a → List (Range a)
rSetRanges (RS ranges) = ranges
{-# COMPILE AGDA2HS rSetRanges #-}

overlap1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Range a → Range a → Bool
overlap1 (Rg _ upper1) (Rg lower2 _) = (upper1 >= lower2)
{-# COMPILE AGDA2HS overlap1 #-}

sortedRangeList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Range a) → Bool
sortedRangeList [] = true
sortedRangeList (r ∷ []) = true
sortedRangeList (r1 ∷ r2 ∷ rs) = (r1 <= r2) && (sortedRangeList (r2 ∷ rs))

validRanges : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Range a) → Bool
validRanges [] = true
validRanges (r ∷ rs) = (rangeLower r <= rangeUpper r) && (validRanges rs)

headandtailSorted : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a))
      → ⦃ ne : NonEmpty rs ⦄ → (IsTrue (sortedRangeList rs))
      → (IsTrue (sortedRangeList (tail rs ⦃ ne ⦄)))
headandtailValidRanges : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a))
      → ⦃ ne : NonEmpty rs ⦄ → (IsTrue (validRanges rs))
      → (IsTrue (validRanges (tail rs ⦃ ne ⦄)))

normalise : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rg : List (Range a))
   → ⦃ IsTrue (sortedRangeList rg) ⦄
   → ⦃ IsTrue (validRanges rg) ⦄
   → List (Range a)

postulate
   sortedList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a))
      -> IsTrue (sortedRangeList (sort (filter (λ r → (rangeIsEmpty r) == false) rs)))

   validRangesList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a))
      -> IsTrue (validRanges (sort (filter (λ r → (rangeIsEmpty r) == false) rs)))

unsafeRangedSet : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                → (rg : List (Range a))
                → ⦃ IsTrue (validRangeList ⦃ o ⦄ ⦃ dio ⦄ rg) ⦄ → RSet a
unsafeRangedSet rs ⦃ prf ⦄  = RS rs {prf}

{-# COMPILE AGDA2HS unsafeRangedSet #-}

validFunction2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a) → (f : Boundary a → Boundary a) → Bool
validFunction2 b f = (f b) > b

validFunction : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a) → (g : Boundary a → Maybe (Boundary a)) → Bool
validFunction b g with (g b)
...                       | Nothing = true
...                       | Just b2 = (b2 > b)

ranges3 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ →
      Maybe (Boundary a) → (f : Boundary a → Boundary a) → (g : Boundary a → Maybe (Boundary a))
      → List (Range a)
{-# TERMINATING #-}
ranges2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
      → (f : Boundary a → Boundary a) → (g : Boundary a → Maybe (Boundary a))
      → List (Range a)
ranges2 b upperFunc succFunc = (Rg b (upperFunc b)) ∷ (ranges3 (succFunc b) upperFunc succFunc)

ranges3 (Just b1) upperFunc succFunc = if ((validFunction2 b1 upperFunc) && (validFunction b1 succFunc)) then
                              (ranges2 b1 upperFunc succFunc) else []
ranges3 Nothing _ _ = []
{-# COMPILE AGDA2HS ranges2 #-}
{-# COMPILE AGDA2HS ranges3 #-}

setBounds1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (xs : List (Boundary a))
   → List (Boundary a)
setBounds1 (BoundaryBelowAll ∷ xs) = xs
setBounds1 xs = (BoundaryBelowAll ∷ xs)
{-# COMPILE AGDA2HS setBounds1 #-}

bounds1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
         → List (Range a) → List (Boundary a)
bounds1 (r ∷ rs) = (rangeLower r) ∷ (rangeUpper r) ∷ (bounds1 rs)
bounds1 [] = []
{-# COMPILE AGDA2HS bounds1 #-}

ranges1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Boundary a)
   → List (Range a)
ranges1 (b1 ∷ b2 ∷ bs) = (Rg b1 b2) ∷ (ranges1 bs)
ranges1 (BoundaryAboveAll ∷ [])  = []
ranges1 (b ∷ []) = (Rg b BoundaryAboveAll) ∷ []
ranges1 _ = []
{-# COMPILE AGDA2HS ranges1 #-}

merge1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Range a) → List (Range a) → List (Range a)
merge1 [] [] = []
merge1 ms1@(h1 ∷ t1) [] = ms1
merge1 [] ms2@(h2 ∷ t2) = ms2
merge1 ms1@(h1 ∷ t1) ms2@(h2 ∷ t2) = if_then_else_ (h1 < h2) (h1 ∷ (merge1 t1 ms2)) (h2 ∷ (merge1 ms1 t2))
{-# COMPILE AGDA2HS merge1 #-}

merge2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
   → List (Range a) → List (Range a) → List (Range a)
merge2 [] [] = []
merge2 ms1@(h1 ∷ t1) [] = []
merge2 [] ms2@(h2 ∷ t2) = []
merge2 ms1@(h1 ∷ t1) ms2@(h2 ∷ t2) =
   (rangeIntersection h1 h2) ∷
   (if_then_else_ (rangeUpper h1 < rangeUpper h2) (merge2 t1 ms2) (merge2 ms1 t2))
{-# COMPILE AGDA2HS merge2 #-}

postulate

   sortedListComposed : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
            → (r1 r2 : Range a) → (ranges : List (Range a))
            → IsTrue (sortedRangeList (r1 ∷ r2 ∷ ranges))
            → IsTrue (sortedRangeList ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ ranges))

   validRangesComposed : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
            → (r1 r2 : Range a) → (ranges : List (Range a))
            → IsTrue (sortedRangeList (r1 ∷ r2 ∷ ranges))
            → IsTrue (validRanges (r1 ∷ r2 ∷ ranges))
            → IsTrue (validRanges ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ ranges))

   rangesLTEQ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b : Boundary a)
                          → (f : Boundary a → Boundary a) → IsTrue (f b > b) → IsTrue (b <= f b)

   stupid1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b b1 : Boundary a)
                          → (f : Boundary a → Boundary a)
                          → (g : Boundary a → Maybe (Boundary a))
                          → IsTrue (validFunction2 b f) → IsTrue (validFunction b g)
                          → (cond : Bool) -- this condition is (validFunction2 b1 f) && (validFunction b1 g)
                          → IsTrue cond
                          → IsTrue (validFunction2 b1 f)
   stupid2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b b1 : Boundary a)
                          → (f : Boundary a → Boundary a)
                          → (g : Boundary a → Maybe (Boundary a))
                          → IsTrue (validFunction2 b f) → IsTrue (validFunction b g)
                          → (cond : Bool) -- this condition is (validFunction2 b1 f) && (validFunction b1 g)
                          → IsTrue cond
                          → IsTrue (validFunction b1 g)

   -- used only when h <= h3
   okSorted : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (h h3 : Range a)
         → sortedRangeList (h ∷ h3 ∷ []) ≡ true

   -- holds only when upper h <= lower(head ms)
   validList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (h : Range a) → (ms : List (Range a))
         → IsTrue (validRangeList ms)
         → validRangeList (h ∷ ms) ≡ true

   validIsSorted :  ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (ms : List (Range a))
                     → IsTrue (validRangeList ms) → IsTrue (sortedRangeList ms)

   -- holds only when h < (head ms)
   validSortedList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (h : Range a) → (ms : List (Range a))
         → IsTrue (sortedRangeList ms)
         → sortedRangeList (h ∷ ms) ≡ true

normalise (r1 ∷ r2 ∷ rs) ⦃ prf ⦄ ⦃ prf2 ⦄ =
   if_then_else_ (overlap1 r1 r2)
      (normalise ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs)
      ⦃ sortedListComposed r1 r2 rs prf ⦄ ⦃ validRangesComposed r1 r2 rs prf prf2 ⦄ )
         (r1 ∷ (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄ ))
normalise rs = rs
{-# COMPILE AGDA2HS normalise #-}

-- some useful proofs
headandtail : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
      → ⦃ ne : NonEmpty (rSetRanges rs) ⦄ → (IsTrue (validRangeList (rSetRanges rs)))
      → (IsTrue (validRangeList (tail (rSetRanges rs) ⦃ ne ⦄)))
okAdjValid : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a)) → (r : Range a)
      → ⦃ ne : NonEmpty rs ⦄ → (IsTrue (validRangeList (r ∷ rs))) → IsTrue (okAdjacent r (head rs ⦃ ne ⦄))
headandtail2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a))
      → ⦃ ne : NonEmpty rs ⦄ → (IsTrue (validRangeList rs))
      → (IsTrue (validRangeList (tail rs ⦃ ne ⦄)))
tailandhead : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
      → ⦃ ne : NonEmpty (rSetRanges rs) ⦄ → (IsTrue (validRangeList (rSetRanges rs)))
      → (IsTrue (validRangeList ((head (rSetRanges rs) ⦃ ne ⦄) ∷ [])))
tailandhead2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : List (Range a))
      → ⦃ ne : NonEmpty rs ⦄ → (IsTrue (validRangeList rs))
      → (IsTrue (validRangeList ((head rs ⦃ ne ⦄) ∷ [])))

okAdjIsTrue :  ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (r : Range a) → (r2 : Range a)
               → okAdjacent r r2 ≡ ((rangeLower r <= rangeUpper r) && (rangeUpper r <= rangeLower r2) && (rangeLower r2 <= rangeUpper r2))

normalisedSortedList0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
         → (ms : List (Range a))
         → (prf : IsTrue (sortedRangeList ms))
         → (prf2 : IsTrue (validRanges ms))
         → validRangeList (normalise ms ⦃ prf ⦄ ⦃ prf2 ⦄) ≡ true

normalisedSortedList00 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
         → (rs : List (Range a))
         → (r1 r2 : Range a) → (prf : IsTrue (sortedRangeList (r1 ∷ r2 ∷ rs))) → (prf2 : IsTrue (validRanges (r1 ∷ r2 ∷ rs)))
         → (b : Bool)
         → validRangeList (if_then_else_ b
      (normalise ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs) ⦃ sortedListComposed r1 r2 rs prf ⦄ ⦃ validRangesComposed r1 r2 rs prf prf2 ⦄)
         (r1 ∷ (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄))) ≡ true

normalisedSortedList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
  → (ms : List (Range a))
  → (prf : IsTrue (sortedRangeList ms))
  → (prf2 : IsTrue (validRanges ms))
  → IsTrue (validRangeList (normalise ms ⦃ prf ⦄ ⦃ prf2 ⦄))

merge1HasValidRanges0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (rs1 rs2 : RSet a)
                          → IsTrue (validRangeList (rSetRanges rs1)) → IsTrue (validRangeList (rSetRanges rs2))
                          → (validRanges (merge1 (rSetRanges rs1) (rSetRanges rs2))) ≡ true

merge1HasValidRanges00 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (rs1 rs2 : RSet a) → (h1 h2 : Range a)
                          → IsTrue (validRangeList (h1 ∷ (rSetRanges rs1))) → IsTrue (validRangeList (h2 ∷ (rSetRanges rs2)))
                          → (b : Bool)
                          → validRanges (if_then_else_ b
                          (h1 ∷ (merge1 (rSetRanges rs1) (h2 ∷ (rSetRanges rs2))))
                          (h2 ∷ (merge1 (h1 ∷ (rSetRanges rs1)) (rSetRanges rs2)))) ≡ true

validListMeansValidRanges : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (rs1 : RSet a)
                          → IsTrue (validRangeList (rSetRanges rs1))
                          → (validRanges (rSetRanges rs1)) ≡ true

merge1HasValidRanges : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
   → (rs1 rs2 : RSet a)
   → IsTrue (validRangeList (rSetRanges rs1))
   → IsTrue (validRangeList (rSetRanges rs2))
   → IsTrue (validRanges (merge1 (rSetRanges rs1) (rSetRanges rs2)))

ranges2HasValidRanges0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b : Boundary a)
                          → (f : Boundary a → Boundary a)
                          → (g : Boundary a → Maybe (Boundary a))
                          → IsTrue (validFunction2 b f) → IsTrue (validFunction b g)
                          → (validRanges (ranges2 b f g)) ≡ true
ranges2HasValidRanges00 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b : Boundary a)
                          → (f : Boundary a → Boundary a)
                          → (g : Boundary a → Maybe (Boundary a))
                          → (mb : Maybe (Boundary a))
                          → IsTrue (validFunction2 b f) → IsTrue (validFunction b g)
                          → (validRanges ((Rg b (f b)) ∷ (ranges3 mb f g))) ≡ true
ranges2HasValidRanges000 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b b1 : Boundary a)
                          → (f : Boundary a → Boundary a)
                          → (g : Boundary a → Maybe (Boundary a))
                          → (cond : Bool)
                          → IsTrue (validFunction2 b f) → IsTrue (validFunction b g)
                          → (validRanges ((Rg b (f b)) ∷ (if cond then (ranges2 b1 f g) else []))) ≡ true

ranges2HasValidRanges : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
                          → (b : Boundary a)
                          → (f : Boundary a → Boundary a)
                          → (g : Boundary a → Maybe (Boundary a))
                          → IsTrue (validFunction2 b f) → IsTrue (validFunction b g)
                          → IsTrue (validRanges (ranges2 b f g))

unfoldSorted : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
            → (f : Boundary a → Boundary a)
            → (g : Boundary a → Maybe (Boundary a))
            → IsTrue (sortedRangeList (ranges2 b f g))

unfoldIsSorted00 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
            → (f : Boundary a → Boundary a)
            → (g : Boundary a → Maybe (Boundary a))
            → (b1 : Boundary a) → (cond : Bool)
            → sortedRangeList ((Rg b (f b)) ∷ (if_then_else_ cond (ranges2 b1 f g) [])) ≡ true

unfoldIsSorted0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
            → (f : Boundary a → Boundary a)
            → (g : Boundary a → Maybe (Boundary a))
            → (mb : Maybe (Boundary a)) → sortedRangeList ((Rg b (f b)) ∷ (ranges3 mb f g)) ≡ true

unfoldIsSorted : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
            → (f : Boundary a → Boundary a)
            → (g : Boundary a → Maybe (Boundary a))
            → sortedRangeList (ranges2 b f g) ≡ true

-- the following proofs are used for proving that intersection is valid
intersection2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
                  → ⦃ ne1 : NonEmpty (rSetRanges rs1) ⦄ → ⦃ ne2 : NonEmpty (rSetRanges rs2) ⦄
                  → IsTrue (validRangeList (rSetRanges rs1)) → IsTrue (validRangeList (rSetRanges rs2))
                  → (b : Bool)
                  →     validRangeList (
       if_then_else_ b

      ((rangeIntersection (head (rSetRanges rs1) ⦃ ne1 ⦄) (head (rSetRanges rs2) ⦃ ne2 ⦄))
      ∷ (filter (λ x → (rangeIsEmpty x == false))
       (if_then_else_ (rangeUpper (head (rSetRanges rs1) ⦃ ne1 ⦄) < rangeUpper (head (rSetRanges rs2) ⦃ ne2 ⦄))
        (merge2 (tail (rSetRanges rs1) ⦃ ne1 ⦄) (rSetRanges rs2))
        (merge2 (rSetRanges rs1) (tail (rSetRanges rs2) ⦃ ne2 ⦄)))))

       (filter (λ x → (rangeIsEmpty x == false))
         (if_then_else_ (rangeUpper (head (rSetRanges rs1) ⦃ ne1 ⦄) < rangeUpper (head (rSetRanges rs2) ⦃ ne2 ⦄))
          (merge2 (tail (rSetRanges rs1) ⦃ ne1 ⦄) (rSetRanges rs2))
          (merge2 (rSetRanges rs1) (tail (rSetRanges rs2) ⦃ ne2 ⦄)))) ) ≡ true
intersection3 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
                  → ⦃ ne1 : NonEmpty (rSetRanges rs1) ⦄ → ⦃ ne2 : NonEmpty (rSetRanges rs2) ⦄
                  → IsTrue (validRangeList (rSetRanges rs1)) → IsTrue (validRangeList (rSetRanges rs2))
                  → (b : Bool)
                  → validRangeList ((filter (λ x → (rangeIsEmpty x == false))
                        (if_then_else_ b
                           (merge2 (tail (rSetRanges rs1) ⦃ ne1 ⦄) (rSetRanges rs2))
                           (merge2 (rSetRanges rs1) (tail (rSetRanges rs2) ⦃ ne2 ⦄))))) ≡ true

intersectionHolds : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
                  → IsTrue (validRangeList (rSetRanges rs1)) → IsTrue (validRangeList (rSetRanges rs2))
                  → validRangeList (filter (λ x → (rangeIsEmpty x == false)) (merge2 (rSetRanges rs1) (rSetRanges rs2))) ≡ true

-- intersection of two valid ranged sets is also valid range set
intersection0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
      → IsTrue (validRangeList (rSetRanges rs1)) → IsTrue (validRangeList (rSetRanges rs2))
      → IsTrue (validRangeList (filter (λ x → (rangeIsEmpty x == false))
                  (merge2 (rSetRanges rs1) (rSetRanges rs2))))
intersection0 ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2 = subst IsTrue (sym (intersectionHolds ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2)) IsTrue.itsTrue

-- used for proving that union is valid (merge1 returns a valid range list)
merge1IsSorted0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (h1 h2 : Range a) → (t1 t2 : RSet a) → (b : Bool)
         → IsTrue (validRangeList (h1 ∷ (rSetRanges t1))) → IsTrue (validRangeList (h2 ∷ (rSetRanges t2)))
         → sortedRangeList (if_then_else_ b (h1 ∷ (merge1 (rSetRanges t1) (h2 ∷ (rSetRanges t2))))
            (h2 ∷ (merge1 (h1 ∷ (rSetRanges t1)) (rSetRanges t2)))) ≡ true
merge1IsSorted1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
         → IsTrue (validRangeList (rSetRanges rs1)) → IsTrue (validRangeList (rSetRanges rs2))
         → sortedRangeList (merge1 (rSetRanges rs1) (rSetRanges rs2)) ≡ true

merge1Sorted : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
   → (rs1 : RSet a) → (rs2 : RSet a)
   → IsTrue (validRangeList (rSetRanges rs1))
   → IsTrue (validRangeList (rSetRanges rs2))
   → IsTrue (sortedRangeList (merge1 (rSetRanges rs1) (rSetRanges rs2)))

merge1Sorted ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2 = subst IsTrue (sym (merge1IsSorted1 rs1 rs2 prf1 prf2)) IsTrue.itsTrue

-- union of two valid ranged sets is also valid range set
unionHolds : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
         → (rs1 : RSet a) → (rs2 : RSet a)
         → (prf1 : IsTrue (validRangeList (rSetRanges rs1)))
         → (prf2 : IsTrue (validRangeList (rSetRanges rs2)))
         → IsTrue (validRangeList (normalise (merge1 (rSetRanges rs1) (rSetRanges rs2))
          ⦃ merge1Sorted rs1 rs2 prf1 prf2 ⦄ ⦃ merge1HasValidRanges rs1 rs2 prf1 prf2 ⦄))
unionHolds ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2 = normalisedSortedList
   (merge1 (rSetRanges rs1) (rSetRanges rs2)) (merge1Sorted rs1 rs2 prf1 prf2)
      (merge1HasValidRanges rs1 rs2 prf1 prf2)

-- used for proving negation is valid
{-# TERMINATING #-}
valid : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
   → {IsTrue (validRangeList (rSetRanges rs))}
   → (validRangeList (rSetRanges rs)) ≡ (validBoundaryList (bounds1 (rSetRanges rs)))

validSetBounds : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
   → (bs : List (Boundary a)) → validBoundaryList (setBounds1 bs) ≡ validBoundaryList bs

validRanges1 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (bs : List (Boundary a))
   → validRangeList (ranges1 bs) ≡ validBoundaryList bs

-- negation of valid ranged set is also valid
prop3 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
   → IsTrue (validRangeList (rSetRanges rs))
   → validRangeList (rSetRanges rs) ≡ validBoundaryList (setBounds1 (bounds1 (rSetRanges rs)))
prop3 ⦃ o ⦄ ⦃ dio ⦄ rs prf = trans (valid rs {prf}) (sym (validSetBounds (bounds1 (rSetRanges rs))))

prop4 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
   → IsTrue (validRangeList (rSetRanges rs))
   → validRangeList (rSetRanges rs) ≡ validRangeList (ranges1 (setBounds1 (bounds1 (rSetRanges rs))))

prop4 ⦃ o ⦄ ⦃ dio ⦄ rs prf = trans (prop3 rs prf) (sym (validRanges1 (setBounds1 (bounds1 (rSetRanges rs)))))

negation : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
   → (IsTrue (validRangeList (rSetRanges rs)))
   → (IsTrue (validRangeList (ranges1 (setBounds1 (bounds1 (rSetRanges rs))))))
negation ⦃ o ⦄ ⦃ dio ⦄ rs prf = subst IsTrue (prop4 rs prf) prf

-- empty range is valid
emptyRangeValid : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (validRangeList ⦃ o ⦄ ⦃ dio ⦄ []) ≡ true
emptyRangeValid = refl
empty : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → IsTrue (validRangeList ⦃ o ⦄ ⦃ dio ⦄ [])
empty ⦃ o ⦄ ⦃ dio ⦄ = subst IsTrue (sym (emptyRangeValid ⦃ o ⦄ ⦃ dio ⦄)) IsTrue.itsTrue

-- full range is valid
fullRangeValid : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ →
      (validRangeList ⦃ o ⦄ ⦃ dio ⦄ (fullRange ⦃ o ⦄ ⦃ dio ⦄ ∷ [])) ≡ true
full0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ →
      IsTrue (validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg BoundaryBelowAll BoundaryAboveAll) ∷ []))
full0 ⦃ o ⦄ ⦃ dio ⦄ = subst IsTrue (sym (fullRangeValid ⦃ o ⦄ ⦃ dio ⦄)) IsTrue.itsTrue

-- any singleton range is valid
singletonRangeValid0 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (x : a) → (validRangeList ((singletonRange x) ∷ [])) ≡ true
singletonRangeValid : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (x : a) → IsTrue (validRangeList ((singletonRange x) ∷ []))
singletonRangeValid x = subst IsTrue (sym (singletonRangeValid0 x)) IsTrue.itsTrue

rSingleton : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → a → RSet a
rSingleton ⦃ o ⦄ ⦃ dio ⦄ a = RS ((singletonRange a) ∷ []) {singletonRangeValid a}
{-# COMPILE AGDA2HS rSingleton #-}

normaliseRangeList : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
   → List (Range a) → List (Range a)
normaliseRangeList [] = []
normaliseRangeList rs@(r1 ∷ rss) =
   normalise (sort (filter (λ r → (rangeIsEmpty r) == false) rs))
      ⦃ sortedList rs ⦄ ⦃ validRangesList rs ⦄
{-# COMPILE AGDA2HS normaliseRangeList #-}

makeRangedSet : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
   → List (Range a) → RSet a
makeRangedSet ⦃ o ⦄ ⦃ dio ⦄ [] = RS [] {empty ⦃ o ⦄ ⦃ dio ⦄}
makeRangedSet ⦃ o ⦄ ⦃ dio ⦄ rs@(r1 ∷ rss) = RS (normaliseRangeList rs)
   { normalisedSortedList (sort (filter (λ r → (rangeIsEmpty r) == false) rs)) (sortedList rs) (validRangesList rs) }
{-# COMPILE AGDA2HS makeRangedSet #-}

rangesAreEmpty : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → List (Range a) → Bool
rangesAreEmpty [] = true
rangesAreEmpty (r ∷ rs) = false
{-# COMPILE AGDA2HS rangesAreEmpty #-}

rSetIsEmpty : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a) → Bool
rSetIsEmpty ⦃ o ⦄ ⦃ dio ⦄ rset@(RS ranges) = rangesAreEmpty ⦃ o ⦄ ⦃ dio ⦄ ranges
{-# COMPILE AGDA2HS rSetIsEmpty #-}

rSetNegation : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rg : RSet a) → {(IsTrue (validRangeList (rSetRanges rg)))} → RSet a
rSetNegation ⦃ o ⦄ ⦃ dio ⦄ set@(RS ranges) {prf} =
   RS (ranges1 (setBounds1 (bounds1 ranges))) {negation set prf}

{-# COMPILE AGDA2HS rSetNegation #-}

rSetIsFull : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
      → {IsTrue (validRangeList (rSetRanges rs))} → Bool
rSetIsFull set {prf} = rSetIsEmpty (rSetNegation set {prf})
{-# COMPILE AGDA2HS rSetIsFull #-}

rSetEmpty : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → RSet a
rSetEmpty ⦃ o ⦄ ⦃ dio ⦄ = RS [] {empty ⦃ o ⦄ ⦃ dio ⦄}
{-# COMPILE AGDA2HS rSetEmpty #-}

rSetFull : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → RSet a
rSetFull ⦃ o ⦄ ⦃ dio ⦄ = RS ((Rg BoundaryBelowAll BoundaryAboveAll) ∷ []) {full0 ⦃ o ⦄ ⦃ dio ⦄}
{-# COMPILE AGDA2HS rSetFull #-}

rSetHas : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a) → {IsTrue (validRangeList (rSetRanges rs))} → a → Bool
rSetHas (RS []) _ = false
rSetHas ⦃ o ⦄ ⦃ dio ⦄ (RS ls@(r ∷ [])) value = rangeHas ⦃ o ⦄ r value
rSetHas ⦃ o ⦄ ⦃ dio ⦄ rst@(RS ls@(r ∷ rs)) {prf} value = (rangeHas ⦃ o ⦄ r value) || (rSetHas (RS rs {headandtail rst prf}) {headandtail rst prf} value)
{-# COMPILE AGDA2HS rSetHas #-}

_-?-_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a) → {IsTrue (validRangeList (rSetRanges rs))} → a → Bool
_-?-_ rs {prf} = rSetHas rs {prf}
{-# COMPILE AGDA2HS _-?-_ #-}

negationHelper : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
         → {tr0 : IsTrue (validRangeList (rSetRanges rs))}
         → validRangeList (rSetRanges (rSetNegation rs {tr0})) ≡ validRangeList (ranges1 (setBounds1 (bounds1 (rSetRanges rs))))

negation2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs : RSet a)
         → {tr0 : IsTrue (validRangeList (rSetRanges rs))}
         → (tr : IsTrue (validRangeList (ranges1 (setBounds1 (bounds1 (rSetRanges rs))))))
         → IsTrue (validRangeList (rSetRanges (rSetNegation rs {tr0})))
negation2 rs {prf0} prf = subst IsTrue (sym (negationHelper rs {prf0})) prf

rSetUnion : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → RSet a
rSetUnion ⦃ o ⦄ ⦃ dio ⦄ r1@(RS ls1) {prf1} r2@(RS ls2) {prf2} =
   RS (normalise (merge1 ls1 ls2) ⦃ merge1Sorted r1 r2 prf1 prf2 ⦄
    ⦃ merge1HasValidRanges r1 r2 prf1 prf2 ⦄)
    {unionHolds r1 r2 prf1 prf2}

{-# COMPILE AGDA2HS rSetUnion #-}

_-\/-_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → RSet a
_-\/-_ rs1 {prf1} rs2 {prf2} = rSetUnion rs1 {prf1} rs2 {prf2}
{-# COMPILE AGDA2HS _-\/-_ #-}

unionHelper : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
         → (prf1 : IsTrue (validRangeList (rSetRanges rs1))) → (prf2 : IsTrue (validRangeList (rSetRanges rs2)))
         → validRangeList (rSetRanges (rSetUnion rs1 {prf1} rs2 {prf2}))
         ≡ validRangeList (normalise (merge1 (rSetRanges rs1) (rSetRanges rs2)) ⦃ merge1Sorted rs1 rs2 prf1 prf2 ⦄ ⦃ merge1HasValidRanges rs1 rs2 prf1 prf2 ⦄)
unionHelper ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ls1) rs2@(RS ls2) prf1 prf2 =
  begin
     validRangeList (rSetRanges (rSetUnion rs1 {prf1} rs2 {prf2}))
  =⟨⟩
     validRangeList (rSetRanges (RS (normalise (merge1 (rSetRanges rs1) (rSetRanges rs2)) ⦃ merge1Sorted rs1 rs2 prf1 prf2 ⦄  ⦃ merge1HasValidRanges rs1 rs2 prf1 prf2 ⦄) {unionHolds rs1 rs2 prf1 prf2}))
  =⟨⟩
     validRangeList (normalise (merge1 (rSetRanges rs1) (rSetRanges rs2)) ⦃ merge1Sorted rs1 rs2 prf1 prf2 ⦄  ⦃ merge1HasValidRanges rs1 rs2 prf1 prf2 ⦄)
  end

union2 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
         → (prf1 : IsTrue (validRangeList (rSetRanges rs1))) → (prf2 : IsTrue (validRangeList (rSetRanges rs2)))
         → IsTrue (validRangeList (normalise (merge1 (rSetRanges rs1) (rSetRanges rs2)) ⦃ merge1Sorted rs1 rs2 prf1 prf2 ⦄  ⦃ merge1HasValidRanges rs1 rs2 prf1 prf2 ⦄))
         → IsTrue (validRangeList (rSetRanges (rSetUnion rs1 {prf1} rs2 {prf2})))
union2 rs1 rs2 prf1 prf2 prf = subst IsTrue (sym (unionHelper rs1 rs2 prf1 prf2)) prf

rSetIntersection : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → RSet a
rSetIntersection ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ls1) {prf1} rs2@(RS ls2) {prf2} =
    RS ⦃ o ⦄ ⦃ dio ⦄
      (filter (λ x → rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false) (merge2 ⦃ o ⦄ ⦃ dio ⦄ ls1 ls2))
         {intersection0 rs1 rs2 prf1 prf2}
{-# COMPILE AGDA2HS rSetIntersection #-}

_-/\-_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → RSet a
_-/\-_ rs1 {prf1} rs2 {prf2} = rSetIntersection rs1 {prf1} rs2 {prf2}
{-# COMPILE AGDA2HS _-/\-_ #-}

intersectHelper : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
         → (prf1 : IsTrue (validRangeList (rSetRanges rs1))) → (prf2 : IsTrue (validRangeList (rSetRanges rs2)))
         → validRangeList (rSetRanges (rSetIntersection rs1 {prf1} rs2 {prf2})) ≡ validRangeList (filter (λ r → (rangeIsEmpty r) == false) (merge2 (rSetRanges rs1) (rSetRanges rs2)))

intersection22 : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (rs1 : RSet a) → (rs2 : RSet a)
         → (prf1 : IsTrue (validRangeList (rSetRanges rs1))) → (prf2 : IsTrue (validRangeList (rSetRanges rs2)))
         → IsTrue (validRangeList (filter (λ r → (rangeIsEmpty r) == false) (merge2 (rSetRanges rs1) (rSetRanges rs2))))
         → IsTrue (validRangeList (rSetRanges (rSetIntersection rs1 {prf1} rs2 {prf2})))
intersection22 ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2 prf = subst IsTrue (sym (intersectHelper rs1 rs2 prf1 prf2)) prf

rSetDifference : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → RSet a
rSetDifference ⦃ o ⦄ ⦃ dio ⦄ rs1 {prf1} rs2 {prf2} =
   rSetIntersection rs1 {prf1} (rSetNegation rs2 {prf2}) {negation2 rs2 (negation rs2 prf2)}
{-# COMPILE AGDA2HS rSetDifference #-}

_-!-_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → RSet a
_-!-_ rs1 {prf1} rs2 {prf2} = rSetDifference rs1 {prf1} rs2 {prf2}
{-# COMPILE AGDA2HS _-!-_ #-}

rSetIsSubset : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → Bool
rSetIsSubset rs1 {prf1} rs2 {prf2} = rSetIsEmpty (rSetDifference rs1 {prf1} rs2 {prf2})
{-# COMPILE AGDA2HS rSetIsSubset #-}

_-<=-_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → Bool
_-<=-_ rs1 {prf1} rs2 {prf2}  = rSetIsSubset rs1 {prf1} rs2 {prf2}
{-# COMPILE AGDA2HS _-<=-_ #-}

rSetIsSubsetStrict : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → Bool
rSetIsSubsetStrict rs1 {prf1} rs2 {prf2} = rSetIsEmpty
   (rSetDifference rs1 {prf1} rs2 {prf2}) && not (rSetIsEmpty (rSetDifference rs2 {prf2} rs1 {prf1}))
{-# COMPILE AGDA2HS rSetIsSubsetStrict #-}

_-<-_ : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄
      → (rs1 : RSet a) → {IsTrue (validRangeList (rSetRanges rs1))}
      → (rs2 : RSet a) → {IsTrue (validRangeList (rSetRanges rs2))} → Bool
_-<-_ rs1 {prf1} rs2 {prf2} = rSetIsSubsetStrict rs1 {prf1} rs2 {prf2}
{-# COMPILE AGDA2HS _-<-_ #-}

instance
    isRangedSetSemigroup : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Semigroup (RSet a)
    isRangedSetSemigroup ._<>_ r1@(RS l1 {prf1}) r2@(RS l2 {prf2}) = rSetUnion r1 {prf1} r2 {prf2}

    isRangedSetMonoid : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → Monoid (RSet a)
    isRangedSetMonoid .mempty = rSetEmpty

rSetUnfold : ⦃ o : Ord a ⦄ → ⦃ dio : DiscreteOrdered a ⦄ → (b : Boundary a)
            → (f : Boundary a → Boundary a)
            → (g : Boundary a → Maybe (Boundary a))
            → ⦃ IsTrue (validFunction2 b f) ⦄
            → ⦃ IsTrue (validFunction b g) ⦄ → RSet a

rSetUnfold ⦃ o ⦄ ⦃ dio ⦄ bound upperFunc succFunc ⦃ fValid ⦄ ⦃ gValid ⦄ =
   RS (normalise (ranges2 bound upperFunc succFunc)
               ⦃ unfoldSorted bound upperFunc succFunc ⦄ ⦃ ranges2HasValidRanges bound upperFunc succFunc fValid gValid ⦄)
      { normalisedSortedList (ranges2 bound upperFunc succFunc)
               (unfoldSorted bound upperFunc succFunc) (ranges2HasValidRanges bound upperFunc succFunc fValid gValid) }

{-# COMPILE AGDA2HS rSetUnfold #-}

okAdjIsTrue ⦃ o ⦄ ⦃ dio ⦄ r@(Rg l1 u1) r2@(Rg l2 u2) = refl

headandtailSorted rs@(r ∷ []) prf = IsTrue.itsTrue
headandtailSorted rs@(r ∷ rss@(r2 ∷ rsss)) prf = isTrue&&₂ {r <= r2} prf

headandtail rs@(RS (r ∷ [])) prf = IsTrue.itsTrue
headandtail rs@(RS (r ∷ rss@(r2 ∷ rsss))) prf = isTrue&&₂ {okAdjacent r r2} prf

tailandhead rs@(RS (r ∷ [])) prf = prf
tailandhead rs@(RS (r ∷ rss@(r2 ∷ rsss))) prf = isTrue&&₁ {rangeLower r <= rangeUpper r}
      (subst IsTrue (okAdjIsTrue r r2) (isTrue&&₁ {okAdjacent r r2} prf))

okAdjValid rs@(r2 ∷ rss) r prf = isTrue&&₁ {okAdjacent r r2} prf

tailandhead2 rs@(r ∷ []) prf = prf
tailandhead2 rs@(r ∷ rss@(r2 ∷ rsss)) prf = isTrue&&₁ {rangeLower r <= rangeUpper r}
      (subst IsTrue (okAdjIsTrue r r2) (isTrue&&₁ {okAdjacent r r2} prf))

headandtail2 rs@(r ∷ []) prf = IsTrue.itsTrue
headandtail2 rs@(r ∷ rss@(r2 ∷ rsss)) prf = isTrue&&₂ {okAdjacent r r2} prf

headandtailValidRanges rs@(r ∷ []) prf = IsTrue.itsTrue
headandtailValidRanges rs@(r ∷ rss@(r2 ∷ rsss)) prf = isTrue&&₂ {rangeLower r <= rangeUpper r} prf

ranges2HasValidRanges ⦃ o ⦄ ⦃ dio ⦄ b f g prf1 prf2 = subst IsTrue (sym (ranges2HasValidRanges0 b f g prf1 prf2)) IsTrue.itsTrue

ranges2HasValidRanges000 ⦃ o ⦄ ⦃ dio ⦄ b b1 f g false prf1 prf2 =
   begin
      (validRanges ⦃ o ⦄ ⦃ dio ⦄ ((Rg b (f b)) ∷ []))
  =⟨⟩
      b <= (f b) && (validRanges ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
      b <= (f b) && true
  =⟨ prop_and_true (b <= (f b)) ⟩
      b <= (f b)
  =⟨ propIsTrue (b <= (f b)) (rangesLTEQ b f prf1) ⟩
     true
   end
ranges2HasValidRanges000 ⦃ o ⦄ ⦃ dio ⦄ b b1 f g true prf1 prf2 =
   begin
      (validRanges ((Rg b (f b)) ∷ (ranges2 b1 f g)))
  =⟨⟩
      b <= (f b) && (validRanges (ranges2 b1 f g))
  =⟨ cong (b <= (f b) &&_) (ranges2HasValidRanges0 b1 f g (stupid1 b b1 f g prf1 prf2 true IsTrue.itsTrue)
         (stupid2 b b1 f g prf1 prf2 true IsTrue.itsTrue) ) ⟩
      b <= (f b) && true
  =⟨ prop_and_true (b <= (f b)) ⟩
      b <= (f b)
  =⟨ propIsTrue (b <= (f b)) (rangesLTEQ b f prf1) ⟩
     true
   end

ranges2HasValidRanges00 ⦃ o ⦄ ⦃ dio ⦄ b f g Nothing prf1 prf2 =
   begin
      (validRanges ⦃ o ⦄ ⦃ dio ⦄ ((Rg b (f b)) ∷ (ranges3 Nothing f g)))
  =⟨⟩
      validRanges ⦃ o ⦄ ⦃ dio ⦄ ((Rg b (f b)) ∷ [])
  =⟨⟩
      (b <= (f b)) && (validRanges ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
      (b <= (f b)) && true
  =⟨ prop_and_true (b <= (f b)) ⟩
      b <= (f b)
  =⟨ propIsTrue (b <= (f b)) (rangesLTEQ b f prf1) ⟩
     true
   end
ranges2HasValidRanges00 ⦃ o ⦄ ⦃ dio ⦄ b f g (Just b1) prf1 prf2 =
   begin
      (validRanges ((Rg b (f b)) ∷ (ranges3 (Just b1) f g)))
  =⟨⟩
      validRanges ((Rg b (f b)) ∷ (if ((validFunction2 b1 f) && (validFunction b1 g)) then (ranges2 b1 f g) else []))
  =⟨ ranges2HasValidRanges000 b b1 f g ((validFunction2 b1 f) && (validFunction b1 g)) prf1 prf2 ⟩
     true
   end

ranges2HasValidRanges0 ⦃ o ⦄ ⦃ dio ⦄ b f g prf1 prf2 =
   begin
      (validRanges (ranges2 b f g))
  =⟨⟩
      validRanges ((Rg b (f b)) ∷ (ranges3 (g b) f g))
  =⟨ ranges2HasValidRanges00 b f g (g b) prf1 prf2 ⟩
      true
   end

merge1HasValidRanges ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2 = subst IsTrue (sym (merge1HasValidRanges0 rs1 rs2 prf1 prf2)) IsTrue.itsTrue

validListMeansValidRanges ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) prf =
   begin
      (validRanges ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
  true
 end
validListMeansValidRanges ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS (r1 ∷ [])) prf =
   begin
      (validRanges (r1 ∷ []))
  =⟨⟩
      (rangeLower r1 <= rangeUpper r1) && (validRanges ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
      (rangeLower r1 <= rangeUpper r1) && true
  =⟨ prop_and_true (rangeLower r1 <= rangeUpper r1) ⟩
   (rangeLower r1 <= rangeUpper r1)
  =⟨ propIsTrue (rangeLower r1 <= rangeUpper r1) prf ⟩
  true
 end
validListMeansValidRanges ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges@(r1 ∷ r2 ∷ r3)) prf =
   begin
      (validRanges ranges)
  =⟨⟩
      (rangeLower r1 <= rangeUpper r1) && (validRanges ⦃ o ⦄ ⦃ dio ⦄ (r2 ∷ r3))
  =⟨ cong ((rangeLower r1 <= rangeUpper r1) &&_) (validListMeansValidRanges (RS (r2 ∷ r3) {headandtail rs1 prf}) (headandtail rs1 prf)) ⟩
      (rangeLower r1 <= rangeUpper r1) && true
  =⟨ prop_and_true (rangeLower r1 <= rangeUpper r1) ⟩
   (rangeLower r1 <= rangeUpper r1)
  =⟨ propIsTrue (rangeLower r1 <= rangeUpper r1) (tailandhead rs1 prf) ⟩
  true
 end

merge1HasValidRanges00 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS t1) rs2@(RS t2) h1 h2 prf1 prf2 true =
   begin
      validRanges (h1 ∷ (merge1 (rSetRanges rs1) (h2 ∷ (rSetRanges rs2))))
  =⟨⟩
      (rangeLower h1 <= rangeUpper h1) && (validRanges (merge1 t1 (h2 ∷ t2)))
  =⟨ cong ((rangeLower h1 <= rangeUpper h1) &&_)
   (merge1HasValidRanges0 rs1 (RS (h2 ∷ t2) {prf2}) (headandtail (RS (h1 ∷ t1) {prf1}) prf1) prf2) ⟩
   (rangeLower h1 <= rangeUpper h1) && true
  =⟨ prop_and_true (rangeLower h1 <= rangeUpper h1) ⟩
   (rangeLower h1 <= rangeUpper h1)
  =⟨ propIsTrue (rangeLower h1 <= rangeUpper h1) (tailandhead (RS (h1 ∷ t1) {prf1}) prf1) ⟩
   true
 end
merge1HasValidRanges00 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS t1) rs2@(RS t2) h1 h2 prf1 prf2 false =
   begin
      validRanges (h2 ∷ (merge1 (h1 ∷ t1) t2))
  =⟨⟩
      (rangeLower h2 <= rangeUpper h2) && (validRanges (merge1 (h1 ∷ t1) t2))
  =⟨ cong ((rangeLower h2 <= rangeUpper h2) &&_)
   (merge1HasValidRanges0 (RS (h1 ∷ t1) {prf1}) rs2 prf1 (headandtail (RS (h2 ∷ t2) {prf2}) prf2)) ⟩
   (rangeLower h2 <= rangeUpper h2) && true
  =⟨ prop_and_true (rangeLower h2 <= rangeUpper h2) ⟩
   (rangeLower h2 <= rangeUpper h2)
  =⟨ propIsTrue (rangeLower h2 <= rangeUpper h2) (tailandhead (RS (h2 ∷ t2) {prf2}) prf2) ⟩
   true
 end

merge1HasValidRanges0 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) rs2@(RS []) prf1 prf2 =
   begin
      (validRanges (merge1 (rSetRanges rs1) (rSetRanges rs2)))
  =⟨⟩
      validRanges ⦃ o ⦄ ⦃ dio ⦄ []
  =⟨⟩
  true
 end
merge1HasValidRanges0 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS (h1 ∷ t1)) rs2@(RS []) prf1 prf2 =
   begin
      (validRanges (merge1 (rSetRanges rs1) (rSetRanges rs2)))
  =⟨⟩
      validRanges (h1 ∷ t1)
  =⟨ validListMeansValidRanges rs1 prf1 ⟩
  true
 end
merge1HasValidRanges0 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) rs2@(RS (h2 ∷ t2)) prf1 prf2 =
   begin
      (validRanges (merge1 (rSetRanges rs1) (rSetRanges rs2)))
  =⟨⟩
      validRanges (h2 ∷ t2)
  =⟨ validListMeansValidRanges rs2 prf2 ⟩
  true
 end
merge1HasValidRanges0 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS (h1 ∷ t1)) rs2@(RS (h2 ∷ t2)) prf1 prf2 =
   begin
      (validRanges (merge1 (rSetRanges rs1) (rSetRanges rs2)))
  =⟨⟩
      validRanges (if_then_else_ (h1 < h2) (h1 ∷ (merge1 t1 (h2 ∷ t2))) (h2 ∷ (merge1 (h1 ∷ t1) (t2))))
  =⟨ merge1HasValidRanges00 (RS t1 {headandtail rs1 prf1}) (RS t2 {headandtail rs2 prf2}) h1 h2 prf1 prf2 (h1 < h2) ⟩
  true
 end

normalisedSortedList ⦃ o ⦄ ⦃ dio ⦄ ms prf prf2 = subst IsTrue (sym (normalisedSortedList0 ms prf prf2)) IsTrue.itsTrue

normalisedSortedList00 ⦃ o ⦄ ⦃ dio ⦄ rs r1 r2 prf prf2 true =
   begin
      validRangeList (if_then_else_ true
      (normalise ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs) ⦃ sortedListComposed r1 r2 rs prf ⦄ ⦃ validRangesComposed r1 r2 rs prf prf2 ⦄)
         (r1 ∷ (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄)))
  =⟨⟩
      validRangeList ((normalise ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs) ⦃ sortedListComposed r1 r2 rs prf ⦄ ⦃ validRangesComposed r1 r2 rs prf prf2 ⦄) )
  =⟨ normalisedSortedList0 ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs) (sortedListComposed r1 r2 rs prf) (validRangesComposed r1 r2 rs prf prf2) ⟩
  true
 end
normalisedSortedList00 ⦃ o ⦄ ⦃ dio ⦄ rs r1 r2 prf prf2 false =
   begin
      validRangeList (if_then_else_ false
      (normalise ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs) ⦃ sortedListComposed r1 r2 rs prf ⦄ ⦃ validRangesComposed r1 r2 rs prf prf2 ⦄)
         (r1 ∷ (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄)))
  =⟨⟩
      validRangeList (r1 ∷ (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄))
  =⟨ validList r1 (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄)
  (normalisedSortedList (r2 ∷ rs) (headandtailSorted (r1 ∷ r2 ∷ rs) prf) (headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2))  ⟩
  true
 end

normalisedSortedList0 ⦃ o ⦄ ⦃ dio ⦄ ms@([]) prf prf2 =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (normalise [] ⦃ prf ⦄ ⦃ prf2 ⦄)
  =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
  =⟨⟩
      true
   end
normalisedSortedList0 ⦃ o ⦄ ⦃ dio ⦄ ms@(m ∷ []) prf prf2 =
   begin
      validRangeList (normalise ms ⦃ prf ⦄ ⦃ prf2 ⦄)
  =⟨⟩
      validRangeList (m ∷ [])
  =⟨⟩
      (rangeLower m <= rangeUpper m)
  =⟨ sym (prop_and_true (rangeLower m <= rangeUpper m))  ⟩
      (rangeLower m <= rangeUpper m) && true
  =⟨⟩
      (rangeLower m <= rangeUpper m) && (validRanges ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
      validRanges ms
  =⟨ propIsTrue (validRanges ms) prf2 ⟩
      true
  end
normalisedSortedList0 ⦃ o ⦄ ⦃ dio ⦄ ms@(r1 ∷ r2 ∷ rs) prf prf2 =
   begin
      validRangeList (normalise ms ⦃ prf ⦄ ⦃ prf2 ⦄)
  =⟨⟩
      validRangeList (if_then_else_ (overlap1 r1 r2)
      (normalise ((Rg (rangeLower r1) (max (rangeUpper r1) (rangeUpper r2))) ∷ rs) ⦃ sortedListComposed r1 r2 rs prf ⦄ ⦃ validRangesComposed r1 r2 rs prf prf2 ⦄)
         (r1 ∷ (normalise (r2 ∷ rs) ⦃ headandtailSorted (r1 ∷ r2 ∷ rs) prf ⦄ ⦃ headandtailValidRanges (r1 ∷ r2 ∷ rs) prf2 ⦄)))
  =⟨ normalisedSortedList00 rs r1 r2 prf prf2 (overlap1 r1 r2) ⟩
      true
  end

unfoldIsSorted00 ⦃ o ⦄ ⦃ dio ⦄ b f g b1 false =
     begin
      sortedRangeList ((Rg b (f b)) ∷ (if_then_else_ false (ranges2 b1 f g) []))
  =⟨⟩
      sortedRangeList ((Rg b (f b)) ∷ [])
  =⟨⟩
   true
   end
unfoldIsSorted00 ⦃ o ⦄ ⦃ dio ⦄ b f g b1 true =
     begin
      sortedRangeList ((Rg b (f b)) ∷ (if_then_else_ true (ranges2 b1 f g) []))
  =⟨⟩
      sortedRangeList ((Rg b (f b)) ∷ (ranges2 b1 f g))
  =⟨ validSortedList (Rg b (f b)) (ranges2 b1 f g) (unfoldSorted b1 f g) ⟩
   true
   end

unfoldIsSorted0 ⦃ o ⦄ ⦃ dio ⦄ b f g Nothing =
     begin
      sortedRangeList ((Rg b (f b)) ∷ (ranges3 Nothing f g))
  =⟨⟩
      sortedRangeList ((Rg b (f b)) ∷ [])
  =⟨⟩
   true
   end
unfoldIsSorted0 ⦃ o ⦄ ⦃ dio ⦄ b f g mb@(Just b1) =
     begin
      sortedRangeList ((Rg b (f b)) ∷ (ranges3 mb f g))
  =⟨⟩
      sortedRangeList ((Rg b (f b)) ∷ (if_then_else_ ((validFunction2 b1 f) && (validFunction b1 g)) (ranges2 b1 f g) []))
  =⟨ unfoldIsSorted00 b f g b1 ((validFunction2 b1 f) && (validFunction b1 g)) ⟩
   true
   end

unfoldIsSorted ⦃ o ⦄ ⦃ dio ⦄ b f g =
   begin
      sortedRangeList (ranges2 b f g)
  =⟨⟩
      sortedRangeList ((Rg b (f b)) ∷ (ranges3 (g b) f g))
  =⟨ unfoldIsSorted0 b f g (g b) ⟩
   true
   end

unfoldSorted ⦃ o ⦄ ⦃ dio ⦄ b f g = subst IsTrue (sym (unfoldIsSorted b f g)) IsTrue.itsTrue

merge1IsSorted0 ⦃ o ⦄ ⦃ dio ⦄ h1 h2 rs1@(RS []) rs2@(RS []) true prf1 prf2 =
   begin
      sortedRangeList (h1 ∷ (merge1 [] (h2 ∷ [])))
  =⟨⟩
      sortedRangeList (h1 ∷ h2 ∷ [])
  =⟨ okSorted h1 h2 ⟩
      true
   end
merge1IsSorted0 ⦃ o ⦄ ⦃ dio ⦄ h1 h2 rs1@(RS []) rs2@(RS t2@(h4 ∷ tt2)) true prf1 prf2 =
   begin
      sortedRangeList (h1 ∷ (merge1 [] (h2 ∷ t2)))
  =⟨⟩
      sortedRangeList (h1 ∷ (h2 ∷ t2))
  =⟨ validSortedList h1 (h2 ∷ t2) (validIsSorted (h2 ∷ t2) prf2) ⟩
      true
   end
merge1IsSorted0 ⦃ o ⦄ ⦃ dio ⦄ h1 h2 rs1@(RS t1@(h3 ∷ tt1)) rs2@(RS t2) true prf1 prf2 =
   begin
      sortedRangeList (h1 ∷ (merge1 t1 (h2 ∷ t2)))
  =⟨ validSortedList h1 (merge1 t1 (h2 ∷ t2)) (merge1Sorted rs1 (RS (h2 ∷ t2) {prf2}) (headandtail (RS (h1 ∷ t1) {prf1}) prf1) prf2) ⟩
      true
   end
merge1IsSorted0 ⦃ o ⦄ ⦃ dio ⦄ h1 h2 rs1@(RS []) rs2@(RS []) false prf1 prf2 =
   begin
      sortedRangeList (h2 ∷ (merge1 (h1 ∷ []) []))
  =⟨⟩
      sortedRangeList (h2 ∷ h1 ∷ [])
  =⟨ okSorted h2 h1 ⟩
      true
   end
merge1IsSorted0 ⦃ o ⦄ ⦃ dio ⦄ h1 h2 rs1@(RS t1@(h3 ∷ tt1)) rs2@(RS []) false prf1 prf2 =
   begin
      sortedRangeList (h2 ∷ (merge1 (h1 ∷ t1) []))
  =⟨⟩
      sortedRangeList (h2 ∷ h1 ∷ t1)
  =⟨ validSortedList h2 (h1 ∷ t1) (validIsSorted (h1 ∷ t1) prf1) ⟩
      true
   end
merge1IsSorted0 ⦃ o ⦄ ⦃ dio ⦄ h1 h2 rs1@(RS t1) rs2@(RS t2@(h4 ∷ tt2)) false prf1 prf2 =
   begin
      sortedRangeList (h2 ∷ (merge1 (h1 ∷ t1) t2))
  =⟨ validSortedList h2 (merge1 (h1 ∷ t1) t2) (merge1Sorted (RS (h1 ∷ t1) {prf1}) rs2 prf1 (headandtail (RS (h2 ∷ t2) {prf2}) prf2)) ⟩
      true
   end

merge1IsSorted1 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) rs2@(RS []) prf1 prf2 = refl
merge1IsSorted1 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ms1@(h1 ∷ t1)) rs2@(RS []) prf1 prf2 = propIsTrue (sortedRangeList (merge1 (rSetRanges rs1) (rSetRanges rs2))) (validIsSorted (merge1 (rSetRanges rs1) (rSetRanges rs2)) prf1)
merge1IsSorted1 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) rs2@(RS ms1@(h1 ∷ t1)) prf1 prf2 = propIsTrue (sortedRangeList (merge1 (rSetRanges rs1) (rSetRanges rs2))) (validIsSorted (merge1 (rSetRanges rs1) (rSetRanges rs2)) prf2)
merge1IsSorted1 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ms1@(h1 ∷ t1)) rs2@(RS ms2@(h2 ∷ t2)) prf1 prf2 =
   begin
      sortedRangeList (merge1 (rSetRanges rs1) (rSetRanges rs2))
  =⟨⟩
      sortedRangeList (if_then_else_ (h1 < h2) (h1 ∷ (merge1 t1 ms2)) (h2 ∷ (merge1 ms1 t2)))
  =⟨ merge1IsSorted0 h1 h2 (RS t1 {headandtail rs1 prf1}) (RS t2 {headandtail rs2 prf2}) (h1 < h2) prf1 prf2 ⟩
      true
   end

singletonRangeValid0 ⦃ o ⦄ ⦃ dio ⦄ x =
  begin
   validRangeList ((singletonRange x) ∷ [])
  =⟨⟩
    ((rangeLower (singletonRange x)) <= (rangeUpper (singletonRange x)))
  =⟨⟩
    ((rangeLower (Rg (BoundaryBelow x) (BoundaryAbove x))) <= (rangeUpper (Rg (BoundaryBelow x) (BoundaryAbove x))))
  =⟨⟩
    (BoundaryBelow x <= BoundaryAbove x)
  =⟨⟩
    ((compare (BoundaryBelow x) (BoundaryAbove x) == LT) || (compare (BoundaryBelow x) (BoundaryAbove x) == EQ))
  =⟨⟩
    (((if_then_else_ (x > x) (if_then_else_ (adjacent x x) EQ GT) LT) == LT) || (compare (BoundaryBelow x) (BoundaryAbove x) == EQ))
  =⟨ cong (_|| (compare (BoundaryBelow x) (BoundaryAbove x) == EQ)) (cong (_== LT) (propIf3 (x > x) (lt x x refl))) ⟩
    ((LT == LT) || (compare (BoundaryBelow x) (BoundaryAbove x) == EQ))
  =⟨⟩
    (true || (compare (BoundaryBelow x) (BoundaryAbove x) == EQ))
  =⟨⟩
    true
  end

intersectHelper ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ls1) rs2@(RS ls2) prf1 prf2 =
  begin
     validRangeList (rSetRanges (rSetIntersection rs1 {prf1} rs2 {prf2}))
  =⟨⟩
     validRangeList (rSetRanges (RS (filter (λ r → (rangeIsEmpty r) == false) (merge2 (rSetRanges rs1) (rSetRanges rs2))) {intersection0 rs1 rs2 prf1 prf2}))
  =⟨⟩
     validRangeList (filter (λ r → (rangeIsEmpty r) == false) (merge2 (rSetRanges rs1) (rSetRanges rs2)))
  end

negationHelper ⦃ o ⦄ ⦃ dio ⦄ rs@(RS ranges) {prf} =
  begin
     validRangeList (rSetRanges (rSetNegation rs {prf}))
  =⟨⟩
     validRangeList (rSetRanges (RS ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ ranges))) {negation rs prf}))
  =⟨⟩
    validRangeList (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ ranges)))
  =⟨⟩
    validRangeList (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs))))
  end

fullRangeValid ⦃ o ⦄ ⦃ dio ⦄ =
  begin
     validRangeList ⦃ o ⦄ ⦃ dio ⦄ (fullRange ⦃ o ⦄ ⦃ dio ⦄ ∷ [])
  =⟨⟩
    ((rangeLower (fullRange ⦃ o ⦄ ⦃ dio ⦄)) <= (rangeUpper (fullRange ⦃ o ⦄ ⦃ dio ⦄)))
  =⟨⟩
    true
  end

intersection3 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges1@(r1 ∷ rss1)) rs2@(RS ranges2@(r2 ∷ rss2)) ⦃ ne1 ⦄ ⦃ ne2 ⦄ prf1 prf2 true =
  begin
    validRangeList (filter (λ x → (rangeIsEmpty x == false))
         (if_then_else_ true
            (merge2 rss1 ranges2) (merge2 ⦃ o ⦄ ⦃ dio ⦄ ranges1 rss2)))
   =⟨⟩
    validRangeList (filter (λ x → (rangeIsEmpty x == false)) (merge2 rss1 ranges2))
   =⟨ intersectionHolds
 ⦃ o ⦄ ⦃ dio ⦄ (RS rss1 {headandtail rs1 ⦃ NonEmpty.itsNonEmpty ⦄ prf1}) rs2 (headandtail ⦃ o ⦄ ⦃ dio ⦄ rs1 ⦃ ne1 ⦄ prf1) prf2 ⟩
      true
   end
intersection3 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges1@(r1 ∷ rss1)) rs2@(RS ranges2@(r2 ∷ rss2)) ⦃ ne1 ⦄ ⦃ ne2 ⦄ prf1 prf2 false =
  begin
    validRangeList (filter (λ x → (rangeIsEmpty x == false))
         (if_then_else_ false
            (merge2 ⦃ o ⦄ ⦃ dio ⦄ rss1 ranges2) (merge2 ranges1 rss2)))
   =⟨⟩
    validRangeList (filter (λ x → (rangeIsEmpty x == false)) (merge2 ranges1 rss2))
   =⟨ intersectionHolds
 ⦃ o ⦄ ⦃ dio ⦄ rs1 (RS rss2 {headandtail rs2 ⦃ NonEmpty.itsNonEmpty ⦄ prf2}) prf1 (headandtail ⦃ o ⦄ ⦃ dio ⦄ rs2 ⦃ ne2 ⦄ prf2) ⟩
      true
   end

intersection2 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges1@(r1 ∷ rss1)) rs2@(RS ranges2@(r2 ∷ rss2)) ⦃ ne1 ⦄ ⦃ ne2 ⦄ prf1 prf2 false =
  begin
        validRangeList (
       if_then_else_ false

      ((rangeIntersection ⦃ o ⦄ ⦃ dio ⦄ r1 r2) ∷ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false))
       (if_then_else_ ((rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1) < (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2))
       (merge2 ⦃ o ⦄ ⦃ dio ⦄ rss1 ranges2) (merge2 ⦃ o ⦄ ⦃ dio ⦄ ranges1 rss2))))

       (filter (λ x → (rangeIsEmpty x == false))
         (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)
         (merge2 rss1 ranges2) (merge2 ranges1 rss2)))
      )
   =⟨⟩
    validRangeList (filter (λ x → (rangeIsEmpty x == false))
    (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)
    (merge2 rss1 ranges2) (merge2 ranges1 rss2)))
   =⟨ intersection3 ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 ⦃ ne1 ⦄ ⦃ ne2 ⦄ prf1 prf2 (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2) ⟩
    true
   end
intersection2 ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges1@(r1 ∷ rss1)) rs2@(RS ranges2@(r2 ∷ rss2)) ⦃ ne1 ⦄ ⦃ ne2 ⦄ prf1 prf2 true =
  begin
        validRangeList (
       if_then_else_ true

      ((rangeIntersection ⦃ o ⦄ ⦃ dio ⦄ r1 r2) ∷ (filter (λ x → (rangeIsEmpty x == false))
       (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)
       (merge2 rss1 ranges2) (merge2 ranges1 rss2))))

       (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false))
         (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)
         (merge2 ⦃ o ⦄ ⦃ dio ⦄ rss1 ranges2) (merge2 ⦃ o ⦄ ⦃ dio ⦄ ranges1 rss2)))
      )
   =⟨⟩
    validRangeList ((rangeIntersection ⦃ o ⦄ ⦃ dio ⦄ r1 r2) ∷ (filter (λ x → (rangeIsEmpty x == false))
       (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)
       (merge2 rss1 ranges2) (merge2 ranges1 rss2))))
   =⟨ validList (rangeIntersection ⦃ o ⦄ ⦃ dio ⦄ r1 r2) (filter (λ x → (rangeIsEmpty x == false))
       (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)
       (merge2 rss1 ranges2) (merge2 ranges1 rss2)))
       (subst IsTrue (sym
       (intersection3 ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 ⦃ ne1 ⦄ ⦃ ne2 ⦄ prf1 prf2 (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2)))
       IsTrue.itsTrue) ⟩
    true
   end

intersectionHolds ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) rs2@(RS []) _ _ =
   begin
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) (merge2 ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs1) (rSetRanges rs2)))
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) (merge2 ⦃ o ⦄ ⦃ dio ⦄ [] []))
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) [])
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
   =⟨⟩
    true
   end
intersectionHolds ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges@(r ∷ rs)) rs2@(RS []) _ _ =
   begin
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) (merge2 ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs1) (rSetRanges rs2)))
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) (merge2 ⦃ o ⦄ ⦃ dio ⦄ ranges []))
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) [])
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
   =⟨⟩
    true
   end

intersectionHolds ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS []) rs2@(RS ranges@(r ∷ rs)) _ _ =
   begin
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) (merge2 ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs1) (rSetRanges rs2)))
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) (merge2 ⦃ o ⦄ ⦃ dio ⦄ [] ranges))
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ (filter (λ x → (rangeIsEmpty ⦃ o ⦄ ⦃ dio ⦄ x == false)) [])
   =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
   =⟨⟩
    true
   end

intersectionHolds ⦃ o ⦄ ⦃ dio ⦄ rs1@(RS ranges1@(r1 ∷ rss1)) rs2@(RS ranges2@(r2 ∷ rss2)) prf1 prf2 =
   begin
    validRangeList (filter (λ x → (rangeIsEmpty x == false)) (merge2 (rSetRanges rs1) (rSetRanges rs2)))
   =⟨⟩
    validRangeList (filter (λ x → (rangeIsEmpty x == false))
      ((rangeIntersection r1 r2) ∷ (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2) (merge2 rss1 ranges2) (merge2 ranges1 rss2))))
   =⟨⟩
    validRangeList (
       if_then_else_ (rangeIsEmpty (rangeIntersection r1 r2) == false)

      ((rangeIntersection r1 r2) ∷ (filter (λ x → (rangeIsEmpty x == false))
       (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2) (merge2 rss1 ranges2) (merge2 ranges1 rss2))))

       (filter (λ x → (rangeIsEmpty x == false))
         (if_then_else_ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r1 < rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r2) (merge2 rss1 ranges2) (merge2 ranges1 rss2)))
      )
   =⟨ intersection2 ⦃ o ⦄ ⦃ dio ⦄ rs1 rs2 prf1 prf2 (rangeIsEmpty (rangeIntersection r1 r2) == false) ⟩
     true
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ [] =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 [])
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
   =⟨⟩
      true
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ []
   end
validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (BoundaryAboveAll ∷ []) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (BoundaryAboveAll  ∷ []))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
   =⟨⟩
      true
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (BoundaryAboveAll ∷ [])
   end
validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (BoundaryBelowAll ∷ []) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (BoundaryBelowAll ∷ []))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg BoundaryBelowAll BoundaryAboveAll) ∷ [])
   =⟨⟩
      true
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (BoundaryBelowAll ∷ [])
   end
validRanges1 ⦃ o ⦄ ⦃ dio ⦄ ((BoundaryAbove x) ∷ []) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ ((BoundaryAbove x) ∷ []))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg (BoundaryAbove x) BoundaryAboveAll) ∷ [])
   =⟨⟩
      (BoundaryAbove x) <= BoundaryAboveAll
   =⟨⟩
      true
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ ((BoundaryAbove x) ∷ [])
   end
validRanges1 ⦃ o ⦄ ⦃ dio ⦄ ((BoundaryBelow x) ∷ []) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ ((BoundaryBelow x) ∷ []))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg (BoundaryBelow x) (BoundaryAboveAll)) ∷ [])
   =⟨⟩
      (BoundaryBelow x) <= BoundaryAboveAll
   =⟨⟩
      true
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ ((BoundaryBelow x) ∷ [])
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ []) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ []))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ ranges1([]))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ [])
   =⟨⟩
      (b1 <= b2)
   =⟨ sym (prop_and_true (b1 <= b2)) ⟩
      ((b1 <= b2) && true)
   =⟨⟩
      ((b1 <= b2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ []))
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ [])
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs@(b3@(BoundaryBelow x) ∷ [])) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (Rg b3 (BoundaryAboveAll)) ∷ [])
   =⟨⟩
      ((okAdjacent (Rg b1 b2) (Rg b3 (BoundaryAboveAll))) && (validRangeList ⦃ o ⦄ ⦃ dio ⦄ []))
   =⟨⟩
      ((okAdjacent (Rg b1 b2) (Rg b3 BoundaryAboveAll)) && true)
   =⟨⟩
      (((b1 <= b2) && (b2 <= b3) && (b3 <= BoundaryAboveAll)) && true)
   =⟨ prop_and_true ((b1 <= b2) && (b2 <= b3) && (b3 <= BoundaryAboveAll)) ⟩
      ((b1 <= b2) && (b2 <= b3) && true)
   =⟨⟩
      ((b1 <= b2) && (b2 <= b3) && (validBoundaryList (b3 ∷ [])))
   =⟨⟩
       ((b1 <= b2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b2 ∷ b3 ∷ [])))
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs)
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs@(b3@(BoundaryAbove x) ∷ [])) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (Rg b3 (BoundaryAboveAll)) ∷ [])
   =⟨⟩
      ((okAdjacent (Rg b1 b2) (Rg b3 BoundaryAboveAll)) && (validRangeList ⦃ o ⦄ ⦃ dio ⦄ []))
   =⟨⟩
      ((okAdjacent (Rg b1 b2) (Rg b3 BoundaryAboveAll)) && true)
   =⟨⟩
      (((b1 <= b2) && (b2 <= b3) && (b3 <= BoundaryAboveAll)) && true)
   =⟨ prop_and_true ((b1 <= b2) && (b2 <= b3) && (b3 <= BoundaryAboveAll)) ⟩
      ((b1 <= b2) && (b2 <= b3) && true)
   =⟨⟩
      ((b1 <= b2) && (b2 <= b3) && (validBoundaryList (b3 ∷ [])))
   =⟨⟩
       ((b1 <= b2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b2 ∷ b3 ∷ [])))
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs)
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs@(b3@(BoundaryBelowAll) ∷ [])) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (Rg b3 (BoundaryAboveAll)) ∷ [])
   =⟨⟩
      ((okAdjacent (Rg b1 b2) (Rg b3 (BoundaryAboveAll))) && (validRangeList ⦃ o ⦄ ⦃ dio ⦄ []))
   =⟨⟩
      ((okAdjacent (Rg b1 b2) (Rg b3 (BoundaryAboveAll))) && true)
   =⟨⟩
      (((b1 <= b2) && (b2 <= b3) && (b3 <= (BoundaryAboveAll))) && true)
   =⟨ prop_and_true ((b1 <= b2) && (b2 <= b3) && (b3 <= (BoundaryAboveAll))) ⟩
      ((b1 <= b2) && (b2 <= b3) && true)
   =⟨⟩
      ((b1 <= b2) && (b2 <= b3) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b3 ∷ [])))
   =⟨⟩
       ((b1 <= b2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b2 ∷ b3 ∷ [])))
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs)
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs@(b3@(BoundaryAboveAll) ∷ [])) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄  (b1 ∷ b2 ∷ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄  bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄  ((Rg b1 b2) ∷ [])
   =⟨⟩
      (b1 <= b2)
   =⟨ sym (prop_and_true (b1 <= b2)) ⟩
      ((b1 <= b2) && true)
   =⟨⟩
      ((b1 <= b2) && (b2 <= b3))
   =⟨ sym (prop_and_true ((b1 <= b2) && (b2 <= b3))) ⟩
      (((b1 <= b2) && (b2 <= b3)) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄  (b3 ∷ [])))
   =⟨ prop_and_assoc (b1 <= b2) (b2 <= b3) (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄  (b3 ∷ [])) ⟩
      ((b1 <= b2) && (b2 <= b3) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄  (b3 ∷ [])))
   =⟨⟩
      ((b1 <= b2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b2 ∷ b3 ∷ [])))
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs)
   end

validRanges1 ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs@(b3 ∷ bss@(b4 ∷ bsss))) =
   begin
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ (ranges1 ⦃ o ⦄ ⦃ dio ⦄  (b1 ∷ b2 ∷ bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄ ((Rg b1 b2) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄  bs))
   =⟨⟩
      validRangeList ⦃ o ⦄ ⦃ dio ⦄  ((Rg b1 b2) ∷ (Rg b3 b4) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bsss))
   =⟨⟩
      (okAdjacent (Rg b1 b2) (Rg b3 b4)) && validRangeList ((Rg b3 b4) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bsss))
   =⟨⟩
      (((b1 <= b2) && (b2 <= b3) && (b3 <= b4)) && (validRangeList ((Rg b3 b4) ∷ (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bsss))))
   =⟨⟩
      (((b1 <= b2) && (b2 <= b3) && (b3 <= b4)) && (validRangeList (ranges1 ⦃ o ⦄ ⦃ dio ⦄ bs)))
   =⟨ cong (((b1 <= b2) && (b2 <= b3) && (b3 <= b4)) &&_) (validRanges1 ⦃ o ⦄ ⦃ dio ⦄ bs) ⟩
      (((b1 <= b2) && ((b2 <= b3) && (b3 <= b4))) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs))
   =⟨ prop_and_assoc (b1 <= b2) ((b2 <= b3) && (b3 <= b4)) (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs) ⟩
      ((b1 <= b2) && (((b2 <= b3) && (b3 <= b4)) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs)))
   =⟨ cong ((b1 <= b2) &&_) (prop_and_assoc (b2 <= b3) (b3 <= b4) (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs)) ⟩
      ((b1 <= b2) && ((b2 <= b3) && (b3 <= b4) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs)))
   =⟨⟩
      ((b1 <= b2) && ((b2 <= b3) && (b3 <= b4) && (b3 <= b4 && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bss))))
   =⟨ cong ((b1 <= b2) &&_) (cong (b2 <= b3 &&_) (prop_and_cancel (b3 <= b4))) ⟩
      ((b1 <= b2) && (b2 <= b3) && (b3 <= b4) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bss))
   =⟨⟩
      ((b1 <= b2) && (b2 <= b3) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs))
   =⟨⟩
      ((b1 <= b2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b2 ∷ bs)))
   =⟨⟩
      validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (b1 ∷ b2 ∷ bs)
   end

validSetBounds ⦃ o ⦄ ⦃ dio ⦄ [] =
  begin
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ []
   end

validSetBounds ⦃ o ⦄ ⦃ dio ⦄ bs@(BoundaryBelowAll ∷ []) =
  begin
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ bs)
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ []
  =⟨⟩
   true
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bs
   end

validSetBounds ⦃ o ⦄ ⦃ dio ⦄ bs@(b0@(BoundaryBelowAll) ∷ bss@(b1 ∷ b2)) =
  begin
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ bs)
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bss
  =⟨⟩
    (true && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bss))
  =⟨ cong (_&& (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ bss)) (sym (BoundaryBelowAllSmaller ⦃ o ⦄ ⦃ dio ⦄ b1)) ⟩
    ((BoundaryBelowAll <= b1) && (validBoundaryList bss))
  =⟨⟩
    validBoundaryList bs
  end

validSetBounds ⦃ o ⦄ ⦃ dio ⦄ bs@(b@(BoundaryBelow x) ∷ bss) =
  begin
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ bs)
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (BoundaryBelowAll ∷ bs)
  =⟨⟩
    ((BoundaryBelowAll <= b) && (validBoundaryList bs))
  =⟨⟩
    (true && (validBoundaryList bs))
  =⟨⟩
    (validBoundaryList bs)
   end

validSetBounds ⦃ o ⦄ ⦃ dio ⦄ bs@(b@(BoundaryAboveAll) ∷ bss) =
  begin
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ bs)
  =⟨⟩
    validBoundaryList (BoundaryBelowAll ∷ bs)
  =⟨⟩
    ((BoundaryBelowAll <= b) && (validBoundaryList bs))
  =⟨⟩
    (true && (validBoundaryList bs))
  =⟨⟩
    (validBoundaryList bs)
   end
validSetBounds ⦃ o ⦄ ⦃ dio ⦄ bs@(b@(BoundaryAbove x) ∷ bss) =
  begin
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (setBounds1 ⦃ o ⦄ ⦃ dio ⦄ bs)
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (BoundaryBelowAll ∷ bs)
  =⟨⟩
    ((BoundaryBelowAll <= b) && (validBoundaryList bs))
  =⟨⟩
    (true && (validBoundaryList bs))
  =⟨⟩
    (validBoundaryList bs)
   end

valid ⦃ o ⦄ ⦃ dio ⦄ rs@(RS []) {_} =
  begin
     validRangeList ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs)
  =⟨⟩
    validRangeList ⦃ o ⦄ ⦃ dio ⦄ []
  =⟨⟩
    true
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ []
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ [])
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs))
  end
valid ⦃ o ⦄ ⦃ dio ⦄ rs@(RS (r ∷ [])) {_} =
  begin
     validRangeList ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs)
  =⟨⟩
     validRangeList ⦃ o ⦄ ⦃ dio ⦄ (r ∷ [])
  =⟨⟩
    ((rangeLower ⦃ o ⦄ ⦃ dio ⦄  r) <= (rangeUpper ⦃ o ⦄ ⦃ dio ⦄  r))
  =⟨ sym (prop_and_true ((rangeLower ⦃ o ⦄ ⦃ dio ⦄  r) <= (rangeUpper ⦃ o ⦄ ⦃ dio ⦄  r))) ⟩
    (((rangeLower ⦃ o ⦄ ⦃ dio ⦄  r) <= (rangeUpper ⦃ o ⦄ ⦃ dio ⦄  r)) && true)
  =⟨⟩
    (((rangeLower ⦃ o ⦄ ⦃ dio ⦄  r) <= (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r)) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ []))
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ ((rangeLower ⦃ o ⦄ ⦃ dio ⦄  r) ∷ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄ r) ∷ [])
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ (r ∷ []))
  =⟨⟩
    validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs))
  end

valid ⦃ o ⦄ ⦃ dio ⦄ rs@(RS ranges@(r@(Rg l1 u1) ∷ r1@(r2@(Rg l2 u2) ∷ rss))) {prf} =
  begin
     validRangeList ⦃ o ⦄ ⦃ dio ⦄ (rSetRanges rs)
  =⟨⟩
     validRangeList ⦃ o ⦄ ⦃ dio ⦄ (r ∷ (r2 ∷ rss))
  =⟨⟩
     ((okAdjacent r r2) && (validRangeList ⦃ o ⦄ ⦃ dio ⦄ r1))
  =⟨⟩
    ((l1 <= u1 && (u1 <= l2 && l2 <= u2)) && (validRangeList ⦃ o ⦄ ⦃ dio ⦄ r1))
  =⟨ cong ((l1 <= u1 && u1 <= l2 && l2 <= u2) &&_) (valid ⦃ o ⦄ ⦃ dio ⦄ (RS r1 {headandtail rs prf}) {headandtail rs prf}) ⟩
     ((l1 <= u1 && (u1 <= l2 && l2 <= u2)) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ r1)))
  =⟨ prop_and_assoc (l1 <= u1) (u1 <= l2 && l2 <= u2) (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ r1)) ⟩
    (l1 <= u1 && ((u1 <= l2  && l2 <= u2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ r1))))
  =⟨ cong (l1 <= u1 &&_) (prop_and_assoc (u1 <= l2) (l2 <= u2) (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ r1))) ⟩
    (l1 <= u1 && u1 <= l2  && (l2 <= u2  && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ r1))))
  =⟨⟩
    (l1 <= u1 && u1 <= l2  && (l2 <= u2
         && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ ((rangeLower ⦃ o ⦄ ⦃ dio ⦄  r2) ∷ (rangeUpper ⦃ o ⦄ ⦃ dio ⦄  r2) ∷ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ rss)))))
  =⟨⟩
    (l1 <= u1 && u1 <= l2 && l2 <= u2 && l2 <= u2
         && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ ((rangeUpper ⦃ o ⦄ ⦃ dio ⦄  r2) ∷ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ rss))))
  =⟨ cong (l1 <= u1 &&_) (cong (u1 <= l2 &&_) (prop_and_cancel (l2 <= u2))) ⟩
    (l1 <= u1 && u1 <= l2 && ((l2 <= u2) && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (u2 ∷ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ rss)))))
  =⟨⟩
    (l1 <= u1 && u1 <= l2 && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (l2 ∷ (u2 ∷ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ rss)))))
  =⟨⟩
    (l1 <= u1 && (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (u1 ∷ l2 ∷ u2 ∷ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ rss))))
  =⟨⟩
   (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (l1 ∷ u1 ∷ l2 ∷ u2 ∷ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ rss)))
  =⟨⟩
   (validBoundaryList ⦃ o ⦄ ⦃ dio ⦄ (bounds1 ⦃ o ⦄ ⦃ dio ⦄ ranges))
  end


text:
------------------------------------------------------------------------
-- INCREMENTAL λ-CALCULUS
--
-- Bags with negative multiplicities, for Nehemiah.
--
-- Instead of implementing bags (with negative multiplicities,
-- like in the paper) in Agda, we postulate that a group of such
-- bags exist. Note that integer bags with integer multiplicities
-- are actually the free group given a singleton operation
-- `Integer -> Bag`, so this should be easy to formalize in
-- principle.
------------------------------------------------------------------------
module Postulate.Bag-Nehemiah where

-- Postulates about bags of integers, version Nehemiah
--
-- This module postulates bags of integers with negative
-- multiplicities as a group under additive union.

open import Relation.Binary.PropositionalEquality
open import Algebra.Structures
open import Data.Integer

-- postulate Bag as an abelion group
postulate Bag : Set
-- singleton
postulate singletonBag : ℤ → Bag
-- union
postulate _++_ : Bag → Bag → Bag
infixr 5 _++_
-- negate = mapMultiplicities (λ z → - z)
postulate negateBag : Bag → Bag
postulate emptyBag : Bag
instance
  postulate abelian-bag : IsAbelianGroup _≡_ _++_ emptyBag negateBag

-- Naming convention follows Algebra.Morphism
-- Homomorphic₁ : morphism preserves negation
Homomorphic₁ :
  {A B : Set} (f : A → B) (negA : A → A) (negB : B → B) → Set
Homomorphic₁ {A} {B} f negA negB = ∀ {x} → f (negA x) ≡ negB (f x)

-- Homomorphic₂ : morphism preserves binary operation.
Homomorphic₂ :
  {A B : Set} (f : A → B) (_+_ : A → A → A) (_*_ : B → B → B) → Set
Homomorphic₂ {A} {B} f _+_ _*_ = ∀ {x y} → f (x + y) ≡ f x * f y

-- postulate map, flatmap and sum to be homomorphisms
postulate mapBag : (f : ℤ → ℤ) (b : Bag) → Bag
postulate flatmapBag : (f : ℤ → Bag) (b : Bag) → Bag
postulate sumBag : Bag → ℤ
postulate homo-map : ∀ {f} → Homomorphic₂ (mapBag f) _++_ _++_
postulate homo-flatmap : ∀ {f} → Homomorphic₂ (flatmapBag f) _++_ _++_
postulate homo-sum : Homomorphic₂ sumBag _++_ _+_
postulate neg-map : ∀ {f} → Homomorphic₁ (mapBag f) negateBag negateBag
postulate neg-flatmap : ∀ {f} → Homomorphic₁ (flatmapBag f) negateBag negateBag

ext: agda

max_stars_repo_name: inc-lc/ilc-agda

max_issues_repo_name: inc-lc/ilc-agda

max_forks_repo_name: inc-lc/ilc-agda


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of functions, such as associativity and commutativity
------------------------------------------------------------------------

-- These properties can (for instance) be used to define algebraic
-- structures.

open import Level
open import Relation.Binary

-- The properties are specified using the following relation as
-- "equality".

module Algebra.FunctionProperties
         {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) where

open import Data.Product

------------------------------------------------------------------------
-- Unary and binary operations

open import Algebra.FunctionProperties.Core public

------------------------------------------------------------------------
-- Properties of operations

Associative : Op₂ A → Set _
Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

Commutative : Op₂ A → Set _
Commutative _∙_ = ∀ x y → (x ∙ y) ≈ (y ∙ x)

LeftIdentity : A → Op₂ A → Set _
LeftIdentity e _∙_ = ∀ x → (e ∙ x) ≈ x

RightIdentity : A → Op₂ A → Set _
RightIdentity e _∙_ = ∀ x → (x ∙ e) ≈ x

Identity : A → Op₂ A → Set _
Identity e ∙ = LeftIdentity e ∙ × RightIdentity e ∙

LeftZero : A → Op₂ A → Set _
LeftZero z _∙_ = ∀ x → (z ∙ x) ≈ z

RightZero : A → Op₂ A → Set _
RightZero z _∙_ = ∀ x → (x ∙ z) ≈ z

Zero : A → Op₂ A → Set _
Zero z ∙ = LeftZero z ∙ × RightZero z ∙

LeftInverse : A → Op₁ A → Op₂ A → Set _
LeftInverse e _⁻¹ _∙_ = ∀ x → (x ⁻¹ ∙ x) ≈ e

RightInverse : A → Op₁ A → Op₂ A → Set _
RightInverse e _⁻¹ _∙_ = ∀ x → (x ∙ (x ⁻¹)) ≈ e

Inverse : A → Op₁ A → Op₂ A → Set _
Inverse e ⁻¹ ∙ = LeftInverse e ⁻¹ ∙ × RightInverse e ⁻¹ ∙

_DistributesOverˡ_ : Op₂ A → Op₂ A → Set _
_*_ DistributesOverˡ _+_ =
  ∀ x y z → (x * (y + z)) ≈ ((x * y) + (x * z))

_DistributesOverʳ_ : Op₂ A → Op₂ A → Set _
_*_ DistributesOverʳ _+_ =
  ∀ x y z → ((y + z) * x) ≈ ((y * x) + (z * x))

_DistributesOver_ : Op₂ A → Op₂ A → Set _
* DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)

_IdempotentOn_ : Op₂ A → A → Set _
_∙_ IdempotentOn x = (x ∙ x) ≈ x

Idempotent : Op₂ A → Set _
Idempotent ∙ = ∀ x → ∙ IdempotentOn x

IdempotentFun : Op₁ A → Set _
IdempotentFun f = ∀ x → f (f x) ≈ f x

_Absorbs_ : Op₂ A → Op₂ A → Set _
_∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x

Absorptive : Op₂ A → Op₂ A → Set _
Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)

Involutive : Op₁ A → Set _
Involutive f = ∀ x → f (f x) ≈ x


text:
------------------------------------------------------------------------------
-- Properties of the divisibility relation
------------------------------------------------------------------------------

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

module LTC-PCF.Data.Nat.Divisibility.By0.Properties where

open import Common.FOL.Relation.Binary.EqReasoning

open import LTC-PCF.Base
open import LTC-PCF.Base.Properties
open import LTC-PCF.Data.Nat
open import LTC-PCF.Data.Nat.Properties
open import LTC-PCF.Data.Nat.Divisibility.By0
open import LTC-PCF.Data.Nat.Inequalities
open import LTC-PCF.Data.Nat.Inequalities.Properties
open import LTC-PCF.Data.Nat.Properties
open import LTC-PCF.Data.Nat.UnaryNumbers
open import LTC-PCF.Data.Nat.UnaryNumbers.Totality

------------------------------------------------------------------------------
-- Any positive number divides 0.
S∣0 : ∀ {n} → N n → succ₁ n ∣ zero
S∣0 {n} Nn = zero , nzero , sym (*-leftZero (succ₁ n))

-- 0 divides 0.
0∣0 : zero ∣ zero
0∣0 = zero , nzero , sym (*-leftZero zero)

-- The divisibility relation is reflexive.
∣-refl : ∀ {n} → N n → n ∣ n
∣-refl {n} Nn = [1] , 1-N , sym (*-leftIdentity Nn)

-- If x divides y and z then x divides y ∸ z.
x∣y→x∣z→x∣y∸z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                       n ≡ k * m →
                       o ≡ k' * m →
                       n ∸ o ≡ (k ∸ k') * m
x∣y→x∣z→x∣y∸z-helper Nm Nk Nk' refl refl = sym (*∸-leftDistributive Nk Nk' Nm)

x∣y→x∣z→x∣y∸z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n ∸ o
x∣y→x∣z→x∣y∸z Nm Nn No (k , Nk , h₁) (k' , Nk' , h₂) =
  k ∸ k' , ∸-N Nk Nk' , x∣y→x∣z→x∣y∸z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and z then x divides y + z.
x∣y→x∣z→x∣y+z-helper : ∀ {m n o k k'} → N m → N k → N k' →
                       n ≡ k * m →
                       o ≡ k' * m →
                       n + o ≡ (k + k') * m
x∣y→x∣z→x∣y+z-helper Nm Nk Nk' refl refl = sym (*+-leftDistributive Nk Nk' Nm)

x∣y→x∣z→x∣y+z : ∀ {m n o} → N m → N n → N o → m ∣ n → m ∣ o → m ∣ n + o
x∣y→x∣z→x∣y+z Nm Nn No (k , Nk , h₁) (k' , Nk' , h₂) =
  k + k' , +-N Nk Nk' , x∣y→x∣z→x∣y+z-helper Nm Nk Nk' h₁ h₂

-- If x divides y and y is positive, then x ≤ y.
x∣S→x≤S : ∀ {m n} → N m → N n → m ∣ (succ₁ n) → m ≤ succ₁ n
x∣S→x≤S {m} Nm Nn (.zero , nzero , Sn≡0*m) =
  ⊥-elim (0≢S (trans (sym (*-leftZero m)) (sym Sn≡0*m)))
x∣S→x≤S {m} Nm Nn (.(succ₁ k) , nsucc {k} Nk , Sn≡Sk*m) =
  subst (λ t₁ → m ≤ t₁)
        (sym Sn≡Sk*m)
        (subst (λ t₂ → m ≤ t₂)
               (sym (*-Sx k m))
               (x≤x+y Nm (*-N Nk Nm)))

0∣x→x≡0 : ∀ {m} → N m → zero ∣ m → m ≡ zero
0∣x→x≡0 nzero          _                 = refl
0∣x→x≡0 (nsucc {m} Nm) (k , Nk , Sm≡k*0) =
  ⊥-elim (0≢S (trans (sym (*-leftZero k))
                     (trans (*-comm nzero Nk) (sym Sm≡k*0))))

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


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

open import lib.Basics
open import lib.NType2
open import lib.types.Pi
open import lib.types.Group

{-
    The definition of G-sets.  Thanks to Daniel Grayson.
-}

module lib.types.GroupSet {i} where

  -- The right group action with respect to the group [grp].
  record GsetStructure (grp : Group i) {j} (El : Type j)
    (_ : is-set El) : Type (lmax i j) where
    constructor gset-structure
    private
      module G = Group grp
      module GS = GroupStructure G.group-struct
    field
      act : El → G.El → El
      unit-r : ∀ x → act x GS.ident == x
      assoc : ∀ x g₁ g₂ → act (act x g₁) g₂ == act x (GS.comp g₁ g₂)

  -- The definition of a G-set.  A set [El] equipped with
  -- a right group action with respect to [grp].
  record Gset (grp : Group i) j : Type (lsucc (lmax i j)) where
    constructor gset
    field
      El : Type j
      El-level : is-set El
      gset-struct : GsetStructure grp El El-level
    open GsetStructure gset-struct public
    El-is-set = El-level

  -- A helper function to establish equivalence between two G-sets.
  -- Many data are just props and this function do the coversion for them
  -- for you.  You only need to show the non-trivial parts.
  module _ {grp : Group i} {j} {El : Type j} {El-level : is-set El} where
    private
      module G = Group grp
      module GS = GroupStructure G.group-struct
    open GsetStructure
    private
      gset-structure=' : ∀ {gss₁ gss₂ : GsetStructure grp El El-level}
        → (act= : act gss₁ == act gss₂)
        → unit-r gss₁ == unit-r gss₂
          [ (λ act → ∀ x → act x GS.ident == x) ↓ act= ]
        → assoc gss₁ == assoc gss₂
          [ (λ act → ∀ x g₁ g₂ →
              act (act x g₁) g₂ == act x (GS.comp g₁ g₂)) ↓ act= ]
        → gss₁ == gss₂
      gset-structure=' {gset-structure _ _ _} {gset-structure ._ ._ ._}
        idp idp idp = idp

    gset-structure= : ∀ {gss₁ gss₂ : GsetStructure grp El El-level}
      → (∀ x g → act gss₁ x g == act gss₂ x g)
      → gss₁ == gss₂
    gset-structure= act= = gset-structure='
      (λ= λ x → λ= λ g → act= x g)
      (prop-has-all-paths-↓ (Π-level λ _ → El-level _ _))
      (prop-has-all-paths-↓
        (Π-level λ _ → Π-level λ _ → Π-level λ _ → El-level _ _))

  module _ {grp : Group i} {j : ULevel} where
    private
      module G = Group grp
      module GS = GroupStructure G.group-struct
    open Gset {grp} {j}
    private
      gset='' : ∀ {gs₁ gs₂ : Gset grp j}
        → (El= : El gs₁ == El gs₂)
        → (El-level : El-level gs₁ == El-level gs₂ [ is-set ↓ El= ])
        → gset-struct gs₁ == gset-struct gs₂
          [ uncurry (GsetStructure grp) ↓ pair= El= El-level ]
        → gs₁ == gs₂
      gset='' {gset _ _ _} {gset ._ ._ ._} idp idp idp = idp

      gset=' : ∀ {gs₁ gs₂ : Gset grp j}
        → (El= : El gs₁ == El gs₂)
        → (El-level : El-level gs₁ == El-level gs₂ [ is-set ↓ El= ])
        → (∀ {x₁} {x₂} (p : x₁ == x₂ [ idf _ ↓ El= ]) g
            → act gs₁ x₁ g == act gs₂ x₂ g [ idf _ ↓ El= ])
        → gs₁ == gs₂
      gset=' {gset _ _ _} {gset ._ ._ _} idp idp act= =
        gset='' idp idp (gset-structure= λ x g → act= idp g)

    gset= : ∀ {gs₁ gs₂ : Gset grp j}
      → (El≃ : El gs₁ ≃ El gs₂)
      → (∀ {x₁} {x₂}
          → –> El≃ x₁ == x₂
          → ∀ g → –> El≃ (act gs₁ x₁ g) == act gs₂ x₂ g)
      → gs₁ == gs₂
    gset= El≃ act= =
      gset='
        (ua El≃)
        (prop-has-all-paths-↓ is-set-is-prop)
        (λ x= g → ↓-idf-ua-in El≃ $ act= (↓-idf-ua-out El≃ x=) g)

  -- The Gset homomorphism.
  record GsetHom {grp : Group i} {j}
    (gset₁ gset₂ : Gset grp j) : Type (lmax i j) where
    constructor gset-hom
    open Gset
    field
      f : El gset₁ → El gset₂
      pres-act : ∀ g x → f (act gset₁ x g) == act gset₂ (f x) g

  private
    gset-hom=' : ∀ {grp : Group i} {j} {gset₁ gset₂ : Gset grp j}
      {gsh₁ gsh₂ : GsetHom gset₁ gset₂}
      → (f= : GsetHom.f gsh₁ == GsetHom.f gsh₂)
      → (GsetHom.pres-act gsh₁ == GsetHom.pres-act gsh₂
        [ (λ f → ∀ g x → f (Gset.act gset₁ x g) == Gset.act gset₂ (f x) g) ↓ f= ] )
      → gsh₁ == gsh₂
    gset-hom=' idp idp = idp

  gset-hom= : ∀ {grp : Group i} {j} {gset₁ gset₂ : Gset grp j}
    {gsh₁ gsh₂ : GsetHom gset₁ gset₂}
    → (∀ x → GsetHom.f gsh₁ x == GsetHom.f gsh₂ x)
    → gsh₁ == gsh₂
  gset-hom= {gset₂ = gset₂} f= =
    gset-hom='
      (λ= f=)
      (prop-has-all-paths-↓ $
        Π-level λ _ → Π-level λ _ → Gset.El-level gset₂ _ _)

max_stars_repo_name: UlrikBuchholtz/HoTT-Agda

max_issues_repo_name: nicolaikraus/HoTT-Agda

max_forks_repo_name: nicolaikraus/HoTT-Agda


text:
module StratSigma where

data Sigma0 (A : Set0) (B : A -> Set0) : Set0 where
    _,_ : (x : A) (y : B x) -> Sigma0 A B

_*0_ : (A : Set0)(B : Set0) -> Set0
A *0 B = Sigma0 A \_ -> B

fst0 : {A : Set0}{B : A -> Set0} -> Sigma0 A B -> A
fst0 (a , _) = a

snd0 : {A : Set0}{B : A -> Set0} (p : Sigma0 A B) -> B (fst0 p)
snd0 (a , b) = b

data Zero0 : Set0 where

data Unit0 : Set0 where
    Void : Unit0

data Sigma1 (A : Set1) (B : A -> Set1) : Set1 where
    _,_ : (x : A) (y : B x) -> Sigma1 A B

_*1_ : (A : Set1)(B : Set1) -> Set1
A *1 B = Sigma1 A \_ -> B

fst1 : {A : Set1}{B : A -> Set1} -> Sigma1 A B -> A
fst1 (a , _) = a

snd1 : {A : Set1}{B : A -> Set1} (p : Sigma1 A B) -> B (fst1 p)
snd1 (a , b) = b

data Zero1 : Set1 where

data Unit1 : Set1 where
    Void : Unit1

data Sigma2 (A : Set2) (B : A -> Set2) : Set2 where
    _,_ : (x : A) (y : B x) -> Sigma2 A B

_*2_ : (A : Set2)(B : Set2) -> Set2
A *2 B = Sigma2 A \_ -> B

fst2 : {A : Set2}{B : A -> Set2} -> Sigma2 A B -> A
fst2 (a , _) = a

snd2 : {A : Set2}{B : A -> Set2} (p : Sigma2 A B) -> B (fst2 p)
snd2 (a , b) = b

data Zero2 : Set2 where

data Unit2 : Set2 where
    Void : Unit2

data Sigma3 (A : Set3) (B : A -> Set3) : Set3 where
    _,_ : (x : A) (y : B x) -> Sigma3 A B

_*3_ : (A : Set3)(B : Set3) -> Set3
A *3 B = Sigma3 A \_ -> B

fst3 : {A : Set3}{B : A -> Set3} -> Sigma3 A B -> A
fst3 (a , _) = a

snd3 : {A : Set3}{B : A -> Set3} (p : Sigma3 A B) -> B (fst3 p)
snd3 (a , b) = b

data Zero3 : Set3 where

data Unit3 : Set3 where
    Void : Unit3

data Sigma4 (A : Set4) (B : A -> Set4) : Set4 where
    _,_ : (x : A) (y : B x) -> Sigma4 A B

_*4_ : (A : Set4)(B : Set4) -> Set4
A *4 B = Sigma4 A \_ -> B

fst4 : {A : Set4}{B : A -> Set4} -> Sigma4 A B -> A
fst4 (a , _) = a

snd4 : {A : Set4}{B : A -> Set4} (p : Sigma4 A B) -> B (fst4 p)
snd4 (a , b) = b

data Zero4 : Set4 where

data Unit4 : Set4 where
    Void : Unit4

data Sigma5 (A : Set5) (B : A -> Set5) : Set5 where
    _,_ : (x : A) (y : B x) -> Sigma5 A B

_*5_ : (A : Set5)(B : Set5) -> Set5
A *5 B = Sigma5 A \_ -> B

fst5 : {A : Set5}{B : A -> Set5} -> Sigma5 A B -> A
fst5 (a , _) = a

snd5 : {A : Set5}{B : A -> Set5} (p : Sigma5 A B) -> B (fst5 p)
snd5 (a , b) = b

data Zero5 : Set5 where

data Unit5 : Set5 where
    Void : Unit5

data Sigma6 (A : Set6) (B : A -> Set6) : Set6 where
    _,_ : (x : A) (y : B x) -> Sigma6 A B

_*6_ : (A : Set6)(B : Set6) -> Set6
A *6 B = Sigma6 A \_ -> B

fst6 : {A : Set6}{B : A -> Set6} -> Sigma6 A B -> A
fst6 (a , _) = a

snd6 : {A : Set6}{B : A -> Set6} (p : Sigma6 A B) -> B (fst6 p)
snd6 (a , b) = b

data Zero6 : Set6 where

data Unit6 : Set6 where
    Void : Unit6

data Sigma7 (A : Set7) (B : A -> Set7) : Set7 where
    _,_ : (x : A) (y : B x) -> Sigma7 A B

_*7_ : (A : Set7)(B : Set7) -> Set7
A *7 B = Sigma7 A \_ -> B

fst7 : {A : Set7}{B : A -> Set7} -> Sigma7 A B -> A
fst7 (a , _) = a

snd7 : {A : Set7}{B : A -> Set7} (p : Sigma7 A B) -> B (fst7 p)
snd7 (a , b) = b

data Zero7 : Set7 where

data Unit7 : Set7 where
    Void : Unit7

data Sigma8 (A : Set8) (B : A -> Set8) : Set8 where
    _,_ : (x : A) (y : B x) -> Sigma8 A B

_*8_ : (A : Set8)(B : Set8) -> Set8
A *8 B = Sigma8 A \_ -> B

fst8 : {A : Set8}{B : A -> Set8} -> Sigma8 A B -> A
fst8 (a , _) = a

snd8 : {A : Set8}{B : A -> Set8} (p : Sigma8 A B) -> B (fst8 p)
snd8 (a , b) = b

data Zero8 : Set8 where

data Unit8 : Set8 where
    Void : Unit8

data Sigma9 (A : Set9) (B : A -> Set9) : Set9 where
    _,_ : (x : A) (y : B x) -> Sigma9 A B

_*9_ : (A : Set9)(B : Set9) -> Set9
A *9 B = Sigma9 A \_ -> B

fst9 : {A : Set9}{B : A -> Set9} -> Sigma9 A B -> A
fst9 (a , _) = a

snd9 : {A : Set9}{B : A -> Set9} (p : Sigma9 A B) -> B (fst9 p)
snd9 (a , b) = b

data Zero9 : Set9 where

data Unit9 : Set9 where
    Void : Unit9

data Sigma10 (A : Set10) (B : A -> Set10) : Set10 where
    _,_ : (x : A) (y : B x) -> Sigma10 A B

_*10_ : (A : Set10)(B : Set10) -> Set10
A *10 B = Sigma10 A \_ -> B

fst10 : {A : Set10}{B : A -> Set10} -> Sigma10 A B -> A
fst10 (a , _) = a

snd10 : {A : Set10}{B : A -> Set10} (p : Sigma10 A B) -> B (fst10 p)
snd10 (a , b) = b

data Zero10 : Set10 where

data Unit10 : Set10 where
    Void : Unit10

data Sigma11 (A : Set11) (B : A -> Set11) : Set11 where
    _,_ : (x : A) (y : B x) -> Sigma11 A B

_*11_ : (A : Set11)(B : Set11) -> Set11
A *11 B = Sigma11 A \_ -> B

fst11 : {A : Set11}{B : A -> Set11} -> Sigma11 A B -> A
fst11 (a , _) = a

snd11 : {A : Set11}{B : A -> Set11} (p : Sigma11 A B) -> B (fst11 p)
snd11 (a , b) = b

data Zero11 : Set11 where

data Unit11 : Set11 where
    Void : Unit11

data Sigma12 (A : Set12) (B : A -> Set12) : Set12 where
    _,_ : (x : A) (y : B x) -> Sigma12 A B

_*12_ : (A : Set12)(B : Set12) -> Set12
A *12 B = Sigma12 A \_ -> B

fst12 : {A : Set12}{B : A -> Set12} -> Sigma12 A B -> A
fst12 (a , _) = a

snd12 : {A : Set12}{B : A -> Set12} (p : Sigma12 A B) -> B (fst12 p)
snd12 (a , b) = b

data Zero12 : Set12 where

data Unit12 : Set12 where
    Void : Unit12

data Sigma13 (A : Set13) (B : A -> Set13) : Set13 where
    _,_ : (x : A) (y : B x) -> Sigma13 A B

_*13_ : (A : Set13)(B : Set13) -> Set13
A *13 B = Sigma13 A \_ -> B

fst13 : {A : Set13}{B : A -> Set13} -> Sigma13 A B -> A
fst13 (a , _) = a

snd13 : {A : Set13}{B : A -> Set13} (p : Sigma13 A B) -> B (fst13 p)
snd13 (a , b) = b

data Zero13 : Set13 where

data Unit13 : Set13 where
    Void : Unit13

data Sigma14 (A : Set14) (B : A -> Set14) : Set14 where
    _,_ : (x : A) (y : B x) -> Sigma14 A B

_*14_ : (A : Set14)(B : Set14) -> Set14
A *14 B = Sigma14 A \_ -> B

fst14 : {A : Set14}{B : A -> Set14} -> Sigma14 A B -> A
fst14 (a , _) = a

snd14 : {A : Set14}{B : A -> Set14} (p : Sigma14 A B) -> B (fst14 p)
snd14 (a , b) = b

data Zero14 : Set14 where

data Unit14 : Set14 where
    Void : Unit14

data Sigma15 (A : Set15) (B : A -> Set15) : Set15 where
    _,_ : (x : A) (y : B x) -> Sigma15 A B

_*15_ : (A : Set15)(B : Set15) -> Set15
A *15 B = Sigma15 A \_ -> B

fst15 : {A : Set15}{B : A -> Set15} -> Sigma15 A B -> A
fst15 (a , _) = a

snd15 : {A : Set15}{B : A -> Set15} (p : Sigma15 A B) -> B (fst15 p)
snd15 (a , b) = b

data Zero15 : Set15 where

data Unit15 : Set15 where
    Void : Unit15

data Sigma16 (A : Set16) (B : A -> Set16) : Set16 where
    _,_ : (x : A) (y : B x) -> Sigma16 A B

_*16_ : (A : Set16)(B : Set16) -> Set16
A *16 B = Sigma16 A \_ -> B

fst16 : {A : Set16}{B : A -> Set16} -> Sigma16 A B -> A
fst16 (a , _) = a

snd16 : {A : Set16}{B : A -> Set16} (p : Sigma16 A B) -> B (fst16 p)
snd16 (a , b) = b

data Zero16 : Set16 where

data Unit16 : Set16 where
    Void : Unit16

data Sigma17 (A : Set17) (B : A -> Set17) : Set17 where
    _,_ : (x : A) (y : B x) -> Sigma17 A B

_*17_ : (A : Set17)(B : Set17) -> Set17
A *17 B = Sigma17 A \_ -> B

fst17 : {A : Set17}{B : A -> Set17} -> Sigma17 A B -> A
fst17 (a , _) = a

snd17 : {A : Set17}{B : A -> Set17} (p : Sigma17 A B) -> B (fst17 p)
snd17 (a , b) = b

data Zero17 : Set17 where

data Unit17 : Set17 where
    Void : Unit17

data Sigma18 (A : Set18) (B : A -> Set18) : Set18 where
    _,_ : (x : A) (y : B x) -> Sigma18 A B

_*18_ : (A : Set18)(B : Set18) -> Set18
A *18 B = Sigma18 A \_ -> B

fst18 : {A : Set18}{B : A -> Set18} -> Sigma18 A B -> A
fst18 (a , _) = a

snd18 : {A : Set18}{B : A -> Set18} (p : Sigma18 A B) -> B (fst18 p)
snd18 (a , b) = b

data Zero18 : Set18 where

data Unit18 : Set18 where
    Void : Unit18

data Sigma19 (A : Set19) (B : A -> Set19) : Set19 where
    _,_ : (x : A) (y : B x) -> Sigma19 A B

_*19_ : (A : Set19)(B : Set19) -> Set19
A *19 B = Sigma19 A \_ -> B

fst19 : {A : Set19}{B : A -> Set19} -> Sigma19 A B -> A
fst19 (a , _) = a

snd19 : {A : Set19}{B : A -> Set19} (p : Sigma19 A B) -> B (fst19 p)
snd19 (a , b) = b

data Zero19 : Set19 where

data Unit19 : Set19 where
    Void : Unit19

data Sigma20 (A : Set20) (B : A -> Set20) : Set20 where
    _,_ : (x : A) (y : B x) -> Sigma20 A B

_*20_ : (A : Set20)(B : Set20) -> Set20
A *20 B = Sigma20 A \_ -> B

fst20 : {A : Set20}{B : A -> Set20} -> Sigma20 A B -> A
fst20 (a , _) = a

snd20 : {A : Set20}{B : A -> Set20} (p : Sigma20 A B) -> B (fst20 p)
snd20 (a , b) = b

data Zero20 : Set20 where

data Unit20 : Set20 where
    Void : Unit20

data Sigma21 (A : Set21) (B : A -> Set21) : Set21 where
    _,_ : (x : A) (y : B x) -> Sigma21 A B

_*21_ : (A : Set21)(B : Set21) -> Set21
A *21 B = Sigma21 A \_ -> B

fst21 : {A : Set21}{B : A -> Set21} -> Sigma21 A B -> A
fst21 (a , _) = a

snd21 : {A : Set21}{B : A -> Set21} (p : Sigma21 A B) -> B (fst21 p)
snd21 (a , b) = b

data Zero21 : Set21 where

data Unit21 : Set21 where
    Void : Unit21

data Sigma22 (A : Set22) (B : A -> Set22) : Set22 where
    _,_ : (x : A) (y : B x) -> Sigma22 A B

_*22_ : (A : Set22)(B : Set22) -> Set22
A *22 B = Sigma22 A \_ -> B

fst22 : {A : Set22}{B : A -> Set22} -> Sigma22 A B -> A
fst22 (a , _) = a

snd22 : {A : Set22}{B : A -> Set22} (p : Sigma22 A B) -> B (fst22 p)
snd22 (a , b) = b

data Zero22 : Set22 where

data Unit22 : Set22 where
    Void : Unit22

data Sigma23 (A : Set23) (B : A -> Set23) : Set23 where
    _,_ : (x : A) (y : B x) -> Sigma23 A B

_*23_ : (A : Set23)(B : Set23) -> Set23
A *23 B = Sigma23 A \_ -> B

fst23 : {A : Set23}{B : A -> Set23} -> Sigma23 A B -> A
fst23 (a , _) = a

snd23 : {A : Set23}{B : A -> Set23} (p : Sigma23 A B) -> B (fst23 p)
snd23 (a , b) = b

data Zero23 : Set23 where

data Unit23 : Set23 where
    Void : Unit23

data Sigma24 (A : Set24) (B : A -> Set24) : Set24 where
    _,_ : (x : A) (y : B x) -> Sigma24 A B

_*24_ : (A : Set24)(B : Set24) -> Set24
A *24 B = Sigma24 A \_ -> B

fst24 : {A : Set24}{B : A -> Set24} -> Sigma24 A B -> A
fst24 (a , _) = a

snd24 : {A : Set24}{B : A -> Set24} (p : Sigma24 A B) -> B (fst24 p)
snd24 (a , b) = b

data Zero24 : Set24 where

data Unit24 : Set24 where
    Void : Unit24

data Sigma25 (A : Set25) (B : A -> Set25) : Set25 where
    _,_ : (x : A) (y : B x) -> Sigma25 A B

_*25_ : (A : Set25)(B : Set25) -> Set25
A *25 B = Sigma25 A \_ -> B

fst25 : {A : Set25}{B : A -> Set25} -> Sigma25 A B -> A
fst25 (a , _) = a

snd25 : {A : Set25}{B : A -> Set25} (p : Sigma25 A B) -> B (fst25 p)
snd25 (a , b) = b

data Zero25 : Set25 where

data Unit25 : Set25 where
    Void : Unit25

data Sigma26 (A : Set26) (B : A -> Set26) : Set26 where
    _,_ : (x : A) (y : B x) -> Sigma26 A B

_*26_ : (A : Set26)(B : Set26) -> Set26
A *26 B = Sigma26 A \_ -> B

fst26 : {A : Set26}{B : A -> Set26} -> Sigma26 A B -> A
fst26 (a , _) = a

snd26 : {A : Set26}{B : A -> Set26} (p : Sigma26 A B) -> B (fst26 p)
snd26 (a , b) = b

data Zero26 : Set26 where

data Unit26 : Set26 where
    Void : Unit26

data Sigma27 (A : Set27) (B : A -> Set27) : Set27 where
    _,_ : (x : A) (y : B x) -> Sigma27 A B

_*27_ : (A : Set27)(B : Set27) -> Set27
A *27 B = Sigma27 A \_ -> B

fst27 : {A : Set27}{B : A -> Set27} -> Sigma27 A B -> A
fst27 (a , _) = a

snd27 : {A : Set27}{B : A -> Set27} (p : Sigma27 A B) -> B (fst27 p)
snd27 (a , b) = b

data Zero27 : Set27 where

data Unit27 : Set27 where
    Void : Unit27

data Sigma28 (A : Set28) (B : A -> Set28) : Set28 where
    _,_ : (x : A) (y : B x) -> Sigma28 A B

_*28_ : (A : Set28)(B : Set28) -> Set28
A *28 B = Sigma28 A \_ -> B

fst28 : {A : Set28}{B : A -> Set28} -> Sigma28 A B -> A
fst28 (a , _) = a

snd28 : {A : Set28}{B : A -> Set28} (p : Sigma28 A B) -> B (fst28 p)
snd28 (a , b) = b

data Zero28 : Set28 where

data Unit28 : Set28 where
    Void : Unit28

data Sigma29 (A : Set29) (B : A -> Set29) : Set29 where
    _,_ : (x : A) (y : B x) -> Sigma29 A B

_*29_ : (A : Set29)(B : Set29) -> Set29
A *29 B = Sigma29 A \_ -> B

fst29 : {A : Set29}{B : A -> Set29} -> Sigma29 A B -> A
fst29 (a , _) = a

snd29 : {A : Set29}{B : A -> Set29} (p : Sigma29 A B) -> B (fst29 p)
snd29 (a , b) = b

data Zero29 : Set29 where

data Unit29 : Set29 where
    Void : Unit29

data Sigma30 (A : Set30) (B : A -> Set30) : Set30 where
    _,_ : (x : A) (y : B x) -> Sigma30 A B

_*30_ : (A : Set30)(B : Set30) -> Set30
A *30 B = Sigma30 A \_ -> B

fst30 : {A : Set30}{B : A -> Set30} -> Sigma30 A B -> A
fst30 (a , _) = a

snd30 : {A : Set30}{B : A -> Set30} (p : Sigma30 A B) -> B (fst30 p)
snd30 (a , b) = b

data Zero30 : Set30 where

data Unit30 : Set30 where
    Void : Unit30

data Sigma31 (A : Set31) (B : A -> Set31) : Set31 where
    _,_ : (x : A) (y : B x) -> Sigma31 A B

_*31_ : (A : Set31)(B : Set31) -> Set31
A *31 B = Sigma31 A \_ -> B

fst31 : {A : Set31}{B : A -> Set31} -> Sigma31 A B -> A
fst31 (a , _) = a

snd31 : {A : Set31}{B : A -> Set31} (p : Sigma31 A B) -> B (fst31 p)
snd31 (a , b) = b

data Zero31 : Set31 where

data Unit31 : Set31 where
    Void : Unit31

data Sigma32 (A : Set32) (B : A -> Set32) : Set32 where
    _,_ : (x : A) (y : B x) -> Sigma32 A B

_*32_ : (A : Set32)(B : Set32) -> Set32
A *32 B = Sigma32 A \_ -> B

fst32 : {A : Set32}{B : A -> Set32} -> Sigma32 A B -> A
fst32 (a , _) = a

snd32 : {A : Set32}{B : A -> Set32} (p : Sigma32 A B) -> B (fst32 p)
snd32 (a , b) = b

data Zero32 : Set32 where

data Unit32 : Set32 where
    Void : Unit32

data Sigma33 (A : Set33) (B : A -> Set33) : Set33 where
    _,_ : (x : A) (y : B x) -> Sigma33 A B

_*33_ : (A : Set33)(B : Set33) -> Set33
A *33 B = Sigma33 A \_ -> B

fst33 : {A : Set33}{B : A -> Set33} -> Sigma33 A B -> A
fst33 (a , _) = a

snd33 : {A : Set33}{B : A -> Set33} (p : Sigma33 A B) -> B (fst33 p)
snd33 (a , b) = b

data Zero33 : Set33 where

data Unit33 : Set33 where
    Void : Unit33

data Sigma34 (A : Set34) (B : A -> Set34) : Set34 where
    _,_ : (x : A) (y : B x) -> Sigma34 A B

_*34_ : (A : Set34)(B : Set34) -> Set34
A *34 B = Sigma34 A \_ -> B

fst34 : {A : Set34}{B : A -> Set34} -> Sigma34 A B -> A
fst34 (a , _) = a

snd34 : {A : Set34}{B : A -> Set34} (p : Sigma34 A B) -> B (fst34 p)
snd34 (a , b) = b

data Zero34 : Set34 where

data Unit34 : Set34 where
    Void : Unit34

data Sigma35 (A : Set35) (B : A -> Set35) : Set35 where
    _,_ : (x : A) (y : B x) -> Sigma35 A B

_*35_ : (A : Set35)(B : Set35) -> Set35
A *35 B = Sigma35 A \_ -> B

fst35 : {A : Set35}{B : A -> Set35} -> Sigma35 A B -> A
fst35 (a , _) = a

snd35 : {A : Set35}{B : A -> Set35} (p : Sigma35 A B) -> B (fst35 p)
snd35 (a , b) = b

data Zero35 : Set35 where

data Unit35 : Set35 where
    Void : Unit35

data Sigma36 (A : Set36) (B : A -> Set36) : Set36 where
    _,_ : (x : A) (y : B x) -> Sigma36 A B

_*36_ : (A : Set36)(B : Set36) -> Set36
A *36 B = Sigma36 A \_ -> B

fst36 : {A : Set36}{B : A -> Set36} -> Sigma36 A B -> A
fst36 (a , _) = a

snd36 : {A : Set36}{B : A -> Set36} (p : Sigma36 A B) -> B (fst36 p)
snd36 (a , b) = b

data Zero36 : Set36 where

data Unit36 : Set36 where
    Void : Unit36

data Sigma37 (A : Set37) (B : A -> Set37) : Set37 where
    _,_ : (x : A) (y : B x) -> Sigma37 A B

_*37_ : (A : Set37)(B : Set37) -> Set37
A *37 B = Sigma37 A \_ -> B

fst37 : {A : Set37}{B : A -> Set37} -> Sigma37 A B -> A
fst37 (a , _) = a

snd37 : {A : Set37}{B : A -> Set37} (p : Sigma37 A B) -> B (fst37 p)
snd37 (a , b) = b

data Zero37 : Set37 where

data Unit37 : Set37 where
    Void : Unit37

data Sigma38 (A : Set38) (B : A -> Set38) : Set38 where
    _,_ : (x : A) (y : B x) -> Sigma38 A B

_*38_ : (A : Set38)(B : Set38) -> Set38
A *38 B = Sigma38 A \_ -> B

fst38 : {A : Set38}{B : A -> Set38} -> Sigma38 A B -> A
fst38 (a , _) = a

snd38 : {A : Set38}{B : A -> Set38} (p : Sigma38 A B) -> B (fst38 p)
snd38 (a , b) = b

data Zero38 : Set38 where

data Unit38 : Set38 where
    Void : Unit38

data Sigma39 (A : Set39) (B : A -> Set39) : Set39 where
    _,_ : (x : A) (y : B x) -> Sigma39 A B

_*39_ : (A : Set39)(B : Set39) -> Set39
A *39 B = Sigma39 A \_ -> B

fst39 : {A : Set39}{B : A -> Set39} -> Sigma39 A B -> A
fst39 (a , _) = a

snd39 : {A : Set39}{B : A -> Set39} (p : Sigma39 A B) -> B (fst39 p)
snd39 (a , b) = b

data Zero39 : Set39 where

data Unit39 : Set39 where
    Void : Unit39

data Sigma40 (A : Set40) (B : A -> Set40) : Set40 where
    _,_ : (x : A) (y : B x) -> Sigma40 A B

_*40_ : (A : Set40)(B : Set40) -> Set40
A *40 B = Sigma40 A \_ -> B

fst40 : {A : Set40}{B : A -> Set40} -> Sigma40 A B -> A
fst40 (a , _) = a

snd40 : {A : Set40}{B : A -> Set40} (p : Sigma40 A B) -> B (fst40 p)
snd40 (a , b) = b

data Zero40 : Set40 where

data Unit40 : Set40 where
    Void : Unit40

data Sigma41 (A : Set41) (B : A -> Set41) : Set41 where
    _,_ : (x : A) (y : B x) -> Sigma41 A B

_*41_ : (A : Set41)(B : Set41) -> Set41
A *41 B = Sigma41 A \_ -> B

fst41 : {A : Set41}{B : A -> Set41} -> Sigma41 A B -> A
fst41 (a , _) = a

snd41 : {A : Set41}{B : A -> Set41} (p : Sigma41 A B) -> B (fst41 p)
snd41 (a , b) = b

data Zero41 : Set41 where

data Unit41 : Set41 where
    Void : Unit41

data Sigma42 (A : Set42) (B : A -> Set42) : Set42 where
    _,_ : (x : A) (y : B x) -> Sigma42 A B

_*42_ : (A : Set42)(B : Set42) -> Set42
A *42 B = Sigma42 A \_ -> B

fst42 : {A : Set42}{B : A -> Set42} -> Sigma42 A B -> A
fst42 (a , _) = a

snd42 : {A : Set42}{B : A -> Set42} (p : Sigma42 A B) -> B (fst42 p)
snd42 (a , b) = b

data Zero42 : Set42 where

data Unit42 : Set42 where
    Void : Unit42

max_stars_repo_name: mietek/epigram

max_issues_repo_name: mietek/epigram

max_forks_repo_name: mietek/epigram