text:
{-

The module CanThetaContinuation contains the continuation-passing
variant of Canθ, which is used as a tool to simplify Canθ-Can
expressions.

The lemmas are mainly about the function Canθ' defined by the equation

    unfold : ∀ sigs S'' p θ →
         Canθ sigs S'' p θ ≡ Canθ' sigs S'' (Can p) θ

The main property proved here is that the search function
Canθ is distributive over the environment:

    canθ'-←-distribute : ∀ sigs sigs' S'' r θ →
      Canθ (SigMap.union sigs sigs') S'' r θ ≡
      Canθ' sigs S'' (Canθ sigs' S'' r) θ

Other properties about how the search is performed are:

    canθ'-inner-shadowing-irr : ∀ sigs S'' sigs' p S status θ →
      S ∈ SigMap.keys sigs' →
        Canθ' sigs S'' (Canθ sigs' 0 p) (θ ← [ (S ₛ) ↦ status ]) ≡
        Canθ' sigs S'' (Canθ sigs' 0 p) θ

    canθ'-search-acc : ∀ sigs S κ θ →
      ∀ S'' status →
        S'' ∉ map (_+_ S)  (SigMap.keys sigs) →
        Canθ' sigs S  κ  (θ ← [ (S'' ₛ) ↦ status ]) ≡
        Canθ' sigs S (κ ∘ (_← [ (S'' ₛ) ↦ status ])) θ

-}
module Esterel.Lang.CanFunction.CanThetaContinuation where

open import utility

open import utility
  renaming (_U̬_ to _∪_ ; _|̌_ to _-_)

open import Esterel.Lang
open import Esterel.Lang.Binding
open import Esterel.Lang.CanFunction
open import Esterel.Lang.CanFunction.Base
open import Esterel.Context
  using (EvaluationContext1 ; EvaluationContext ; _⟦_⟧e ; _≐_⟦_⟧e)
open import Esterel.Context.Properties
  using (plug ; unplug)
open import Esterel.Environment as Env
  using (Env ; Θ ; _←_ ; Dom ; module SigMap ; module ShrMap ; module VarMap)
open import Esterel.CompletionCode as Code
  using () renaming (CompletionCode to Code)
open import Esterel.Variable.Signal as Signal
  using (Signal ; _ₛ)
open import Esterel.Variable.Shared as SharedVar
  using (SharedVar ; _ₛₕ)
open import Esterel.Variable.Sequential as SeqVar
  using (SeqVar)

open EvaluationContext1
open _≐_⟦_⟧e

open import Data.Bool
  using (Bool ; not ; if_then_else_)
open import Data.Empty
  using (⊥ ; ⊥-elim)
open import Data.List
  using (List ; [] ; _∷_ ; _++_ ; map ; concatMap ; foldr)
open import Data.List.Properties
  using (map-id)
open import Data.List.Any
  using (Any ; any ; here ; there)
open import Data.List.Any.Properties
  using ()
  renaming (++⁺ˡ to ++ˡ ; ++⁺ʳ to ++ʳ)
open import Data.Maybe
  using (Maybe ; maybe ; just ; nothing)
open import Data.Nat
  using (ℕ ; zero ; suc ; _≟_ ; _+_)
open import Data.Nat.Properties.Simple
  using (+-comm)
open import Data.Product
  using (Σ ; proj₁ ; proj₂ ; ∃ ; _,_ ; _,′_ ; _×_)
open import Data.Sum
  using (_⊎_ ; inj₁ ; inj₂)
open import Function
  using (_∘_ ; id ; _∋_)
open import Relation.Nullary
  using (¬_ ; Dec ; yes ; no)
open import Relation.Nullary.Decidable
  using (⌊_⌋)
open import Relation.Binary.PropositionalEquality
  using (_≡_ ; _≢_ ; refl ; trans ; sym ; cong ; subst ; module ≡-Reasoning)

open ListSet Data.Nat._≟_
  using (set-subtract ; set-subtract-[] ; set-subtract-split ; set-subtract-merge
       ; set-subtract-notin
       ; set-remove ; set-remove-mono-∈ ; set-remove-removed ; set-remove-not-removed
       ; set-subtract-[a]≡set-remove)

open import Data.OrderedListMap Signal Signal.unwrap Signal.Status as SigM
open import Data.OrderedListMap SharedVar SharedVar.unwrap (Σ SharedVar.Status (λ _ → ℕ)) as ShrM
open import Data.OrderedListMap SeqVar SeqVar.unwrap ℕ as SeqM

open ≡-Reasoning

-- equation: Canθ sig S'' p θ = Canθ' sig S'' (Can p) θ
Canθ'   : SigMap.Map Signal.Status → ℕ →
  (Env → SigSet.ST × CodeSet.ST × ShrSet.ST) →
  Env → SigSet.ST × CodeSet.ST × ShrSet.ST
Canθ' [] S κ θ = κ θ
Canθ' (nothing             ∷ sig') S κ θ = Canθ' sig' (suc S) κ θ
Canθ' (just Signal.present ∷ sig') S κ θ = Canθ' sig' (suc S) κ (θ ← [S]-env-present (S ₛ))
Canθ' (just Signal.absent  ∷ sig') S κ θ = Canθ' sig' (suc S) κ (θ ← [S]-env-absent (S ₛ))
Canθ' (just Signal.unknown ∷ sig') S κ θ with
  any (_≟_ S) (proj₁ (Canθ' sig' (suc S) κ (θ ← [S]-env (S ₛ))))
... | yes S∈can-p-θ←[S] = Canθ' sig' (suc S) κ (θ ← [S]-env (S ₛ))
... | no  S∉can-p-θ←[S] = Canθ' sig' (suc S) κ (θ ← [S]-env-absent (S ₛ))

unfold : ∀ sigs S'' p θ → Canθ sigs S'' p θ ≡ Canθ' sigs S'' (Can p) θ
unfold [] S'' p θ = refl
unfold (nothing ∷ sigs) S'' p θ = unfold sigs (suc S'') p θ
unfold (just Signal.present ∷ sigs) S'' p θ =
  unfold sigs (suc S'') p (θ ← [S]-env-present (S'' ₛ))
unfold (just Signal.absent ∷ sigs) S'' p θ =
  unfold sigs (suc S'') p (θ ← [S]-env-absent (S'' ₛ))
