------------------------------------------------------------------------
-- 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.Mode 𝕄
open import Graded.Usage.Erased-matches
open import Graded.Usage.Restrictions.Instance R
open import Graded.Usage.Restrictions.Natrec 𝕄
open import Definition.Untyped M

open import Tools.Bool using (T; true; false)
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat; 1+)
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation

infix 10 _β–Έ[_]_

private
  variable
    n l : 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
    nm : Natrec-mode

-- 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 natrec.

βŒˆβŒ‰-natrec :
  ⦃ ok : Natrec-mode-supports-usage-inference nm ⦄ β†’
  (p r : M) (Ξ³ Ξ΄ Ξ· : Conβ‚˜ n) β†’ Conβ‚˜ n
βŒˆβŒ‰-natrec ⦃ ok = Nr ⦃ (has-nr) ⦄ ⦄ p r Ξ³ Ξ΄ Ξ· = nrᢜ ⦃ has-nr ⦄ p r Ξ³ Ξ΄ Ξ·
βŒˆβŒ‰-natrec ⦃ ok = No-nr-glb has-GLB ⦄ p r Ξ³ Ξ΄ Ξ· =
  let x , _ = has-GLB r πŸ™ p
      Ο‡ , _ = nrᡒᢜ-has-GLBᢜ has-GLB r Ξ³ Ξ΄
  in  x ·ᢜ Ξ· +ᢜ Ο‡

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

infix 50 ⌈_βŒ‰

mutual
  ⌈_βŒ‰ :
    ⦃ ok : Natrec-mode-supports-usage-inference natrec-mode ⦄ β†’
    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 =
    βŒˆβŒ‰-natrec 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

-- 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).
--
-- * Definition.Untyped.Erased.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 Definition.Typed.Properties.Admissible.Erased).
--   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
  sub       : Ξ³ β–Έ[ m ] t
            β†’ Ξ΄ β‰€αΆœ Ξ³
            β†’ Ξ΄ β–Έ[ m ] t

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

  Uβ‚˜        : 𝟘ᢜ β–Έ[ m ] U l

  Emptyβ‚˜    : 𝟘ᢜ β–Έ[ m ] Empty

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

  Unitβ‚˜     : 𝟘ᢜ β–Έ[ m ] Unit s l

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

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

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

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

  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

  -- 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

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

  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

  β„•β‚˜        : 𝟘ᢜ β–Έ[ m ] β„•

  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 : Nr-available ⦄
            β†’ Ξ³ β–Έ[ 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.Examples.Bad.No-nr,
  -- Graded.Modality.Instances.Affine.Examples.Bad.No-nr and
  -- Graded.Modality.Instances.Linear-or-affine.Examples.Bad.No-nr
  -- for some examples.
  natrec-no-nrβ‚˜ :
            βˆ€ {n s} ⦃ no-nr : Nr-not-available ⦄
            β†’ Ξ³ β–Έ[ 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

  -- Another usage rule for natrec which applies if a dedicated nr function
  -- is not available.
  --
  -- The usage count of natrec is assumed to consist of one part representing
  -- the usage contributions of the natural number and one part representing
  -- the usage contributions of the zero and successor cases.
  --
  -- The contribution of the natural number argument is given by the greatest
  -- lower bound of the sequence nrα΅’Β rΒ πŸ™Β p. The elements of the sequence
  -- represents the usage count of the natural number for a given number of
  -- unfoldings.
  -- When the natural number argument is zero the natural number argument is used
  -- once (for matching). This is represented by nrβ‚€Β rΒ πŸ™Β pΒ β‰‘Β πŸ™. When the natural
  -- number argument is sucΒ n, the argument is used p times (by the successor case)
  -- plus an additional number of times in the recursive call. Assuming a
  -- suitable substitution lemma, the total usage counts become pΒ +Β rΒ Β·Β nrα΅’Β rΒ πŸ™Β p
  -- where nrα΅’Β rΒ πŸ™Β p is the usage count of the recursive call (being unfolded
  -- one time less). The greatest lower bound of all these usage counts is
  -- then compatible with all possible unfoldings (via subsumption)
  --
  -- The contribution of the zero and successor cases is similarly given by
  -- the greatest lower bound of the sequence nrᡒᢜ r γ δ. As before, each
  -- element of the sequence corresponds to the total usage count for a given
  -- number of unfoldings.

  natrec-no-nr-glbβ‚˜ :
           βˆ€ {n s x} ⦃ no-nr : Nr-not-available-GLB ⦄
           β†’ Ξ³ β–Έ[ m ] z
           β†’ Ξ΄ βˆ™ ⌜ m ⌝ Β· p βˆ™ ⌜ m ⌝ Β· r β–Έ[ m ] s
           β†’ Ξ· β–Έ[ m ] n
           β†’ ΞΈ βˆ™ ⌜ 𝟘ᡐ? ⌝ Β· q β–Έ[ 𝟘ᡐ? ] A
           β†’ Greatest-lower-bound x (nrα΅’ r πŸ™ p)
           β†’ Greatest-lower-boundᢜ Ο‡ (nrᡒᢜ r Ξ³ Ξ΄)
           β†’ x ·ᢜ Ξ· +ᢜ Ο‡ β–Έ[ m ] natrec p q r A z s n

  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
            β†’ []-cong-allowed-mode s m
            β†’ 𝟘ᢜ β–Έ[ m ] []-cong s A t u v

-- Usage with implicit mode πŸ™α΅

_β–Έ_ : (Ξ³ : Conβ‚˜ n) (t : Term n) β†’ Set a
Ξ³ β–Έ t = Ξ³ β–Έ[ πŸ™α΅ ] t

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