```------------------------------------------------------------------------
-- The proof of small⇒big⟶∞ uses the lemmas proved here
------------------------------------------------------------------------

module Semantics.Equivalence.Lemmas where

open import Syntax
open import Infinite
open import Semantics.SmallStep

open import Data.Empty
open import Data.Function

helper : ∀ {t} {y : Exprˢ t} {m i} →
run (done (nat m) ⊕ y) ⟶∞[ i ] → y ⟶∞[ i ]
helper (Red Add₁           ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Red Add₃           ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Red (Int int)      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Addʳ ⟶             ◅∞ ⟶∞) ~ ⟶ ◅∞ helper ⟶∞
helper (Addˡ (Red (Int _)) ◅∞ Red (Int ())        ◅∞ ⟶∞)
helper (Addˡ (Red (Int _)) ◅∞ Addˡ (Red (Int ())) ◅∞ ⟶∞)
⊥-elim (done↛∞ ⟶∞)

data Pred {t} (y : Exprˢ t) i : Exprˢ t → Set where
• : ∀ n (y⟶∞ : y ⟶∞[ i ]) → Pred y i (done (nat n))

lemma : ∀ {t} {x y : Exprˢ t} {i} →
run (x ⊕ y) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred y i
lemma (Red Add₁      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red Add₂      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red Add₃      ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Addˡ ⟶        ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
lemma (Addʳ ⟶        ◅∞ ⟶∞) = ε (• _ (⟶ ◅∞ helper ⟶∞))

module Seqn where

open Add public using (Pred; •)

lemma : ∀ {t} {x y : Exprˢ t} {i} →
run (x >> y) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred y i
lemma (Red Seqn₁     ◅∞ ⟶∞) = ε (• _ ⟶∞)
lemma (Red Seqn₂     ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Seqnˡ ⟶       ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞

module Catch where

helper : ∀ {t} {y : Exprˢ t} {i} →
run (done throw catch y) ⟶∞[ i ] → y ⟶∞[ B ]
helper (Red Catch₂            ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Red (Int int)         ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
helper (Catchˡ (Red (Int ())) ◅∞ ⟶∞)
helper (Catchʳ ⟶              ◅∞ ⟶∞) ~ ⟶ ◅∞ helper ⟶∞

data Pred {t} (y : Exprˢ t) i : Exprˢ t → Set where
• : (y⟶∞ : y ⟶∞[ B ]) → Pred y i (done throw)

lemma : ∀ {t} {x y : Exprˢ t} {i} →
run (x catch y) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred y i
lemma (Red Catch₁    ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red Catch₂    ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Catchˡ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞
lemma (Catchʳ ⟶      ◅∞ ⟶∞) = ε (• (⟶ ◅∞ helper ⟶∞))

module Block where

lemma : ∀ {t} {x : Exprˢ t} {i} → run (block x) ⟶∞[ i ] → x ⟶∞[ B ]
lemma (Red Block     ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Blockˡ ⟶      ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞

module Unblock where

lemma : ∀ {t} {x : Exprˢ t} {i} → run (unblock x) ⟶∞[ i ] → x ⟶∞[ U ]
lemma (Red Unblock   ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
lemma (Unblockˡ ⟶    ◅∞ ⟶∞) ~ ⟶ ◅∞ lemma ⟶∞

module Loop where

data Pred i : Exprˢ partial → Set where
• : ∀ n → Pred i (done (nat n))

helper : ∀ {y i x} → Seqn.Pred y i x → Pred i x
helper (Seqn.• n _) = • n

lemma : ∀ {x i} → run (loop x) ⟶∞[ i ] → x ⟶⋆∞[ i ] Pred i
lemma (Red Loop      ◅∞ ⟶∞) = map⋆∞ id id helper (Seqn.lemma ⟶∞)
lemma (Red (Int int) ◅∞ ⟶∞) = ⊥-elim (done↛∞ ⟶∞)
```