text:
module Esterel.Lang.CanFunction.MergePotentialRuleLeftBase where

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.Lang.CanFunction.CanThetaContinuation
open import Esterel.Lang.CanFunction.MergePotentialRuleCan
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

distinct'-S∷Ss⇒[S] : ∀ {xs S Ss} status →
  distinct' xs (S ∷ Ss) →
  distinct' xs (proj₁ (Dom [ (S ₛ) ↦ status ] ))
distinct'-S∷Ss⇒[S] {xs} {S} {Ss} status xs≠S∷Ss S' S'∈xs S'∈[S]
  rewrite Env.sig-single-∈-eq (S' ₛ) (S ₛ) status S'∈[S]
  = xs≠S∷Ss S S'∈xs (here refl)

canθₖ-mergeˡ-E-induction-base-par₁ : ∀ {E q E⟦nothin⟧∥q BV FV} sigs' S' r θ →
  E⟦nothin⟧∥q ≐ (epar₁ q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧∥q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
    Canθₖ sigs' S' ((E ⟦ r ⟧e) ∥ q) θ ≡
    concatMap (λ k → map (Code._⊔_ k) (Canₖ q θ)) (Canθₖ sigs' S' (E ⟦ r ⟧e) θ)
canθₖ-mergeˡ-E-induction-base-par₁ [] S' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  = refl
canθₖ-mergeˡ-E-induction-base-par₁ (nothing ∷ sigs') S' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₖ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (depar₁ E⟦nothin⟧) cb FV≠sigs'
canθₖ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.present ∷ sigs') S' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r
            (θ ← [S]-env-present (S' ₛ)) (depar₁ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
canθₖ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.absent ∷ sigs') S' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (depar₁ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
canθₖ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) ∥ q) (θ ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-E⟦r⟧∥q-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r
            (θ ← [S]-env (S' ₛ)) (depar₁ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
... | no  S'∉canθ-sigs'-E⟦r⟧∥q-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (depar₁ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
... | yes S'∈canθ-sigs'-E⟦r⟧∥q-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←[S']
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← [S]-env (S' ₛ))
          (depar₁ dehole) (CBpar CBnothing cbq distinct-empty-left distinct-empty-left
                                               distinct-empty-left (λ _ ()))
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧∥q-θ←[S']))
... | no  S'∉canθ-sigs'-E⟦r⟧∥q-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S'] =
  ⊥-elim
    (S'∉canθ-sigs'-E⟦r⟧∥q-θ←[S']
      (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← [S]-env (S' ₛ))
        (epar₁ q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←[S']))

canθₖ-mergeˡ-E-induction-base-par₂ : ∀ {E q q∥E⟦nothin⟧ BV FV} sigs' S' r θ →
  q∥E⟦nothin⟧ ≐ (epar₂ q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding q∥E⟦nothin⟧ BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
    Canθₖ sigs' S' (q ∥ (E ⟦ r ⟧e)) θ ≡
    concatMap (λ k → map (Code._⊔_ k) (Canθₖ sigs' S' (E ⟦ r ⟧e) θ)) (Canₖ q θ)
canθₖ-mergeˡ-E-induction-base-par₂ [] S' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  = refl
canθₖ-mergeˡ-E-induction-base-par₂ (nothing ∷ sigs') S' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₖ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (depar₂ E⟦nothin⟧) cb FV≠sigs'
canθₖ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.present ∷ sigs') S' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left dist'++ˡ
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r
            (θ ← [S]-env-present (S' ₛ)) (depar₂ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
canθₖ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.absent ∷ sigs') S' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left dist'++ˡ
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (depar₂ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
canθₖ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  with any (_≟_ S') (Canθₛ sigs' (suc S') (q ∥ (E ⟦ r ⟧e)) (θ ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-q∥E⟦r⟧-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left dist'++ˡ
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r
            (θ ← [S]-env (S' ₛ)) (depar₂ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
... | no  S'∉canθ-sigs'-q∥E⟦r⟧-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left dist'++ˡ
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (depar₂ E⟦nothin⟧)
            cb (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')
        = refl
... | yes S'∈canθ-sigs'-q∥E⟦r⟧-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←[S']
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← [S]-env (S' ₛ))
          (depar₂ dehole) (CBpar cbq CBnothing distinct-empty-right distinct-empty-right
                                               distinct-empty-right (λ _ _ ()))
          (λ S' S'∈map-+-suc-S'-sigs' S'∈FVq++[] →
            FV≠sigs' S' (++ˡ (x∈xs++[]→x∈xs {xs = proj₁ FVp} S'∈FVq++[]))
              (there S'∈map-+-suc-S'-sigs'))
          (S' ₛ)
          (λ S'∈FVq++[] →
            FV≠sigs' S' (++ˡ (x∈xs++[]→x∈xs {xs = proj₁ FVp} S'∈FVq++[])) (here refl))
          S'∈canθ-sigs'-q∥E⟦r⟧-θ←[S']))
... | no  S'∉canθ-sigs'-q∥E⟦r⟧-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S'] =
  ⊥-elim
    (S'∉canθ-sigs'-q∥E⟦r⟧-θ←[S']
      (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← [S]-env (S' ₛ))
        (epar₂ q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←[S']))

canθₖ-mergeˡ-E-induction-base-seq-notin : ∀ {E q E⟦nothin⟧>>q BV FV} sigs' S' r θ →
  E⟦nothin⟧>>q ≐ (eseq q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧>>q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  Code.nothin ∉ Canθₖ sigs' S' (E ⟦ r ⟧e) θ →
    Canθₖ sigs' S' ((E ⟦ r ⟧e) >> q) θ ≡
    Canθₖ sigs' S' (E ⟦ r ⟧e) θ
canθₖ-mergeˡ-E-induction-base-seq-notin {E} [] S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∉canθ-sigs'-E⟦r⟧-θ
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ r ⟧e) θ)
... | no  nothin∉can-E⟦r⟧-θ = refl
... | yes nothin∈can-E⟦r⟧-θ = ⊥-elim (nothin∉canθ-sigs'-E⟦r⟧-θ nothin∈can-E⟦r⟧-θ)
canθₖ-mergeˡ-E-induction-base-seq-notin (nothing ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∉canθ-sigs'-E⟦r⟧-θ
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | canθₖ-mergeˡ-E-induction-base-seq-notin sigs' (suc S') r
            θ (deseq E⟦nothin⟧) cb FV≠sigs' nothin∉canθ-sigs'-E⟦r⟧-θ
  = refl
canθₖ-mergeˡ-E-induction-base-seq-notin {E} (just Signal.present ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∉canθ-sigs'-E⟦r⟧-θ
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | canθₖ-mergeˡ-E-induction-base-seq-notin sigs' (suc S') r
            (θ ← [S]-env-present (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs') nothin∉canθ-sigs'-E⟦r⟧-θ
  = refl
canθₖ-mergeˡ-E-induction-base-seq-notin {E} (just Signal.absent ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∉canθ-sigs'-E⟦r⟧-θ
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | canθₖ-mergeˡ-E-induction-base-seq-notin sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs') nothin∉canθ-sigs'-E⟦r⟧-θ
  = refl
canθₖ-mergeˡ-E-induction-base-seq-notin {E} {q} (just Signal.unknown ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∉canθ-sigs'-E⟦r⟧-θ
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) >> q) (θ ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | canθₖ-mergeˡ-E-induction-base-seq-notin sigs' (suc S') r
            (θ ← [S]-env (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs') nothin∉canθ-sigs'-E⟦r⟧-θ
  = refl
... | no  S'∉canθ-sigs'-E⟦r⟧>>q-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | canθₖ-mergeˡ-E-induction-base-seq-notin sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs') nothin∉canθ-sigs'-E⟦r⟧-θ
  = refl
... | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←[S']
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← [S]-env (S' ₛ))
          (deseq dehole) (CBseq CBnothing cbq distinct-empty-left)
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧>>q-θ←[S']))
... | no  S'∉canθ-sigs'-E⟦r⟧>>q-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S'] =
  ⊥-elim
    (S'∉canθ-sigs'-E⟦r⟧>>q-θ←[S']
      (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← [S]-env (S' ₛ))
        (eseq q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←[S']))

canθₖ-mergeˡ-E-induction-base-seq-in : ∀ {E q E⟦nothin⟧>>q BV FV} sigs' S' r θ →
  E⟦nothin⟧>>q ≐ (eseq q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧>>q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  Code.nothin ∈ Canθₖ sigs' S' (E ⟦ r ⟧e) θ →
    Canθₖ sigs' S' ((E ⟦ r ⟧e) >> q) θ ≡
    CodeSet.set-remove (Canθₖ sigs' S' (E ⟦ r ⟧e) θ) Code.nothin ++ Canₖ q θ
canθₖ-mergeˡ-E-induction-base-seq-in {E} [] S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∈canθ-sigs'-E⟦r⟧-θ
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ r ⟧e) θ)
... | no  nothin∉can-E⟦r⟧-θ = ⊥-elim (nothin∉can-E⟦r⟧-θ nothin∈canθ-sigs'-E⟦r⟧-θ)
... | yes nothin∈can-E⟦r⟧-θ = refl
canθₖ-mergeˡ-E-induction-base-seq-in (nothing ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∈canθ-sigs'-E⟦r⟧-θ
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | canθₖ-mergeˡ-E-induction-base-seq-in sigs' (suc S') r
            θ (deseq E⟦nothin⟧) cb FV≠sigs' nothin∈canθ-sigs'-E⟦r⟧-θ
  = refl
canθₖ-mergeˡ-E-induction-base-seq-in {E} {q} (just Signal.present ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∈canθ-sigs'-E⟦r⟧-θ
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-seq-in sigs' (suc S') r
            (θ ← [S]-env-present (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' ∷ []} FV≠sigs') nothin∈canθ-sigs'-E⟦r⟧-θ
  = refl
canθₖ-mergeˡ-E-induction-base-seq-in {E} {q} (just Signal.absent ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∈canθ-sigs'-E⟦r⟧-θ
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-seq-in sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' ∷ []} FV≠sigs') nothin∈canθ-sigs'-E⟦r⟧-θ
  = refl
canθₖ-mergeˡ-E-induction-base-seq-in {E} {q} (just Signal.unknown ∷ sigs') S' r θ
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} cbp cbq _) FV≠sigs' nothin∈canθ-sigs'-E⟦r⟧-θ
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) >> q) (θ ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) (θ ← [S]-env (S' ₛ)))
... | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-seq-in sigs' (suc S') r
            (θ ← [S]-env (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' ∷ []} FV≠sigs') nothin∈canθ-sigs'-E⟦r⟧-θ
  = refl
... | no  S'∉canθ-sigs'-E⟦r⟧>>q-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite +-comm S' 0
        | map-+-compose-suc S' (SigMap.keys sigs')
        | can-irr θ ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | canθₖ-mergeˡ-E-induction-base-seq-in sigs' (suc S') r
            (θ ← [S]-env-absent (S' ₛ)) (deseq E⟦nothin⟧) cb
            (dist'++ʳ {V2 = S' ∷ []} FV≠sigs') nothin∈canθ-sigs'-E⟦r⟧-θ
  = refl
... | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←[S'] | no  S'∉canθ-sigs'-E⟦r⟧-θ←[S']
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←[S']
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← [S]-env (S' ₛ))
          (deseq dehole) (CBseq CBnothing cbq distinct-empty-left)
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧>>q-θ←[S']))
... | no  S'∉canθ-sigs'-E⟦r⟧>>q-θ←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←[S'] =
  ⊥-elim
    (S'∉canθ-sigs'-E⟦r⟧>>q-θ←[S']
      (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← [S]-env (S' ₛ))
        (eseq q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←[S']))

canθₛ-mergeˡ-E-induction-base-par₁ : ∀ {E q E⟦nothin⟧∥q BV FV} sigs' S' r θ θo →
  E⟦nothin⟧∥q ≐ (epar₁ q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧∥q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  ∀ S'' →
    S'' ∈ Canθₛ sigs' S' ((E ⟦ r ⟧e) ∥ q) (θ ← θo) →
    S'' ∈ Canθₛ sigs' S' (E ⟦ r ⟧e) (θ ← θo) ⊎ S'' ∈ Canₛ q (θ ← θo)
canθₛ-mergeˡ-E-induction-base-par₁ {E} [] S' r θ θo
  E⟦nothin⟧∥q cb FV≠sigs' S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  with ++⁻ (Canₛ (E ⟦ r ⟧e) (θ ← θo)) S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ S''∈can-E⟦r⟧-θ←θo = inj₁ S''∈can-E⟦r⟧-θ←θo
... | inj₂ S''∈can-q-θ←θo = inj₂ S''∈can-q-θ←θo
canθₛ-mergeˡ-E-induction-base-par₁ (nothing ∷ sigs') S' r θ θo
  E⟦nothin⟧∥q cb FV≠sigs' S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₛ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ θo E⟦nothin⟧∥q cb
      FV≠sigs' S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.present ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-present (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env-present (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present]
... | inj₂ S''∈can-q-θ←θo←[S'↦present]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-present (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦present]
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.absent ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ S''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦absent]
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb FV≠sigs' S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) ∥ q) ((θ ← θo) ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) ((θ ← θo) ← [S]-env (S' ₛ)))
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown]
... | inj₂ S''∈can-q-θ←θo←[S'↦unknown]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦unknown]
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | no  S'∉canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ S''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦absent]
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | no  S'∉canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧∥q-θ←θo←[S]
        (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (epar₁ q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]))
canθₛ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbp cbq _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (depar₁ dehole) (CBpar CBnothing cbq distinct-empty-left distinct-empty-left
                                               distinct-empty-left (λ _ ()))
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧∥q-θ←θo←[S]))

canθₛ-mergeˡ-E-induction-base-par₂ : ∀ {E q q∥E⟦nothin⟧ BV FV} sigs' S' r θ θo →
  q∥E⟦nothin⟧ ≐ (epar₂ q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding q∥E⟦nothin⟧ BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  ∀ S'' →
    S'' ∈ Canθₛ sigs' S' (q ∥ (E ⟦ r ⟧e)) (θ ← θo) →
    S'' ∈ Canθₛ sigs' S' (E ⟦ r ⟧e) (θ ← θo) ⊎ S'' ∈ Canₛ q (θ ← θo)
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} [] S' r θ θo
  q∥E⟦nothin⟧ cb FV≠sigs' S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  with ++⁻ (Canₛ q (θ ← θo)) S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₂ S''∈can-E⟦r⟧-θ←θo = inj₁ S''∈can-E⟦r⟧-θ←θo
... | inj₁ S''∈can-q-θ←θo = inj₂ S''∈can-q-θ←θo
canθₛ-mergeˡ-E-induction-base-par₂ (nothing ∷ sigs') S' r θ θo
  q∥E⟦nothin⟧ cb FV≠sigs' S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₛ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ θo q∥E⟦nothin⟧ cb
      FV≠sigs' S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.present ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-present (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env-present (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present]
... | inj₂ S''∈can-q-θ←θo←[S'↦present]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-present (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦present]
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.absent ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ S''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦absent]
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb FV≠sigs' S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  with any (_≟_ S') (Canθₛ sigs' (suc S') (q ∥ (E ⟦ r ⟧e)) ((θ ← θo) ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) ((θ ← θo) ← [S]-env (S' ₛ)))
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | yes S'∈canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown]
... | inj₂ S''∈can-q-θ←θo←[S'↦unknown]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦unknown]
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | no  S'∉canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ S''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ S''∈can-q-θ←θo←[S'↦absent]
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | no  S'∉canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
  = ⊥-elim
      (S'∉canθ-sigs'-q∥E⟦r⟧-θ←θo←[S]
        (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (epar₂ q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]))
canθₛ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  S'' S''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | yes S'∈canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (depar₂ dehole) (CBpar cbq CBnothing distinct-empty-right distinct-empty-right
                                               distinct-empty-right (λ _ _ ()))
          (λ S''' S'''∈map-+-suc-S'-sigs' S'''∈FVq++[] →
            FV≠sigs' S''' (++ˡ (x∈xs++[]→x∈xs {xs = proj₁ FVp} S'''∈FVq++[]))
              (there S'''∈map-+-suc-S'-sigs'))
          (S' ₛ) (λ S'∈FVq++[] → FV≠sigs' S' (++ˡ (x∈xs++[]→x∈xs {xs = proj₁ FVp} S'∈FVq++[])) (here refl))
          S'∈canθ-sigs'-q∥E⟦r⟧-θ←θo←[S]))

canθₛ-mergeˡ-E-induction-base-seq : ∀ {E q E⟦nothin⟧>>q BV FV} sigs' S' r θ θo →
  E⟦nothin⟧>>q ≐ (eseq q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧>>q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  ∀ S'' →
    S'' ∈ Canθₛ sigs' S' ((E ⟦ r ⟧e) >> q) (θ ← θo) →
      S'' ∈ Canθₛ sigs' S' (E ⟦ r ⟧e) (θ ← θo) ⊎
      (S'' ∈ Canₛ q (θ ← θo) × Code.nothin ∈ Canθₖ sigs' S' (E ⟦ r ⟧e) (θ ← θo))
canθₛ-mergeˡ-E-induction-base-seq {E} {q} [] S' r θ θo
  E⟦nothin⟧>>q cb FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ r ⟧e) (θ ← θo))
... | no  nothin∉can-E⟦r⟧-θ←θo = inj₁ S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | yes nothin∈can-E⟦r⟧-θ←θo
  with ++⁻ (Canₛ (E ⟦ r ⟧e) (θ ← θo)) S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ S''∈can-E⟦r⟧-θ←θo = inj₁ S''∈can-E⟦r⟧-θ←θo
... | inj₂ S''∈can-q-θ←θo = inj₂ (S''∈can-q-θ←θo ,′ nothin∈can-E⟦r⟧-θ←θo)
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (nothing ∷ sigs') S' r θ θo E⟦nothin⟧>>q
  cb FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₛ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ θo
      E⟦nothin⟧>>q cb FV≠sigs' S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.present ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-present (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env-present (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present]
... | inj₂ (S''∈can-q-θ←θo←[S'↦present] , nothin∈can-E⟦r⟧-θ←θo←[S'↦present])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-present (S' ₛ))
  = inj₂ (S''∈can-q-θ←θo←[S'↦present] , nothin∈can-E⟦r⟧-θ←θo←[S'↦present])
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.absent ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ (S''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ (S''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) >> q) ((θ ← θo) ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) ((θ ← θo) ← [S]-env (S' ₛ)))
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown]
... | inj₂ (S''∈can-q-θ←θo←[S'↦unknown] , nothin∈can-E⟦r⟧-θ←θo←[S'↦unknown])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env (S' ₛ))
  = inj₂ (S''∈can-q-θ←θo←[S'↦unknown] , nothin∈can-E⟦r⟧-θ←θo←[S'↦unknown])
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | no S'∉canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | no S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ S''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ (S''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ (S''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | no S'∉canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧>>q-θ←θo←[S']
        (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (eseq q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S']))
canθₛ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  S'' S''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | no S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S']
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (deseq dehole) (CBseq CBnothing cbq distinct-empty-left)
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧>>q-θ←θo←[S']))

canθₛₕ-mergeˡ-E-induction-base-par₁ : ∀ {E q E⟦nothin⟧∥q BV FV} sigs' S' r θ θo →
  E⟦nothin⟧∥q ≐ (epar₁ q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧∥q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  ∀ s'' →
    s'' ∈ Canθₛₕ sigs' S' ((E ⟦ r ⟧e) ∥ q) (θ ← θo) →
    s'' ∈ Canθₛₕ sigs' S' (E ⟦ r ⟧e) (θ ← θo) ⊎ s'' ∈ Canₛₕ q (θ ← θo)
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} [] S' r θ θo
  E⟦nothin⟧∥q cb FV≠sigs' s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  with ++⁻ (Canₛₕ (E ⟦ r ⟧e) (θ ← θo)) s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ s''∈can-E⟦r⟧-θ←θo = inj₁ s''∈can-E⟦r⟧-θ←θo
... | inj₂ s''∈can-q-θ←θo = inj₂ s''∈can-q-θ←θo
canθₛₕ-mergeˡ-E-induction-base-par₁ (nothing ∷ sigs') S' r θ θo
  E⟦nothin⟧∥q cb FV≠sigs' s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₛₕ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ θo E⟦nothin⟧∥q cb
      FV≠sigs' s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.present ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-present (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env-present (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present]
... | inj₂ s''∈can-q-θ←θo←[S'↦present]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-present (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦present]
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.absent ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ s''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦absent]
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb FV≠sigs' s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) ∥ q) ((θ ← θo) ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) ((θ ← θo) ← [S]-env (S' ₛ)))
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown]
... | inj₂ s''∈can-q-θ←θo←[S'↦unknown]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦unknown]
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | no  S'∉canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₁ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₁ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ s''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦absent]
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} _ cbq _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | no  S'∉canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧∥q-θ←θo←[S]
        (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (epar₁ q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]))
canθₛₕ-mergeˡ-E-induction-base-par₁ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₁ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbp cbq _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧∥q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧∥q-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (depar₁ dehole) (CBpar CBnothing cbq distinct-empty-left distinct-empty-left
                                               distinct-empty-left (λ _ ()))
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧∥q-θ←θo←[S]))

canθₛₕ-mergeˡ-E-induction-base-par₂ : ∀ {E q q∥E⟦nothin⟧ BV FV} sigs' S' r θ θo →
  q∥E⟦nothin⟧ ≐ (epar₂ q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding q∥E⟦nothin⟧ BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  ∀ s'' →
    s'' ∈ Canθₛₕ sigs' S' (q ∥ (E ⟦ r ⟧e)) (θ ← θo) →
    s'' ∈ Canθₛₕ sigs' S' (E ⟦ r ⟧e) (θ ← θo) ⊎ s'' ∈ Canₛₕ q (θ ← θo)
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} [] S' r θ θo
  q∥E⟦nothin⟧ cb FV≠sigs' s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  with ++⁻ (Canₛₕ q (θ ← θo)) s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₂ s''∈can-E⟦r⟧-θ←θo = inj₁ s''∈can-E⟦r⟧-θ←θo
... | inj₁ s''∈can-q-θ←θo = inj₂ s''∈can-q-θ←θo
canθₛₕ-mergeˡ-E-induction-base-par₂ (nothing ∷ sigs') S' r θ θo
  q∥E⟦nothin⟧ cb FV≠sigs' s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₛₕ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ θo q∥E⟦nothin⟧ cb
      FV≠sigs' s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.present ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-present (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env-present (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present]
... | inj₂ s''∈can-q-θ←θo←[S'↦present]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-present (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦present]
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.absent ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ s''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦absent]
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb FV≠sigs' s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  with any (_≟_ S') (Canθₛ sigs' (suc S') (q ∥ (E ⟦ r ⟧e)) ((θ ← θo) ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) ((θ ← θo) ← [S]-env (S' ₛ)))
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | yes S'∈canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown]
... | inj₂ s''∈can-q-θ←θo←[S'↦unknown]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦unknown]
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | no  S'∉canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-par₂ sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (depar₂ E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ s''∈can-q-θ←θo←[S'↦absent]
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ˡ)
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ s''∈can-q-θ←θo←[S'↦absent]
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar cbq _ _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | no  S'∉canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
  = ⊥-elim
      (S'∉canθ-sigs'-q∥E⟦r⟧-θ←θo←[S]
        (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (epar₂ q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S]))
canθₛₕ-mergeˡ-E-induction-base-par₂ {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (depar₂ E⟦nothin⟧) cb@(CBpar {FVp = FVp} cbq _ _ _ _ _) FV≠sigs'
  s'' s''∈canθ-sigs'-q∥E⟦r⟧-θ←θo
  | yes S'∈canθ-sigs'-q∥E⟦r⟧-θ←θo←[S] | no  S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S]
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (depar₂ dehole) (CBpar cbq CBnothing distinct-empty-right distinct-empty-right
                                               distinct-empty-right (λ _ _ ()))
          (λ s''' s'''∈map-+-suc-S'-sigs' s'''∈FVq++[] →
            FV≠sigs' s''' (++ˡ (x∈xs++[]→x∈xs {xs = proj₁ FVp} s'''∈FVq++[]))
              (there s'''∈map-+-suc-S'-sigs'))
          (S' ₛ) (λ S'∈FVq++[] → FV≠sigs' S' (++ˡ (x∈xs++[]→x∈xs {xs = proj₁ FVp} S'∈FVq++[])) (here refl))
          S'∈canθ-sigs'-q∥E⟦r⟧-θ←θo←[S]))

canθₛₕ-mergeˡ-E-induction-base-seq : ∀ {E q E⟦nothin⟧>>q BV FV} sigs' S' r θ θo →
  E⟦nothin⟧>>q ≐ (eseq q ∷ E) ⟦ nothin ⟧e →
  CorrectBinding E⟦nothin⟧>>q BV FV →
  distinct' (proj₁ FV) (map (_+_ S') (SigMap.keys sigs')) →
  ∀ s'' →
    s'' ∈ Canθₛₕ sigs' S' ((E ⟦ r ⟧e) >> q) (θ ← θo) →
      s'' ∈ Canθₛₕ sigs' S' (E ⟦ r ⟧e) (θ ← θo) ⊎
      (s'' ∈ Canₛₕ q (θ ← θo) × Code.nothin ∈ Canθₖ sigs' S' (E ⟦ r ⟧e) (θ ← θo))
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} [] S' r θ θo
  E⟦nothin⟧>>q cb FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  with any (Code._≟_ Code.nothin) (Canₖ (E ⟦ r ⟧e) (θ ← θo))
... | no  nothin∉can-E⟦r⟧-θ←θo = inj₁ s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | yes nothin∈can-E⟦r⟧-θ←θo
  with ++⁻ (Canₛₕ (E ⟦ r ⟧e) (θ ← θo)) s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ s''∈can-E⟦r⟧-θ←θo = inj₁ s''∈can-E⟦r⟧-θ←θo
... | inj₂ s''∈can-q-θ←θo = inj₂ (s''∈can-q-θ←θo ,′ nothin∈can-E⟦r⟧-θ←θo)
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (nothing ∷ sigs') S' r θ θo E⟦nothin⟧>>q
  cb FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  rewrite map-+-compose-suc S' (SigMap.keys sigs')
  = canθₛₕ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ θo
      E⟦nothin⟧>>q cb FV≠sigs' s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.present ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-present (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env-present (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦present]
... | inj₂ (s''∈can-q-θ←θo←[S'↦present] , nothin∈can-E⟦r⟧-θ←θo←[S'↦present])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-present (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.present FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-present (S' ₛ))
  = inj₂ (s''∈can-q-θ←θo←[S'↦present] , nothin∈can-E⟦r⟧-θ←θo←[S'↦present])
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.absent ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ (s''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ (s''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  with any (_≟_ S') (Canθₛ sigs' (suc S') ((E ⟦ r ⟧e) >> q) ((θ ← θo) ← [S]-env (S' ₛ)))
     | any (_≟_ S') (Canθₛ sigs' (suc S') (E ⟦ r ⟧e) ((θ ← θo) ← [S]-env (S' ₛ)))
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦unknown]
... | inj₂ (s''∈can-q-θ←θo←[S'↦unknown] , nothin∈can-E⟦r⟧-θ←θo←[S'↦unknown])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.unknown FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env (S' ₛ))
  = inj₂ (s''∈can-q-θ←θo←[S'↦unknown] , nothin∈can-E⟦r⟧-θ←θo←[S'↦unknown])
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | no S'∉canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | no S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env-absent (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
  with canθₛₕ-mergeˡ-E-induction-base-seq sigs' (suc S') r θ (θo ← [S]-env-absent (S' ₛ))
         (deseq E⟦nothin⟧) cb (dist'++ʳ {V2 = S' + 0 ∷ []} FV≠sigs')
         s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
... | inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent] =
  inj₁ s''∈canθ-sigs'-E⟦r⟧-θ←θo←[S'↦absent]
... | inj₂ (s''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
  rewrite +-comm S' 0
        | can-irr (θ ← θo) ([S]-env-absent (S' ₛ)) q cbq
            (distinct'-to-left (dist'++ʳ {V2 = proj₁ FVp})
              (distinct'-S∷Ss⇒[S] Signal.absent FV≠sigs'))
        | Env.←-assoc θ θo ([S]-env-absent (S' ₛ))
  = inj₂ (s''∈can-q-θ←θo←[S'↦absent] , nothin∈can-E⟦r⟧-θ←θo←[S'↦absent])
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | no S'∉canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | yes S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧>>q-θ←θo←[S']
        (canθₛ-p⊆canθₛ-E₁⟦p⟧ sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (eseq q) (E ⟦ r ⟧e) (S' ₛ) S'∈canθ-sigs'-E⟦r⟧-θ←θo←[S']))
canθₛₕ-mergeˡ-E-induction-base-seq {E} {q} (just Signal.unknown ∷ sigs') S' r θ θo
  (deseq E⟦nothin⟧) cb@(CBseq {FVp = FVp} _ cbq _) FV≠sigs'
  s'' s''∈canθ-sigs'-E⟦r⟧>>q-θ←θo
  | yes S'∈canθ-sigs'-E⟦r⟧>>q-θ←θo←[S'] | no S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S']
  rewrite sym (Env.←-assoc θ θo ([S]-env (S' ₛ)))
        | map-+-compose-suc S' (SigMap.keys sigs')
        | +-comm S' 0
  = ⊥-elim
      (S'∉canθ-sigs'-E⟦r⟧-θ←θo←[S']
        (canθₛ-E₁⟦p⟧⊆canθₛ-p sigs' (suc S') (θ ← (θo ← [S]-env (S' ₛ)))
          (deseq dehole) (CBseq CBnothing cbq distinct-empty-left)
          (dist'++ʳ {V2 = proj₁ FVp} (distinct'-sym (dist'++ʳ {V2 = S' ∷ []} FV≠sigs')))
          (S' ₛ) (λ S'∈FVq → FV≠sigs' S' (++ʳ (proj₁ FVp) S'∈FVq) (here refl))
          S'∈canθ-sigs'-E⟦r⟧>>q-θ←θo←[S']))

max_stars_repo_name: florence/esterel-calculus

max_issues_repo_name: florence/esterel-calculus

max_forks_repo_name: florence/esterel-calculus


text:
{-
This second-order signature was created from the following second-order syntax description:

syntax CommMonoid | CM

type
  * : 0-ary

term
  unit : * | ε
  add  : *  *  ->  * | _⊕_ l20

theory
  (εU⊕ᴸ) a |> add (unit, a) = a
  (εU⊕ᴿ) a |> add (a, unit) = a
  (⊕A) a b c |> add (add(a, b), c) = add (a, add(b, c))
  (⊕C) a b |> add(a, b) = add(b, a)
-}

module CommMonoid.Signature where

open import SOAS.Context

open import SOAS.Common

open import SOAS.Syntax.Signature *T public
open import SOAS.Syntax.Build *T public

-- Operator symbols
data CMₒ : Set where
  unitₒ addₒ : CMₒ

-- Term signature
CM:Sig : Signature CMₒ
CM:Sig = sig λ
  {  unitₒ  → ⟼₀ *
  ;  addₒ   → (⊢₀ *) , (⊢₀ *) ⟼₂ *
  }

open Signature CM:Sig public

ext: agda

max_stars_repo_name: JoeyEremondi/agda-soas

max_issues_repo_name: JoeyEremondi/agda-soas

max_forks_repo_name: JoeyEremondi/agda-soas


text:
{-#  OPTIONS --type-in-type #-}
module AgdaPrelude where

data Nat : Set where
  Zero : Nat
  Succ : Nat -> Nat

natElim : (m : Nat -> Set) -> (mz : m Zero) -> (ms : (l : Nat) -> m l -> m (Succ l)) -> (k : Nat) -> m k
natElim m mz ms Zero = mz
natElim m mz ms (Succ k) = ms k (natElim m mz ms k)

data Vec : Set -> Nat -> Set where
  Nil : (a : Set) -> Vec a Zero
  Cons : (a : Set) -> (n : Nat) -> (x : a) -> (xs : Vec a n) -> Vec a (Succ n)

data Eq : (a : Set) -> a -> a -> Set where
  Refl : (a : Set) -> (x : a) -> Eq a x x

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module TypeSig where

f
  : {A : Set}
  → A
  → A
f x
  = x

g
  : {A : Set}
  → A
  → A
g x
  = x

h
  : {A : Set}
  → A
  → A
h x
  = f x

_
  : {A : Set}
  → A
  → A
_
  = λ x → x

max_stars_repo_name: msuperdock/agda-unused

max_issues_repo_name: msuperdock/agda-unused

max_forks_repo_name: msuperdock/agda-unused


text:
module Issue317 (A : Set) where

postulate F : Set → Set

-- Try evaluating F A at the top-level:
--
-- 1,3-4
-- Not in scope:
--   A at 1,3-4
-- when scope checking A
--
-- OK, in that case the inferred type of F should be
-- (A : Set) → Set → Set, right? No, it isn't, it's Set → Set.
--
-- I think the parameters should be in scope when "top-level" commands
-- are executed, because these commands should behave in the same way
-- as commands executed in a top-level goal at the end of the module.
-- It seems as if the implementation of
-- Agda.Interaction.BasicOps.atTopLevel has to be modified.

max_stars_repo_name: shlevy/agda

max_issues_repo_name: shlevy/agda

max_forks_repo_name: Agda-zh/agda


text:
-- In this document we'll consider various encodings of mutual data types,
-- including those that are System Fω compatible.

module MutualData where

open import Function
open import Data.Unit.Base
open import Data.Sum
open import Data.Product

-- In the first part of this document we'll demostrate how various encodings work taking
-- the rose tree data type as an example:

mutual
  data Tree₀ (A : Set) : Set where
    node₀ : A -> Forest₀ A -> Tree₀ A

  data Forest₀ (A : Set) : Set where
    nil₀  : Forest₀ A
    cons₀ : Tree₀ A -> Forest₀ A -> Forest₀ A

module Joined where
  -- For encoding a family of mutually recursive data types in terms of a single data type we can
  -- create the type of tags each of which denotes a particular data type from the family, then
  -- merge all constructors of the original data types together into a single data type and index
  -- each of the constructors by the tag representing the data type it constructs.

  -- Since we encode a family consisting of two data types, the type of tags has two inhabitants:

  data TreeForestᵗ : Set where
    Treeᵗ Forestᵗ : TreeForestᵗ

  -- The encoding:

  mutual
    -- There is nothing inherently mutual about these data types.
    -- `Tree` and `Forest` are just aliases defined for convenience and readability.

    Tree : Set -> Set
    Tree A = TreeForest A Treeᵗ

    Forest : Set -> Set
    Forest A = TreeForest A Forestᵗ

    -- Now we have one big data type that contains all constructors of the `Tree`-`Forest` family:

    data TreeForest (A : Set) : TreeForestᵗ -> Set where
      node : A -> Forest A -> Tree A
      nil  : Forest A
      cons : Tree A -> Forest A -> Forest A

    -- Note that the constructors have exactly the same type signatures as before,
    -- but now `Tree` and `Forest` are instances of the same data type.

  -- As a sanity check we show one side (just to save space and because it's demonstrative enough)
  -- of the isomorphism between the original family and its encoded version:

  mutual
    toTree₀ : ∀ {A} -> Tree A -> Tree₀ A
    toTree₀ (node x forest) = node₀ x (toForest₀ forest)

    toForest₀ : ∀ {A} -> Forest A -> Forest₀ A
    toForest₀  nil               = nil₀
    toForest₀ (cons tree forest) = cons₀ (toTree₀ tree) (toForest₀ forest)

  -- The encoding technique described in this module is fairly well-known.

module JoinedCompute where
  -- In this section we'll make `TreeForest` a data type with a single constructor,
  -- the contents of which depends on the type being constructed.

  data TreeForestᵗ : Set where
    Treeᵗ Forestᵗ : TreeForestᵗ

  mutual
    -- Again, `Tree` and `Forest` are just aliases.

    Tree : Set -> Set
    Tree A = TreeForest A Treeᵗ

    Forest : Set -> Set
    Forest A = TreeForest A Forestᵗ

    -- `TreeForestF` matches on the `TreeForestᵗ` index in order to figure out which data type
    -- from the original family is being constructed.
    -- Like in the previous section `TreeForest` defines both the `Tree` and `Forest` data types,
    -- but now it contains a single constructor that only captures the notion of recursion.
    -- What data to store in this constructor is determined by the `TreeForestF` function.

    TreeForestF : Set -> TreeForestᵗ -> Set
    TreeForestF A Treeᵗ   = A × Forest A           -- The only constructor of `Tree` is `node` which
                                                   -- carries an `A` and a `Forest A`.
    TreeForestF A Forestᵗ = ⊤ ⊎ Tree A × Forest A  -- There are two constructors of `Forest`:
                                                   -- `nil` and `cons`. The former one doesn't
                                                   -- carry any information while the latter one
                                                   -- receives a `Tree` and a `Forest`.

    data TreeForest (A : Set) (tfᵗ : TreeForestᵗ) : Set where
      treeForest : TreeForestF A tfᵗ -> TreeForest A tfᵗ

  -- For convenience, we'll be using pattern synonyms in this module and the modules below.

  pattern node x forest    = treeForest (x , forest)
  pattern nil              = treeForest (inj₁ tt)
  pattern cons tree forest = treeForest (inj₂ (tree , forest))

  -- The sanity check.

  mutual
    toTree₀ : ∀ {A} -> Tree A -> Tree₀ A
    toTree₀ (node x forest) = node₀ x (toForest₀ forest)

    toForest₀ : ∀ {A} -> Forest A -> Forest₀ A
    toForest₀  nil               = nil₀
    toForest₀ (cons tree forest) = cons₀ (toTree₀ tree) (toForest₀ forest)

-- In the previous section we had the `TreeForest` data type and its `treeForest` constructor
-- which together captured the notion of recursion. This pattern can be abstracted, so that we can
-- tie knots in arbitrary other data types -- not just `Tree` and `Forest`. Enter `IFix`:

{-# NO_POSITIVITY_CHECK #-}
data IFix {α β} {A : Set α} (B : (A -> Set β) -> A -> Set β) (x : A) : Set β where
  wrap : B (IFix B) x -> IFix B x

module JoinedComputeIFix where
  -- In this module we define the `TreeForest` data type using `IFix`.
  -- The type of tags is as before:

  data TreeForestᵗ : Set where
    Treeᵗ Forestᵗ : TreeForestᵗ

  -- The definition of `TreeForest` is similar to the definition from the previous section:
  -- we again have the `Tree` and `Forest` type aliases, they're just local now,
  -- and as before we dispatch on `tfᵗ` and describe the constructors of the `Tree` and `Forest`
  -- data types using the sum-of-products representation:

  TreeForest : Set -> TreeForestᵗ -> Set
  TreeForest A =
    IFix λ Rec tfᵗ ->
      let Tree   = Rec Treeᵗ
          Forest = Rec Forestᵗ
        in case tfᵗ of λ
          { Treeᵗ   -> A × Forest
          ; Forestᵗ -> ⊤ ⊎ Tree × Forest
          }

  -- We've cheated a little bit here by keeping `A` outside of the pattern functor.
  -- That's just for simplicity, there is no fundamental limitation that prevents us
  -- from taking fixed points of pattern functors of arbitrary arity.
  -- Which is a topic for another document.

  Tree : Set -> Set
  Tree A = TreeForest A Treeᵗ

  Forest : Set -> Set
  Forest A = TreeForest A Forestᵗ

  pattern node x forest    = wrap (x , forest)
  pattern nil              = wrap (inj₁ tt)
  pattern cons tree forest = wrap (inj₂ (tree , forest))

  -- The sanity check.

  mutual
    toTree₀ : ∀ {A} -> Tree A -> Tree₀ A
    toTree₀ (node x forest) = node₀ x (toForest₀ forest)

    toForest₀ : ∀ {A} -> Forest A -> Forest₀ A
    toForest₀  nil               = nil₀
    toForest₀ (cons tree forest) = cons₀ (toTree₀ tree) (toForest₀ forest)

module JoinedComputeIFixFω where
  -- The types we had previously are not System Fω compatible, because we matched on tags at the
  -- type level. Can we avoid this? Yes, easily. Instead of defining data types representing tags
  -- we can just lambda-encode them, because we do have lambdas at the type level in System Fω.

  -- The Church-encoded version of `TreeForestᵗ` at the type level looks like this:

  -- ∀ R -> (Set -> Set -> R) -> R

  -- However this is still not System Fω compatible, because here we quantify over `R` which in
  -- System Fω is a kind and we can't quatify over kinds there. But looking at

  -- TreeForestF : Set -> TreeForestᵗ -> Set
  -- TreeForestF A Treeᵗ   = A × Forest A
  -- TreeForestF A Forestᵗ = ⊤ ⊎ Tree A × Forest A

  -- we see that we match on a `TreeForestᵗ` only to return a `Set`. Hence we can just instantiate
  -- `R` to `Set` right away as we do not do anything else with tags. We arrive at

  TreeForestᵗ : Set₁
  TreeForestᵗ = Set -> Set -> Set

  Treeᵗ : TreeForestᵗ
  Treeᵗ A B = A

  Forestᵗ : TreeForestᵗ
  Forestᵗ A B = B

  -- Where `TreeForestᵗ` is the type of inlined matchers which always return a `Set` and
  -- `Treeᵗ` and `Forestᵗ` are such matchers. The rest is straightforward:

  TreeForest : Set -> TreeForestᵗ -> Set
  TreeForest A =
    IFix λ Rec tfᵗ ->
      let Tree   = Rec Treeᵗ
          Forest = Rec Forestᵗ
        in tfᵗ
             (A × Forest)         -- Returned when `tfᵗ` is `Treeᵗ`.
             (⊤ ⊎ Tree × Forest)  -- Returned when `tfᵗ` is `Forestᵗ`.

  Tree : Set -> Set
  Tree A = TreeForest A Treeᵗ

  Forest : Set -> Set
  Forest A = TreeForest A Forestᵗ

  -- All types are System Fω compatible (except the definition of `TreeForestᵗ` has to be inlined)
  -- as System Fω does not support kind aliases.

  pattern node x forest    = wrap (x , forest)
  pattern nil              = wrap (inj₁ tt)
  pattern cons tree forest = wrap (inj₂ (tree , forest))

  -- The sanity check.

  mutual
    toTree₀ : ∀ {A} -> Tree A -> Tree₀ A
    toTree₀ (node x forest) = node₀ x (toForest₀ forest)

    toForest₀ : ∀ {A} -> Forest A -> Forest₀ A
    toForest₀  nil               = nil₀
    toForest₀ (cons tree forest) = cons₀ (toTree₀ tree) (toForest₀ forest)

  -- An additional test:

  mutual
    mapTree : ∀ {A B} -> (A -> B) -> Tree A -> Tree B
    mapTree f (node x forest) = node (f x) (mapForest f forest)

    mapForest : ∀ {A B} -> (A -> B) -> Forest A -> Forest B
    mapForest f  nil               = nil
    mapForest f (cons tree forest) = cons (mapTree f tree) (mapForest f forest)

-- The first part ends here.  We've just seen how to encode mutual data types in pure System Fω
-- with build-in isorecursive `IFix :: ((k -> *) -> k -> *) -> k -> *`.

-- In the second part we'll see how to encode mutual data types with distinct kind signatures.
-- Due to my lack of imagination, we'll take the following family as an example:

mutual
  data M₀ (A : Set) : Set where
    p₀ : A -> M₀ A
    n₀ : N₀ -> M₀ A

  data N₀ : Set where
    m₀ : M₀ ⊤ -> N₀

-- `M₀` is of kind `Set -> Set` while `N₀` is of kind `Set`.

module DistinctParamsJoined where
  -- As in the first part we start with a single data type that contains all the constructors of
  -- the family of data types being encoded.

  -- The only thing we need to do, is to add all the parameters to the constructors of the type
  -- of tags. The rest just follows.

  data MNᵗ : Set₁ where
    Mᵗ : Set -> MNᵗ  -- `M` is parameterized by a `Set`, hence one `Set` argument.
    Nᵗ : MNᵗ         -- `N` is not parameterized, hence no arguments.

  -- The encoding itself follows the same pattern we've seen previously:

  mutual
    M : Set -> Set
    M A = MN (Mᵗ A)

    N : Set
    N = MN Nᵗ

    data MN : MNᵗ -> Set where
      -- `∀ {A} -> ...` is an artifact of this particular encoding, it'll disappear later.
      p : ∀ {A} -> A -> M A
      n : ∀ {A} -> N -> M A
      m : M ⊤ -> N

  -- The sanity check.

  mutual
    toM₀ : ∀ {A} -> M A -> M₀ A
    toM₀ (p x) = p₀ x
    toM₀ (n y) = n₀ (toN₀ y)

    toN₀ : N -> N₀
    toN₀ (m y) = m₀ (toM₀ y)

module DistinctParamsJoinedComputeIFix where
  -- We skip the `JoinedCompute` stage and jump straight to `JoinedComputeIFix`.

  -- Again, we just add arguments to tags and the rest follows:

  data MNᵗ : Set₁ where
    Mᵗ : Set -> MNᵗ
    Nᵗ : MNᵗ

  MN : MNᵗ -> Set
  MN =
    IFix λ Rec mnᵗ ->
      let M A = Rec (Mᵗ A)
          N   = Rec Nᵗ
        in case mnᵗ of λ
          { (Mᵗ A) -> A ⊎ N  -- `M` has two constructors: one receives an `A` and
                             -- the other receives an `N`.
          ;  Nᵗ    -> M ⊤    -- `N` has one constructor which receives an `M ⊤`.
          }

  M : Set -> Set
  M A = MN (Mᵗ A)

  N : Set
  N = MN Nᵗ

  pattern p x = wrap (inj₁ x)
  pattern n y = wrap (inj₂ y)
  pattern m y = wrap y

  -- The sanity check.

  mutual
    toM₀ : ∀ {A} -> M A -> M₀ A
    toM₀ (p x) = p₀ x
    toM₀ (n y) = n₀ (toN₀ y)

    toN₀ : N -> N₀
    toN₀ (m y) = m₀ (toM₀ y)

module DistinctParamsJoinedComputeIFixFω where
  -- Mechanically performing the restricted Church-encoding transformation that allows to bring
  -- the types into the realms of System Fω, we get

  MNᵗ : Set₁
  MNᵗ = (Set -> Set) -> Set -> Set

  Mᵗ : Set -> MNᵗ
  Mᵗ A = λ rM rN -> rM A

  Nᵗ : MNᵗ
  Nᵗ = λ rM rN -> rN

  -- Nothing new here:

  MN : MNᵗ -> Set
  MN =
    IFix λ Rec mnᵗ ->
      let M A = Rec (Mᵗ A)
          N   = Rec Nᵗ
        in mnᵗ (λ A -> A ⊎ N) (M ⊤)

  M : Set -> Set
  M A = MN (Mᵗ A)

  N : Set
  N = MN Nᵗ

  pattern p x = wrap (inj₁ x)
  pattern n y = wrap (inj₂ y)
  pattern m y = wrap y

  -- The sanity check.

  mutual
    toM₀ : ∀ {A} -> M A -> M₀ A
    toM₀ (p x) = p₀ x
    toM₀ (n y) = n₀ (toN₀ y)

    toN₀ : N -> N₀
    toN₀ (m y) = m₀ (toM₀ y)

module FakingFix where
  -- We can look at encoding mutual data types from entirely distinct perspective.
  -- One of the standard approaches is to have kind-level products and use `Fix :: (k -> k) -> k`
  -- over them. There is no such `Fix` in Agda, but we can pretend it exists:

  postulate
    Fix : ∀ {α} {A : Set α} -> (A -> A) -> A

  -- Then we can encode `MN` as

  MN : (Set -> Set) × Set
  MN =
    Fix λ Rec ->
      let M A = proj₁ Rec A
          N   = proj₂ Rec
        in (λ A -> A ⊎ N) , M ⊤

  -- This all is very similar to what we've seen in the previous section: the local definitions
  -- of `M` and `N` differ and we construct a type-level tuple rather than a `Set`, but the
  -- pattern is the same.

  -- The global definitions of `M` and `N` are

  M : Set -> Set
  M = proj₁ MN

  N : Set
  N = proj₂ MN

  -- And now we can perform the same restricted Church-encoding trick again and use
  -- `((Set -> Set) -> Set -> Set) -> Set` instead of `(Set -> Set) × Set`.
  -- Note that the new type then is exactly the same as the one of `MN` from the previous section:

  -- MN : MNᵗ -> Set

  -- which being inlined becomes:

  -- MN : ((Set -> Set) -> Set -> Set) -> Set

  -- Hence we arrived at the same encoding taking a folklore technique as a starting point.

max_stars_repo_name: robkorn/plutus

max_issues_repo_name: robkorn/plutus

max_forks_repo_name: robkorn/plutus


text:
module Luau.RuntimeError.ToString where

open import Agda.Builtin.Float using (primShowFloat)
open import FFI.Data.String using (String; _++_)
open import Luau.RuntimeError using (RuntimeErrorᴮ; RuntimeErrorᴱ; local; return; TypeMismatch; UnboundVariable; SEGV; app₁; app₂; block; bin₁; bin₂)
open import Luau.RuntimeType.ToString using (runtimeTypeToString)
open import Luau.Addr.ToString using (addrToString)
open import Luau.Syntax.ToString using (exprToString)
open import Luau.Var.ToString using (varToString)
open import Luau.Value.ToString using (valueToString)
open import Luau.Syntax using (name; _$_)

errToStringᴱ : ∀ {a H B} → RuntimeErrorᴱ {a} H B → String
errToStringᴮ : ∀ {a H B} → RuntimeErrorᴮ {a} H B → String

errToStringᴱ (UnboundVariable x) = "variable " ++ varToString x ++ " is unbound"
errToStringᴱ (SEGV a x) = "address " ++ addrToString a ++ " is unallocated"
errToStringᴱ (app₁ E) = errToStringᴱ E
errToStringᴱ (app₂ E) = errToStringᴱ E
errToStringᴱ (bin₁ E) = errToStringᴱ E
errToStringᴱ (bin₂ E) = errToStringᴱ E
errToStringᴱ (block b E) = errToStringᴮ E ++ "\n  in call of function " ++ varToString b
errToStringᴱ (TypeMismatch t v _) = "value " ++ valueToString v ++ " is not a " ++ runtimeTypeToString t

errToStringᴮ (local x E) = errToStringᴱ E ++ "\n  in definition of " ++ varToString (name x)
errToStringᴮ (return E) = errToStringᴱ E ++ "\n  in return statement"


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.DStructures.Structures.SplitEpi 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.Type
open import Cubical.DStructures.Structures.Constant
open import Cubical.DStructures.Structures.Group

private
  variable
    ℓ ℓ' : Level

open URGStr

---------------------------------------------
-- URG structures on the type of split epis,
-- and displayed structures over that
--
--     B
--     |
--  isSplit
--     |
--   G²FB
---------------------------------------------

module _ (ℓ ℓ' : Level) where

  -- type of Split epimorphisms
  SplitEpi = Σ[ ((G , H) , f , b) ∈ G²FB ℓ ℓ' ] isGroupSplitEpi f b
  SplitEpi' = Σ[ G ∈ Group {ℓ} ] Σ[ H ∈ Group {ℓ'} ] Σ[ (f , b) ∈ (GroupHom G H) × (GroupHom H G) ] isGroupSplitEpi f b

  IsoSplitEpi' : Iso SplitEpi' SplitEpi
  IsoSplitEpi' = compIso (invIso Σ-assoc-Iso)
                         (invIso Σ-assoc-Iso)

  -- split epimorphisms + a map back
  SplitEpiB = Σ[ (((G , H) , f , b) , isRet) ∈ SplitEpi ] GroupHom H G

  -- split epimorphisms displayed over pairs of groups
  𝒮ᴰ-SplitEpi : URGStrᴰ (𝒮-G²FB ℓ ℓ')
                        (λ ((G , H) , (f , b)) → isGroupSplitEpi f b)
                        ℓ-zero
  𝒮ᴰ-SplitEpi =
    Subtype→Sub-𝒮ᴰ (λ ((G , H) , (f , b)) → isGroupSplitEpi f b , isPropIsGroupSplitEpi f b)
                   (𝒮-G²FB ℓ ℓ')

  -- URG structure on type of split epimorphisms
  𝒮-SplitEpi : URGStr SplitEpi (ℓ-max ℓ ℓ')
  𝒮-SplitEpi = ∫⟨ 𝒮-G²FB ℓ ℓ' ⟩ 𝒮ᴰ-SplitEpi

  -- morphisms back displayed over split epimorphisms,
  -- obtained by lifting the morphisms back over
  -- 𝒮-G² twice
  𝒮ᴰ-G²FBSplit\B : URGStrᴰ 𝒮-SplitEpi
                           (λ (((G , H) , _) , _) → GroupHom H G)
                           (ℓ-max ℓ ℓ')
  𝒮ᴰ-G²FBSplit\B =
    VerticalLift2-𝒮ᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                     (𝒮ᴰ-G²\B ℓ ℓ')
                     (𝒮ᴰ-G²\FB ℓ ℓ')
                     𝒮ᴰ-SplitEpi

  -- URG structure on split epis with an extra
  -- morphism back
  𝒮-SplitEpiB : URGStr SplitEpiB (ℓ-max ℓ ℓ')
  𝒮-SplitEpiB = ∫⟨ 𝒮-SplitEpi ⟩ 𝒮ᴰ-G²FBSplit\B

  𝒮ᴰ-G\GFBSplitEpi : URGStrᴰ (𝒮-group ℓ)
                             (λ G → Σ[ H ∈ Group {ℓ'} ] Σ[ (f , b) ∈ (GroupHom G H) × (GroupHom H G) ] isGroupSplitEpi f b )
                             (ℓ-max ℓ ℓ')
  𝒮ᴰ-G\GFBSplitEpi =
    splitTotal-𝒮ᴰ (𝒮-group ℓ)
                  (𝒮ᴰ-const (𝒮-group ℓ) (𝒮-group ℓ'))
                  (splitTotal-𝒮ᴰ (𝒮-group ℓ ×𝒮 𝒮-group ℓ')
                                 (𝒮ᴰ-G²\FB ℓ ℓ')
                                 𝒮ᴰ-SplitEpi)

--------------------------------------------------
-- This module introduces convenient notation
-- when working with a single split epimorphism
---------------------------------------------------

module SplitEpiNotation {G₀ : Group {ℓ}} {G₁ : Group {ℓ'}}
                        (ι : GroupHom G₀ G₁) (σ : GroupHom G₁ G₀)
                        (split : isGroupSplitEpi ι σ) where
  open GroupNotation₀ G₀
  open GroupNotation₁ G₁
  ι∘σ : GroupHom G₁ G₁
  ι∘σ = compGroupHom σ ι
  s = GroupHom.fun σ
  -- i is reserved for an interval variable (i : I) so we use 𝒾 instead
  𝒾 = GroupHom.fun ι
  -i = λ (x : ⟨ G₀ ⟩) → -₁ (𝒾 x)
  s- = λ (x : ⟨ G₁ ⟩) → s (-₁ x)
  si = λ (x : ⟨ G₀ ⟩) → s (𝒾 x)
  is = λ (x : ⟨ G₁ ⟩) → 𝒾 (s x)
  -si = λ (x : ⟨ G₀ ⟩) → -₀ (si x)
  -is = λ (x : ⟨ G₁ ⟩) → -₁ (is x)
  si- = λ (x : ⟨ G₀ ⟩) → si (-₀ x)
  is- = λ (x : ⟨ G₁ ⟩) → is (-₁ x)
  s-i = λ (x : ⟨ G₀ ⟩) → s (-₁ (𝒾 x))
  isi = λ (x : ⟨ G₀ ⟩) → 𝒾 (s (𝒾 x))

max_stars_repo_name: Schippmunk/cubical

max_issues_repo_name: Schippmunk/cubical

max_forks_repo_name: Schippmunk/cubical


text:
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
open import Data.Sum

import SingleSorted.AlgebraicTheory as SS

module SingleSorted.Combinators where

module Sum {𝓈} (Σ₁ Σ₂ : SS.Signature) (T₁ : SS.Theory 𝓈 Σ₁) (T₂ : SS.Theory 𝓈 Σ₂) where

  -- disjoint sum of signatures
  S : SS.Signature
  S = record { oper = SS.Signature.oper Σ₁  ⊎  SS.Signature.oper Σ₂
             ; oper-arity = [ SS.Signature.oper-arity Σ₁ , SS.Signature.oper-arity Σ₂ ]
             }

  inj-term-l : ∀ {Γ : SS.Context} →  SS.Signature.Term Σ₁ Γ → SS.Signature.Term S Γ
  inj-term-l {Γ} (SS.Signature.tm-var x) = SS.Signature.tm-var x
  inj-term-l {Γ} (SS.Signature.tm-oper f ts) = SS.Signature.tm-oper (inj₁ f) λ{ i → inj-term-l (ts i)}

  inj-term-r : ∀ {Γ : SS.Context} →  SS.Signature.Term Σ₂ Γ → SS.Signature.Term S Γ
  inj-term-r {Γ} (SS.Signature.tm-var x) = SS.Signature.tm-var x
  inj-term-r {Γ} (SS.Signature.tm-oper f ts) = SS.Signature.tm-oper (inj₂ f) λ{ i → inj-term-r (ts i)}

  coerce₁ : SS.Signature.Equation Σ₁ → SS.Signature.Equation S
  coerce₁ eq = record { eq-ctx = SS.Signature.Equation.eq-ctx eq
                      ; eq-lhs = inj-term-l (SS.Signature.Equation.eq-lhs eq)
                      ; eq-rhs = inj-term-l (SS.Signature.Equation.eq-rhs eq)
                      }

  coerce₂ : SS.Signature.Equation Σ₂ → SS.Signature.Equation S
  coerce₂ eq = record { eq-ctx = SS.Signature.Equation.eq-ctx eq
                      ; eq-lhs = inj-term-r (SS.Signature.Equation.eq-lhs eq)
                      ; eq-rhs = inj-term-r (SS.Signature.Equation.eq-rhs eq)
                      }

  -- define a theory with the set of axioms a union of the axioms of both theories
  T : SS.Theory 𝓈 S
  T = record { ax = SS.Theory.ax T₁ ⊎ SS.Theory.ax T₂
             ; ax-eq = [ (λ a → coerce₁ (SS.Theory.ax-eq T₁ a)) , (λ a → coerce₂ (SS.Theory.ax-eq T₂ a)) ]
             }

max_stars_repo_name: cilinder/formaltt

max_issues_repo_name: andrejbauer/formaltt

max_forks_repo_name: andrejbauer/formaltt


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

module Type.Cubical.Path.Proofs where

import      Lvl
open import Type
open import Type.Cubical
open import Type.Cubical.Path

private variable ℓ ℓ₁ ℓ₂ : Lvl.Level

module _ where
  private variable A B : Type{ℓ}
  private variable P : Interval → Type{ℓ}
  private variable x y z w : A

  -- The full path from the starting point to the end.
  path : (point : Interval → A) → Path(point(Interval.𝟎)) (point(Interval.𝟏))
  path point i = point i

  -- The point on the path, given a point of the interval indexing the path.
  pointOn : ∀{x y : A} → Path x y → (Interval → A)
  pointOn p i = p i

  -- The path from a point to itself.
  -- This path only consists of the point itself.
  point : Path x x
  point{x = x} _ = x

  -- The reverse path of a path.
  -- Reverses the direction of a path by flipping all points around the point of symmetry.
  reverseP : PathP(P) x y → PathP(\i → P(Interval.flip i)) y x
  reverseP p(i) = p(Interval.flip i)

  reverse : Path x y → Path y x
  reverse = reverseP

  -- A function mapping points between two spaces, given a path between the spaces.
  spaceMap : Path A B → (A → B)
  spaceMap p = Interval.transp (pointOn p) Interval.𝟎

  -- TODO: Move
  module _ {A : Type{ℓ}} where
    private variable a₀ a₁ a₂ a₃ : A
    private variable a₀₀ a₀₁ a₁₀ a₁₁ : A
    private variable a₀₀₀ a₀₀₁ a₀₁₀ a₀₁₁ a₁₀₀ a₁₀₁ a₁₁₀ a₁₁₁ : A
    private variable p₀₀₋ p₀₁₋ p₀₋₀ p₀₋₁ p₁₀₋ p₁₁₋ p₁₋₀ p₁₋₁ p₋₀₀ p₋₀₁ p₋₁₀ p₋₁₁ : Path a₀ a₁

    Path-missingSide : A → A
    Path-missingSide a = Interval.hComp diag a where
      diag : Interval → Interval.Partial Interval.𝟎 A
      diag i ()

    module _
      (p₀₋ : Path a₀₀ a₀₁)
      (p₁₋ : Path a₁₀ a₁₁)
      (p₋₀ : Path a₀₀ a₁₀)
      (p₋₁ : Path a₀₁ a₁₁)
      where
      -- a₀₁ → p₋₁ → a₁₁
      --  ↑           ↑
      -- p₀₋         p₁₋
      --  ↑           ↑
      -- a₀₀ → p₋₀ → a₁₀
      Square : Type
      Square = PathP (\i → Path (p₋₀ i) (p₋₁ i)) p₀₋ p₁₋
    module Square where
      missingSide : Path a₀₀ a₀₁ → Path a₁₀ a₁₁ → Path a₀₀ a₁₀ → Path a₀₁ a₁₁
      missingSide p₀₋ p₁₋ p₋₀ ix = Interval.hComp diagram (p₋₀ ix) where
        diagram : Interval → Interval.Partial(Interval.max ix (Interval.flip ix)) A
        diagram iy (ix = Interval.𝟎) = p₀₋ iy
        diagram iy (ix = Interval.𝟏) = p₁₋ iy

      module _
        {p₀₋ : Path a₀₀ a₀₁}
        {p₁₋ : Path a₁₀ a₁₁}
        {p₋₀ : Path a₀₀ a₁₀}
        {p₋₁ : Path a₀₁ a₁₁}
        (s : Square p₀₋ p₁₋ p₋₀ p₋₁)
        where

        diagonal : Path a₀₀ a₁₁
        diagonal i = s i i

        rotate₊ : Square p₋₁ p₋₀ (reverse p₀₋) (reverse p₁₋)
        rotate₊ iy ix = s ix (Interval.flip iy)

        rotate₋ : Square (reverse p₋₀) (reverse p₋₁) p₁₋ p₀₋
        rotate₋ iy ix = s (Interval.flip ix) iy

        flipX : Square p₁₋ p₀₋ (reverse p₋₀) (reverse p₋₁)
        flipX iy ix = s (Interval.flip iy) ix

        flipY : Square (reverse p₀₋) (reverse p₁₋) p₋₁ p₋₀
        flipY iy ix = s iy (Interval.flip ix)

      module _
        {a₀ a₁ : A}
        (p : Path a₀ a₁)
        where

        lineX : Square point point p p
        lineX ix iy = p ix

        lineY : Square p p point point
        lineY ix iy = p iy

        min : Square point p point p
        min ix iy = p(Interval.min ix iy)

        max : Square p point p point
        max ix iy = p(Interval.max ix iy)

    module _
      (p₀₋₋ : Square p₀₀₋ p₀₁₋ p₀₋₀ p₀₋₁)
      (p₁₋₋ : Square p₁₀₋ p₁₁₋ p₁₋₀ p₁₋₁)
      (p₋₀₋ : Square p₀₀₋ p₁₀₋ p₋₀₀ p₋₀₁)
      (p₋₁₋ : Square p₀₁₋ p₁₁₋ p₋₁₀ p₋₁₁)
      (p₋₋₀ : Square p₀₋₀ p₁₋₀ p₋₀₀ p₋₁₀)
      (p₋₋₁ : Square p₀₋₁ p₁₋₁ p₋₀₁ p₋₁₁)
      where

      Cube : Type
      Cube = PathP (\i → Square (p₋₀₋ i) (p₋₁₋ i) (p₋₋₀ i) (p₋₋₁ i)) p₀₋₋ p₁₋₋
    {-
    module Cube where
      module _
        (p₀₋₋ : Square p₀₀₋ p₀₁₋ p₀₋₀ p₀₋₁)
        (p₁₋₋ : Square p₁₀₋ p₁₁₋ p₁₋₀ p₁₋₁)
        (p₋₀₋ : Square p₀₀₋ p₁₀₋ p₋₀₀ p₋₀₁)
        (p₋₁₋ : Square p₀₁₋ p₁₁₋ p₋₁₀ p₋₁₁)
        (p₋₋₀ : Square p₀₋₀ p₁₋₀ p₋₀₀ p₋₁₀)
        where
        missingSide : Square p₀₋₁ p₁₋₁ p₋₀₁ p₋₁₁
        missingSide ix iy = Interval.hComp diagram (p₋₋₀ ix iy) where -- (Square.max {!!} ix iy)
          diagram : Interval → Interval.Partial {!!} A
          {-diagram : (i : Interval) → Interval.Partial (Interval.max (Interval.max ix (Interval.flip ix)) (Interval.max iy (Interval.flip iy))) _
          diagram iz (ix = Interval.𝟎) = Square.max p₀₋₁ ix iy
          diagram iz (ix = Interval.𝟏) = Square.min p₁₋₁ ix iy
          diagram iz (iy = Interval.𝟎) = Square.max p₋₀₁ ix iy
          diagram iz (iy = Interval.𝟏) = Square.min p₋₁₁ ix iy-}
    -}

  -- Concatenates (joins the ends of) two paths.
  concat : Path x y → Path y z → Path x z
  concat xy yz = Square.missingSide point yz xy

module _ where
  private variable X : Type{ℓ}
  private variable Y : X → Type{ℓ}

  -- Maps a path into another space.
  mapP : (f : (x : X) → Y(x)) → ∀{x y} → (path : Path x y) → PathP(\i → Y(path(i))) (f(x)) (f(y))
  mapP(f) p(i) = f(p(i))

  -- When there is a path between two space mappings.
  mapping : ∀{f g : (x : X) → Y(x)} → (∀{x} → Path(f(x)) (g(x))) → Path f g
  mapping ppt i x = ppt{x} i

  mappingPoint : ∀{f g : (x : X) → Y(x)} → Path f g → (∀{x} → Path(f(x)) (g(x)))
  mappingPoint pfg {x} i = pfg i x

module _ where
  private variable X : Type{ℓ}
  private variable Y : X → Type{ℓ}
  private variable Z : (x : X) → Y(x) → Type{ℓ}

  -- mapP₂' : (f : (x : X) → (y : Y(x)) → Z(x)(y)) → ∀{a₁ b₁ : X}{a₂ : Y(a₁)}{b₂ : Y(b₁)} → (path₁ : Path a₁ b₁) → (path₂ : Path a₂ b₂) → PathP(\i → Z(path₁(i))(?)) (f a₁ a₂) (f b₁ b₂)

  mapP₂ : (f : (x : X) → (y : (x : X) → Y(x)) → Z(x)(y)) → ∀{a₁ b₁ : X}{a₂ b₂ : (x : X) → Y(x)} → (path₁ : Path a₁ b₁) → (path₂ : Path a₂ b₂) → PathP(\i → Z(path₁(i))(path₂(i))) (f a₁ a₂) (f b₁ b₂)
  mapP₂ f ab1 ab2 i = mapP (mapP f ab1 i) ab2 i

  -- mapP₂ : (f : (x : X) → (y : Y(x)) → Z(x)(y)) → ∀{x₁ x₂} → (path : Path x₁ x₂) → PathP(\i → Y(path(i))) (f(x)) (f(y))
  -- mapP₂(f) = ?

module _ where
  private variable X X₁ X₂ Y Y₁ Y₂ : Type{ℓ}

  map : (f : X → Y) → ∀{a b} → Path a b → Path (f(a)) (f(b))
  map = mapP

  map₂ : (f : X₁ → X₂ → Y) → ∀{a₁ b₁}{a₂ b₂} → Path a₁ b₁ → Path a₂ b₂ → Path (f a₁ a₂) (f b₁ b₂)
  map₂ f ab1 ab2 i = mapP (mapP f ab1 i) ab2 i

  liftedSpaceMap : (S : X → Type{ℓ}) → ∀{a b} → Path a b → S(a) → S(b)
  liftedSpaceMap S p = spaceMap(map S p)

  liftedSpaceMap₂ : (S : X → Y → Type{ℓ}) → ∀{a₁ b₁}{a₂ b₂} → Path a₁ b₁ → Path a₂ b₂ → S a₁ a₂ → S b₁ b₂
  liftedSpaceMap₂ S p q = spaceMap(map₂ S p q)

-- TODO: Move
data Loop{ℓ} : Type{ℓ} where
  base : Loop
  loop : Path base base

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:
open import lib
open import eq-reas-nouni

equiv = _≡_

Val = nat

data Expn : Set where
  val : Val -> Expn
  plus : Expn -> Expn -> Expn

eval : Expn -> Val
eval (val v) = v
eval (plus e1 e2) = (eval e1) + (eval e2)

data evalsTo : Expn -> Val -> Set where

  e-val : forall {v : Val}
          ------------------------
          -> (evalsTo (val v) v)

  e-add : forall {e1 e2 : Expn}{v1 v2 : Val}
          -> (evalsTo e1 v1)
          -> (evalsTo e2 v2)
          -------------------------------------
          -> (evalsTo (plus e1 e2) (v1 + v2))

e-thm-fwd : forall {e : Expn}{v : Val}
  -> evalsTo e v -> equiv (eval e) v

e-thm-fwd (e-val{v}) =
  begin
    eval (val v)
  equiv[ refl ]
    v
  qed
e-thm-fwd (e-add{e1}{e2}{v1}{v2} e1-evalsTo-v1 e2-evalsTo-v2) =
  let
    eval-e1-is-v1 = e-thm-fwd e1-evalsTo-v1
    eval-e2-is-v2 = e-thm-fwd e2-evalsTo-v2
  in begin
    eval (plus e1 e2)
  equiv[ refl ]
    (eval e1) + (eval e2)
  equiv[ cong2 _+_ eval-e1-is-v1 eval-e2-is-v2 ]
    v1 + v2
  qed

e-thm-alt : forall (e : Expn) -> evalsTo e (eval e)
e-thm-alt (val v) = e-val
e-thm-alt (plus e1 e2) = (e-add (e-thm-alt e1) (e-thm-alt e2))

max_stars_repo_name: JimFixGroupResearch/imper-ial

max_issues_repo_name: JimFixGroupResearch/imper-ial

max_forks_repo_name: JimFixGroupResearch/imper-ial


text:
{-# OPTIONS --cubical --safe #-}
module Cubical.HITs.PropositionalTruncation where

open import Cubical.HITs.PropositionalTruncation.Base public
open import Cubical.HITs.PropositionalTruncation.Properties public

max_stars_repo_name: limemloh/cubical

max_issues_repo_name: limemloh/cubical

max_forks_repo_name: limemloh/cubical


text:
-- Kleene's three-valued logic

module bool-kleene where

open import bool
open import eq

data 𝔹ₖ : Set where
  tt : 𝔹ₖ
  ff : 𝔹ₖ
  uu : 𝔹ₖ

infix  7 ~ₖ_
infixr 6 _&&ₖ_
infixr 5 _||ₖ_
--infixr 4 _impₖ_

~ₖ_ : 𝔹ₖ → 𝔹ₖ
~ₖ tt = ff
~ₖ ff = tt
~ₖ uu = uu

-- and
_&&ₖ_ : 𝔹ₖ → 𝔹ₖ → 𝔹ₖ
tt &&ₖ b = b
ff &&ₖ b = ff
uu &&ₖ ff = ff
uu &&ₖ b = uu

-- or
_||ₖ_ : 𝔹ₖ → 𝔹ₖ → 𝔹ₖ
ff ||ₖ b = b
tt ||ₖ b = tt
uu ||ₖ tt = tt
uu ||ₖ b = uu

-- implication
_impₖ_ : 𝔹ₖ → 𝔹ₖ → 𝔹ₖ
tt impₖ b2 = b2
ff impₖ b2 = tt
uu impₖ tt = tt
uu impₖ b = uu

knownₖ : 𝔹ₖ → 𝔹
knownₖ tt = tt
knownₖ ff = tt
knownₖ uu = ff

to-𝔹 : (b : 𝔹ₖ) → knownₖ b ≡ tt → 𝔹
to-𝔹 tt p = tt
to-𝔹 ff p = ff
to-𝔹 uu ()

max_stars_repo_name: rfindler/ial

max_issues_repo_name: rfindler/ial

max_forks_repo_name: rfindler/ial


text:
{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.HITs.Wedge.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Pointed
open import Cubical.HITs.Pushout.Base
open import Cubical.Data.Unit

_⋁_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Type (ℓ-max ℓ ℓ')
_⋁_ (A , ptA) (B , ptB) = Pushout {A = Unit} {B = A} {C = B} (λ _ → ptA) (λ _ → ptB)

-- pointed versions

_⋁∙ₗ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋁∙ₗ B = (A ⋁ B) , (inl (snd A))

_⋁∙ᵣ_ : ∀ {ℓ ℓ'} → Pointed ℓ → Pointed ℓ' → Pointed (ℓ-max ℓ ℓ')
A ⋁∙ᵣ B = (A ⋁ B) , (inr (snd B))


text:
module Numeral.Natural.Oper.FlooredDivision.Proofs.Inverse where

import Lvl
open import Data
open import Functional
open import Logic.Propositional
open import Numeral.Natural
open import Numeral.Natural.Oper
open import Numeral.Natural.Oper.DivMod.Proofs
open import Numeral.Natural.Oper.FlooredDivision
open import Numeral.Natural.Oper.Modulo
open import Numeral.Natural.Oper.Modulo.Proofs
open import Numeral.Natural.Oper.Proofs
open import Numeral.Natural.Oper.Proofs.Multiplication
open import Numeral.Natural.Relation
open import Numeral.Natural.Relation.Divisibility
open import Numeral.Natural.Relation.Divisibility.Proofs
open import Numeral.Natural.Relation.Order
open import Relator.Equals
open import Relator.Equals.Proofs
open import Structure.Function
open import Structure.Operator
open import Structure.Operator.Properties
open import Structure.Relator.Properties
open import Syntax.Transitivity

[⋅][⌊/⌋]-inverseOperatorᵣ : ∀{x y} ⦃ pos : Positive(y) ⦄ → (y ∣ x) → (x ⌊/⌋ y ⋅ y ≡ x)
[⋅][⌊/⌋]-inverseOperatorᵣ {x}{𝐒 y} div =
  x ⌊/⌋ 𝐒(y) ⋅ 𝐒(y)                  🝖[ _≡_ ]-[]
  x ⌊/⌋ 𝐒(y) ⋅ 𝐒(y) + 𝟎              🝖[ _≡_ ]-[ congruence₂ᵣ(_+_)(_) ([↔]-to-[←] mod-divisibility div) ]-sym
  (x ⌊/⌋ 𝐒(y) ⋅ 𝐒(y)) + (x mod 𝐒(y)) 🝖[ _≡_ ]-[ [⌊/⌋][mod]-is-division-with-remainder {x}{y} ]
  x                                  🝖-end

[⌊/⌋][⋅]-inverseOperatorᵣ : ∀{x y} ⦃ pos : Positive(y) ⦄ → ((x ⋅ y) ⌊/⌋ y ≡ x)
[⌊/⌋][⋅]-inverseOperatorᵣ {x}{𝐒 y} = [⋅]-cancellationᵣ {𝐒(y)} ([⋅][⌊/⌋]-inverseOperatorᵣ (divides-with-[⋅] {𝐒(y)}{x} ([∨]-introᵣ (reflexivity(_∣_)))))

[⌊/⌋][swap⋅]-inverseOperatorᵣ : ∀{x y} ⦃ pos : Positive(x) ⦄ → ((x ⋅ y) ⌊/⌋ x ≡ y)
[⌊/⌋][swap⋅]-inverseOperatorᵣ {x}{y} = congruence₁(_⌊/⌋ x) (commutativity(_⋅_) {x}{y}) 🝖 [⌊/⌋][⋅]-inverseOperatorᵣ {y}{x}

[⋅][⌊/⌋₀]-inverseOperatorᵣ : ∀{x y} → (y > 0) → (y ∣ x) → ((x ⌊/⌋₀ y) ⋅ y ≡ x)
[⋅][⌊/⌋₀]-inverseOperatorᵣ {x}{𝐒 y} _ = [⋅][⌊/⌋]-inverseOperatorᵣ {x}{𝐒 y}