module LabelExpr.CatchUp where

open import Data.Nat
open import Data.Unit using (⊀; tt)
open import Data.Bool using (true; false) renaming (Bool to 𝔹)
open import Data.List hiding ([_])
open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_)
open import Data.Maybe
open import Relation.Nullary using (Β¬_; Dec; yes; no)
open import Relation.Binary.PropositionalEquality using (_≑_; refl)
open import Function using (case_of_)

open import Common.Utils
open import Common.SecurityLabels
open import Common.BlameLabels

open import LabelExpr.LabelExpr

open import CoercionExpr.CoercionExpr renaming (_β€”β†’βŸ¨_⟩_ to _β€”β†’β‚—βŸ¨_⟩_ ; _∎ to _βˆŽβ‚—)
open import CoercionExpr.Precision renaming (precβ†’βŠ‘ to precβ‚—β†’βŠ‘)
open import CoercionExpr.SyntacComp
open import CoercionExpr.CatchUp renaming (catchup to catchupβ‚—)


catchup : βˆ€ {g gβ€²} {M Vβ€²}
  β†’ LVal Vβ€²
  β†’ ⊒ M βŠ‘ Vβ€² ⇐ g βŠ‘ gβ€²
    -----------------------------------------------------------
  β†’ βˆƒ[ V ] (LVal V) Γ— (M β€”β† β‚‘ V) Γ— (⊒ V βŠ‘ Vβ€² ⇐ g βŠ‘ gβ€²)
catchup v-l βŠ‘-l = ⟨ _ , v-l , _ ∎ , βŠ‘-l ⟩
catchup v-l (βŠ‘-castl {g₁} {gβ‚‚} {gβ€²} {M} {Mβ€²} {cΜ…} MβŠ‘β„“ cΜ…βŠ‘β„“)
  with catchup v-l MβŠ‘β„“
... | ⟨ l β„“ , v-l , Mβ† V , βŠ‘-l ⟩ =
  case catchupβ‚— cΜ… (id gβ€²) id (βŠ‘-left-expand cΜ…βŠ‘β„“) of Ξ» where
  ⟨ id _ , id , _ βˆŽβ‚— , cΜ…β‚™βŠ‘id ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-l ⟩
  ⟨ id _ , id , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘id ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫        β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-l ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , _ βˆŽβ‚— , cΜ…β‚™βŠ‘id ⟩ β†’
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , plug-congβ‚‘ Mβ† V ,
      βŠ‘-castl βŠ‘-l (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘id ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-castl βŠ‘-l (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , cΜ…β† cΜ…β‚™ , βŠ‘-castl _ lβŠ‘l () ⟩ {- a coercion value from high β‡’ low is impossible -}
... | ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V , βŠ‘-castl βŠ‘-l cΜ…β‚βŠ‘β„“ ⟩ =
  case catchupβ‚— (c̅₁ ⨟ cΜ…) (id gβ€²) id (βŠ‘-left-expand (comp-pres-βŠ‘-ll cΜ…β‚βŠ‘β„“ cΜ…βŠ‘β„“)) of Ξ» where
  ⟨ id _ , id , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘id ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ id) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-l ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘id ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (inj 𝓋)) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-castl βŠ‘-l (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , βŠ‘-castl _ lβŠ‘l () ⟩ {- a coercion value from high β‡’ low is impossible -}
catchup (v-cast (ir 𝓋′ x )) (βŠ‘-cast {g₁} {g₁′} {gβ‚‚} {gβ‚‚β€²} {M} {Mβ€²} {cΜ…} {cΜ…β€²} MβŠ‘Vβ€² cΜ…βŠ‘cΜ…β€²)
  with catchup v-l MβŠ‘Vβ€²
... | ⟨ l β„“ , v-l , Mβ† V , βŠ‘-l ⟩ =
  case catchupβ‚— cΜ… cΜ…β€² 𝓋′ cΜ…βŠ‘cΜ…β€² of Ξ» where
  ⟨ id _ , id , _ βˆŽβ‚— , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l (βŠ‘-right-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
  ⟨ id _ , id , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫        β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l (βŠ‘-right-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , _ βˆŽβ‚— , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , plug-congβ‚‘ Mβ† V , βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ , βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , up id , _ βˆŽβ‚— , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘cΜ…β€²) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’ ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up id) x ) , plug-congβ‚‘ Mβ† V , βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , up id , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) (up id) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘cΜ…β€²) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’ ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up id) x ) , β™₯ , βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
... | ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V , βŠ‘-castl βŠ‘-l cΜ…β‚βŠ‘β„“ ⟩ =
  case catchupβ‚— (c̅₁ ⨟ cΜ…) cΜ…β€² 𝓋′ (comp-pres-βŠ‘-lb cΜ…β‚βŠ‘β„“ cΜ…βŠ‘cΜ…β€²) of Ξ» where
  ⟨ id _ , id , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ id) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l (βŠ‘-right-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (inj 𝓋)) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , up id , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘cΜ…β€²) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’
      let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
              (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
              l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (up id)) (up id) ⟩
              l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
      ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up id) x) , β™₯ ,
        βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
catchup (v-cast (ir 𝓋′ x )) (βŠ‘-castl {g₁} {gβ‚‚} {gβ€²} {M} {Mβ€²} {cΜ…} MβŠ‘Vβ€² cΜ…βŠ‘gβ€²)
  with catchup (v-cast (ir 𝓋′ x)) MβŠ‘Vβ€²
... | ⟨ l β„“ , v-l , Mβ† V , βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€² ⟩ =
  case catchupβ‚— cΜ… (id gβ€²) id (βŠ‘-left-expand cΜ…βŠ‘gβ€²) of Ξ» where
  ⟨ id _ , id , _ βˆŽβ‚— , cΜ…β‚™βŠ‘id ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€² ⟩
  ⟨ id _ , id , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘id ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫        β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , _ βˆŽβ‚— , cΜ…β‚™βŠ‘id ⟩ β†’
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , plug-congβ‚‘ Mβ† V ,
      βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘id ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , _ βˆŽβ‚— , cΜ…β‚™βŠ‘id ⟩ β†’
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘id) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’
      ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up 𝓋) x) , plug-congβ‚‘ Mβ† V ,
             βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , _ β€”β†’β‚—βŸ¨ r ⟩ r* , cΜ…β‚™βŠ‘id ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ cast (_ β€”β†’β‚—βŸ¨ r ⟩ r*) (up 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘id) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’
      ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up 𝓋) x) , β™₯ ,
             βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) (βŠ‘-left-contract cΜ…β‚™βŠ‘id) ⟩
... | ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V , βŠ‘-cast βŠ‘-l cΜ…β‚βŠ‘cΜ…β€² ⟩ =
  case catchupβ‚— (c̅₁ ⨟ cΜ…) _ 𝓋′ (comp-pres-βŠ‘-bl cΜ…β‚βŠ‘cΜ…β€² cΜ…βŠ‘gβ€²) of Ξ» where
  ⟨ id _ , id , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ id) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l (βŠ‘-right-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (inj 𝓋)) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘cΜ…β€²) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’
      let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
              (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
              l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (up 𝓋)) (up 𝓋) ⟩
              l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
      ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up 𝓋) x) , β™₯ ,
        βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
... | ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V , βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) cΜ…β‚βŠ‘gβ€² ⟩ =
  case catchupβ‚— (c̅₁ ⨟ cΜ…) (id gβ€²) id (βŠ‘-left-expand (comp-pres-βŠ‘-ll cΜ…β‚βŠ‘gβ€² cΜ…βŠ‘gβ€²)) of Ξ» where
  ⟨ id _ , id , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ id) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (inj 𝓋)) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) (βŠ‘-left-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘cΜ…β€²) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’
      let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
              (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
              l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (up 𝓋)) (up 𝓋) ⟩
              l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
      ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up 𝓋) x) , β™₯ ,
        βŠ‘-castl (βŠ‘-castr βŠ‘-l β„“βŠ‘cΜ…β€²) (βŠ‘-left-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
... | ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V , βŠ‘-castr (βŠ‘-castl βŠ‘-l cΜ…β‚βŠ‘β„“) gβ‚βŠ‘cΜ…β€² ⟩ =
  case catchupβ‚— (c̅₁ ⨟ cΜ…) _ 𝓋′ (comp-pres-βŠ‘-bl (comp-pres-βŠ‘-lr cΜ…β‚βŠ‘β„“ gβ‚βŠ‘cΜ…β€²) cΜ…βŠ‘gβ€²) of Ξ» where
  ⟨ id _ , id , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let ♣ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ id) id ⟩
             l β„“ βŸͺ id (l β„“) ⟫ β€”β†’βŸ¨ Ξ²-id ⟩
             l β„“ ∎) in
    ⟨ l β„“ , v-l , ♣ , βŠ‘-castr βŠ‘-l (βŠ‘-right-contract cΜ…β‚™βŠ‘cΜ…β€²) ⟩
  ⟨ cΜ…β‚™ , inj 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
            (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
             l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (inj 𝓋)) (inj 𝓋) ⟩
             l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
    ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (inj 𝓋) (Ξ» ())) , β™₯ ,
      βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
  ⟨ cΜ…β‚™ , up 𝓋 , cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ , cΜ…β‚™βŠ‘cΜ…β€² ⟩ β†’
    case (precβ‚—β†’βŠ‘ _ _ cΜ…β‚™βŠ‘cΜ…β€²) of Ξ» where
    ⟨ _ , lβŠ‘l ⟩ β†’
      let β™₯ = β† β‚‘-trans (plug-congβ‚‘ Mβ† V)
              (l β„“ βŸͺ c̅₁ ⟫ βŸͺ cΜ… ⟫ β€”β†’βŸ¨ comp i ⟩
              l β„“ βŸͺ c̅₁ ⨟ cΜ… ⟫   β€”β†’βŸ¨ cast (comp-→⁺ cΜ…β‚β¨ŸcΜ…β† cΜ…β‚™ (up 𝓋)) (up 𝓋) ⟩
              l β„“ βŸͺ cΜ…β‚™ ⟫ ∎) in
      ⟨ l β„“ βŸͺ cΜ…β‚™ ⟫ , v-cast (ir (up 𝓋) x) , β™₯ ,
        βŠ‘-cast βŠ‘-l cΜ…β‚™βŠ‘cΜ…β€² ⟩
catchup (v-cast (ir 𝓋′ x)) (βŠ‘-castr {g} {g₁′} {gβ‚‚β€²} {M} {Mβ€²} {cΜ…β€²} MβŠ‘Vβ€² gβŠ‘cΜ…)
  with catchup v-l MβŠ‘Vβ€²
... | ⟨ l β„“ , v-l , Mβ† V , βŠ‘-l ⟩ =
  ⟨ l β„“ , v-l , Mβ† V , βŠ‘-castr βŠ‘-l gβŠ‘cΜ… ⟩
... | ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V , βŠ‘-castl βŠ‘-l cΜ…β‚βŠ‘β„“ ⟩ =
  ⟨ l β„“ βŸͺ c̅₁ ⟫ , v-cast i , Mβ† V ,
    βŠ‘-castr (βŠ‘-castl βŠ‘-l cΜ…β‚βŠ‘β„“) gβŠ‘cΜ… ⟩