------------------------------------------------------------------------
-- Inversion properties of the heap reduction relations.
------------------------------------------------------------------------

open import Graded.Modality
open import Graded.Mode
open import Graded.Usage.Restrictions
open import Definition.Typed.Variant
open import Graded.Usage.Restrictions.Natrec

module Graded.Heap.Reduction.Inversion
  {a b} {M : Set a} {Mode : Set b}
  {𝕄 : Modality M}
  {𝐌 : IsMode Mode 𝕄}
  (type-variant : Type-variant)
  (UR : Usage-restrictions 𝕄 𝐌)
  (open Usage-restrictions UR)
  (factoring-nr :
    ⦃ has-nr : Nr-available ⦄ β†’
    Is-factoring-nr M (Natrec-mode-Has-nr 𝕄 has-nr))
  (∣Ρ∣ : M)
  where

open Type-variant type-variant
open Modality 𝕄

open import Definition.Untyped M
open import Definition.Untyped.Properties M

open import Graded.Heap.Untyped type-variant UR factoring-nr ∣Ρ∣
open import Graded.Heap.Reduction type-variant UR factoring-nr ∣Ρ∣

open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Nat
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum

private variable
  m n mβ€² nβ€² nβ€³ k : Nat
  H : Heap _ _
  x : Fin _
  A B t u v w : Term _
  l : Lvl _
  ρ ρ′ : Wk _ _
  S : Stack _
  s : State _ _ _
  sβ€² : Strength
  l₁ lβ‚‚ : Universe-level
  p pβ€² q qβ€² r : M

opaque

  -- Inversion of variables

  β‡Ύβ‚‘-inv-var :
    ⟨ H , var x , ρ , S ⟩ β‡Ύβ‚‘ s β†’
    βˆƒ Ξ» p β†’ ∣ S βˆ£β‰‘ p Γ— State.stack s ≑ S Γ—
    H ⊒ wkVar ρ x ↦[ p ] State.head s , State.env s β¨Ύ State.heap s
  β‡Ύβ‚‘-inv-var (var x y) = _ , x , refl , y
  β‡Ύβ‚‘-inv-var (β‡’β‚‘ ())

opaque

  -- Inversion of variables

  β‡’β‚‘-inv-var :
    ⟨ H , var x , ρ , S ⟩ β‡’β‚‘ s β†’
    State.heap s ≑ H Γ— State.stack s ≑ S Γ—
    H ⊒ wkVar ρ x ↦ (State.head s , State.env s)
  β‡’β‚‘-inv-var (var x) = refl , refl , x
  β‡’β‚‘-inv-var (β‡’β‚‘ ())

opaque

  -- Inversion of lower

  β‡’β‚‘-inv-lower :
    ⟨ H , lower t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , lowerβ‚‘ βˆ™ S ⟩
  β‡’β‚‘-inv-lower lowerβ‚• = refl

opaque

  -- Inversion of application

  β‡’β‚‘-inv-∘ :
    ⟨ H , t ∘⟨ p ⟩ u , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , βˆ˜β‚‘ p u ρ βˆ™ S ⟩
  β‡’β‚‘-inv-∘ appβ‚• = refl

opaque

  -- Inversion of fst

  β‡’β‚‘-inv-fst :
    ⟨ H , fst p t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , fstβ‚‘ p βˆ™ S ⟩
  β‡’β‚‘-inv-fst fstβ‚• = refl

opaque

  -- Inversion of snd

  β‡’β‚‘-inv-snd :
    ⟨ H , snd p t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , sndβ‚‘ p βˆ™ S ⟩
  β‡’β‚‘-inv-snd sndβ‚• = refl

opaque

  -- Inversion of prodrec

  β‡’β‚‘-inv-prodrec :
    ⟨ H , prodrec r p q A t u , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , prodrecβ‚‘ r p q A u ρ βˆ™ S ⟩
  β‡’β‚‘-inv-prodrec prodrecβ‚• = refl