unfold (just Signal.unknown ∷ sigs) S'' p θ
  with any (_≟_ S'') (proj₁ (Canθ  sigs (suc S'') p       (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Can p) (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ-sigs-θ←[S''] | yes S''∈canθ'-sigs-θ←[S''] =
  unfold sigs (suc S'') p (θ ← [S]-env (S'' ₛ))
... | no  S''∉canθ-sigs-θ←[S''] | no  S''∉canθ'-sigs-θ←[S''] =
  unfold sigs (suc S'') p (θ ← [S]-env-absent (S'' ₛ))
... | yes S''∈canθ-sigs-θ←[S''] | no  S''∉canθ'-sigs-θ←[S'']
  rewrite unfold sigs (suc S'') p (θ ← [S]-env (S'' ₛ))
  = ⊥-elim (S''∉canθ'-sigs-θ←[S''] S''∈canθ-sigs-θ←[S''])
... | no  S''∉canθ-sigs-θ←[S''] | yes S''∈canθ'-sigs-θ←[S'']
  rewrite unfold sigs (suc S'') p (θ ← [S]-env (S'' ₛ))
  = ⊥-elim (S''∉canθ-sigs-θ←[S''] S''∈canθ'-sigs-θ←[S''])

canθ'-cong : ∀ sigs S'' κ κ' θ →
  (∀ θ* → κ θ* ≡ κ' θ*) →
  Canθ' sigs S'' κ θ ≡ Canθ' sigs S'' κ' θ
canθ'-cong [] S'' κ κ' θ κ≗κ' = κ≗κ' θ
canθ'-cong (nothing ∷ sigs) S'' κ κ' θ κ≗κ' =
  canθ'-cong sigs (suc S'') κ κ' θ κ≗κ'
canθ'-cong (just Signal.present ∷ sigs) S'' κ κ' θ κ≗κ' =
  canθ'-cong sigs (suc S'') κ κ' (θ ← [S]-env-present (S'' ₛ)) κ≗κ'
canθ'-cong (just Signal.absent ∷ sigs) S'' κ κ' θ κ≗κ' =
  canθ'-cong sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ)) κ≗κ'
canθ'-cong (just Signal.unknown ∷ sigs) S'' κ κ' θ κ≗κ'
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ  (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ' (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-κ-θ←[S''] | yes S''∈canθ'-sigs-κ'-θ←[S''] =
  canθ'-cong sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ≗κ'
... | no  S''∉canθ'-sigs-κ-θ←[S''] | no  S''∉canθ'-sigs-κ'-θ←[S''] =
  canθ'-cong sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ)) κ≗κ'
... | yes S''∈canθ'-sigs-κ-θ←[S''] | no  S''∉canθ'-sigs-κ'-θ←[S'']
  rewrite canθ'-cong sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ≗κ'
  = ⊥-elim (S''∉canθ'-sigs-κ'-θ←[S''] S''∈canθ'-sigs-κ-θ←[S''])
... | no  S''∉canθ'-sigs-κ-θ←[S''] | yes S''∈canθ'-sigs-κ'-θ←[S'']
  rewrite canθ'-cong sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ≗κ'
  = ⊥-elim (S''∉canθ'-sigs-κ-θ←[S''] S''∈canθ'-sigs-κ'-θ←[S''])

canθₛ'-cong : ∀ sigs S'' κ κ' θ →
  (∀ θ* → proj₁ (κ θ*) ≡ proj₁ (κ' θ*)) →
  proj₁ (Canθ' sigs S'' κ θ) ≡ proj₁ (Canθ' sigs S'' κ' θ)
canθₛ'-cong [] S'' κ κ' θ κ≗κ' = κ≗κ' θ
canθₛ'-cong (nothing ∷ sigs) S'' κ κ' θ κ≗κ' =
  canθₛ'-cong sigs (suc S'') κ κ' θ κ≗κ'
canθₛ'-cong (just Signal.present ∷ sigs) S'' κ κ' θ κ≗κ' =
  canθₛ'-cong sigs (suc S'') κ κ' (θ ← [S]-env-present (S'' ₛ)) κ≗κ'
canθₛ'-cong (just Signal.absent ∷ sigs) S'' κ κ' θ κ≗κ' =
  canθₛ'-cong sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ)) κ≗κ'
canθₛ'-cong (just Signal.unknown ∷ sigs) S'' κ κ' θ κ≗κ'
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ  (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ' (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-κ-θ←[S''] | yes S''∈canθ'-sigs-κ'-θ←[S''] =
  canθₛ'-cong sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ≗κ'
... | no  S''∉canθ'-sigs-κ-θ←[S''] | no  S''∉canθ'-sigs-κ'-θ←[S''] =
  canθₛ'-cong sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ)) κ≗κ'
... | yes S''∈canθ'-sigs-κ-θ←[S''] | no  S''∉canθ'-sigs-κ'-θ←[S'']
  rewrite canθₛ'-cong sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ≗κ'
  = ⊥-elim (S''∉canθ'-sigs-κ'-θ←[S''] S''∈canθ'-sigs-κ-θ←[S''])
... | no  S''∉canθ'-sigs-κ-θ←[S''] | yes S''∈canθ'-sigs-κ'-θ←[S'']
  rewrite canθₛ'-cong sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ≗κ'
  = ⊥-elim (S''∉canθ'-sigs-κ-θ←[S''] S''∈canθ'-sigs-κ'-θ←[S''])

canθ'-map-comm : ∀ f sigs S κ θ →
  Canθ' sigs S (map-second f ∘ κ) θ ≡ map-second f (Canθ' sigs S κ θ)
canθ'-map-comm f [] S κ θ = refl
canθ'-map-comm f (nothing ∷ sigs) S κ θ =
  canθ'-map-comm f sigs (suc S) κ θ
canθ'-map-comm f (just Signal.present ∷ sigs) S κ θ =
  canθ'-map-comm f sigs (suc S) κ (θ ← [S]-env-present (S ₛ))
canθ'-map-comm f (just Signal.absent ∷ sigs) S κ θ =
  canθ'-map-comm f sigs (suc S) κ (θ ← [S]-env-absent (S ₛ))
canθ'-map-comm f (just Signal.unknown ∷ sigs) S κ θ
  with any (_≟_ S) (proj₁ (Canθ' sigs (suc S) (map-second f ∘ κ) (θ ← [S]-env (S ₛ))))
     | any (_≟_ S) (proj₁ (Canθ' sigs (suc S) κ (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-f∘κ-θ←[S] | yes S∈canθ'-sigs-κ-θ←[S] =
  canθ'-map-comm f sigs (suc S) κ (θ ← [S]-env (S ₛ))
... | no  S∉canθ'-sigs-f∘κ-θ←[S] | no  S∉canθ'-sigs-κ-θ←[S] =
  canθ'-map-comm f sigs (suc S) κ (θ ← [S]-env-absent (S ₛ))
... | yes S∈canθ'-sigs-f∘κ-θ←[S] | no  S∉canθ'-sigs-κ-θ←[S]
  rewrite canθ'-map-comm f sigs (suc S) κ (θ ← [S]-env (S ₛ))
  = ⊥-elim (S∉canθ'-sigs-κ-θ←[S] S∈canθ'-sigs-f∘κ-θ←[S])
... | no  S∉canθ'-sigs-f∘κ-θ←[S] | yes S∈canθ'-sigs-κ-θ←[S]
  rewrite canθ'-map-comm f sigs (suc S) κ (θ ← [S]-env (S ₛ))
  = ⊥-elim (S∉canθ'-sigs-f∘κ-θ←[S] S∈canθ'-sigs-κ-θ←[S])

canθ'ₛ-add-sig-monotonic : ∀ sigs S'' κ θ S status →
  (∀ θ S status S' →
    S' ∈ proj₁ (κ (θ ← Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty)) →
    S' ∈ proj₁ (κ (θ ← [S]-env S))) →
  ∀ S' →
    S' ∈ proj₁ (Canθ' sigs S'' κ (θ ← Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty)) →
    S' ∈ proj₁ (Canθ' sigs S'' κ (θ ← [S]-env S))
canθ'ₛ-add-sig-monotonic [] S'' κ θ S status κ-add-sig-monotonic
  S' S'∈canθ'-sigs-p-θ←[S↦status] =
  κ-add-sig-monotonic θ S status S' S'∈canθ'-sigs-p-θ←[S↦status]
canθ'ₛ-add-sig-monotonic (nothing ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] =
  canθ'ₛ-add-sig-monotonic sigs (suc S'') κ θ S status
    κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status]
canθ'ₛ-add-sig-monotonic (just x ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] with Signal.unwrap S ≟ S''
canθ'ₛ-add-sig-monotonic (just Signal.present ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] | yes refl
  rewrite Env.sig-single-←-←-overwrite θ (S'' ₛ) Signal.unknown Signal.present
        | Env.sig-single-←-←-overwrite θ (S'' ₛ) status         Signal.present
  = S'∈canθ'-sigs-p-θ←[S↦status]
canθ'ₛ-add-sig-monotonic (just Signal.absent ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] | yes refl
  rewrite Env.sig-single-←-←-overwrite θ (S'' ₛ) Signal.unknown Signal.absent
        | Env.sig-single-←-←-overwrite θ (S'' ₛ) status         Signal.absent
  = S'∈canθ'-sigs-p-θ←[S↦status]
canθ'ₛ-add-sig-monotonic (just Signal.unknown ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] | yes refl
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ ((θ ← [S]-env (S'' ₛ)) ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ ((θ ← [ (S'' ₛ) ↦ status ]) ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-κ-θ←[S''↦unknown]←[S''] | yes S''∈canθ'-sigs-κ-θ←[S''↦status]←[S'']
  rewrite Env.sig-single-←-←-overwrite θ (S'' ₛ) Signal.unknown Signal.unknown
        | Env.sig-single-←-←-overwrite θ (S'' ₛ) status         Signal.unknown
  = S'∈canθ'-sigs-p-θ←[S↦status]
... | no  S''∉canθ'-sigs-κ-θ←[S''↦unknown]←[S''] | no  S''∉canθ'-sigs-κ-θ←[S''↦status]←[S'']
  rewrite Env.sig-single-←-←-overwrite θ (S'' ₛ) Signal.unknown Signal.absent
        | Env.sig-single-←-←-overwrite θ (S'' ₛ) status         Signal.absent
  = S'∈canθ'-sigs-p-θ←[S↦status]
... | yes S''∈canθ'-sigs-κ-θ←[S''↦unknown]←[S''] | no  S''∉canθ'-sigs-κ-θ←[S''↦status]←[S'']
  rewrite Env.sig-single-←-←-overwrite θ (S'' ₛ) Signal.unknown Signal.unknown
        | Env.sig-single-←-←-overwrite θ (S'' ₛ) status         Signal.unknown
  = ⊥-elim (S''∉canθ'-sigs-κ-θ←[S''↦status]←[S'']
              S''∈canθ'-sigs-κ-θ←[S''↦unknown]←[S''])
... | no  S''∉canθ'-sigs-κ-θ←[S''↦unknown]←[S''] | yes S''∈canθ'-sigs-κ-θ←[S''↦status]←[S'']
  rewrite Env.sig-single-←-←-overwrite θ (S'' ₛ) Signal.unknown Signal.unknown
        | Env.sig-single-←-←-overwrite θ (S'' ₛ) status         Signal.unknown
  = ⊥-elim (S''∉canθ'-sigs-κ-θ←[S''↦unknown]←[S'']
              S''∈canθ'-sigs-κ-θ←[S''↦status]←[S''])
canθ'ₛ-add-sig-monotonic (just Signal.present ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] | no S≢S''
  rewrite Env.←-assoc-comm θ ([S]-env S) ([S]-env-present (S'' ₛ))
            (Env.sig-single-noteq-distinct S Signal.unknown
              (S'' ₛ) Signal.present S≢S'')
  = canθ'ₛ-add-sig-monotonic sigs (suc S'') κ
      (θ ← [S]-env-present (S'' ₛ)) S status κ-add-sig-monotonic S'
      (subst (S' ∈_)
        (cong (proj₁ ∘ Canθ' sigs (suc S'') κ)
          (Env.←-assoc-comm θ [ S ↦ status ] ([S]-env-present (S'' ₛ))
              (Env.sig-single-noteq-distinct S status
                (S'' ₛ) Signal.present S≢S'')))
        S'∈canθ'-sigs-p-θ←[S↦status])
canθ'ₛ-add-sig-monotonic (just Signal.absent ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] | no S≢S''
  rewrite Env.←-assoc-comm θ ([S]-env S) ([S]-env-absent (S'' ₛ))
            (Env.sig-single-noteq-distinct S Signal.unknown
              (S'' ₛ) Signal.absent S≢S'')
  = canθ'ₛ-add-sig-monotonic sigs (suc S'') κ
      (θ ← [S]-env-absent (S'' ₛ)) S status κ-add-sig-monotonic S'
      (subst (S' ∈_)
        (cong (proj₁ ∘ Canθ' sigs (suc S'') κ)
          (Env.←-assoc-comm θ [ S ↦ status ] ([S]-env-absent (S'' ₛ))
              (Env.sig-single-noteq-distinct S status
                (S'' ₛ) Signal.absent S≢S'')))
        S'∈canθ'-sigs-p-θ←[S↦status])
canθ'ₛ-add-sig-monotonic (just Signal.unknown ∷ sigs) S'' κ θ S status
  κ-add-sig-monotonic S' S'∈canθ'-sigs-p-θ←[S↦status] | no S≢S''
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ ((θ ← [S]-env S) ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ ((θ ← [ S ↦ status ]) ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-κ-θ←[S↦unknown]←[S''] | yes S''∈canθ'-sigs-κ-θ←[S↦status]←[S'']
  rewrite Env.←-assoc-comm θ ([S]-env S) ([S]-env (S'' ₛ))
            (Env.sig-single-noteq-distinct S Signal.unknown
              (S'' ₛ) Signal.unknown S≢S'')
  = canθ'ₛ-add-sig-monotonic sigs (suc S'') κ
      (θ ← [S]-env (S'' ₛ)) S status κ-add-sig-monotonic S'
      (subst (S' ∈_)
        (cong (proj₁ ∘ Canθ' sigs (suc S'') κ)
          (Env.←-assoc-comm θ [ S ↦ status ] ([S]-env (S'' ₛ))
              (Env.sig-single-noteq-distinct S status
                (S'' ₛ) Signal.unknown S≢S'')))
        S'∈canθ'-sigs-p-θ←[S↦status])
... | no  S''∉canθ'-sigs-κ-θ←[S↦unknown]←[S''] | no  S''∉canθ'-sigs-κ-θ←[S↦status]←[S'']
  rewrite Env.←-assoc-comm θ ([S]-env S) ([S]-env-absent (S'' ₛ))
            (Env.sig-single-noteq-distinct S Signal.unknown
              (S'' ₛ) Signal.absent S≢S'')
  = canθ'ₛ-add-sig-monotonic sigs (suc S'') κ
      (θ ← [S]-env-absent (S'' ₛ)) S status κ-add-sig-monotonic S'
      (subst (S' ∈_)
        (cong (proj₁ ∘ Canθ' sigs (suc S'') κ)
          (Env.←-assoc-comm θ [ S ↦ status ] ([S]-env-absent (S'' ₛ))
              (Env.sig-single-noteq-distinct S status
                (S'' ₛ) Signal.absent S≢S'')))
        S'∈canθ'-sigs-p-θ←[S↦status])
... | yes S''∈canθ'-sigs-κ-θ←[S↦unknown]←[S''] | no  S''∉canθ'-sigs-κ-θ←[S↦status]←[S'']
  rewrite Env.←-assoc-comm θ ([S]-env S) ([S]-env (S'' ₛ))
            (Env.sig-single-noteq-distinct S Signal.unknown
              (S'' ₛ) Signal.unknown S≢S'')
  = canθ'ₛ-add-sig-monotonic sigs (suc S'') κ (θ ← [S]-env (S'' ₛ))
      S status κ-add-sig-monotonic S'
      (subst (S' ∈_)
        (cong (proj₁ ∘ Canθ' sigs (suc S'') κ)
          (Env.←-assoc-comm θ [ S ↦ status ] ([S]-env (S'' ₛ))
            (Env.sig-single-noteq-distinct S status
              (S'' ₛ) Signal.unknown S≢S'')))
        (canθ'ₛ-add-sig-monotonic sigs (suc S'') κ (θ ← [ S ↦ status ])
          (S'' ₛ) Signal.absent κ-add-sig-monotonic
            S' S'∈canθ'-sigs-p-θ←[S↦status]))
... | no  S''∉canθ'-sigs-κ-θ←[S↦unknown]←[S''] | yes S''∈canθ'-sigs-κ-θ←[S↦status]←[S'']
  rewrite Env.←-assoc-comm θ ([S]-env S) ([S]-env (S'' ₛ))
            (Env.sig-single-noteq-distinct S Signal.unknown
              (S'' ₛ) Signal.unknown S≢S'')
  = ⊥-elim
    (S''∉canθ'-sigs-κ-θ←[S↦unknown]←[S'']
      (canθ'ₛ-add-sig-monotonic sigs (suc S'') κ (θ ← [S]-env (S'' ₛ)) S
         status κ-add-sig-monotonic S''
         (subst (S'' ∈_)
           (cong (proj₁ ∘ Canθ' sigs (suc S'') κ)
             (Env.←-assoc-comm θ [ S ↦ status ] ([S]-env (S'' ₛ))
               (Env.sig-single-noteq-distinct S status
                 (S'' ₛ) Signal.unknown S≢S'')))
           S''∈canθ'-sigs-κ-θ←[S↦status]←[S''])))

canθ'ₛ-canθ-add-sig-monotonic : ∀ sigs S sigs' S' p θ S''' status →
  ∀ S'' →
    S'' ∈ proj₁ (Canθ' sigs S (Canθ sigs' S' p)
                  (θ ← Θ SigMap.[ S''' ↦ status ] ShrMap.empty VarMap.empty)) →
    S'' ∈ proj₁ (Canθ' sigs S (Canθ sigs' S' p)
                  (θ ← [S]-env S'''))
canθ'ₛ-canθ-add-sig-monotonic sigs S sigs' S' p θ S''' status
  S'' S''∈canθ'-sigs-p-θ←[S↦status] =
  canθ'ₛ-add-sig-monotonic sigs S (Canθ sigs' S' p) θ S''' status
    (canθₛ-add-sig-monotonic sigs' S' p)
    S'' S''∈canθ'-sigs-p-θ←[S↦status]

canθ'ₛ-subset-lemma : ∀ sigs S'' κ κ' θ →
  (∀ θ' S → S ∈ proj₁ (κ θ') → S ∈ proj₁ (κ' θ')) →
  (∀ θ S status S' →
    S' ∈ proj₁ (κ' (θ ← Θ SigMap.[ S ↦ status ] ShrMap.empty VarMap.empty)) →
    S' ∈ proj₁ (κ' (θ ← [S]-env S))) →
  ∀ S → S ∈ proj₁ (Canθ' sigs S'' κ θ) → S ∈ proj₁ (Canθ' sigs S'' κ' θ)
canθ'ₛ-subset-lemma [] S'' κ κ' θ κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ =
  κ⊆κ' θ S S∈canθ'-κ-θ
canθ'ₛ-subset-lemma (nothing ∷ sigs) S'' κ κ' θ
  κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ =
  canθ'ₛ-subset-lemma sigs (suc S'') κ κ' θ κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ
canθ'ₛ-subset-lemma (just Signal.present ∷ sigs) S'' κ κ' θ
  κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ =
  canθ'ₛ-subset-lemma sigs (suc S'') κ κ' (θ ← [S]-env-present (S'' ₛ))
    κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ
canθ'ₛ-subset-lemma (just Signal.absent ∷ sigs) S'' κ κ' θ
  κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ =
  canθ'ₛ-subset-lemma sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ)) κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ
canθ'ₛ-subset-lemma (just Signal.unknown ∷ sigs) S'' κ κ' θ
  κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ  (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') κ' (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-κ-θ' | yes S''∈canθ-κ'-θ' =
  canθ'ₛ-subset-lemma sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ))
    κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ
... | no  S''∉canθ'-κ-θ' | no  S''∉canθ-q-θ' =
  canθ'ₛ-subset-lemma sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ))
    κ⊆κ' κ'-add-sig-monotonic S S∈canθ'-κ-θ
... | yes S''∈canθ'-κ-θ' | no  S''∉canθ-q-θ' =
  ⊥-elim
    (S''∉canθ-q-θ'
      (canθ'ₛ-subset-lemma sigs (suc S'') κ κ' (θ ← [S]-env (S'' ₛ)) κ⊆κ'
        κ'-add-sig-monotonic S'' S''∈canθ'-κ-θ'))
... | no  S''∉canθ'-κ-θ' | yes S''∈canθ-κ'-θ' =
  canθ'ₛ-add-sig-monotonic sigs (suc S'') κ' θ (S'' ₛ) Signal.absent
    κ'-add-sig-monotonic S
    (canθ'ₛ-subset-lemma sigs (suc S'') κ κ' (θ ← [S]-env-absent (S'' ₛ)) κ⊆κ'
      κ'-add-sig-monotonic S S∈canθ'-κ-θ)

canθ'-inner-shadowing-irr' : ∀ sigs S'' sigs' p S status θ θo →
  S ∈ SigMap.keys sigs' →
    Canθ' sigs S'' (Canθ sigs' 0 p) ((θ ← [ (S ₛ) ↦ status ]) ← θo) ≡
    Canθ' sigs S'' (Canθ sigs' 0 p) (θ ← θo)
canθ'-inner-shadowing-irr' [] S'' sigs' p S status θ θo S∈sigs'
  rewrite sym (map-id (SigMap.keys sigs'))
  = canθ-shadowing-irr' sigs' 0 p S status θ θo S∈sigs'
canθ'-inner-shadowing-irr' (nothing ∷ sigs) S'' sigs' p S status θ θo S∈sigs' = canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ θo S∈sigs'
canθ'-inner-shadowing-irr' (just Signal.present ∷ sigs) S'' sigs' p S status θ θo S∈sigs'
  rewrite sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env-present (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env-present (S'' ₛ)))
  = canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ (θo ← ([S]-env-present (S'' ₛ))) S∈sigs'
canθ'-inner-shadowing-irr' (just Signal.absent ∷ sigs) S'' sigs' p S status θ θo S∈sigs'
  rewrite sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env-absent (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env-absent (S'' ₛ)))
  = canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ (θo ← ([S]-env-absent (S'' ₛ))) S∈sigs'
canθ'-inner-shadowing-irr' (just Signal.unknown ∷ sigs) S'' sigs' p S status θ θo S∈sigs'
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ sigs' 0 p) (((θ ← [ (S ₛ) ↦ status ]) ← θo) ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ sigs' 0 p) ((θ ← θo) ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-Canθ-θ←[S]-absent←S←θo←[S''] | yes S''∈canθ'-sigs-Canθ-θ←[S]←S←θo←[S'']
  rewrite sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env (S'' ₛ)))
  = canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ (θo ← ([S]-env (S'' ₛ))) S∈sigs'
... | no  S''∉canθ'-sigs-Canθ-θ←[S]-absent←S←θo←[S''] | no  S''∉canθ'-sigs-Canθ-θ←[S]←S←θo←[S'']
  rewrite sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env-absent (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env-absent (S'' ₛ)))
  = canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ (θo ← ([S]-env-absent (S'' ₛ))) S∈sigs'
... | yes S''∈canθ'-sigs-Canθ-θ←[S]-absent←S←θo←[S''] | no  S''∉canθ'-sigs-Canθ-θ←[S]←S←θo←[S'']
  rewrite sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env (S'' ₛ)))
        | canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ (θo ← ([S]-env (S'' ₛ))) S∈sigs'
  = ⊥-elim (S''∉canθ'-sigs-Canθ-θ←[S]←S←θo←[S'']
              S''∈canθ'-sigs-Canθ-θ←[S]-absent←S←θo←[S''])
... | no  S''∉canθ'-sigs-Canθ-θ←[S]-absent←S←θo←[S''] | yes S''∈canθ'-sigs-Canθ-θ←[S]←S←θo←[S'']
  rewrite sym (Env.←-assoc (θ ← [ (S ₛ) ↦ status ]) θo ([S]-env (S'' ₛ)))
        | sym (Env.←-assoc θ θo ([S]-env (S'' ₛ)))
        | canθ'-inner-shadowing-irr' sigs (suc S'') sigs' p S status θ (θo ← ([S]-env (S'' ₛ))) S∈sigs'
  = ⊥-elim (S''∉canθ'-sigs-Canθ-θ←[S]-absent←S←θo←[S'']
              S''∈canθ'-sigs-Canθ-θ←[S]←S←θo←[S''])

canθ'-inner-shadowing-irr : ∀ sigs S'' sigs' p S status θ →
  S ∈ SigMap.keys sigs' →
    Canθ' sigs S'' (Canθ sigs' 0 p) (θ ← [ (S ₛ) ↦ status ]) ≡
    Canθ' sigs S'' (Canθ sigs' 0 p) θ
canθ'-inner-shadowing-irr sigs S'' sigs' p S status θ S∈sigs'
  rewrite cong (Canθ' sigs S'' (Canθ sigs' 0 p))
            (Env.←-comm Env.[]env θ distinct-empty-left)
        | cong (Canθ' sigs S'' (Canθ sigs' 0 p))
            (Env.←-comm Env.[]env (θ ← [ (S ₛ) ↦ status ]) distinct-empty-left)
  = canθ'-inner-shadowing-irr' sigs S'' sigs' p S status θ Env.[]env S∈sigs'

canθ'-search-acc : ∀ sigs S κ θ →
  ∀ S'' status →
    S'' ∉ map (_+_ S)  (SigMap.keys sigs) →
    Canθ' sigs S  κ  (θ ← [ (S'' ₛ) ↦ status ]) ≡
    Canθ' sigs S (κ ∘ (_← [ (S'' ₛ) ↦ status ])) θ
canθ'-search-acc [] S κ θ S'' status S''∉map-+-S-sigs =
  refl
canθ'-search-acc (nothing ∷ sigs) S κ θ S'' status S''∉map-+-S-sigs
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  = canθ'-search-acc sigs (suc S) κ θ S'' status S''∉map-+-S-sigs
canθ'-search-acc (just Signal.present ∷ sigs) S κ θ S'' status S''∉map-+-S-sigs
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env-present (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.present (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc sigs (suc S) κ (θ ← [S]-env-present (S ₛ)) S'' status
      (S''∉map-+-S-sigs ∘ there)
canθ'-search-acc (just Signal.absent ∷ sigs) S κ θ S'' status S''∉map-+-S-sigs
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env-absent (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.absent (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc sigs (suc S) κ (θ ← [S]-env-absent (S ₛ)) S'' status
      (S''∉map-+-S-sigs ∘ there)
canθ'-search-acc (just Signal.unknown ∷ sigs) S κ θ S'' status S''∉map-+-S-sigs
  with any (_≟_ S) (proj₁ (Canθ' sigs (suc S) (λ θ* → κ (θ* ← [ (S'' ₛ) ↦ status ])) (θ ← [S]-env (S ₛ))))
     | any (_≟_ S) (proj₁ (Canθ' sigs (suc S) κ ((θ ← [ (S'' ₛ) ↦ status ]) ← [S]-env (S ₛ))))
... | yes S∈canθ'-⟨canθ-←[S'']⟩-θ←[S] | yes S∈canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc sigs (suc S) κ (θ ← [S]-env (S ₛ)) S'' status
      (S''∉map-+-S-sigs ∘ there)
... | no  S∉canθ'-⟨canθ-←[S'']⟩-θ←[S] | no  S∉canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env-absent (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.absent (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc sigs (suc S) κ (θ ← [S]-env-absent (S ₛ)) S'' status
      (S''∉map-+-S-sigs ∘ there)
... | yes S∈canθ'-⟨canθ-←[S'']⟩-θ←[S] | no  S∉canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | canθ'-search-acc sigs (suc S) κ (θ ← [S]-env (S ₛ)) S'' status
            (S''∉map-+-S-sigs ∘ there)
  = ⊥-elim (S∉canθ'-canθ-θ←[S'']←[S] S∈canθ'-⟨canθ-←[S'']⟩-θ←[S])
... | no  S∉canθ'-⟨canθ-←[S'']⟩-θ←[S] | yes S∈canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | canθ'-search-acc sigs (suc S) κ (θ ← [S]-env (S ₛ)) S'' status
            (S''∉map-+-S-sigs ∘ there)
  = ⊥-elim (S∉canθ'-⟨canθ-←[S'']⟩-θ←[S] S∈canθ'-canθ-θ←[S'']←[S])

canθ'-search-acc-set-irr : ∀ sigs S κ θ →
  ∀ S'' status status' →
    S'' ∉ map (_+_ S)  (SigMap.keys sigs) →
    Canθ' sigs S κ (θ ← [ (S'' ₛ) ↦ status ]) ≡
    Canθ' sigs S (κ ∘ (_← [ (S'' ₛ) ↦ status ])) (θ ← [ (S'' ₛ) ↦ status' ])
canθ'-search-acc-set-irr [] S κ θ S'' status status' S''∉map-+-S-sigs
  rewrite sym (Env.←-assoc θ [ (S'' ₛ) ↦ status' ] [ (S'' ₛ) ↦ status ])
        | cong (θ ←_) (Env.←-single-overwrite-sig (S'' ₛ) status' [ (S'' ₛ) ↦ status ]
            (Env.sig-∈-single (S'' ₛ) status))
  = refl
canθ'-search-acc-set-irr (nothing ∷ sigs) S κ θ S'' status status' S''∉map-+-S-sigs
  rewrite map-+-compose-suc S (SigMap.keys sigs)
  = canθ'-search-acc-set-irr sigs (suc S) κ θ S'' status status' S''∉map-+-S-sigs
canθ'-search-acc-set-irr (just Signal.present ∷ sigs) S κ θ S'' status status' S''∉map-+-S-sigs
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env-present (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.present (S''∉map-+-S-sigs ∘ here))
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status' ] ([S]-env-present (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status' (S ₛ) Signal.present (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc-set-irr sigs (suc S) κ (θ ← [S]-env-present (S ₛ)) S'' status status'
      (S''∉map-+-S-sigs ∘ there)
canθ'-search-acc-set-irr (just Signal.absent ∷ sigs) S κ θ S'' status status' S''∉map-+-S-sigs
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env-absent (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.absent (S''∉map-+-S-sigs ∘ here))
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status' ] ([S]-env-absent (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status' (S ₛ) Signal.absent (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc-set-irr sigs (suc S) κ (θ ← [S]-env-absent (S ₛ)) S'' status status'
      (S''∉map-+-S-sigs ∘ there)
canθ'-search-acc-set-irr (just Signal.unknown ∷ sigs) S κ θ S'' status status' S''∉map-+-S-sigs
  with any (_≟_ S) (proj₁ (Canθ' sigs (suc S) (λ θ* → κ (θ* ← [ (S'' ₛ) ↦ status ])) ((θ ← [ (S'' ₛ) ↦ status' ]) ← [S]-env (S ₛ))))
     | any (_≟_ S) (proj₁ (Canθ' sigs (suc S) κ ((θ ← [ (S'' ₛ) ↦ status ]) ← [S]-env (S ₛ))))
... | yes S∈canθ'-⟨canθ-←[S'']⟩-θ←[S'']←[S] | yes S∈canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status' ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status' (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc-set-irr sigs (suc S) κ (θ ← [S]-env (S ₛ)) S'' status status'
      (S''∉map-+-S-sigs ∘ there)
... | no  S∉canθ'-⟨canθ-←[S'']⟩-θ←[S'']←[S] | no  S∉canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env-absent (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.absent (S''∉map-+-S-sigs ∘ here))
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status' ] ([S]-env-absent (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status' (S ₛ) Signal.absent (S''∉map-+-S-sigs ∘ here))
  = canθ'-search-acc-set-irr sigs (suc S) κ (θ ← [S]-env-absent (S ₛ)) S'' status status'
      (S''∉map-+-S-sigs ∘ there)
... | yes S∈canθ'-⟨canθ-←[S'']⟩-θ←[S'']←[S] | no  S∉canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status' ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status' (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | canθ'-search-acc-set-irr sigs (suc S) κ (θ ← [S]-env (S ₛ)) S'' status status'
            (S''∉map-+-S-sigs ∘ there)
  = ⊥-elim (S∉canθ'-canθ-θ←[S'']←[S] S∈canθ'-⟨canθ-←[S'']⟩-θ←[S'']←[S])
... | no  S∉canθ'-⟨canθ-←[S'']⟩-θ←[S'']←[S] | yes S∈canθ'-canθ-θ←[S'']←[S]
  rewrite map-+-compose-suc S (SigMap.keys sigs)
        | +-comm S 0
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | Env.←-assoc-comm θ [ (S'' ₛ) ↦ status' ] ([S]-env (S ₛ))
            (Env.sig-single-noteq-distinct (S'' ₛ) status' (S ₛ) Signal.unknown (S''∉map-+-S-sigs ∘ here))
        | canθ'-search-acc-set-irr sigs (suc S) κ (θ ← [S]-env (S ₛ)) S'' status status'
            (S''∉map-+-S-sigs ∘ there)
  = ⊥-elim (S∉canθ'-⟨canθ-←[S'']⟩-θ←[S'']←[S] S∈canθ'-canθ-θ←[S'']←[S])

canθ'-canθ-propagate-up-in : ∀ sigs S r θ →
  ∀ sigs' S' S'' →
    S' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) θ) →
    S'' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) θ) →
    S'' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r θ*) θ)
canθ'-canθ-propagate-up-in [] S r θ sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
  with any (_≟_ S') (Canθₛ sigs' (suc S') r (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-r-θ*←[S'] =
  S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
... | no  S'∉canθ-sigs'-r-θ*←[S'] =
  ⊥-elim (S'∉canθ-sigs'-r-θ*←[S'] S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩)
canθ'-canθ-propagate-up-in (nothing ∷ sigs) S r θ sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ =
  canθ'-canθ-propagate-up-in sigs (suc S) r θ sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
canθ'-canθ-propagate-up-in (just Signal.present ∷ sigs) S r θ sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ =
  canθ'-canθ-propagate-up-in sigs (suc S) r (θ ← [S]-env-present (S ₛ)) sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
canθ'-canθ-propagate-up-in (just Signal.absent ∷ sigs) S r θ sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ =
  canθ'-canθ-propagate-up-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
canθ'-canθ-propagate-up-in (just Signal.unknown ∷ sigs) S r θ sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
  with any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S) (Canθ (just Signal.unknown ∷ sigs') S' r) (θ ← [S]-env (S ₛ))))
     | any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S) (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-up-in sigs (suc S) r (θ ← [S]-env (S ₛ)) sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-up-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'ₛ-canθ-add-sig-monotonic sigs (suc S) (just Signal.unknown ∷ sigs') S' r θ
    (S ₛ) Signal.absent S''
    (canθ'-canθ-propagate-up-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) sigs' S' S''
      S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
      S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩)
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  ⊥-elim
    (S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S]
      (canθ'-canθ-propagate-up-in sigs (suc S) r (θ ← [S]-env (S ₛ)) sigs' S' S
        S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
        S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]))

canθₛ-a∷s⊆canθₛ-u∷s : ∀ sigs r S' θ S →
  S ∈ Canθₛ (just Signal.absent ∷ sigs) S' r θ →
  S ∈ Canθₛ (just Signal.unknown ∷ sigs) S' r θ
canθₛ-a∷s⊆canθₛ-u∷s sigs r S' θ S S∈can-sigs-r-θ←[S↦absent]
  with any (_≟_ S') (Canθₛ sigs (suc S') r (θ ← [S]-env (S' ₛ)))
... | yes a = canθₛ-add-sig-monotonic sigs (suc S') r θ (S' ₛ) Signal.absent S
                S∈can-sigs-r-θ←[S↦absent]
... | no na = S∈can-sigs-r-θ←[S↦absent]

canθ'-canθ-propagate-down-not-in : ∀ sigs S r θ →
  ∀ S' sigs' →
    S' ∉ proj₁ (Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r θ*) θ) →
    Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r θ*) θ ≡
    Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env-absent (S' ₛ))) θ
canθ'-canθ-propagate-down-not-in [] S r θ S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
  with any (_≟_ S') (Canθₛ sigs' (suc S') r (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-r-θ←[S'] =
  ⊥-elim (S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ S'∈canθ-sigs'-r-θ←[S'])
... | no  S'∉canθ-sigs'-r-θ←[S'] = refl
canθ'-canθ-propagate-down-not-in (nothing ∷ sigs) S r θ S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-not-in sigs (suc S) r θ S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-not-in (just Signal.present ∷ sigs) S r θ S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-not-in sigs (suc S) r (θ ← [S]-env-present (S ₛ)) S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-not-in (just Signal.absent ∷ sigs) S r θ S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-not-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-not-in (just Signal.unknown ∷ sigs) S r θ S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
  with any (_≟_ S)
          (proj₁
            (Canθ' sigs (suc S)
              (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r θ*)
              (θ ← [S]-env (S ₛ))))
     | any (_≟_ S)
          (proj₁
            (Canθ' sigs (suc S)
              (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env-absent (S' ₛ)))
              (θ ← [S]-env (S ₛ))))
... | yes a | yes b =
  canθ'-canθ-propagate-down-not-in sigs (suc S) r (θ ← [S]-env (S ₛ)) S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
... | no na | no nb =
  canθ'-canθ-propagate-down-not-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
... | yes a | no nb
  rewrite sym (canθ'-canθ-propagate-down-not-in sigs (suc S) r (θ ← [S]-env (S ₛ)) S' sigs' S'∉canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩)
  = ⊥-elim (nb a)
... | no na | yes b
  = ⊥-elim (na (canθ'ₛ-subset-lemma sigs (suc S) (Canθ (just Signal.absent ∷ sigs') S' r) (Canθ (just Signal.unknown ∷ sigs') S' r) (θ ← [S]-env (S ₛ)) (canθₛ-a∷s⊆canθₛ-u∷s sigs' r S') (canθₛ-add-sig-monotonic (just Signal.unknown ∷ sigs') S' r) S b))

canθ'-canθ-propagate-down-in : ∀ sigs S r θ →
  ∀ S' sigs' →
    S' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r θ*) θ) →
    Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r θ*) θ ≡
    Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) θ
canθ'-canθ-propagate-down-in [] S r θ S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
  with any (_≟_ S') (Canθₛ sigs' (suc S') r (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-r-θ←[S'] = refl
... | no  S'∉canθ-sigs'-r-θ←[S'] =
  ⊥-elim
    (S'∉canθ-sigs'-r-θ←[S']
      (canθₛ-add-sig-monotonic sigs' (suc S') r θ (S' ₛ) Signal.absent S'
         S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩))
canθ'-canθ-propagate-down-in (nothing ∷ sigs) S r θ S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-in sigs (suc S) r θ S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-in (just Signal.present ∷ sigs) S r θ S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-in sigs (suc S) r (θ ← [S]-env-present (S ₛ)) S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-in (just Signal.absent ∷ sigs) S r θ S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-in (just Signal.unknown ∷ sigs) S r θ S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
  with any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S)
             (Canθ (just Signal.unknown ∷ sigs') S' r)
             (θ ← [S]-env (S ₛ))))
     | any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S)
             (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ)))
             (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-down-in sigs (suc S) r (θ ← [S]-env (S ₛ)) S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-down-in sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
  = ⊥-elim
      (S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
        (subst (S ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in sigs (suc S) r (θ ← [S]-env (S ₛ)) S' sigs'
              S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩))
          S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S]))
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
  = ⊥-elim
    (S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S]
      (subst (S ∈_)
        (cong proj₁
          (sym (canθ'-canθ-propagate-down-in sigs (suc S) r (θ ← [S]-env (S ₛ)) S' sigs'
            (canθ'ₛ-canθ-add-sig-monotonic sigs (suc S) (just Signal.unknown ∷ sigs') S'
              r θ (S ₛ) Signal.absent S'
              S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩))))
        S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]))

canθ'-canθ-propagate-up-in-set-irr : ∀ sigs S r θ status →
  ∀ sigs' S' S'' →
    S' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) θ) →
    S'' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) θ) →
    S'' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r (θ* ← [ (S' ₛ) ↦ status ])) θ)
canθ'-canθ-propagate-up-in-set-irr [] S r θ status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
  with any (_≟_ S') (Canθₛ sigs' (suc S') r ((θ ← [ (S' ₛ) ↦ status ]) ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-r-θ*←[S']
  rewrite Env.sig-single-←-←-overwrite θ (S' ₛ) status Signal.unknown
  = S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
... | no  S'∉canθ-sigs'-r-θ*←[S']
  rewrite Env.sig-single-←-←-overwrite θ (S' ₛ) status Signal.unknown
  = ⊥-elim (S'∉canθ-sigs'-r-θ*←[S'] S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩)
canθ'-canθ-propagate-up-in-set-irr (nothing ∷ sigs) S r θ status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ =
  canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r θ status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
canθ'-canθ-propagate-up-in-set-irr (just Signal.present ∷ sigs) S r θ status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ =
  canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r (θ ← [S]-env-present (S ₛ)) status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
canθ'-canθ-propagate-up-in-set-irr (just Signal.absent ∷ sigs) S r θ status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ =
  canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
canθ'-canθ-propagate-up-in-set-irr (just Signal.unknown ∷ sigs) S r θ status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
  with any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S) (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r (θ* ← [ (S' ₛ) ↦ status ])) (θ ← [S]-env (S ₛ))))
     | any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S) (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r (θ ← [S]-env (S ₛ)) status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) status sigs' S' S'' S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩ S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
  = canθ'ₛ-add-sig-monotonic sigs (suc S)
       (Canθ (just Signal.unknown ∷ sigs') S' r ∘ (_← [ (S' ₛ) ↦ status ]))
       θ (S ₛ) Signal.absent
       (λ θ* S* status* S'' S''∈ →
         canθₛ-cong-←-add-sig-monotonic (just Signal.unknown ∷ sigs') S' r
         θ* [ (S' ₛ) ↦ status ] S* status* S'' S''∈) S''
       (canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r (θ ← [S]-env-absent (S ₛ))
         status sigs' S' S''
         S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
         S''∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩)
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  ⊥-elim
    (S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S]
      (canθ'-canθ-propagate-up-in-set-irr sigs (suc S) r (θ ← [S]-env (S ₛ)) status sigs' S' S
        S'∈canθ'-sigs-⟨canθ-sigs'-r-θ*←[S']⟩
        S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]))

canθ'-canθ-propagate-down-in-set-irr : ∀ sigs S r θ status →
  ∀ S' sigs' →
    S' ∈ proj₁ (Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r (θ* ← [ (S' ₛ) ↦ status ])) θ) →
    Canθ' sigs S (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r (θ* ← [ (S' ₛ) ↦ status ])) θ ≡
    Canθ' sigs S (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ))) θ
canθ'-canθ-propagate-down-in-set-irr [] S r θ status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
  with any (_≟_ S') (Canθₛ sigs' (suc S') r ((θ ← [ (S' ₛ) ↦ status ]) ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-r-θ←[S'] rewrite Env.sig-single-←-←-overwrite θ (S' ₛ) status Signal.unknown = refl
... | no  S'∉canθ-sigs'-r-θ←[S'] =
  ⊥-elim
    (S'∉canθ-sigs'-r-θ←[S']
      (canθₛ-add-sig-monotonic sigs' (suc S') r (θ ← [ (S' ₛ) ↦ status ]) (S' ₛ) Signal.absent S'
         S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩))
canθ'-canθ-propagate-down-in-set-irr (nothing ∷ sigs) S r θ status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r θ status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-in-set-irr (just Signal.present ∷ sigs) S r θ status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r (θ ← [S]-env-present (S ₛ)) status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-in-set-irr (just Signal.absent ∷ sigs) S r θ status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩ =
  canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
canθ'-canθ-propagate-down-in-set-irr (just Signal.unknown ∷ sigs) S r θ status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
  with any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S)
             (λ θ* → Canθ (just Signal.unknown ∷ sigs') S' r (θ* ← [ (S' ₛ) ↦ status ]))
             (θ ← [S]-env (S ₛ))))
     | any (_≟_ S)
         (proj₁
           (Canθ' sigs (suc S)
             (λ θ* → Canθ sigs' (suc S') r (θ* ← [S]-env (S' ₛ)))
             (θ ← [S]-env (S ₛ))))
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r (θ ← [S]-env (S ₛ)) status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S] =
  canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r (θ ← [S]-env-absent (S ₛ)) status S' sigs' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩
... | yes S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | no  S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
  = ⊥-elim
      (S∉canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
        (subst (S ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r (θ ← [S]-env (S ₛ)) status S' sigs'
              S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩))
          S∈canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S]))
... | no  S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S] | yes S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]
  = ⊥-elim
    (S∉canθ'-sigs-⟨canθ-u∷sigs'-r⟩-θ←[S]
      (subst (S ∈_)
        (cong proj₁
          (sym (canθ'-canθ-propagate-down-in-set-irr sigs (suc S) r (θ ← [S]-env (S ₛ)) status S' sigs'
            (canθ'ₛ-add-sig-monotonic sigs (suc S)
               (Canθ (just Signal.unknown ∷ sigs') S' r ∘
                (λ section → section ← [ (S' ₛ) ↦ status ]))
               θ (S ₛ) Signal.absent
               (λ θ* S* status* →
                 canθₛ-cong-←-add-sig-monotonic (just Signal.unknown ∷ sigs') S' r
                   θ* [ (S' ₛ) ↦ status ] S* status*)
               S' S'∈canθ'-sigs-⟨Canθ-u∷sigs'-θ*⟩))))
        S∈canθ'-sigs-⟨canθ-sigs'-θ*←[S']⟩-θ←[S]))

canθ'-←-distribute : ∀ sigs sigs' S'' r θ →
  Canθ (SigMap.union sigs sigs') S'' r θ ≡
  Canθ' sigs S'' (Canθ sigs' S'' r) θ
canθ'-←-distribute [] sigs' S'' r θ = refl
canθ'-←-distribute sigs [] S'' r θ
  rewrite SigMap.union-comm sigs SigMap.empty (λ _ _ ())
        | unfold sigs S'' r θ
  = refl
canθ'-←-distribute (nothing ∷ sigs) (nothing ∷ sigs') S'' r θ =
  canθ'-←-distribute sigs sigs' (suc S'') r θ
canθ'-←-distribute (just Signal.present ∷ sigs) (nothing ∷ sigs') S'' r θ =
  canθ'-←-distribute sigs sigs' (suc S'') r
    (θ ← [S]-env-present (S'' ₛ))
canθ'-←-distribute (just Signal.absent ∷ sigs) (nothing ∷ sigs') S'' r θ =
  canθ'-←-distribute sigs sigs' (suc S'') r
    (θ ← [S]-env-absent (S'' ₛ))
canθ'-←-distribute (just Signal.unknown ∷ sigs) (nothing ∷ sigs') S'' r θ
  with any (_≟_ S'') (proj₁ (Canθ (SigMap.union sigs sigs') (suc S'') r (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ sigs' (suc S'') r) (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨canθ-sigs'⟩-θ←[S''] =
  canθ'-←-distribute sigs sigs' (suc S'') r
    (θ ← [S]-env (S'' ₛ))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨canθ-sigs'⟩-θ←[S''] =
  canθ'-←-distribute sigs sigs' (suc S'') r
    (θ ← [S]-env-absent (S'' ₛ))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨canθ-sigs'⟩-θ←[S'']
  rewrite canθ'-←-distribute sigs sigs' (suc S'') r (θ ← [S]-env (S'' ₛ))
  = ⊥-elim (S''∉canθ'-sigs-⟨canθ-sigs'⟩-θ←[S''] S''∈canθ'-sigs←sigs'-r-θ←[S''])
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨canθ-sigs'⟩-θ←[S'']
  rewrite canθ'-←-distribute sigs sigs' (suc S'') r (θ ← [S]-env (S'' ₛ))
  = ⊥-elim (S''∉canθ'-sigs←sigs'-r-θ←[S''] S''∈canθ'-sigs-⟨canθ-sigs'⟩-θ←[S''])
canθ'-←-distribute (nothing ∷ sigs) (just Signal.present ∷ sigs') S'' r θ =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-present (S'' ₛ)))
    (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.present
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (nothing ∷ sigs) (just Signal.absent ∷ sigs') S'' r θ =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-absent (S'' ₛ)))
    (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (nothing ∷ sigs) (just Signal.unknown ∷ sigs') S'' r θ
  with any (_≟_ S'') (proj₁ (Canθ (SigMap.union sigs sigs') (suc S'') r (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-in sigs (suc S'') r θ S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env (S'' ₛ)))
      (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-not-in sigs (suc S'') r θ S'' sigs' S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env-absent (S'' ₛ)))
      (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
  = ⊥-elim
      (S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
        (canθ'-canθ-propagate-up-in sigs (suc S'') r θ sigs' S'' S'' S''∈canθ'-sigs←sigs'-r-θ←[S''] S''∈canθ'-sigs←sigs'-r-θ←[S'']))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
  = ⊥-elim
      (S''∉canθ'-sigs←sigs'-r-θ←[S'']
        (subst (S'' ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in sigs (suc S'') r θ S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
          S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
canθ'-←-distribute (just Signal.present ∷ sigs) (just Signal.present ∷ sigs') S'' r θ =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-present (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.present Signal.present
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (just Signal.absent ∷ sigs)  (just Signal.present ∷ sigs') S'' r θ =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-present (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.present Signal.absent
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (just Signal.unknown ∷ sigs) (just Signal.present ∷ sigs') S'' r θ
  with any (_≟_ S'')
         (proj₁
           (Canθ' sigs (suc S'')
             (λ θ* → Canθ sigs' (suc S'') r (θ* ← [S]-env-present (S'' ₛ)))
             (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-⟨Canθ-sigs'-r-θ*←[S'']⟩-θ←[S''] =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-present (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.present Signal.unknown
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs-⟨Canθ-sigs'-r-θ*←[S'']⟩-θ←[S''] =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-present (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.present Signal.absent
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (just Signal.present ∷ sigs) (just Signal.absent ∷ sigs') S'' r θ =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-absent (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.present
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (just Signal.absent ∷ sigs)  (just Signal.absent ∷ sigs') S'' r θ =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-absent (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.absent
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (just Signal.unknown ∷ sigs) (just Signal.absent ∷ sigs') S'' r θ
  with any (_≟_ S'')
         (proj₁
           (Canθ' sigs (suc S'')
             (λ θ* → Canθ sigs' (suc S'') r (θ* ← [S]-env-absent (S'' ₛ)))
             (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs-⟨Canθ-sigs'-r-θ*←[S'']⟩-θ←[S''] =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-absent (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.unknown
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs-⟨Canθ-sigs'-r-θ*←[S'']⟩-θ←[S''] =
  trans
    (canθ'-←-distribute sigs sigs' (suc S'') r
     (θ ← [S]-env-absent (S'' ₛ)))
    (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.absent
      (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
canθ'-←-distribute (just Signal.present ∷ sigs) (just Signal.unknown ∷ sigs') S'' r θ
  with any (_≟_ S'') (proj₁ (Canθ (SigMap.union sigs sigs') (suc S'') r (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) (θ ← [S]-env-present (S'' ₛ))))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-in sigs (suc S'') r (θ ← [S]-env-present (S'' ₛ)) S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown Signal.present
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-not-in sigs (suc S'') r (θ ← [S]-env-present (S'' ₛ)) S'' sigs' S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env-absent (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.present
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
  = ⊥-elim
      (S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
        (subst (S'' ∈_)
          (sym
            (cong proj₁
              (canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.present
                (n∉map-suc-n-+ S'' (SigMap.keys sigs)))))
          (canθ'-canθ-propagate-up-in-set-irr sigs (suc S'') r θ Signal.present sigs' S'' S'' S''∈canθ'-sigs←sigs'-r-θ←[S''] S''∈canθ'-sigs←sigs'-r-θ←[S''])))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
        | canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.present
                (n∉map-suc-n-+ S'' (SigMap.keys sigs))
  = ⊥-elim
      (S''∉canθ'-sigs←sigs'-r-θ←[S'']
        (subst (S'' ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in-set-irr sigs (suc S'') r θ Signal.present S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
          S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
canθ'-←-distribute (just Signal.absent ∷ sigs)  (just Signal.unknown ∷ sigs') S'' r θ
  with any (_≟_ S'') (proj₁ (Canθ (SigMap.union sigs sigs') (suc S'') r (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) (θ ← [S]-env-absent (S'' ₛ))))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-in sigs (suc S'') r (θ ← [S]-env-absent (S'' ₛ)) S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown Signal.absent
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-not-in sigs (suc S'') r (θ ← [S]-env-absent (S'' ₛ)) S'' sigs' S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env-absent (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.absent
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
  = ⊥-elim
      (S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
        (subst (S'' ∈_)
          (sym
            (cong proj₁
              (canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.absent
                (n∉map-suc-n-+ S'' (SigMap.keys sigs)))))
          (canθ'-canθ-propagate-up-in-set-irr sigs (suc S'') r θ Signal.absent sigs' S'' S'' S''∈canθ'-sigs←sigs'-r-θ←[S''] S''∈canθ'-sigs←sigs'-r-θ←[S''])))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
        | canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.absent
                (n∉map-suc-n-+ S'' (SigMap.keys sigs))
  = ⊥-elim
      (S''∉canθ'-sigs←sigs'-r-θ←[S'']
        (subst (S'' ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in-set-irr sigs (suc S'') r θ Signal.absent S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
          S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
canθ'-←-distribute (just Signal.unknown ∷ sigs) (just Signal.unknown ∷ sigs') S'' r θ
  with any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (λ θ* → Canθ (just Signal.unknown ∷ sigs') S'' r θ*) (θ ← [S]-env (S'' ₛ))))
canθ'-←-distribute (just Signal.unknown ∷ sigs) (just Signal.unknown ∷ sigs') S'' r θ | yes p
  with any (_≟_ S'') (proj₁ (Canθ (SigMap.union sigs sigs') (suc S'') r (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) (θ ← [S]-env (S'' ₛ))))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-in sigs (suc S'') r (θ ← [S]-env (S'' ₛ)) S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown Signal.unknown
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-not-in sigs (suc S'') r (θ ← [S]-env (S'' ₛ)) S'' sigs' S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env-absent (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.unknown
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
  = ⊥-elim
      (S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
        (subst (S'' ∈_)
          (sym
            (cong proj₁
              (canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.unknown
                (n∉map-suc-n-+ S'' (SigMap.keys sigs)))))
          (canθ'-canθ-propagate-up-in-set-irr sigs (suc S'') r θ Signal.unknown sigs' S'' S'' S''∈canθ'-sigs←sigs'-r-θ←[S''] S''∈canθ'-sigs←sigs'-r-θ←[S''])))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
        | canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.unknown
                (n∉map-suc-n-+ S'' (SigMap.keys sigs))
  = ⊥-elim
      (S''∉canθ'-sigs←sigs'-r-θ←[S'']
        (subst (S'' ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in-set-irr sigs (suc S'') r θ Signal.unknown S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
          S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
canθ'-←-distribute (just Signal.unknown ∷ sigs) (just Signal.unknown ∷ sigs') S'' r θ | no ¬p
  with any (_≟_ S'') (proj₁ (Canθ (SigMap.union sigs sigs') (suc S'') r (θ ← [S]-env (S'' ₛ))))
     | any (_≟_ S'') (proj₁ (Canθ' sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) (θ ← [S]-env-absent (S'' ₛ))))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-in sigs (suc S'') r (θ ← [S]-env-absent (S'' ₛ)) S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown Signal.absent
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite canθ'-canθ-propagate-down-not-in sigs (suc S'') r (θ ← [S]-env-absent (S'' ₛ)) S'' sigs' S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  = trans
      (canθ'-←-distribute sigs sigs' (suc S'') r
       (θ ← [S]-env-absent (S'' ₛ)))
      (canθ'-search-acc-set-irr sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.absent Signal.absent
        (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
... | yes S''∈canθ'-sigs←sigs'-r-θ←[S''] | no  S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
  = ⊥-elim
      (S''∉canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
        (subst (S'' ∈_)
          (sym
            (cong proj₁
              (canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.absent
                (n∉map-suc-n-+ S'' (SigMap.keys sigs)))))
          (canθ'-canθ-propagate-up-in-set-irr sigs (suc S'') r θ Signal.absent sigs' S'' S'' S''∈canθ'-sigs←sigs'-r-θ←[S''] S''∈canθ'-sigs←sigs'-r-θ←[S''])))
... | no  S''∉canθ'-sigs←sigs'-r-θ←[S''] | yes S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩
  rewrite trans
            (canθ'-←-distribute sigs sigs' (suc S'') r
              (θ ← [S]-env (S'' ₛ)))
            (canθ'-search-acc sigs (suc S'') (Canθ sigs' (suc S'') r) θ S'' Signal.unknown
              (n∉map-suc-n-+ S'' (SigMap.keys sigs)))
        | canθ'-search-acc sigs (suc S'') (Canθ (just Signal.unknown ∷ sigs') S'' r) θ
                S'' Signal.absent
                (n∉map-suc-n-+ S'' (SigMap.keys sigs))
  = ⊥-elim
      (S''∉canθ'-sigs←sigs'-r-θ←[S'']
        (subst (S'' ∈_)
          (cong proj₁
            (canθ'-canθ-propagate-down-in-set-irr sigs (suc S'') r θ Signal.absent S'' sigs' S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))
          S''∈canθ'-sigs-⟨Canθ-u∷sigs'-r-θ⟩))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
module Structure.Relator.Apartness where

import      Lvl
open import Logic
open import Logic.Propositional
open import Structure.Relator.Properties
  hiding (irreflexivity ; symmetry ; cotransitivity)
open import Type

private variable ℓ₁ ℓ₂ : Lvl.Level

-- An apartness relation is a irreflexive, symmetric and cotransitive relation.
record Apartness {T : Type{ℓ₁}} (_#_ : T → T → Stmt{ℓ₂}) : Stmt{ℓ₁ Lvl.⊔ ℓ₂} where
  instance constructor intro
  field
    instance ⦃ irreflexivity ⦄  : Irreflexivity  (_#_)
    instance ⦃ symmetry ⦄       : Symmetry       (_#_)
    instance ⦃ cotransitivity ⦄ : CoTransitivity (_#_)

ext: agda

max_stars_repo_name: Lolirofle/stuff-in-agda

max_issues_repo_name: Lolirofle/stuff-in-agda

max_forks_repo_name: Lolirofle/stuff-in-agda


text:
module Issue852 where

open import Common.Level

const : ∀ {a b} {A : Set a} {B : Set b} → A → B → A
const x = λ _ → x

ℓ : Level
ℓ = const lzero (Set ℓ)

ℓ′ : Level
ℓ′ = const lzero (Set ℓ′)

-- Error message using Agda 2.3.2 (the batch-mode command, not the
-- Emacs interface):
--
--   Termination checking failed for the following functions:
--     ℓ, ℓ′
--   Problematic calls:
--     ℓ
--     ℓ (at [...])
--     ℓ′
--     ℓ′
--       (at [...])
--
-- With the current development version of Agda:
--
--   Termination checking failed for the following functions:
--     ℓ, ℓ′
--   Problematic calls:
--     ℓ
--     ℓ (at [...])
--     ℓ′
--       (at [...])

max_issues_repo_name: masondesu/agda

max_forks_repo_name: masondesu/agda


text:
open import IO using ( run ; putStrLn )
open import Data.String using ( _++_ )
open import Data.Natural using ( # ; _+_ ; toString )

module Data.Bindings.Examples.HelloFour where

main = run (putStrLn ("Hello, " ++ toString (#(2) + #(2)) ++ "."))

max_stars_repo_name: agda/agda-data-bindings

max_issues_repo_name: agda/agda-data-bindings

max_forks_repo_name: agda/agda-data-bindings


text:
-- Import all the material (useful to check that everything typechecks)
{-# OPTIONS --cubical #-}
module Everything where

import Warmup
import Part1
import Part2
import Part3
import Part4
import ExerciseSession1
import ExerciseSession2
import ExerciseSession3


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

open import HoTT
open import cw.CW

module cw.examples.Unit where

cw-unit-skel : Skeleton {lzero} 0
cw-unit-skel = Unit , Unit-is-set
CWUnit = ⟦ cw-unit-skel ⟧

CWUnit-equiv-Unit : CWUnit ≃ Unit
CWUnit-equiv-Unit = ide _

max_stars_repo_name: mikeshulman/HoTT-Agda

max_issues_repo_name: mikeshulman/HoTT-Agda

max_forks_repo_name: mikeshulman/HoTT-Agda


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.ReflGraph where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Isomorphism
open import Cubical.Foundations.Structure

open import Cubical.Functions.FunExtEquiv

open import Cubical.Homotopy.Base

open import Cubical.Data.Sigma

open import Cubical.Relation.Binary

open import Cubical.Algebra.Group
open import Cubical.Structures.LeftAction

open import Cubical.DStructures.Base
open import Cubical.DStructures.Meta.Properties
open import Cubical.DStructures.Structures.Constant

open import Cubical.DStructures.Structures.Type
open import Cubical.DStructures.Structures.Group
open import Cubical.DStructures.Structures.SplitEpi

open GroupLemmas
open MorphismLemmas

private
  variable
    ℓ ℓ' : Level

---------------------------------------------
-- Reflexive graphs in the category of groups
--
-- ReflGraph
--     |
-- SplitEpiB
--
---------------------------------------------

module _ (ℓ ℓ' : Level) where
  -- type of internal reflexive graphs in the category of groups
  ReflGraph = Σ[ ((((G₀ , G₁) , ι , σ) , split-σ) , τ) ∈ (SplitEpiB ℓ ℓ') ] isGroupSplitEpi ι τ

  -- reflexive graphs displayed over split epimorphisms with an
  -- extra morphism back
  𝒮ᴰ-ReflGraph : URGStrᴰ (𝒮-SplitEpiB ℓ ℓ')
                        (λ ((((G , H) , f , b) , isRet) , b')
                          → isGroupSplitEpi f b')
                        ℓ-zero
  𝒮ᴰ-ReflGraph = Subtype→Sub-𝒮ᴰ (λ ((((G , H) , f , b) , isRet) , b')
                                   → isGroupSplitEpi f b' , isPropIsGroupSplitEpi f b')
                                (𝒮-SplitEpiB ℓ ℓ')

  -- the URG structure on the type of reflexive graphs
  𝒮-ReflGraph : URGStr ReflGraph (ℓ-max ℓ ℓ')
  𝒮-ReflGraph = ∫⟨ (𝒮-SplitEpiB ℓ ℓ') ⟩ 𝒮ᴰ-ReflGraph

--------------------------------------------------
-- This module introduces convenient notation
-- when working with a single reflexive graph
---------------------------------------------------
module ReflGraphNotation (𝒢 : ReflGraph ℓ ℓ') where

    -- extract the components of the Σ-type
    G₁ = snd (fst (fst (fst (fst 𝒢))))
    G₀ = fst (fst (fst (fst (fst 𝒢))))
    σ = snd (snd (fst (fst (fst 𝒢))))
    τ = snd (fst 𝒢)
    ι = fst (snd (fst (fst (fst 𝒢))))
    split-τ = snd 𝒢
    split-σ = snd (fst (fst 𝒢))

    -- open other modules containing convenient notation
    open SplitEpiNotation ι σ split-σ public
    open GroupNotation₁ G₁ public
    open GroupNotation₀ G₀ public
    open GroupHom public

    -- underlying maps
    t = GroupHom.fun τ

    -- combinations of maps to reduce
    -- amount of parentheses in proofs
    𝒾s = λ (g : ⟨ G₁ ⟩) → 𝒾 (s g) -- TODO: remove
    𝒾t = λ (g : ⟨ G₁ ⟩) → 𝒾 (t g) -- TODO: remove
    it = λ (g : ⟨ G₁ ⟩) → 𝒾 (t g)
    ti = λ (g : ⟨ G₀ ⟩) → t (𝒾 g)
    -it = λ (x : ⟨ G₁ ⟩) → -₁ (𝒾t x)
    it- = λ (x : ⟨ G₁ ⟩) →  𝒾t (-₁ x)

    ι∘τ : GroupHom G₁ G₁
    ι∘τ = compGroupHom τ ι

    -- extract what it means for σ and τ to be split
    σι-≡-fun : (g : ⟨ G₀ ⟩) → si g ≡ g
    σι-≡-fun = λ (g : ⟨ G₀ ⟩) → funExt⁻ (cong GroupHom.fun split-σ) g
    τι-≡-fun : (g : ⟨ G₀ ⟩) → ti g ≡ g
    τι-≡-fun = λ (g : ⟨ G₀ ⟩) → funExt⁻ (cong GroupHom.fun split-τ) g

-------------------------------------------
-- Lemmas about reflexive graphs in groups
-------------------------------------------

module ReflGraphLemmas (𝒢 : ReflGraph ℓ ℓ') where
    open ReflGraphNotation 𝒢

    -- the property for two morphisms to be composable
    isComposable : (g f : ⟨ G₁ ⟩) → Type ℓ
    isComposable g f = s g ≡ t f

    -- isComposable is a proposition, because G₀ is a set
    isPropIsComposable : (g f : ⟨ G₁ ⟩) → isProp (isComposable g f)
    isPropIsComposable g f c c' = set₀ (s g) (t f) c c'

    -- further reductions that are used often
    abstract
      -- σ (g -₁ ι (σ g)) ≡ 0₀
      σ-g--isg : (g : ⟨ G₁ ⟩) → s (g -₁ (𝒾s g)) ≡ 0₀
      σ-g--isg g = s (g -₁ (𝒾s g))
                    ≡⟨ σ .isHom g (-₁ 𝒾s g) ⟩
                  s g +₀ s (-₁ 𝒾s g)
                    ≡⟨ cong (s g +₀_)
                            (mapInv σ (𝒾s g)) ⟩
                  s g -₀ s (𝒾s g)
                    ≡⟨ cong (λ z → s g -₀ z)
                            (σι-≡-fun (s g)) ⟩
                  s g -₀ s g
                    ≡⟨ rCancel₀ (s g) ⟩
                  0₀ ∎

      -- g is composable with ι (σ g)
      isComp-g-isg : (g : ⟨ G₁ ⟩) → isComposable g (𝒾s g)
      isComp-g-isg g = sym (τι-≡-fun (s g))

      -- ι (τ f) is composable with f
      isComp-itf-f : (f : ⟨ G₁ ⟩) → isComposable (it f) f
      isComp-itf-f f = σι-≡-fun (t f)

      -- ι (σ (-₁ ι g)) ≡ -₁ (ι g)
      ισ-ι : (g : ⟨ G₀ ⟩) → 𝒾s (-₁ (𝒾 g)) ≡ -₁ (𝒾 g)
      ισ-ι g = mapInv ι∘σ (𝒾 g) ∙ cong (λ z → -₁ (𝒾 z)) (σι-≡-fun g)

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
------------------------------------------------------------------------
-- The Agda standard library
--
-- Floating point numbers
------------------------------------------------------------------------

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

module Data.Float where

------------------------------------------------------------------------
-- Re-export base definitions and decidability of equality

open import Data.Float.Base public
open import Data.Float.Properties using (_≈?_; _<?_; _≟_; _==_) public


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

module 1-type-theory where

import 00-preamble
open 00-preamble public

-- Exercise 1.1 (From ../02-pi.agda)
_∘-1-1_ :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} →
  (B → C) → ((A → B) → (A → C))
(g ∘-1-1 f) a = g (f a)

import 04-inductive-types
open 04-inductive-types public

-- Exercise 1.2
recursorOfProjections :
  {i j k : Level} {A : UU i} {B : UU j} {C : UU k} →
  (A → B → C) → (prod A B) → C
recursorOfProjections f p = f (pr1 p) (pr2 p)

-- Exercise 1.11 is neg-triple-neg

exercise-1-12-i : {i j : Level} {A : UU i} {B : UU j} → A → B → A
exercise-1-12-i x y = x

exercise-1-12-ii : {i : Level} {A : UU i} → A → ¬ (¬ A)
exercise-1-12-ii a = (\ f → f a)

exercise-1-12-iii :
  {i j : Level} {A : UU i} {B : UU j} →
  (coprod (¬ A) (¬ B)) → (¬ (prod A B))
exercise-1-12-iii (inl fa) = (\ p → fa (pr1 p))
exercise-1-12-iii (inr fb) = (\ p → fb (pr2 p))

kian-ex-1-13 :
  {i : Level} {A : UU i}
  → ¬ (¬ (coprod A (¬ A)))
kian-ex-1-13 = (\ f → (\ g → f (inr g)) (\ a → f (inl a)))

import 05-identity-types
open 05-identity-types public

exercise-1-15 :
  {i j : Level} {A : UU i} (C : A → UU j) (x : A) (y : A) → (Id x y) → (C x) → (C y)
exercise-1-15 C x y eq = ind-Id x (\ y' eq' → (C(x) → C(y'))) (\ x → x) y eq

max_stars_repo_name: hemangandhi/HoTT-Intro

max_issues_repo_name: hemangandhi/HoTT-Intro

max_forks_repo_name: hemangandhi/HoTT-Intro


text:
{-# OPTIONS --universe-polymorphism #-}
module Categories.Lan where

open import Level
open import Categories.Category
open import Categories.Functor hiding (_≡_)
open import Categories.NaturalTransformation

record Lan {o₀ ℓ₀ e₀} {o₁ ℓ₁ e₁} {o₂ ℓ₂ e₂}
           {A : Category o₀ ℓ₀ e₀} {B : Category o₁ ℓ₁ e₁} {C : Category o₂ ℓ₂ e₂}
           (F : Functor A B) (X : Functor A C) : Set (o₀ ⊔ ℓ₀ ⊔ e₀ ⊔ o₁ ⊔ ℓ₁ ⊔ e₁ ⊔ o₂ ⊔ ℓ₂ ⊔ e₂) where
  field
    L : Functor B C
    ε : NaturalTransformation X (L ∘ F)

    σ : (M : Functor B C) → (α : NaturalTransformation X (M ∘ F)) → NaturalTransformation L M

    .σ-unique : {M : Functor B C} → {α : NaturalTransformation X (M ∘ F)} →
                (σ′ : NaturalTransformation L M) → α ≡ (σ′ ∘ʳ F) ∘₁ ε → σ′ ≡ σ M α
    .commutes : (M : Functor B C) → (α : NaturalTransformation X (M ∘ F)) → α ≡ (σ M α ∘ʳ F) ∘₁ ε

max_stars_repo_name: copumpkin/categories

max_issues_repo_name: p-pavel/categories

max_forks_repo_name: p-pavel/categories


text:
open import FRP.JS.Bool using ( Bool ; not )
open import FRP.JS.Event using ( Evt ; accumBy )
open import FRP.JS.RSet using ( RSet ; _⇒_ ; ⟦_⟧ ; ⟨_⟩ )

module FRP.JS.Behaviour where

postulate
  Beh : RSet → RSet
  map : ∀ {A B} → ⟦ A ⇒ B ⟧ → ⟦ Beh A ⇒ Beh B ⟧
  map2 : ∀ {A B C} → ⟦ A ⇒ B ⇒ C ⟧ → ⟦ Beh A ⇒ Beh B ⇒ Beh C ⟧
  [_] : ∀ {A} → A → ⟦ Beh ⟨ A ⟩ ⟧
  join : ∀ {A} → ⟦ Beh (Beh A) ⇒ Beh A ⟧
  hold : ∀ {A} → ⟦ ⟨ A ⟩ ⇒ Evt ⟨ A ⟩ ⇒ Beh ⟨ A ⟩ ⟧

{-# COMPILED_JS map function(A) { return function(B) {
  return function(f) { return function(s) { return function(b) {
    return b.map(function (t,v) { return f(t)(v); });
  }; }; };
}; } #-}

{-# COMPILED_JS map2 function(A) { return function(B) { return function(C) {
  return function(f) { return function(s) { return function(a) { return function(b) {
    return a.map2(b, function (t,v1,v2) { return f(t)(v1)(v2); });
  }; }; }; };
}; }; } #-}

{-# COMPILED_JS [_] function(A) { return function(a) { return function(s) {
  return require("agda.frp").constant(a);
}; }; } #-}

{-# COMPILED_JS join function(A) { return function(s) { return function(b) {
  return b.join();
}; }; } #-}

{-# COMPILED_JS hold function(A) { return function(s) { return function(a) { return function(e) {
  return e.hold(a);
}; }; }; } #-}

accumHoldBy : ∀ {A B} → ⟦ (⟨ B ⟩ ⇒ A ⇒ ⟨ B ⟩) ⟧ → B → ⟦ Evt A ⇒ Beh ⟨ B ⟩ ⟧
accumHoldBy f b σ = hold b (accumBy f b σ)

not* : ⟦ Beh ⟨ Bool ⟩ ⇒ Beh ⟨ Bool ⟩ ⟧
not* = map not

max_stars_repo_name: agda/agda-frp-js

max_issues_repo_name: agda/agda-frp-js

max_forks_repo_name: agda/agda-frp-js


text:
module Records where

open import Common.Nat
open import Common.IO
open import Common.Unit

record Test : Set where
  constructor mkTest
  field
    a b c : Nat

f : Test -> Nat
f (mkTest a b c) = a + b + c

open Test

g : Nat
g = (f (mkTest 34 12 54)) + (f (record {a = 100; b = 120; c = 140})) + a m + b m + c m
  where m = mkTest 200 300 400

main : IO Unit
main = printNat g

max_stars_repo_name: cruhland/agda

max_issues_repo_name: cruhland/agda

max_forks_repo_name: cruhland/agda


text:
------------------------------------------------------------------------
-- A depth-first backend
------------------------------------------------------------------------

-- Based on the parser combinators in Wadler's "How to Replace Failure
-- by a List of Successes".

module StructurallyRecursiveDescentParsing.DepthFirst where

open import Data.Bool
open import Data.Product as Prod
import Data.List as L; open L using (List)
import Data.List.Categorical
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec using ([]; _∷_)
open import Data.Vec.Bounded hiding ([]; _∷_)
open import Function
open import Category.Applicative.Indexed
open import Category.Monad.Indexed
open import Category.Monad.State
open import Codata.Musical.Notation
import Level

open import StructurallyRecursiveDescentParsing.Simplified

------------------------------------------------------------------------
-- Parser monad

private

  P : Set → IFun ℕ Level.zero
  P Tok = IStateT (Vec≤ Tok) List

  open module M₁ {Tok : Set} =
    RawIMonadPlus (StateTIMonadPlus (Vec≤ Tok)
                     Data.List.Categorical.monadPlus)
    using ()
    renaming ( return to return′
             ; _>>=_  to _>>=′_
             ; _>>_   to _>>′_
             ; ∅      to fail′
             ; _∣_    to _∣′_
             )

  open module M₂ {Tok : Set} =
    RawIMonadState (StateTIMonadState (Vec≤ Tok)
                      Data.List.Categorical.monad)
    using ()
    renaming ( get    to get′
             ; put    to put′
             ; modify to modify′
             )

------------------------------------------------------------------------
-- Run function for the parsers

-- For every successful parse the run function returns the remaining
-- string. (Since there can be several successful parses a list of
-- strings is returned.)

-- This function is structurally recursive with respect to the
-- following lexicographic measure:
--
-- 1) The upper bound of the length of the input string.
-- 2) The parser's proper left corner tree.

mutual
  parse↓ : ∀ {Tok e R} n → Parser Tok e R →
           P Tok n (if e then n else n ∸ 1) R
  parse↓ n       (return x)                  = return′ x
  parse↓ n       fail                        = fail′
  parse↓ n       (_∣_ {true}          p₁ p₂) = parse↓ n       p₁   ∣′       parse↑ n     p₂
  parse↓ n       (_∣_ {false} {true}  p₁ p₂) = parse↑ n       p₁   ∣′       parse↓ n     p₂
  parse↓ n       (_∣_ {false} {false} p₁ p₂) = parse↓ n       p₁   ∣′       parse↓ n     p₂
  parse↓ n       (p₁ ?>>= p₂)                = parse↓ n       p₁ >>=′ λ x → parse↓ n    (p₂ x)
  parse↓ zero    (p₁ !>>= p₂)                = fail′
  parse↓ (suc n) (p₁ !>>= p₂)                = parse↓ (suc n) p₁ >>=′ λ x → parse↑ n (♭ (p₂ x))
  parse↓ n       token                       = get′ >>=′ eat
    where
    eat : ∀ {Tok n} → Vec≤ Tok n → P Tok n (n ∸ 1) Tok
    eat ([] , _)      = fail′
    eat s@(c ∷ _ , _) = put′ (drop 1 s) >>′ return′ c

  parse↑ : ∀ {e Tok R} n → Parser Tok e R → P Tok n n R
  parse↑ {true}  n       p = parse↓ n p
  parse↑ {false} zero    p = fail′
  parse↑ {false} (suc n) p = parse↓ (suc n) p           >>=′ λ r →
                             modify′ (≤-cast (n≤1+n _)) >>′
                             return′ r

-- Exported run function.

parse : ∀ {Tok i R} → Parser Tok i R → List Tok → List (R × List Tok)
parse p s = L.map (Prod.map id toList) (parse↓ _ p (fromList s))

-- A variant which only returns parses which leave no remaining input.

parseComplete : ∀ {Tok i R} → Parser Tok i R → List Tok → List R
parseComplete p s =
  L.map proj₁ (L.boolFilter (L.null ∘ proj₂) (parse p s))

max_stars_repo_name: nad/parser-combinators

max_issues_repo_name: nad/parser-combinators

max_forks_repo_name: nad/parser-combinators


text:
------------------------------------------------------------------------------
-- Arithmetic properties using instances of the induction principle
------------------------------------------------------------------------------

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

module FOT.FOTC.Data.Nat.Induction.AdditionalHypothesis.Instances.PropertiesATP
  where

open import FOTC.Base
open import FOTC.Data.Nat hiding ( N-ind )

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

-- Induction principle with the additional hypothesis.
N-ind₁ : (A : D → Set) →
         A zero →
         (∀ {n} → N n → A n → A (succ₁ n)) →
         ∀ {n} → N n → A n
N-ind₁ A A0 h nzero      = A0
N-ind₁ A A0 h (nsucc Nn) = h Nn (N-ind₁ A A0 h Nn)

-- From now on we will use the N-ind₁ induction principle.
N-ind = N-ind₁

------------------------------------------------------------------------------
-- Totality properties

pred-N-ind-instance :
  N (pred₁ zero) →
  (∀ {n} → N n → N (pred₁ n) → N (pred₁ (succ₁ n))) →
  ∀ {n} → N n → N (pred₁ n)
pred-N-ind-instance = N-ind₁ (λ i → N (pred₁ i))

postulate pred-N : ∀ {n} → N n → N (pred₁ n)
{-# ATP prove pred-N pred-N-ind-instance #-}

+-N-ind-instance :
  ∀ {n} →
  N (zero + n) →
  (∀ {m} → N m → N (m + n) → N (succ₁ m + n)) →
  ∀ {m} → N m → N (m + n)
+-N-ind-instance {n} = N-ind (λ i → N (i + n))

postulate +-N : ∀ {m n} → N m → N n → N (m + n)
{-# ATP prove +-N +-N-ind-instance #-}

∸-N-ind-instance :
  ∀ {m} →
  N (m ∸ zero) →
  (∀ {n} → N n → N (m ∸ n) → N (m ∸ succ₁ n)) →
  ∀ {n} → N n → N (m ∸ n)
∸-N-ind-instance {n} = N-ind (λ i → N (n ∸ i))

postulate ∸-N : ∀ {m n} → N m → N n → N (m ∸ n)
{-# ATP prove ∸-N ∸-N-ind-instance pred-N #-}

*-N-ind-instance :
  ∀ {n} →
  N (zero * n) →
  (∀ {m} → N m → N (m * n) → N (succ₁ m * n)) →
  ∀ {m} → N m → N (m * n)
*-N-ind-instance {n} = N-ind (λ i → N (i * n))

postulate *-N : ∀ {m n} → N m → N n → N (m * n)
{-# ATP prove *-N *-N-ind-instance +-N #-}

+-rightIdentity-ind-instance :
  zero + zero ≡ zero →
  (∀ {n} → N n → n + zero ≡ n → succ₁ n + zero ≡ succ₁ n) →
  ∀ {n} → N n → n + zero ≡ n
+-rightIdentity-ind-instance = N-ind (λ i → i + zero ≡ i)

postulate +-rightIdentity : ∀ {n} → N n → n + zero ≡ n
{-# ATP prove +-rightIdentity +-rightIdentity-ind-instance #-}

+-assoc-ind-instance :
  ∀ {n} {o} →
  zero + n + o ≡ zero + (n + o) →
  (∀ {m} → N m →
    m + n + o ≡ m + (n + o) → succ₁ m + n + o ≡ succ₁ m + (n + o)) →
  ∀ {m} → N m → m + n + o ≡ m + (n + o)
+-assoc-ind-instance {n} {o} = N-ind (λ i → i + n + o ≡ i + (n + o))

postulate +-assoc : ∀ {m} → N m → ∀ n o → m + n + o ≡ m + (n + o)
{-# ATP prove +-assoc +-assoc-ind-instance #-}

x+Sy≡S[x+y]-ind-instance :
  ∀ {n} →
  zero + succ₁ n ≡ succ₁ (zero + n) →
  (∀ {m} → N m →
    m + succ₁ n ≡ succ₁ (m + n) → succ₁ m + succ₁ n ≡ succ₁ (succ₁ m + n)) →
  ∀ {m} → N m → m + succ₁ n ≡ succ₁ (m + n)
x+Sy≡S[x+y]-ind-instance {n} = N-ind (λ i → i + succ₁ n ≡ succ₁ (i + n))

postulate x+Sy≡S[x+y] : ∀ {m} → N m → ∀ n → m + succ₁ n ≡ succ₁ (m + n)
{-# ATP prove x+Sy≡S[x+y] x+Sy≡S[x+y]-ind-instance #-}

+-comm-ind-instance :
  ∀ {n} →
  zero + n ≡ n + zero →
  (∀ {m} → N m → m + n ≡ n + m → succ₁ m + n ≡ n + succ₁ m) →
  ∀ {m} → N m → m + n ≡ n + m
+-comm-ind-instance {n} = N-ind (λ i → i + n ≡ n + i)

postulate +-comm : ∀ {m n} → N m → N n → m + n ≡ n + m
{-# ATP prove +-comm +-comm-ind-instance +-rightIdentity x+Sy≡S[x+y] #-}

max_stars_repo_name: asr/fotc

max_issues_repo_name: asr/fotc

max_forks_repo_name: asr/fotc


text:
postulate
  A : Set

data B (a : A) : Set where
  conB : B a → B a → B a

data C (a : A) : B a → Set where
  conC : {bl br : B a} → C a bl → C a br → C a (conB bl br)

-- Second bug, likely same as first bug.
{-
An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Abstract.hs:133
-}
data F : Set where
  conF : F

boo : (a : A) (b : B a) (c : C a _) → Set
boo a b (conC tl tr) with tr | conF
... | _ | _ = _

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda