------------------------------------------------------------------------
-- The usage relation.
------------------------------------------------------------------------

import Graded.Modality
open import Graded.Usage.Restrictions

module Graded.Usage
  {a} {M : Set a}
  (open Graded.Modality M)
  (𝕄 : Modality)
  (R : Usage-restrictions 𝕄)
  where

open Modality 𝕄
open Usage-restrictions R

open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Modality.Dedicated-nr 𝕄
open import Graded.Mode 𝕄
open import Graded.Usage.Erased-matches
open import Definition.Untyped M hiding (_βˆ™_)

open import Tools.Bool using (T; true; false)
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum using (_⊎_)

infix 10 _β–Έ[_]_

private
  variable
    n : Nat
    p q r : M
    Ξ³ Ξ³β€² γ₁ Ξ³β‚‚ γ₃ Ξ³β‚„ Ξ³β‚… γ₆ Ξ΄ Ξ· ΞΈ Ο‡ : Conβ‚˜ n
    A B F G : Term n
    t u v w z : Term n
    x : Fin n
    m mβ€² : Mode
    b : BinderMode
    s : Strength
    em : Erased-matches

-- A view used in the implementation of ⌈_βŒ‰.

data βŒˆβŒ‰-view (A : Set a) (em : Erased-matches) : Set a where
  is-all      : em ≑ all β†’ βŒˆβŒ‰-view A em
  is-some-yes : em ≑ some β†’ A β†’ βŒˆβŒ‰-view A em
  is-other    : em ≀ᡉᡐ some β†’ (em ≑ some β†’ Β¬ A) β†’ βŒˆβŒ‰-view A em

opaque

  -- The view βŒˆβŒ‰-viewΒ AΒ em is inhabited if A is decided.

  βŒˆβŒ‰-view-inhabited : {A : Set a} β†’ Dec A β†’ βˆ€ em β†’ βŒˆβŒ‰-view A em
  βŒˆβŒ‰-view-inhabited _       all  = is-all refl
  βŒˆβŒ‰-view-inhabited (yes p) some = is-some-yes refl p
  βŒˆβŒ‰-view-inhabited (no p)  some = is-other _ (Ξ» _ β†’ p)
  βŒˆβŒ‰-view-inhabited _       none = is-other _ (Ξ» ())

opaque

  -- An instantiation of βŒˆβŒ‰-view-inhabited used forΒ J.

  J-view : βˆ€ p q m β†’ βŒˆβŒ‰-view (p ≑ 𝟘 Γ— q ≑ 𝟘) (erased-matches-for-J m)
  J-view p q _ = βŒˆβŒ‰-view-inhabited (is-𝟘? p Γ—-dec is-𝟘? q) _

opaque

  -- An instantiation of βŒˆβŒ‰-view-inhabited used forΒ K.

  K-view : βˆ€ p m β†’ βŒˆβŒ‰-view (p ≑ 𝟘) (erased-matches-for-K m)
  K-view p _ = βŒˆβŒ‰-view-inhabited (is-𝟘? p) _

-- Modality context inference (for modalities with nr functions).

infix 50 ⌈_βŒ‰

mutual
  ⌈_βŒ‰ :
    ⦃ has-nr : Has-nr semiring-with-meet ⦄ β†’
    Term n β†’ Mode β†’ Conβ‚˜ n
  ⌈ var x βŒ‰ m = 𝟘ᢜ , x ≔ ⌜ m ⌝
  ⌈ U βŒ‰ _ = 𝟘ᢜ
  ⌈ ΠΣ⟨ _ ⟩ p , q β–· F β–Ή G βŒ‰ m = ⌈ F βŒ‰ (m ᡐ· p) +ᢜ tailβ‚˜ (⌈ G βŒ‰ m)
  ⌈ lam p t βŒ‰ m = tailβ‚˜ (⌈ t βŒ‰ m)
  ⌈ t ∘⟨ p ⟩ u βŒ‰ m = ⌈ t βŒ‰ m +ᢜ p ·ᢜ ⌈ u βŒ‰ (m ᡐ· p)
  ⌈ prod 𝕨 p t u βŒ‰ m = p ·ᢜ ⌈ t βŒ‰ (m ᡐ· p) +ᢜ ⌈ u βŒ‰ m
  ⌈ prod 𝕀 p t u βŒ‰ m = p ·ᢜ ⌈ t βŒ‰ (m ᡐ· p) ∧ᢜ ⌈ u βŒ‰ m
  ⌈ fst p t βŒ‰ m = ⌈ t βŒ‰ m
  ⌈ snd p t βŒ‰ m = ⌈ t βŒ‰ m
  ⌈ prodrec r _ _ _ t u βŒ‰ m =
    r ·ᢜ ⌈ t βŒ‰ (m ᡐ· r) +ᢜ tailβ‚˜ (tailβ‚˜ (⌈ u βŒ‰ m))
  ⌈ β„• βŒ‰ _ = 𝟘ᢜ
  ⌈ zero βŒ‰ _ = 𝟘ᢜ
  ⌈ suc t βŒ‰ m = ⌈ t βŒ‰ m
  ⌈ natrec p _ r _ z s n βŒ‰ m =
    nrᢜ p r (⌈ z βŒ‰ m) (tailβ‚˜ (tailβ‚˜ (⌈ s βŒ‰ m))) (⌈ n βŒ‰ m)
  ⌈ Unit! βŒ‰ _ = 𝟘ᢜ
  ⌈ star! βŒ‰ _ = 𝟘ᢜ
  ⌈ unitrec p q A t u βŒ‰ m = p ·ᢜ ⌈ t βŒ‰ (m ᡐ· p) +ᢜ ⌈ u βŒ‰ m
  ⌈ Empty βŒ‰ _ = 𝟘ᢜ
  ⌈ emptyrec p _ t βŒ‰ m = p ·ᢜ ⌈ t βŒ‰ (m ᡐ· p)
  ⌈ Id _ t u βŒ‰ m = case Id-erased? of Ξ» where
    (yes _) β†’ 𝟘ᢜ
    (no _)  β†’ ⌈ t βŒ‰ m +ᢜ ⌈ u βŒ‰ m
  ⌈ rfl βŒ‰ _ = 𝟘ᢜ
  ⌈ J p q _ t B u v w βŒ‰ m with J-view p q m
  … | is-all _        = ⌈ u βŒ‰ m
  … | is-some-yes _ _ = Ο‰ ·ᢜ (tailβ‚˜ (tailβ‚˜ (⌈ B βŒ‰ m)) +ᢜ ⌈ u βŒ‰ m)
  … | is-other _ _    =
        Ο‰ ·ᢜ
        (⌈ t βŒ‰ m +ᢜ tailβ‚˜ (tailβ‚˜ (⌈ B βŒ‰ m)) +ᢜ
         ⌈ u βŒ‰ m +ᢜ ⌈ v βŒ‰ m +ᢜ ⌈ w βŒ‰ m)
  ⌈ K p _ t B u v βŒ‰ m with K-view p m
  … | is-all _        = ⌈ u βŒ‰ m
  … | is-some-yes _ _ = Ο‰ ·ᢜ (tailβ‚˜ (⌈ B βŒ‰ m) +ᢜ ⌈ u βŒ‰ m)
  … | is-other _ _    =
        Ο‰ ·ᢜ (⌈ t βŒ‰ m +ᢜ tailβ‚˜ (⌈ B βŒ‰ m) +ᢜ ⌈ u βŒ‰ m +ᢜ ⌈ v βŒ‰ m)
  ⌈ []-cong _ _ _ _ _ βŒ‰ _ = 𝟘ᢜ

-- Well-usage of variables
data _β—‚_∈_  : (x : Fin n) (p : M) (Ξ³ : Conβ‚˜ n) β†’ Set a where
  here  :                       x0 β—‚ p ∈ Ξ³ βˆ™ p
  there : (h : x β—‚ p ∈ Ξ³) β†’ (x +1) β—‚ p ∈ Ξ³ βˆ™ q

open import Graded.Modality.Dedicated-nr.Instance

-- Well-usage relation for terms.
--
-- The definition is partly based on Robert Atkey's "Syntax and
-- Semantics of Quantitative Type Theory".
--
-- There are several sets of usage rules for Id, J and K. One (where
-- Id-erased is not inhabited and erased-matches-for-J and
-- erased-matches-for-K are both equal to none) is based on the work
-- of Abel, Danielsson and Vezzosi on adding support for erasure to
-- cubical type theory, and is similar to the following Agda code:
--
--   {-# OPTIONS --erasure --safe --cubical-compatible #-}
--
--   data Id {@0 a} {@0 A : Set a} (x : A) : A β†’ Set a where
--     refl : Id x x
--
--   J :
--     βˆ€ {@0 a} {p} {@0 A : Set a} {x : A}
--     (P : βˆ€ {y} β†’ Id x y β†’ Set p) β†’
--     P (refl {x = x}) β†’
--     {y : A} (x≑y : Id x y) β†’ P x≑y
--   J _ r refl = r
--
-- Note that (at the time of writing) Agda rejects the code if one of
-- the non-erased arguments is made erased. In particular, "P" cannot
-- be made erased.
--
-- Another set of usage rules (where Id-erased is inhabited and
-- erased-matches-for-J and erased-matches-for-K are both equal to
-- all) is based on the following Agda code:
--
--   {-# OPTIONS --erasure --safe --with-K #-}
--
--   open import Agda.Builtin.Sigma
--
--   data Id {@0 a} {@0 A : Set a} (@0 x : A) : @0 A β†’ Set a where
--     refl : Id x x
--
--   J :
--     βˆ€ {@0 a p} {@0 A : Set a} {@0 x : A}
--     (@0 P : βˆ€ {y} β†’ Id x y β†’ Set p) β†’
--     P (refl {x = x}) β†’
--     {@0 y : A} (@0 x≑y : Id x y) β†’ P x≑y
--   J _ r refl = r
--
--   -- One variant of the K rule.
--
--   K :
--     βˆ€ {@0 a p} {@0 A : Set a} {@0 x : A}
--     (@0 P : Id x x β†’ Set p) β†’
--     P refl β†’
--     (@0 x≑x : Id x x) β†’ P x≑x
--   K _ r refl = r
--
--   -- Another variant of the K rule, which can be defined using the
--   -- first variant.
--
--   Kβ€² :
--     βˆ€ {@0 a p} {@0 A : Set a}
--     (@0 P : βˆ€ x β†’ Id x x β†’ Set p) β†’
--     (βˆ€ x β†’ P x refl) β†’
--     (x : A) (@0 x≑x : Id x x) β†’ P x x≑x
--   Kβ€² P r x x≑x = K (P x) (r x) x≑x
--
--   _ :
--     βˆ€ {@0 a p} {@0 A : Set a}
--     (@0 P : βˆ€ x β†’ Id x x β†’ Set p)
--     (r : βˆ€ x β†’ P x refl)
--     (x : A) β†’
--     Id (Kβ€² P r x refl) (r x)
--   _ = Ξ» _ _ _ β†’ refl
--
--   -- The first variant of the K rule can also be defined using the
--   -- second (and J).
--
--   Kβ€³ :
--     βˆ€ {@0 a p} {@0 A : Set a} {@0 x : A}
--     (@0 P : Id x x β†’ Set p) β†’
--     P refl β†’
--     (@0 x≑x : Id x x) β†’ P x≑x
--   Kβ€³ P r x≑x =
--     J (Ξ» {y = eq} _ β†’ P refl β†’ P eq)
--       (Ξ» p β†’ p)
--       (Kβ€² (Ξ» x (x≑x : Id x x) β†’ Id refl x≑x) (Ξ» _ β†’ refl) _ x≑x)
--       r
--
--   _ :
--     βˆ€ {@0 a p} {@0 A : Set a} {@0 x : A}
--     (@0 P : Id x x β†’ Set p)
--     (r : P refl)
--     (@0 x≑x : Id x x) β†’
--     Id (Kβ€³ P r refl) r
--   _ = Ξ» _ _ _ β†’ refl
--
-- Note that the K rule is active in the Agda code. However, the
-- variant of the J rule with an erased motive P can be considered
-- also in the absence of the K rule.
--
-- Yet another set of usage rules (where erased-matches-for-J and
-- erased-matches-for-K are both equal to "some") provides an
-- alternative to []-cong. If 𝟘ᡐ is allowed, then the given usage
-- rules for J more or less give the power of []-cong plus the "none"
-- variants of the usage rules forΒ J:
--
-- * Graded.Box-cong.[]-cong-J is a variant of []-cong defined
--   usingΒ J. This term former satisfies typing rules that are similar
--   to those for []-cong (see Graded.Box-cong), and if the "some"
--   variants of the usage rules for J are used, then the term former
--   satisfies a usage rule that is similar to []-congβ‚˜ (see
--   Graded.Box-cong.β–Έ[]-cong-J).
--
-- * Graded.Derived.Erased.Untyped.Jᡉ is a variant of J that is
--   defined using []-cong. If []-cong is allowed (which at the time
--   of writing implies that the modality is non-trivial, see
--   Definition.Typed.Restrictions.Type-restrictions.[]-cong→¬Trivial),
--   then this term former satisfies typing rules that are similar to
--   those forΒ J (see Graded.Derived.Erased.Typed). Furthermore the
--   term former satisfies a usage rule that is similar to Jβ‚€β‚˜β‚ if 𝟘ᡐ
--   is allowed (see Graded.Derived.Erased.Usage.β–ΈJᡉ).
--
-- The "some" variants of the usage rules for K were included to
-- mirror the rules forΒ J, but if the K rule is available, then it
-- might be a better idea to use the "all" rules.
data _β–Έ[_]_ {n : Nat} : (Ξ³ : Conβ‚˜ n) β†’ Mode β†’ Term n β†’ Set a where
  Uβ‚˜        : 𝟘ᢜ β–Έ[ m ] U
  β„•β‚˜        : 𝟘ᢜ β–Έ[ m ] β„•
  Emptyβ‚˜    : 𝟘ᢜ β–Έ[ m ] Empty
  Unitβ‚˜     : 𝟘ᢜ β–Έ[ m ] Unit s

  Ξ Ξ£β‚˜       : Ξ³ β–Έ[ m ᡐ· p ] F
            β†’ Ξ΄ βˆ™ ⌜ m ⌝ Β· q β–Έ[ m ] G
            β†’ Ξ³ +ᢜ Ξ΄ β–Έ[ m ] ΠΣ⟨ b ⟩ p , q β–· F β–Ή G

  var       : (𝟘ᢜ , x ≔ ⌜ m ⌝) β–Έ[ m ] var x

  lamβ‚˜      : Ξ³ βˆ™ ⌜ m ⌝ Β· p β–Έ[ m ] t
            β†’ Ξ³ β–Έ[ m ] lam p t

  _βˆ˜β‚˜_      : Ξ³ β–Έ[ m ] t
            β†’ Ξ΄ β–Έ[ m ᡐ· p ] u
            β†’ Ξ³ +ᢜ p ·ᢜ Ξ΄ β–Έ[ m ] t ∘⟨ p ⟩ u

  prodΚ·β‚˜    : Ξ³ β–Έ[ m ᡐ· p ] t
            β†’ Ξ΄ β–Έ[ m ] u
            β†’ p ·ᢜ Ξ³ +ᢜ Ξ΄ β–Έ[ m ] prodΚ· p t u

  prodΛ’β‚˜   : Ξ³ β–Έ[ m ᡐ· p ] t
           β†’ Ξ΄ β–Έ[ m ] u
           β†’ p ·ᢜ Ξ³ ∧ᢜ Ξ΄ β–Έ[ m ] prodΛ’ p t u

  -- Note that either pΒ β‰€Β πŸ™ or mβ€²Β β‰‘Β πŸ˜α΅
  fstβ‚˜      : βˆ€ m
            β†’ Ξ³ β–Έ[ m ᡐ· p ] t
            β†’ m ᡐ· p ≑ mβ€²
            β†’ (mβ€² ≑ πŸ™α΅ β†’ p ≀ πŸ™)
            β†’ Ξ³ β–Έ[ mβ€² ] fst p t

  sndβ‚˜      : Ξ³ β–Έ[ m ] t
            β†’ Ξ³ β–Έ[ m ] snd p t

  prodrecβ‚˜  : Ξ³ β–Έ[ m ᡐ· r ] t
            β†’ Ξ΄ βˆ™ ⌜ m ⌝ Β· r Β· p βˆ™ ⌜ m ⌝ Β· r β–Έ[ m ] u
            β†’ Ξ· βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· q β–Έ[ 𝟘ᡐ? ] A
            β†’ Prodrec-allowed m r p q
            β†’ r ·ᢜ Ξ³ +ᢜ Ξ΄ β–Έ[ m ] prodrec r p q A t u

  zeroβ‚˜     : 𝟘ᢜ β–Έ[ m ] zero
  sucβ‚˜      : Ξ³ β–Έ[ m ] t
            β†’ Ξ³ β–Έ[ m ] suc t

  -- A usage rule for natrec which applies if a dedicated nr function
  -- ("natrec usage function") is available.
  natrecβ‚˜   : βˆ€ {s n} ⦃ has-nr : Dedicated-nr ⦄
            β†’ Ξ³ β–Έ[ m ] z
            β†’ Ξ΄ βˆ™ ⌜ m ⌝ Β· p βˆ™ ⌜ m ⌝ Β· r β–Έ[ m ] s
            β†’ Ξ· β–Έ[ m ] n
            β†’ ΞΈ βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· q β–Έ[ 𝟘ᡐ? ] A
            β†’ nrᢜ p r Ξ³ Ξ΄ Ξ· β–Έ[ m ] natrec p q r A z s n

  -- A usage rule for natrec which applies if a dedicated nr function
  -- is not available.
  --
  -- There are four inequality assumptions:
  --
  -- * Two are always required to hold. These assumptions are (at the
  --   time of writing) for instance used to prove the natrec-zero and
  --   natrec-suc cases of the subject reduction lemma
  --   Graded.Reduction.usagePresTerm.
  --
  -- * The assumption Ο‡Β β‰€αΆœΒ Ξ· is only required to hold if the
  --   modality's zero is well-behaved. This assumption is (at the
  --   time of writing) used, together with the two unrestricted
  --   assumptions, to prove the fundamental lemma
  --   Graded.Erasure.LogicalRelation.Fundamental.Fundamental.fundamental
  --   (among other things). The statement of this lemma includes the
  --   assumption that the modality's zero is well-behaved.
  --
  -- * The assumption Ο‡Β β‰€αΆœΒ Ξ΄ is only required to hold if 𝟘ᡐ is
  --   allowed. This assumption is used to prove the substitution
  --   lemma Graded.Substitution.Properties.substβ‚˜-lemma.
  --
  -- Note that this rule may not always be appropriate. See
  -- Graded.Modality.Instances.Linearity.Bad.No-dedicated-nr,
  -- Graded.Modality.Instances.Affine.Bad.No-dedicated-nr and
  -- Graded.Modality.Instances.Linear-or-affine.Bad.No-dedicated-nr
  -- for some examples.
  natrec-no-nrβ‚˜ :
            βˆ€ {n s} ⦃ no-nr : No-dedicated-nr ⦄
            β†’ Ξ³ β–Έ[ m ] z
            β†’ Ξ΄ βˆ™ ⌜ m ⌝ Β· p βˆ™ ⌜ m ⌝ Β· r β–Έ[ m ] s
            β†’ Ξ· β–Έ[ m ] n
            β†’ ΞΈ βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· q β–Έ[ 𝟘ᡐ? ] A
            β†’ Ο‡ β‰€αΆœ Ξ³
            β†’ (T 𝟘ᡐ-allowed β†’
               Ο‡ β‰€αΆœ Ξ΄)
            β†’ (⦃ 𝟘-well-behaved :
                   Has-well-behaved-zero semiring-with-meet ⦄ β†’
               Ο‡ β‰€αΆœ Ξ·)
            β†’ Ο‡ β‰€αΆœ Ξ΄ +ᢜ p ·ᢜ Ξ· +ᢜ r ·ᢜ Ο‡
            β†’ Ο‡ β–Έ[ m ] natrec p q r A z s n

  emptyrecβ‚˜ : Ξ³ β–Έ[ m ᡐ· p ] t
            β†’ Ξ΄ β–Έ[ 𝟘ᡐ? ] A
            β†’ Emptyrec-allowed m p
            β†’ p ·ᢜ Ξ³ β–Έ[ m ] emptyrec p A t

  starΚ·β‚˜    : 𝟘ᢜ β–Έ[ m ] starΚ·

  -- If the strong unit type is not allowed to be used as a sink
  -- then its resources must be 𝟘ᢜ.
  starΛ’β‚˜    : (Β¬StarΛ’-sink β†’ 𝟘ᢜ β‰ˆαΆœ Ξ³)
            β†’ ⌜ m ⌝ ·ᢜ Ξ³ β–Έ[ m ] starΛ’

  unitrecβ‚˜ : Ξ³ β–Έ[ m ᡐ· p ] t
           β†’ Ξ΄ β–Έ[ m ] u
           β†’ Ξ· βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· q β–Έ[ 𝟘ᡐ? ] A
           β†’ Unitrec-allowed m p q
           β†’ p ·ᢜ Ξ³ +ᢜ Ξ΄ β–Έ[ m ] unitrec p q A t u

  Idβ‚˜       : Β¬ Id-erased
            β†’ Ξ³ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ΄ β–Έ[ m ] t
            β†’ Ξ· β–Έ[ m ] u
            β†’ Ξ΄ +ᢜ Ξ· β–Έ[ m ] Id A t u
  Idβ‚€β‚˜      : Id-erased
            β†’ Ξ³ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ΄ β–Έ[ 𝟘ᡐ? ] t
            β†’ Ξ· β–Έ[ 𝟘ᡐ? ] u
            β†’ 𝟘ᢜ β–Έ[ m ] Id A t u
  rflβ‚˜      : 𝟘ᢜ β–Έ[ m ] rfl
  Jβ‚˜        : erased-matches-for-J m ≀ᡉᡐ some
            β†’ (erased-matches-for-J m ≑ some β†’ Β¬ (p ≑ 𝟘 Γ— q ≑ 𝟘))
            β†’ γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ m ] t
            β†’ γ₃ βˆ™ ⌜ m ⌝ Β· p βˆ™ ⌜ m ⌝ Β· q β–Έ[ m ] B
            β†’ Ξ³β‚„ β–Έ[ m ] u
            β†’ Ξ³β‚… β–Έ[ m ] v
            β†’ γ₆ β–Έ[ m ] w
            β†’ Ο‰ ·ᢜ (Ξ³β‚‚ +ᢜ γ₃ +ᢜ Ξ³β‚„ +ᢜ Ξ³β‚… +ᢜ γ₆) β–Έ[ m ] J p q A t B u v w
  Jβ‚€β‚˜β‚      : erased-matches-for-J m ≑ some
            β†’ p ≑ 𝟘
            β†’ q ≑ 𝟘
            β†’ γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ 𝟘ᡐ? ] t
            β†’ γ₃ βˆ™ 𝟘 βˆ™ 𝟘 β–Έ[ m ] B
            β†’ Ξ³β‚„ β–Έ[ m ] u
            β†’ Ξ³β‚… β–Έ[ 𝟘ᡐ? ] v
            β†’ γ₆ β–Έ[ 𝟘ᡐ? ] w
            β†’ Ο‰ ·ᢜ (γ₃ +ᢜ Ξ³β‚„) β–Έ[ m ] J p q A t B u v w
  Jβ‚€β‚˜β‚‚      : erased-matches-for-J m ≑ all
            β†’ γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ 𝟘ᡐ? ] t
            β†’ γ₃ βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· p βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· q β–Έ[ 𝟘ᡐ? ] B
            β†’ Ξ³β‚„ β–Έ[ m ] u
            β†’ Ξ³β‚… β–Έ[ 𝟘ᡐ? ] v
            β†’ γ₆ β–Έ[ 𝟘ᡐ? ] w
            β†’ Ξ³β‚„ β–Έ[ m ] J p q A t B u v w
  Kβ‚˜        : erased-matches-for-K m ≀ᡉᡐ some
            β†’ (erased-matches-for-K m ≑ some β†’ p β‰’ 𝟘)
            β†’ γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ m ] t
            β†’ γ₃ βˆ™ ⌜ m ⌝ Β· p β–Έ[ m ] B
            β†’ Ξ³β‚„ β–Έ[ m ] u
            β†’ Ξ³β‚… β–Έ[ m ] v
            β†’ Ο‰ ·ᢜ (Ξ³β‚‚ +ᢜ γ₃ +ᢜ Ξ³β‚„ +ᢜ Ξ³β‚…) β–Έ[ m ] K p A t B u v
  Kβ‚€β‚˜β‚      : erased-matches-for-K m ≑ some
            β†’ p ≑ 𝟘
            β†’ γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ 𝟘ᡐ? ] t
            β†’ γ₃ βˆ™ 𝟘 β–Έ[ m ] B
            β†’ Ξ³β‚„ β–Έ[ m ] u
            β†’ Ξ³β‚… β–Έ[ 𝟘ᡐ? ] v
            β†’ Ο‰ ·ᢜ (γ₃ +ᢜ Ξ³β‚„) β–Έ[ m ] K p A t B u v
  Kβ‚€β‚˜β‚‚      : erased-matches-for-K m ≑ all
            β†’ γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ 𝟘ᡐ? ] t
            β†’ γ₃ βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· p β–Έ[ 𝟘ᡐ? ] B
            β†’ Ξ³β‚„ β–Έ[ m ] u
            β†’ Ξ³β‚… β–Έ[ 𝟘ᡐ? ] v
            β†’ Ξ³β‚„ β–Έ[ m ] K p A t B u v
  []-congβ‚˜  : γ₁ β–Έ[ 𝟘ᡐ? ] A
            β†’ Ξ³β‚‚ β–Έ[ 𝟘ᡐ? ] t
            β†’ γ₃ β–Έ[ 𝟘ᡐ? ] u
            β†’ Ξ³β‚„ β–Έ[ 𝟘ᡐ? ] v
            β†’ 𝟘ᢜ β–Έ[ m ] []-cong s A t u v

  sub       : Ξ³ β–Έ[ m ] t
            β†’ Ξ΄ β‰€αΆœ Ξ³
            β†’ Ξ΄ β–Έ[ m ] t

starβ‚˜ : 𝟘ᢜ {n} β–Έ[ m ] star s
starβ‚˜ {s = 𝕀} =
  sub (starΛ’β‚˜ Ξ» _ β†’ β‰ˆαΆœ-refl)
      (β‰€αΆœ-reflexive (β‰ˆαΆœ-sym (·ᢜ-zeroΚ³ _)))
starβ‚˜ {s = 𝕨} = starΚ·β‚˜