opaque

  -- Inversion of natrec

  β‡’β‚‘-inv-natrec :
    ⟨ H , natrec p q r A u v t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , natrecβ‚‘ p q r A u v ρ βˆ™ S ⟩
  β‡’β‚‘-inv-natrec natrecβ‚• = refl

opaque

  -- Inversion of unitrec

  β‡’β‚‘-inv-unitrec :
    ⟨ H , unitrec p q A t u , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , unitrecβ‚‘ p q A u ρ βˆ™ S ⟩ Γ— Β¬ UnitΚ·-Ξ·
  β‡’β‚‘-inv-unitrec (unitrecβ‚• x) = refl , x

opaque

  -- Inversion of emptyrec

  β‡’β‚‘-inv-emptyrec :
    ⟨ H , emptyrec p A t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , emptyrecβ‚‘ p A ρ βˆ™ S ⟩
  β‡’β‚‘-inv-emptyrec emptyrecβ‚• = refl

opaque

  -- Inversion of J

  β‡’β‚‘-inv-J :
    ⟨ H , J p q A u B v w t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , Jβ‚‘ p q A u B v w ρ βˆ™ S ⟩
  β‡’β‚‘-inv-J Jβ‚• = refl

opaque

  -- Inversion of K

  β‡’β‚‘-inv-K : ⟨ H , K p A u B v t , ρ , S ⟩ β‡’β‚‘ s β†’
             s ≑ ⟨ H , t , ρ , Kβ‚‘ p A u B v ρ βˆ™ S ⟩
  β‡’β‚‘-inv-K Kβ‚• = refl

opaque

  -- Inversion of []-cong

  β‡’β‚‘-inv-[]-cong :
    ⟨ H , []-cong sβ€² l A u v t , ρ , S ⟩ β‡’β‚‘ s β†’
    s ≑ ⟨ H , t , ρ , []-congβ‚‘ sβ€² l A u v ρ βˆ™ S ⟩
  β‡’β‚‘-inv-[]-cong []-congβ‚• = refl

opaque

  -- Inversion of lift

  β‡’α΅₯-inv-lift :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , lift t , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒ Ξ» Sβ€² β†’ Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      S ≑ lowerβ‚‘ βˆ™ Sβ€² Γ— substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , t , ρ , Sβ€² ⟩
  β‡’α΅₯-inv-lift liftβ‚• = _ , refl , refl , refl , refl

opaque

  -- Inversion of lift with lower on top of the stack

  β‡’α΅₯-inv-lift-lowerβ‚‘ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , lift t , ρ , lowerβ‚‘ βˆ™ S ⟩ β‡’α΅₯ s β†’
    Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , t , ρ , S ⟩
  β‡’α΅₯-inv-lift-lowerβ‚‘ d =
    case β‡’α΅₯-inv-lift d of Ξ» where
      (_ , refl , refl , refl , refl) β†’
        refl , refl , refl

opaque

  -- Inversion of lambda

  β‡’α΅₯-inv-lam :
    {H : Heap k mβ€²} {t : Term (1+ nβ€²)} {s : State _ m n} β†’
    ⟨ H , lam p t , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚… Ξ» k q u (ρ′ : Wk _ k) Sβ€² β†’ ∣ Sβ€² βˆ£β‰‘ q Γ— S ≑ βˆ˜β‚‘ p u ρ′ βˆ™ Sβ€² Γ—
       Ξ£ (m ≑ 1+ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ 1+ nβ€²) Ξ» n≑ β†’
         substβ‚‚ (State _) m≑ n≑ s ≑
           ⟨ H βˆ™ (q Β· p , u , ρ′) , t , lift ρ , wk1Λ’ Sβ€² ⟩
  β‡’α΅₯-inv-lam (lamβ‚• x) = _ , _ , _ , _ , _ , x , refl , refl , refl , refl

opaque

  -- Inversion of lambda with an application on top of the stack

  β‡’α΅₯-inv-lam-βˆ˜β‚‘ :
    {H : Heap k mβ€²} {t : Term (1+ nβ€²)} {s : State _ m n} β†’
    ⟨ H , lam p t , ρ , βˆ˜β‚‘ q u ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    βˆƒ Ξ» q β†’ ∣ S βˆ£β‰‘ q Γ—
    Ξ£ (m ≑ 1+ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ 1+ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑
        ⟨ H βˆ™ (q Β· p , u , ρ′) , t , lift ρ , wk1Λ’ S ⟩
  β‡’α΅₯-inv-lam-βˆ˜β‚‘ d =
    case β‡’α΅₯-inv-lam d of Ξ» {
      (_ , _ , _ , _ , _ , ∣Sβˆ£β‰‘ , refl , refl , refl , refl) β†’
    _ , ∣Sβˆ£β‰‘ , refl , refl , refl }

opaque

  -- Inversion of prodΛ’

  β‡’α΅₯-inv-prodΛ’ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , prodΛ’ p t u , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒ Ξ» Sβ€² β†’ Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      (S ≑ fstβ‚‘ p βˆ™ Sβ€² Γ— substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , t , ρ , Sβ€² ⟩ ⊎
       S ≑ sndβ‚‘ p βˆ™ Sβ€² Γ— substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ , Sβ€² ⟩)
  β‡’α΅₯-inv-prodΛ’ prod˒ₕ₁ = _ , refl , refl , inj₁ (refl , refl)
  β‡’α΅₯-inv-prodΛ’ prodΛ’β‚•β‚‚ = _ , refl , refl , injβ‚‚ (refl , refl)

opaque

  -- Inversion of prodΛ’ with a first projection on top of the stack

  β‡’α΅₯-inv-prodΛ’-fstβ‚‘ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , prodΛ’ p t u , ρ , fstβ‚‘ q βˆ™ S ⟩ β‡’α΅₯ s β†’
    Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , t , ρ , S ⟩
  β‡’α΅₯-inv-prodΛ’-fstβ‚‘ d =
    case β‡’α΅₯-inv-prodΛ’ d of Ξ» where
      (_ , refl , refl , inj₁ (refl , refl)) β†’
        refl , refl , refl
      (_ , _ , _ , injβ‚‚ (() , _))

opaque

  -- Inversion of prodΛ’ with a second projection on top of the stack

  β‡’α΅₯-inv-prodΛ’-sndβ‚‘ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , prodΛ’ p t u , ρ , sndβ‚‘ q βˆ™ S ⟩ β‡’α΅₯ s β†’
      Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
        substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ , S ⟩
  β‡’α΅₯-inv-prodΛ’-sndβ‚‘ d =
    case β‡’α΅₯-inv-prodΛ’ d of Ξ» where
      (_ , _    , _    , inj₁ (() , _))
      (_ , refl , refl , injβ‚‚ (refl , refl)) β†’
        refl , refl , refl

opaque

  -- Inversion of prodΚ·

  β‡’α΅₯-inv-prodΚ· :
    {H : Heap k mβ€²} {t u : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , prodΚ· p t u , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚ˆ Ξ» k r q qβ€² A v (ρ′ : Wk _ k) Sβ€² β†’ ∣ Sβ€² βˆ£β‰‘ qβ€² Γ— S ≑ prodrecβ‚‘ r p q A v ρ′ βˆ™ Sβ€² Γ—
    Ξ£ (m ≑ 2+ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ 2+ k) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑
        ⟨ H βˆ™ (qβ€² Β· r Β· p , t , ρ) βˆ™ (qβ€² Β· r , u , step ρ) , v
           , liftn ρ′ 2 , wk2Λ’ Sβ€² ⟩
  β‡’α΅₯-inv-prodΚ· (prodΚ·β‚• x) =
    _ , _ , _ , _ , _ , _ , _ , _ , x , refl , refl , refl , refl

opaque

  -- Inversion of prodΚ· with prodrec on top of the stack

  β‡’α΅₯-inv-prodΚ·-prodrecβ‚‘ :
    {H : Heap k mβ€²} {v : Term (2+ nβ€³)} {s : State _ m n} β†’
    ⟨ H , prodΚ· p t u , ρ , prodrecβ‚‘ r pβ€² q A v ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    βˆƒ Ξ» qβ€² β†’ ∣ S βˆ£β‰‘ qβ€² Γ—
    Ξ£ (m ≑ 2+ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ 2+ nβ€³) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑
        ⟨ H βˆ™ (qβ€² Β· r Β· p , t , ρ) βˆ™ (qβ€² Β· r , u , step ρ) , v
           , liftn ρ′ 2 , wk2Λ’ S ⟩
  β‡’α΅₯-inv-prodΚ·-prodrecβ‚‘ d =
    case β‡’α΅₯-inv-prodΚ· d of Ξ» {
      (_ , _ , _  , _ , _ , _ , _ , _ , ∣Sβˆ£β‰‘ , refl , refl , refl , refl) β†’
    _ , ∣Sβˆ£β‰‘ , refl , refl , refl}

opaque

  -- Inversion of zero

  β‡’α΅₯-inv-zero :
    {H : Heap k mβ€²} {s : State _ m n} β†’
    ⟨ H , zero , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚‰ Ξ» nβ€² p q r A u v (ρ′ : Wk _ nβ€²) Sβ€² β†’
       S ≑ natrecβ‚‘ p q r A u v ρ′ βˆ™ Sβ€² Γ—
       Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
         substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ′ , Sβ€² ⟩
  β‡’α΅₯-inv-zero zeroβ‚• =
    _ , _ , _ , _ , _ , _ , _ , _ , _ , refl , refl , refl , refl

opaque

  -- Inversion of zero with natrec on top of the stack

  β‡’α΅₯-inv-zero-natrecβ‚‘ :
    {H : Heap k mβ€²} {u : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , zero , ρ , natrecβ‚‘ p q r A u v ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ′ , S ⟩
  β‡’α΅₯-inv-zero-natrecβ‚‘ d =
    case β‡’α΅₯-inv-zero d of Ξ» {
      (_ , _ , _ , _ , _ , _ , _ , _ , _
         , refl , refl , refl , refl) β†’
    refl , refl , refl }

opaque

  -- Inversion of suc

  β‡’α΅₯-inv-suc :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , suc t , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚β‚ Ξ» nβ€² p q r qβ€² pβ€² A u v (ρ′ : Wk _ nβ€²) Sβ€² β†’
       ∣ Sβ€² βˆ£β‰‘ qβ€² Γ— ∣natrec p , r βˆ£β‰‘ pβ€² Γ—
       S ≑ natrecβ‚‘ p q r A u v ρ′ βˆ™ Sβ€² Γ—
       Ξ£ (m ≑ 2+ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ 2+ nβ€²) Ξ» n≑ β†’
         substβ‚‚ (State _) m≑ n≑ s ≑
           ⟨ H βˆ™ (qβ€² Β· pβ€² , t , ρ)
              βˆ™ (qβ€² Β· r , natrec p q r (wk (lift (step id)) A)
                              (wk1 u) (wk (liftn (step id) 2) v) (var x0)
                            , lift ρ′)
              , v , liftn ρ′ 2  , wk2Λ’ Sβ€² ⟩
  β‡’α΅₯-inv-suc (sucβ‚• ∣Sβˆ£β‰‘ ∣nrβˆ£β‰‘) =
    _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _ , ∣Sβˆ£β‰‘ , ∣nrβˆ£β‰‘ , refl , refl , refl , refl

opaque

  -- Inversion of suc with natrec on top of the stack

  β‡’α΅₯-inv-suc-natrecβ‚‘ :
    {H : Heap k mβ€²} {u : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , suc t , ρ , natrecβ‚‘ p q r A u v ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚‚ Ξ» qβ€² pβ€² β†’ ∣ S βˆ£β‰‘ qβ€² Γ— ∣natrec p , r βˆ£β‰‘ pβ€² Γ—
    Ξ£ (m ≑ 2+ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ 2+ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑
        ⟨ H βˆ™ (qβ€² Β· pβ€² , t , ρ)
            βˆ™ (qβ€² Β· r , natrec p q r (wk (lift (step id)) A) (wk1 u)
                             (wk (liftn (step id) 2) v) (var x0)
                         , lift ρ′)
            , v , liftn ρ′ 2  , wk2Λ’ S ⟩
  β‡’α΅₯-inv-suc-natrecβ‚‘ d =
    case β‡’α΅₯-inv-suc d of Ξ» {
      (_ , _ , _ , _ , _ , _ , _ , _ , _ , _ , _
         , ∣Sβˆ£β‰‘ , ∣nrβˆ£β‰‘ , refl , refl , refl , refl) β†’
    _ , _ , ∣Sβˆ£β‰‘ , ∣nrβˆ£β‰‘ , refl , refl , refl}

opaque

  -- Inversion of starΚ·

  β‡’α΅₯-inv-starΚ· :
    {H : Heap k mβ€²} {s : State _ m n} β†’
    ⟨ H , starΚ· , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚‡ Ξ» nβ€² p q A u (ρ′ : Wk _ nβ€²) Sβ€² β†’
    S ≑ unitrecβ‚‘ p q A u ρ′ βˆ™ Sβ€² Γ—
    βˆƒβ‚‚ Ξ» (m≑ : m ≑ mβ€²) (n≑ : n ≑ nβ€²) β†’
    substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ′ , Sβ€² ⟩
  β‡’α΅₯-inv-starΚ· starΚ·β‚• =
    _ , _ , _ , _ , _ , _ , _ , refl , refl , refl , refl

opaque

  -- Inversion of starΚ· with unitrec on top of the stack

  β‡’α΅₯-inv-starΚ·-unitrecβ‚‘ :
    {H : Heap k mβ€²} {u : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , starΚ· , ρ , unitrecβ‚‘ p q A u ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚‚ Ξ» (m≑ : m ≑ mβ€²) (n≑ : n ≑ nβ€²) β†’
    substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ′ , S ⟩
  β‡’α΅₯-inv-starΚ·-unitrecβ‚‘ d =
    case β‡’α΅₯-inv-starΚ· d of Ξ» {
      (_ , _ , _ , _ , _ , _ , _ , refl , refl , refl , refl) β†’
    refl , refl , refl }

opaque

  -- Inversion of unitrec with eta equality turned on

  β‡’α΅₯-inv-unitrec-Ξ· :
    {H : Heap k mβ€²} {s : State _ m n} β†’
    ⟨ H , unitrec p q A t u , ρ , S ⟩ β‡’α΅₯ s β†’
    UnitΚ·-Ξ· Γ— βˆƒβ‚‚ Ξ» (m≑ : m ≑ mβ€²) (n≑ : n ≑ nβ€²) β†’
    substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ , S ⟩
  β‡’α΅₯-inv-unitrec-Ξ· (unitrec-Ξ·β‚• x) = x , refl , refl , refl

opaque

  -- Inversion of rfl

  β‡’α΅₯-inv-rfl :
    {H : Heap k mβ€²} {s : State _ m n} β†’
    ⟨ H , rfl , ρ , S ⟩ β‡’α΅₯ s β†’
    βˆƒβ‚… Ξ» Sβ€² A t u ρ′ β†’ Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’
      (βˆƒβ‚„ Ξ» p q B v β†’ S ≑ Jβ‚‘ p q A t B u v ρ′ βˆ™ Sβ€² Γ—
          subst (Ξ» m β†’ State _ m _) m≑ s ≑ ⟨ H , u , ρ′ , Sβ€² ⟩) ⊎
      (βˆƒβ‚‚ Ξ» p B β†’ S ≑ Kβ‚‘ p A t B u ρ′ βˆ™ Sβ€² Γ—
          subst (Ξ» m β†’ State _ m _) m≑ s ≑ ⟨ H , u , ρ′ , Sβ€² ⟩) ⊎
      (βˆƒβ‚‚ Ξ» sβ€² l β†’ S ≑ []-congβ‚‘ sβ€² l A t u ρ′ βˆ™ Sβ€² Γ—
         subst (Ξ» m β†’ State _ m _) m≑ s ≑ ⟨ H , rfl , ρ′ , Sβ€² ⟩)
  β‡’α΅₯-inv-rfl rflβ‚•β±Ό =
    _ , _ , _ , _ , _ , refl , inj₁ (_ , _ , _ , _ , refl , refl)
  β‡’α΅₯-inv-rfl rflβ‚•β‚– =
    _ , _ , _ , _ , _ , refl , injβ‚‚ (inj₁ (_ , _ , refl , refl))
  β‡’α΅₯-inv-rfl rflβ‚•β‚‘ =
    _ , _ , _ , _ , _ , refl , injβ‚‚ (injβ‚‚ (_ , _ , refl , refl))

opaque

  -- Inversion of rfl with Jβ‚‘ on top of the stack

  β‡’α΅₯-inv-rfl-Jβ‚‘ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , rfl , ρ , Jβ‚‘ p q A t B u v ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ′ , S ⟩
  β‡’α΅₯-inv-rfl-Jβ‚‘ d =
    case β‡’α΅₯-inv-rfl d of Ξ» where
      (_ , _ , _ , _ , _ , refl , inj₁ (_ , _ , _ , _ , refl , refl)) β†’
        refl , refl , refl
      (_ , _ , _ , _ , _ , refl , injβ‚‚ (inj₁ (_ , _ , () , _)))
      (_ , _ , _ , _ , _ , refl , injβ‚‚ (injβ‚‚ ()))

opaque

  -- Inversion of rfl with Kβ‚‘ on top of the stack

  β‡’α΅₯-inv-rfl-Kβ‚‘ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , rfl , ρ , Kβ‚‘ p A t B u ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , u , ρ′ , S ⟩
  β‡’α΅₯-inv-rfl-Kβ‚‘ d =
    case β‡’α΅₯-inv-rfl d of Ξ» where
      (_ , _ , _ , _ , _ , refl , inj₁ (_ , _ , _ , _ , () , _))
      (_ , _ , _ , _ , _ , refl , injβ‚‚ (inj₁ (_ , _ , refl , refl))) β†’
        refl , refl , refl
      (_ , _ , _ , _ , _ , refl , injβ‚‚ (injβ‚‚ ()))

opaque

  -- Inversion of rfl with []-congβ‚‘ on top of the stack

  β‡’α΅₯-inv-rfl-[]-congβ‚‘ :
    {H : Heap k mβ€²} {t : Term nβ€²} {s : State _ m n} β†’
    ⟨ H , rfl , ρ , []-congβ‚‘ sβ€² l A t u ρ′ βˆ™ S ⟩ β‡’α΅₯ s β†’
    Ξ£ (m ≑ mβ€²) Ξ» m≑ β†’ Ξ£ (n ≑ nβ€²) Ξ» n≑ β†’
      substβ‚‚ (State _) m≑ n≑ s ≑ ⟨ H , rfl , ρ′ , S ⟩
  β‡’α΅₯-inv-rfl-[]-congβ‚‘ d =
    case β‡’α΅₯-inv-rfl d of Ξ» where
      (_ , _ , _ , _ , _ , refl , inj₁ (_ , _ , _ , _ , () , _))
      (_ , _ , _ , _ , _ , refl , injβ‚‚ (inj₁ (_ , _ , () , _)))
      (_ , _ , _ , _ , _ , refl , injβ‚‚ (injβ‚‚ (_ , _ , refl , refl))) β†’
        refl , refl , refl

opaque

  -- Inversion of suc

  β‡’β‚™-inv-suc :
    Β¬ Numeral t β†’ ⟨ H , suc t , ρ , S ⟩ β‡’β‚™ s β†’
    βˆƒ Ξ» k β†’ S ≑ sucβ‚› k Γ— s ≑ ⟨ H , t , ρ , sucβ‚‘ βˆ™ S ⟩
  β‡’β‚™-inv-suc _ (sucβ‚• _) = _ , refl , refl
  β‡’β‚™-inv-suc Β¬n (numβ‚• (sucβ‚™ n)) = βŠ₯-elim (Β¬n n)

opaque

  -- Inversion of numerals

  β‡’β‚™-inv-num :
    Numeral t β†’ ⟨ H , t , ρ , S ⟩ β‡’β‚™ s β†’
    βˆƒ Ξ» Sβ€² β†’ S ≑ sucβ‚‘ βˆ™ Sβ€² Γ— s ≑ ⟨ H , suc t , ρ , Sβ€² ⟩
  β‡’β‚™-inv-num (sucβ‚™ n) (sucβ‚• Β¬n) = βŠ₯-elim (Β¬n n)
  β‡’β‚™-inv-num _ (numβ‚• _) = _ , refl , refl

opaque

  -- Inversion of variable

  β‡’α΅₯-inv-var : ⟨ H , var x , ρ , S ⟩ β‡’α΅₯ s β†’ βŠ₯
  β‡’α΅₯-inv-var ()

opaque

  -- Inversion of lift

  β‡’β‚‘-inv-lift : ⟨ H , lift t , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-lift ()

opaque

  -- Inversion of lambda

  β‡’β‚‘-inv-lam : ⟨ H , lam p t , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-lam ()

opaque

  -- Inversion of prod

  β‡’β‚‘-inv-prod : ⟨ H , prod sβ€² p t u , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-prod ()

opaque

  -- Inversion of zero

  β‡’β‚‘-inv-zero : ⟨ H , zero , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-zero ()

opaque

  -- Inversion of suc

  β‡’β‚‘-inv-suc : ⟨ H , suc t , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-suc ()

opaque

  -- Inversion of star

  β‡’β‚‘-inv-star : ⟨ H , star sβ€² , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-star ()

opaque

  -- Inversion of unitrec with Ξ·-equality

  β‡’β‚‘-inv-unitrec-Ξ· :
    UnitΚ·-Ξ· β†’ ⟨ H , unitrec p q A t u , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-unitrec-Ξ· Ξ· (unitrecβ‚• no-Ξ·) = no-Ξ· Ξ·

opaque

  -- Inversion of rfl

  β‡’β‚‘-inv-rfl : ⟨ H , rfl , ρ , S ⟩ β‡’β‚‘ s β†’ βŠ₯
  β‡’β‚‘-inv-rfl ()

opaque

  -- Inversion of variable

  β‡’β‚™-inv-var : ⟨ H , var x , ρ , S ⟩ β‡’β‚™ s β†’ βŠ₯
  β‡’β‚™-inv-var (numβ‚• ())

opaque

  -- Inversion of natrec

  β‡’β‚™-inv-natrec : ⟨ H , natrec p q r A t u v , ρ , S ⟩ β‡’β‚™ s β†’ βŠ₯
  β‡’β‚™-inv-natrec (numβ‚• ())

opaque

  -- Inversion for sucⁿ.

  β† -inv-sucⁿ : ⟨ H , sucⁿ k , ρ , Ξ΅ ⟩ β†  s β†’ βŠ₯
  β† -inv-sucⁿ {k = 0} (β‡Ύβ‚‘β€² x) = β‡’β‚‘-inv-zero x
  β† -inv-sucⁿ {k = 1+ k} (β‡Ύβ‚‘β€² x) = β‡’β‚‘-inv-suc x
  β† -inv-sucⁿ {k = 0} (β‡’α΅₯ ())
  β† -inv-sucⁿ {k = 1+ k} (β‡’α΅₯ ())
  β† -inv-sucⁿ {k = 0} (β‡’β‚™ ())
  β† -inv-sucⁿ {k = 1+ k} (β‡’β‚™ x) =
    case β‡’β‚™-inv-num (sucⁿ-Numeral _) x of Ξ» where
      (_ , () , _)