You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
  inductive Value : Type where
    | unit : Value
    | const : Constant → Value
    | constr_app : (constr : Name) → (args_rev : List Value) → Value
    | closure : (env : List Object) → (value : Expr) → Value
    deriving Inhabited

  inductive Object : Type where
    | value : Value → Object
    | delayed : (env : List Object) → Expr → Object
    deriving Inhabited

abbrev Env : Type := List Object

abbrev cons_value (v : Value) (env : Env) : Env := Object.value v :: env

partial def eval (env : Env) : Expr -> Value
  | Expr.var _ idx => match env[idx]! with
    | Object.value val => val
    | Object.delayed env' expr => eval env' expr
  | Expr.unit => Value.unit
  | Expr.const c => Value.const c
  | Expr.constr name => Value.constr_app name []
  | Expr.app f arg => match eval env f with
    | Value.closure env' body => eval (eval env arg ∷ env') body
    | _ => panic! "expected closure"
  | Expr.constr_app ctr arg => match eval env ctr with
    | Value.constr_app ctr_name ctr_args_rev => Value.constr_app ctr_name (eval env arg :: ctr_args_rev)
    | _ => panic! "expected constructor application"
  | Expr.binop op arg₁ arg₂ => match eval env arg₁, eval env arg₂ with
    | Value.const (Constant.int val₁), Value.const (Constant.int val₂) =>
      Value.const (Constant.int (eval_binop_int op val₁ val₂))
    | _, _ => panic! "expected integer constants"
  | Expr.lambda _ body => Value.closure env body
  | Expr.save _ value body => eval (eval env value ∷ env) body
  | Expr.branch name _ body next => match env with
    | Object.value (Value.constr_app name' args_rev) :: env' =>
      if name = name' then
        eval (args_rev.map Object.value ++ env') body
      else
        eval env next
    | _ => panic! "expected constructor application"
  | Expr.recur name body =>
    eval (Object.delayed env (Expr.recur name body) :: env) body
  | Expr.fail => panic! "evaluation failed"

def Value.Approx.Indexed (n : Nat) (v₁ v₂ : Value) : Prop :=
  (v₁ = Value.unit ∧ v₂ = Value.unit) ∨
  (∃ c, v₁ = Value.const c ∧ v₂ = Value.const c) ∨
  (∃ ctr_name args_rev args_rev',
    v₁ = Value.constr_app ctr_name args_rev ∧
    v₂ = Value.constr_app ctr_name args_rev' ∧
    (∀ k < n, List.Forall₂ (Value.Approx.Indexed k) args_rev args_rev')) ∨
  (∃ env₁ body₁ env₂ body₂,
    v₁ = Value.closure env₁ body₁ ∧
    v₂ = Value.closure env₂ body₂ ∧
    (∀ n₁ n₂, n₁ + n₂ < n →
      ∀ a₁ a₂ r₁,
        Value.Approx.Indexed (n₁ + n₂) a₁ a₂ →
        a₁ ∷ env₁ ⊢ body₁ ↦(n₁) r₁ →
        ∃ r₂,
          a₂ ∷ env₂ ⊢ body₂ ↦ r₂ ∧
          Value.Approx.Indexed n₂ r₁ r₂))

def Expr.Approx.Param.Indexed (n : Nat) (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop :=
  (∀ n₁ n₂ v₁, n₁ + n₂ ≤ n → env₁ ⊢ e₁ ↦(n₁) v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂)

inductive Object.Approx.Indexed' (n : Nat) : Object → Object → Prop where
  | value {v₁ v₂} :
    v₁ ≲ᵥ(n) v₂ →
    Object.Approx.Indexed' n (Object.value v₁) (Object.value v₂)
  | delayed {env₁ env₂ e₁ e₂} :
    e₁ ≲(n)⟨env₁, env₂⟩ e₂ →
    Object.Approx.Indexed' n (Object.delayed env₁ e₁) (Object.delayed env₂ e₂)
  | delayed_eq {env₁ env₂ e} :
    List.Forall₂ (Object.Approx.Indexed' n) env₁ env₂ →
    Object.Approx.Indexed' n (Object.delayed env₁ e) (Object.delayed env₂ e)

def Env.Approx.Indexed' (n : Nat) : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ (Object.Approx.Indexed' n)

def Expr.Approx.Indexed' (n : Nat) (e₁ e₂ : Expr) : Prop :=
  (∀ n₁ n₂ v₁, n₁ + n₂ ≤ n →
    ∀ env₁ env₂, env₁ ≲ₑ'(n₁ + n₂) env₂ → env₁ ⊢ e₁ ↦(n₁) v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂)

@[aesop safe cases]
inductive Value.Approx.Indexed.Inversion (n : Nat) : Value → Value → Prop where
  | unit : Value.Approx.Indexed.Inversion n Value.unit Value.unit
  | const {c} : Value.Approx.Indexed.Inversion n (Value.const c) (Value.const c)
  | constr_app {ctr_name args_rev args_rev'} :
    (∀ k < n, args_rev ≲ₐ(k) args_rev') →
    Value.Approx.Indexed.Inversion n (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev')
  | closure {env₁ body₁ env₂ body₂} :
    (∀ n₁ n₂, n₁ + n₂ < n →
      ∀ a₁ a₂ v₁,
        a₁ ≲ᵥ(n₁ + n₂) a₂ →
        a₁ ∷ env₁ ⊢ body₁ ↦(n₁) v₁ →
        ∃ v₂, a₂ ∷ env₂ ⊢ body₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂) →
    Value.Approx.Indexed.Inversion n (Value.closure env₁ body₁) (Value.closure env₂ body₂)

def Value.Approx.Indexed.Preservation (k : Nat) : Prop :=
  ∀ m n env env' e v,
    m + n < k →
    env ≲ₑ'(m + n) env' →
    env ⊢ e ↦(n) v →
    ∃ v', env' ⊢ e ↦ v' ∧ v ≲ᵥ(m) v'

def Expr.Approx.Contextual (e₁ e₂ : Expr) : Prop :=
  ∀ (C : Context) env, env ⊢ C.subst e₁ ↓ → env ⊢ C.subst e₂ ↓

def eval_binop_int (op : BinaryOp) (i₁ i₂ : Int) : Int :=
  match op with
  | BinaryOp.add_int => i₁ + i₂
  | BinaryOp.sub_int => i₁ - i₂
  | BinaryOp.mul_int => i₁ * i₂
  | BinaryOp.div_int => i₁ / i₂

@[aesop unsafe constructors]
inductive Eval : Env → Expr → Value → Prop where
  | var {env name idx val} :
    env[idx]? = some (Object.value val) →
    Eval env (Expr.var name idx) val
  | var_rec {env name idx env' expr val} :
    env[idx]? = some (Object.delayed env' expr) →
    Eval env' expr val →
    Eval env (Expr.var name idx) val
  | unit {env} :
    Eval env Expr.unit Value.unit
  | const {env c} :
    Eval env (Expr.const c) (Value.const c)
  | constr {env name} :
    Eval env (Expr.constr name) (Value.constr_app name [])
  | app {env env' f body arg val val'} :
    Eval env f (Value.closure env' body) →
    Eval env arg val →
    Eval (val ∷ env') body val' →
    Eval env (Expr.app f arg) val'
  | constr_app {env ctr ctr_name ctr_args_rev arg val} :
    Eval env ctr (Value.constr_app ctr_name ctr_args_rev) →
    Eval env arg val →
    Eval env (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
  | binop {env op arg₁ arg₂ val₁ val₂} :
    Eval env arg₁ (Value.const (Constant.int val₁)) →
    Eval env arg₂ (Value.const (Constant.int val₂)) →
    Eval env (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
  | lambda {env name body} :
    Eval env (Expr.lambda name body) (Value.closure env body)
  | save {env name value body val val'} :
    Eval env value val →
    Eval (val ∷ env) body val' →
    Eval env (Expr.save name value body) val'
  | branch_matches {env name args_rev body val} :
    Eval (args_rev.map Object.value ++ env) body val →
    Eval (Value.constr_app name args_rev ∷ env) (Expr.branch name _ body _) val
  | branch_fails {env name name' args_rev next val} :
    name ≠ name' →
    Eval (Value.constr_app name args_rev ∷ env) next val →
    Eval (Value.constr_app name args_rev ∷ env) (Expr.branch name' _ _ next) val
  | recur {env name body val} :
    Eval (Object.delayed env (Expr.recur name body) :: env) body val →
    Eval env (Expr.recur name body) val

def Eval.Defined (env : Env) (e : Expr) : Prop :=
  ∃ v, env ⊢ e ↦ v

def Context.Indexed.Preserved (k : Nat) : Prop :=
  ∀ n m,
    n + m < k →
    ∀ e₁ e₂,
      e₁ ≲'(n + m) e₂ → ∀ (C : Context) env₁ env₂ v₁,
      env₁ ≲ₑ'(n + m) env₂ →
      env₁ ⊢ C.subst e₁ ↦(n) v₁ →
      ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≲ᵥ(m) v₂

inductive Eval.Indexed : Nat → Env → Expr → Value → Prop where
  | var {n env name idx val} :
    env[idx]? = some (Object.value val) →
    Eval.Indexed n env (Expr.var name idx) val
  | var_rec {n env name idx env' expr val} :
    env[idx]? = some (Object.delayed env' expr) →
    Eval.Indexed n env' expr val →
    Eval.Indexed n env (Expr.var name idx) val
  | unit {n env} :
    Eval.Indexed n env Expr.unit Value.unit
  | const {n env c} :
    Eval.Indexed n env (Expr.const c) (Value.const c)
  | constr {n env name} :
    Eval.Indexed n env (Expr.constr name) (Value.constr_app name [])
  | app {n n₁ n₂ env env' f body arg val val'} :
    n₁ + n₂ + 1 ≤ n →
    Eval.Indexed n₁ env f (Value.closure env' body) →
    Eval.Indexed (n₁ + 1) env arg val →
    Eval.Indexed n₂ (val ∷ env') body val' →
    Eval.Indexed n env (Expr.app f arg) val'
  | constr_app {n n' env ctr ctr_name ctr_args_rev arg val} :
    n' < n →
    Eval.Indexed n env ctr (Value.constr_app ctr_name ctr_args_rev) →
    Eval.Indexed n' env arg val →
    Eval.Indexed n env (Expr.constr_app ctr arg) (Value.constr_app ctr_name (val :: ctr_args_rev))
  | binop {n env op arg₁ arg₂ val₁ val₂} :
    Eval.Indexed n env arg₁ (Value.const (Constant.int val₁)) →
    Eval.Indexed n env arg₂ (Value.const (Constant.int val₂)) →
    Eval.Indexed n env (Expr.binop op arg₁ arg₂) (Value.const (Constant.int (eval_binop_int op val₁ val₂)))
  | lambda {n env name body} :
    Eval.Indexed n env (Expr.lambda name body) (Value.closure env body)
  | save {n n₁ n₂ env name value body val val'} :
    n₁ + n₂ ≤ n →
    Eval.Indexed n₁ env value val →
    Eval.Indexed n₂ (val ∷ env) body val' →
    Eval.Indexed n env (Expr.save name value body) val'
  | branch_matches {n n' env name args_rev body val} :
    n' < n →
    Eval.Indexed n' (args_rev.map Object.value ++ env) body val →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) (Expr.branch name _ body _) val
  | branch_fails {n env name name' args_rev next val} :
    name ≠ name' →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) next val →
    Eval.Indexed n (Value.constr_app name args_rev ∷ env) (Expr.branch name' _ _ next) val
  | recur {n n' env name body val} :
    n' < n →
    Eval.Indexed n' (Object.delayed env (Expr.recur name body) :: env) body val →
    Eval.Indexed n env (Expr.recur name body) val

def Value.Equiv (v v' : Value) : Prop :=
  v ≲ᵥ v' ∧ v' ≲ᵥ v

def Object.Equiv (o o' : Object) : Prop :=
  o ≲ₒ o' ∧ o' ≲ₒ o

def Env.Equiv : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ Object.Equiv

def Expr.Equiv.Param (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop :=
  e₁ ≲⟨env₁, env₂⟩ e₂ ∧ e₂ ≲⟨env₂, env₁⟩ e₁

def Expr.Equiv (e₁ e₂ : Expr) : Prop :=
  e₁ ≲ e₂ ∧ e₂ ≲ e₁

inductive Context : Type where
  | hole : Context
  | app_left : Context → Expr → Context
  | app_right : Expr → Context → Context
  | constr_app_left : Context → Expr → Context
  | constr_app_right : Expr → Context → Context
  | binop_left : (oper : BinaryOp) → (arg₁ : Context) → (arg₂ : Expr) → Context
  | binop_right : (oper : BinaryOp) → (arg₁ : Expr) → (arg₂ : Context) → Context
  | lambda : (var_name : String) → (body : Context) → Context
  | save_left : (var_name : String) → (value : Context) → (body : Expr) → Context
  | save_right : (var_name : String) → (value : Expr) → (body : Context) → Context
  | branch_left : (constr : Name) → (var_names : List Name) → (body : Context) → (next : Expr) → Context
  | branch_right : (constr : Name) → (var_names : List Name) → (body : Expr) → (next : Context) → Context
  | recur : (var_name : Name) → (ctx : Context) → Context
  deriving Inhabited, BEq

@[simp]
def Context.subst (C : Context) (e : Expr) : Expr :=
  match C with
  | Context.hole => e
  | Context.app_left C' e' => Expr.app (C'.subst e) e'
  | Context.app_right e' C' => Expr.app e' (C'.subst e)
  | Context.constr_app_left C' e' => Expr.constr_app (C'.subst e) e'
  | Context.constr_app_right e' C' => Expr.constr_app e' (C'.subst e)
  | Context.binop_left oper C₁ e₂ => Expr.binop oper (C₁.subst e) e₂
  | Context.binop_right oper e₁ C₂ => Expr.binop oper e₁ (C₂.subst e)
  | Context.lambda s C' => Expr.lambda s (C'.subst e)
  | Context.save_left s C' e' => Expr.save s (C'.subst e) e'
  | Context.save_right s e' C' => Expr.save s e' (C'.subst e)
  | Context.branch_left constr names C' next => Expr.branch constr names (C'.subst e) next
  | Context.branch_right constr names body C' => Expr.branch constr names body (C'.subst e)
  | Context.recur name C' => Expr.recur name (C'.subst e)

def Value.Approx (v v' : Value) : Prop :=
  ∀ n, v ≲ᵥ(n) v'

def Expr.Approx.Param (env₁ env₂ : Env) (e₁ e₂ : Expr) : Prop :=
  (∀ v₁, env₁ ⊢ e₁ ↦ v₁ → ∃ v₂, env₂ ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂)

inductive Object.Approx : Object → Object → Prop where
  | value {v₁ v₂} : v₁ ≲ᵥ v₂ → Object.Approx (Object.value v₁) (Object.value v₂)
  | delayed {env₁ env₂ e₁ e₂} :
    e₁ ≲⟨env₁, env₂⟩ e₂ →
    Object.Approx (Object.delayed env₁ e₁) (Object.delayed env₂ e₂)

def Env.Approx : (env₁ env₂ : Env) → Prop :=
  List.Forall₂ Object.Approx

def Expr.Approx (e₁ e₂ : Expr) : Prop :=
  ∀ env₁ env₂, env₁ ≲ₑ env₂ → e₁ ≲⟨env₁, env₂⟩ e₂

@[aesop safe cases]
inductive Value.Approx.Inversion : Value -> Value -> Prop where
  | unit : Value.Approx.Inversion Value.unit Value.unit
  | const {c} : Value.Approx.Inversion (Value.const c) (Value.const c)
  | constr_app {ctr_name args_rev args_rev'} :
    args_rev ≲ₐ args_rev' →
    Value.Approx.Inversion (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev')
  | closure {env₁ body₁ env₂ body₂} :
    (∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) →
    Value.Approx.Inversion (Value.closure env₁ body₁) (Value.closure env₂ body₂)

abbrev Name : Type := String

inductive Constant : Type where
  | int : Int → Constant
  | string : String → Constant
  deriving Inhabited, BEq, DecidableEq

inductive BinaryOp : Type where
  | add_int : BinaryOp
  | sub_int : BinaryOp
  | mul_int : BinaryOp
  | div_int : BinaryOp
  deriving Inhabited, BEq, DecidableEq

inductive Expr : Type where
  | var : (name : String) → (index : Nat) → Expr
  | unit : Expr
  | const : Constant → Expr
  | constr : Name → Expr
  | app : Expr → Expr → Expr
  | constr_app : Expr → Expr → Expr
  | binop : (oper : BinaryOp) → (arg₁ arg₂ : Expr) → Expr
  | lambda : (var_name : String) → (body : Expr) → Expr
  | save : (var_name : String) → (value : Expr) → (body : Expr) → Expr
  | branch : (constr : Name) → (var_names : List Name) → (body : Expr) → (next : Expr) → Expr
  | recur : (var_name : Name) → (body : Expr) → Expr
  | fail : Expr
  deriving Inhabited, BEq, DecidableEq

def Expr.mk_app (f : Expr) : List Expr → Expr
  | [] => f
  | x :: xs => Expr.mk_app (Expr.app f x) xs

def mkLambdas {m} [Monad m] [MonadQuotation m] (ss : TSyntaxArray `ident) (e : TSyntax `expr) : m (TSyntax `term) := do
  let body ← `(⟪ $e ⟫)
  ss.foldrM (fun s acc => `(Expr.lambda $(Lean.Syntax.mkStrLit s.getId.toString) $acc)) body

def mkConstrApp {m} [Monad m] [MonadQuotation m] (s : TSyntax `ident) (es : TSyntaxArray `expr) : m (TSyntax `term) := do
  let ctr ← `(Expr.constr $(Lean.Syntax.mkStrLit s.getId.toString))
  es.foldlM (fun acc e => `(Expr.constr_app $acc ⟪$e⟫)) ctr

instance : Coe Syntax (TSyntax `expr) where
  coe s := ⟨s⟩

def mkVar {m} [Monad m] [MonadRef m] (name : Ident) (i : TSyntax `num) : m Syntax := do
  let info ← Lean.MonadRef.mkInfoFromRefPos
  pure $
      Lean.Syntax.node3 info `Juvix.Core.Main.Syntax.term_of_expr
            (Lean.Syntax.atom info "⟪")
            (Lean.Syntax.node3 info `Juvix.Core.Main.Syntax.expr_var
              name (Lean.Syntax.atom info "♯") i)
            (Lean.Syntax.atom info "⟫")

def mkConstrApp {m} [Monad m] [MonadRef m] (name : Ident) (es : TSyntaxArray `expr) : m Syntax := do
  let info ← Lean.MonadRef.mkInfoFromRefPos
  pure $
    Lean.Syntax.node3 info `Juvix.Core.Main.Syntax.term_of_expr
      (Lean.Syntax.atom info "⟪")
      (Lean.Syntax.node2 info `Juvix.Core.Main.Syntax.expr_constr_app
        name
        (Lean.Syntax.node info `null es))
      (Lean.Syntax.atom info "⟫")

def unfoldListLit (node : Syntax) : Option (List String) :=
  match node with
  | (Lean.Syntax.node _ _ args0) =>
    match args0 with
    | #[Lean.Syntax.atom _ "[", node', Lean.Syntax.atom _ "]"] =>
      match node' with
      | (Lean.Syntax.node _ _ args) =>
        let rec go : List Syntax → List String → Option (List String)
          | [], acc => some acc.reverse
          | [ ns ], acc =>
            match ns with
            | `($s:str) =>
              some (s.getString :: acc).reverse
            | _ => none
          | ( ns :: Lean.Syntax.atom _ "," :: xs), acc =>
            match ns with
            | `($s:str) =>
                go xs (s.getString :: acc)
            | _ => none
          | _, _ => none
        go args.toList []
      | _ => none
    | _ => none
  | _ => none

@[app_unexpander Expr.var]
def unexpandVar : Unexpander
  | `($_var $s:str $i:num) =>
    let name := mkIdent $ Name.mkSimple s.getString
    mkVar name i
  | _ => throw ()

@[app_unexpander Expr.unit]
def unexpandUnit : Unexpander
  | `($_unit) => `(⟪υ⟫)

@[app_unexpander Expr.const]
def unexpandConst : Unexpander
  | `($_const $x) =>
    match x with
    | `($_ $n:num) => `(⟪$n⟫)
    | `($_ $s:str) => `(⟪$s⟫)
    | _ => throw ()
  | _ => throw ()

@[app_unexpander Expr.app]
def unexpandApp : Unexpander
  | `($_app ⟪$e₁⟫ ⟪$e₂⟫) => `(⟪$e₁ $e₂⟫)
  | _ => throw ()

@[app_unexpander Expr.constr]
def unexpandConstr : Unexpander
  | `($_constr $s:str) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪ $name ⟫)
  | _ => throw ()

@[app_unexpander Expr.constr_app]
def unexpandConstrApp : Unexpander
  | `($_constr_app ⟪ $s ⟫ ⟪$e⟫) => `(⟪ $s $e⟫)
  | `($_constr_app ⟪ $s:ident $es* ⟫ ⟪$e⟫) => mkConstrApp s (es.push e)
  | _ => throw ()

@[app_unexpander Expr.lambda]
def unexpandLambda : Unexpander
  | `($_lambda $s:str ⟪λ $ss:ident* . $e:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪λ $name $ss* . $e⟫)
  | `($_lambda $s:str ⟪$e⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪λ $name . $e⟫)
  | _ => throw ()

@[delab app.Juvix.Core.Main.Expr.binop]
def delabBinop : Delab := do
  let e ← getExpr
  guard $ e.isAppOfArity' `Juvix.Core.Main.Expr.binop 3
  match e.getAppArgs' with
  | #[Lean.Expr.const op _, e₁, e₂] =>
    let e₁' ← match ← delab e₁ with
      | `(⟪$e'⟫) => pure e'
      | _ => failure
    let e₂' ← match ← delab e₂ with
      | `(⟪$e'⟫) => pure e'
      | _ => failure
    match op with
    | `Juvix.Core.Main.BinaryOp.add_int => `(⟪$e₁' + $e₂'⟫)
    | `Juvix.Core.Main.BinaryOp.sub_int => `(⟪$e₁' - $e₂'⟫)
    | `Juvix.Core.Main.BinaryOp.mul_int => `(⟪$e₁' * $e₂'⟫)
    | `Juvix.Core.Main.BinaryOp.div_int => `(⟪$e₁' / $e₂'⟫)
    | _ => failure
  | _ => failure

@[app_unexpander Expr.branch]
def unexpandBranch : Unexpander
  | `($_branch $s:str $lst ⟪$body:expr⟫ ⟪cases| $c:cases⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    match unfoldListLit lst with
    | some ss =>
      let names := List.toArray $ ss.map fun s' => mkIdent (Name.mkSimple s')
      if ss.isEmpty then
        `(⟪cases| | $name => $body $c⟫)
      else
        `(⟪cases| | $name $names* => $body $c⟫)
    | none =>
      throw ()
  | `($_branch $s:str $lst ⟪$body:expr⟫ ⟪⊥⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    match unfoldListLit lst with
    | some ss =>
      let names := List.toArray $ ss.map fun s' => mkIdent (Name.mkSimple s')
      if ss.isEmpty then
        `(⟪cases| | $name => $body⟫)
      else
        `(⟪cases| | $name $names* => $body⟫)
    | none =>
      throw ()
  | `($_branch $s:str $lst ⟪$body:expr⟫ ⟪$next:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    match unfoldListLit lst with
    | some ss =>
      let names := List.toArray $ ss.map fun s' => mkIdent (Name.mkSimple s')
      if ss.isEmpty then
        `(⟪cases| | $name => $body | _ => $next⟫)
      else
        `(⟪cases| | $name $names* => $body | _ => $next⟫)
    | none =>
      throw ()
  | _ => throw ()

@[app_unexpander Expr.save]
def unexpandSave : Unexpander
  | `($_save "_case_" ⟪$v:expr⟫ ⟪cases| $c⟫) =>
    `(⟪case $v of $c end⟫)
  | `($_save $s:str ⟪rec $sname:ident $v:expr⟫ ⟪$b:expr⟫) =>
    if sname.getId.toString == s.getString then
      `(⟪letrec $sname := $v in $b⟫)
    else
      throw ()
  | `($_save $s:str ⟪$v:expr⟫ ⟪$b:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪let $name := $v in $b⟫)
  | _ => throw ()

@[app_unexpander Expr.recur]
def unexpandRecur : Unexpander
  | `($_recur $s:str ⟪$b:expr⟫) =>
    let name := mkIdent $ Name.mkSimple s.getString
    `(⟪rec $name $b⟫)
  | _ => throw ()

@[app_unexpander Expr.fail]
def unexpandFail : Unexpander
  | `($_bot) => `(⟪⊥⟫)

@[category_parenthesizer expr]
def expr.parenthesizer : CategoryParenthesizer := term.parenthesizer

def Expr.Equiv.Contextual (e₁ e₂ : Expr) : Prop :=
  e₁ ≲ᶜ e₂ ∧ e₂ ≲ᶜ e₁

List in Init.Prelude

List.Forall₂ in Batteries.Data.List.Basic

Transitive in Mathlib.Order.Defs.Unbundled

closure in Mathlib.Topology.Defs.Basic

Lean.MonadRef in Init.Prelude

Lean.Syntax in Init.Prelude

Lean.TSyntax in Init.Prelude

Monad in Init.Prelude

Lean.MonadRef.mkInfoFromRefPos in Init.Prelude

Lean.Syntax.atom in Init.Prelude

Lean.Syntax.node3 in Init.Prelude

Lean.TSyntaxArray in Init.Prelude

Lean.Syntax.node in Init.Prelude

Lean.Syntax.node2 in Init.Prelude

Option in Init.Prelude

String in Init.Prelude

Lean.Name.mkSimple in Init.Prelude

Lean.mkIdent in Init.Meta.Defs

guard in Init.Control.Basic

Lean.Expr in Lean.Expr

Lean.Expr.const in Lean.Expr

List.toArray in Init.Prelude

BEq in Init.Prelude

Inhabited in Init.Prelude

DecidableEq in Init.Prelude

Int in Init.Data.Int.Basic

Nat in Init.Prelude

Lean.MonadQuotation in Init.Prelude

Lean.Syntax.mkStrLit in Init.Meta.Defs

Coe in Init.Coe

IsEmpty in Mathlib.Logic.IsEmpty

List.Forall₂.cons in Batteries.Data.List.Basic

List.Forall₂.nil in Batteries.Data.List.Basic

List.map in Init.Prelude

Prod in Init.Prelude

reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

List.cons in Init.Prelude

List.nil in Init.Prelude
</all_available_defs>

<all_available_lemmas>
lemma Env.Approx.Indexed'.get {n i : Nat} {env env' o₁}
  (h₁ : env ≲ₑ'(n) env')
  (h₂ : env[i]? = some o₁) :
  ∃ o₂, env'[i]? = some o₂ ∧ o₁ ≲ₒ'(n) o₂

lemma Env.Approx.Indexed'.value {n i : Nat} {env env' v}
  (h₁ : env ≲ₑ'(n) env')
  (h₂ : env[i]? = some (Object.value v)) :
  ∃ v', env'[i]? = some (Object.value v') ∧ v ≲ᵥ(n) v'

lemma Env.Approx.Indexed'.delayed {n i : Nat} {env₁ env₂ env e}
  (h₁ : env₁ ≲ₑ'(n) env₂)
  (h₂ : env₁[i]? = some (Object.delayed env e)) :
  (∃ env' e', e ≲(n)⟨env, env'⟩ e' ∧ env₂[i]? = some (Object.delayed env' e')) ∨
  ∃ env', env ≲ₑ'(n) env' ∧ env₂[i]? = some (Object.delayed env' e)

lemma Env.Approx.Indexed'.from_value {n l₁ l₂} (h : l₁ ≲ₐ(n) l₂) :
  List.map Object.value l₁ ≲ₑ'(n) List.map Object.value l₂

lemma Env.Approx.Indexed'.from_delayed {n env₁ env₂ l} (h : env₁ ≲ₑ'(n) env₂) :
  List.map (Object.delayed env₁) l ≲ₑ'(n) List.map (Object.delayed env₂) l

lemma Env.Approx.Indexed'.concat {n env₁ env₂ env₁' env₂'}
  (h₁ : env₁ ≲ₑ'(n) env₁')
  (h₂ : env₂ ≲ₑ'(n) env₂') :
  env₁ ++ env₂ ≲ₑ'(n) env₁' ++ env₂'

lemma Env.Approx.Indexed'.cons {n o₁ o₂ env₁ env₂}
  (h₁ : o₁ ≲ₒ'(n) o₂)
  (h₂ : env₁ ≲ₑ'(n) env₂) :
  o₁ :: env₁ ≲ₑ'(n) o₂ :: env₂

@[aesop unsafe apply]
lemma Value.Approx.Indexed.unit {n} : Value.unit ≲ᵥ(n) Value.unit

@[aesop unsafe apply]
lemma Value.Approx.Indexed.const {n c} : Value.const c ≲ᵥ(n) Value.const c

@[aesop unsafe apply]
lemma Value.Approx.Indexed.constr_app {n ctr_name args_rev args_rev'} :
    (∀ k < n, args_rev ≲ₐ(k) args_rev') →
    Value.constr_app ctr_name args_rev ≲ᵥ(n) Value.constr_app ctr_name args_rev'

@[aesop unsafe apply]
lemma Value.Approx.Indexed.closure {n env₁ body₁ env₂ body₂} :
    (∀ n₁ n₂, n₁ + n₂ < n →
      ∀ a₁ a₂ v₁,
        a₁ ≲ᵥ(n₁ + n₂) a₂ →
        a₁ ∷ env₁ ⊢ body₁ ↦(n₁) v₁ →
        ∃ v₂, a₂ ∷ env₂ ⊢ body₂ ↦ v₂ ∧ v₁ ≲ᵥ(n₂) v₂) →
    Value.closure env₁ body₁ ≲ᵥ(n) Value.closure env₂ body₂

@[aesop unsafe destruct]
lemma Value.Approx.Indexed.invert {n v v'} :
  v ≲ᵥ(n) v' →
  Value.Approx.Indexed.Inversion n v v'

lemma Value.Approx.Indexed.anti_monotone {n n' v₁ v₂} (h : v₁ ≲ᵥ(n) v₂) (h' : n' ≤ n) : v₁ ≲ᵥ(n') v₂

lemma Expr.Approx.Param.Indexed.anti_monotone {n n' env₁ env₂ e₁ e₂}
  (h : e₁ ≲(n)⟨env₁, env₂⟩ e₂)
  (h' : n' ≤ n)
  : e₁ ≲(n')⟨env₁, env₂⟩ e₂

lemma Expr.Approx.Indexed'.anti_monotone {n n' e₁ e₂}
  (h : e₁ ≲'(n) e₂)
  (h' : n' ≤ n)
  : e₁ ≲'(n') e₂

  lemma Env.Approx.Indexed'.anti_monotone {n n' env₁ env₂}
    (h : env₁ ≲ₑ'(n) env₂)
    (h' : n' ≤ n)
    : env₁ ≲ₑ'(n') env₂

  lemma Object.Approx.Indexed'.anti_monotone {n n' o₁ o₂} (h : o₁ ≲ₒ'(n) o₂) (h' : n' ≤ n) : o₁ ≲ₒ'(n') o₂

lemma Value.Approx.Indexed.Preservation.anti_monotone {k k'} (h : Value.Approx.Indexed.Preservation k) (h' : k' ≤ k) : Value.Approx.Indexed.Preservation k'

lemma Value.Approx.Indexed.preserved_step {k} :
  (∀ k' < k, Preservation k') → Preservation k

lemma Value.Approx.Indexed.preserved' {k} : Preservation k

  lemma Env.Approx.Indexed'.refl' {n env} (h : ∀ v, v ≲ᵥ(n) v) : env ≲ₑ'(n) env

  lemma Object.Approx.Indexed'.refl' {n o} (h : ∀ v, v ≲ᵥ(n) v) : o ≲ₒ'(n) o

@[refl]
lemma Value.Approx.Indexed.refl {n} v : v ≲ᵥ(n) v

@[refl]
lemma Env.Approx.Indexed'.refl {n env} : env ≲ₑ'(n) env

@[refl]
lemma Object.Approx.Indexed'.refl {n o} : o ≲ₒ'(n) o

lemma Termination.var {env name i v} :
  env[i]? = some (Object.value v) →
  env ⊢ Expr.var name i ↓

lemma Termination.var_rec {env name i env' e} :
    env[i]? = some (Object.delayed env' e) →
    env' ⊢ e ↓ →
    env ⊢ (Expr.var name i) ↓

lemma Termination.unit {env} :
  env ⊢ Expr.unit ↓

lemma Termination.const {env c} :
  env ⊢ Expr.const c ↓

lemma Termination.constr {env nm} :
  env ⊢ Expr.constr nm ↓

lemma Termination.app {env e₁ e₂ v env' body} :
  env ⊢ e₁ ↦ Value.closure env' body →
  env ⊢ e₂ ↦ v →
  v ∷ env' ⊢ body ↓ →
  env ⊢ Expr.app e₁ e₂ ↓

lemma Termination.constr_app {env e₁ e₂ e₁₁ e₁₂} :
  env ⊢ e₁ ↦ Value.constr_app e₁₁ e₁₂ →
  env ⊢ e₂ ↓ →
  env ⊢ Expr.constr_app e₁ e₂ ↓

lemma Termination.binop {env op e₁ e₂ c₁ c₂} :
  env ⊢ e₁ ↦ Value.const (Constant.int c₁) →
  env ⊢ e₂ ↦ Value.const (Constant.int c₂) →
  env ⊢ Expr.binop op e₁ e₂ ↓

lemma Termination.lambda {env name e} : env ⊢ Expr.lambda name e ↓

lemma Termination.save {env name e₁ e₂ v} :
  env ⊢ e₁ ↦ v →
  v ∷ env ⊢ e₂ ↓ →
  env ⊢ Expr.save name e₁ e₂ ↓

lemma Termination.branch_matches {env name vnames args_rev e e'} :
  args_rev.map Object.value ++ env ⊢ e ↓ →
  Value.constr_app name args_rev ∷ env ⊢ Expr.branch name vnames e e' ↓

lemma Termination.branch_fails {env name name' vnames args_rev e e'} :
  name ≠ name' →
  Value.constr_app name args_rev ∷ env ⊢ e' ↓ →
  Value.constr_app name args_rev ∷ env ⊢ Expr.branch name' vnames e e' ↓

lemma Termination.recur {env name e} :
  Object.delayed env (Expr.recur name e) :: env ⊢ e ↓ →
  env ⊢ Expr.recur name e ↓

theorem Eval.deterministic {env e v₁ v₂} (h₁ : env ⊢ e ↦ v₁) (h₂ : env ⊢ e ↦ v₂) : v₁ = v₂

lemma Expr.Approx.congruence {e₁ e₂} (C : Context) : e₁ ≲ e₂ → C.subst e₁ ≲ C.subst e₂

lemma Expr.Approx.cong_app₁ {e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.app e₁ e₂ ≲ Expr.app e₁' e₂

lemma Expr.Approx.cong_app₂ {e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.app e₁ e₂ ≲ Expr.app e₁ e₂'

lemma Expr.Approx.cong_app {e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.app e₁ e₂ ≲ Expr.app e₁' e₂'

lemma Expr.Approx.cong_constr_app₁ {e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁' e₂

lemma Expr.Approx.cong_constr_app₂ {e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁ e₂'

lemma Expr.Approx.cong_constr_app {e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.constr_app e₁ e₂ ≲ Expr.constr_app e₁' e₂'

lemma Expr.Approx.cong_binop₁ {op e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁' e₂

lemma Expr.Approx.cong_binop₂ {op e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁ e₂'

lemma Expr.Approx.cong_binop {op e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.binop op e₁ e₂ ≲ Expr.binop op e₁' e₂'

lemma Expr.Approx.cong_lambda {name e e'} : e ≲ e' → Expr.lambda name e ≲ Expr.lambda name e'

lemma Expr.Approx.cong_save₁ {name e₁ e₂ e₁'} : e₁ ≲ e₁' → Expr.save name e₁ e₂ ≲ Expr.save name e₁' e₂

lemma Expr.Approx.cong_save₂ {name e₁ e₂ e₂'} : e₂ ≲ e₂' → Expr.save name e₁ e₂ ≲ Expr.save name e₁ e₂'

lemma Expr.Approx.cong_save {name e₁ e₂ e₁' e₂'} : e₁ ≲ e₁' → e₂ ≲ e₂' → Expr.save name e₁ e₂ ≲ Expr.save name e₁' e₂'

lemma Expr.Approx.cong_branch₁ {constr names e e' next} : e ≲ e' → Expr.branch constr names e next ≲ Expr.branch constr names e' next

lemma Expr.Approx.cong_branch₂ {constr names e next next'} : next ≲ next' → Expr.branch constr names e next ≲ Expr.branch constr names e next'

lemma Expr.Approx.cong_branch {constr names e e' next next'} : e ≲ e' → next ≲ next' → Expr.branch constr names e next ≲ Expr.branch constr names e' next'

lemma Expr.Approx.cong_recur {name e e'} : e ≲ e' → Expr.recur name e ≲ Expr.recur name e'

lemma Expr.Approx.Param.cong_var {v v' x x' env env' name name'} :
  env[x]? = some (Object.value v) →
  env'[x']? = some (Object.value v') →
  v ≲ᵥ v' →
  Expr.var name x ≲⟨env, env'⟩ Expr.var name' x'

lemma Expr.Approx.Param.cong_unit {env env'} :
  Expr.unit ≲⟨env, env'⟩ Expr.unit

lemma Expr.Approx.Param.cong_const {c env env'} :
  Expr.const c ≲⟨env, env'⟩ Expr.const c

lemma Expr.Approx.Param.cong_constr {cname env env'} :
  Expr.constr cname ≲⟨env, env'⟩ Expr.constr cname

lemma Expr.Approx.Param.cong_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≲⟨env, env'⟩ e₁' →
  e₂ ≲⟨env, env'⟩ e₂' →
  Expr.app e₁ e₂ ≲⟨env, env'⟩ Expr.app e₁' e₂'

lemma Expr.Approx.Param.cong_constr_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≲⟨env, env'⟩ e₁' →
  e₂ ≲⟨env, env'⟩ e₂' →
  Expr.constr_app e₁ e₂ ≲⟨env, env'⟩ Expr.constr_app e₁' e₂'

lemma Expr.Approx.Param.cong_binop {op e₁ e₂ e₁' e₂' env env'} :
  e₁ ≲⟨env, env'⟩ e₁' →
  e₂ ≲⟨env, env'⟩ e₂' →
  Expr.binop op e₁ e₂ ≲⟨env, env'⟩ Expr.binop op e₁' e₂'

lemma Expr.Approx.Param.cong_lambda {e e' env₁ env₂ name₁ name₂} :
  (∀ a₁ a₂, a₁ ≲ᵥ a₂ → e ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ e') →
  Expr.lambda name₁ e ≲⟨env₁, env₂⟩ Expr.lambda name₂ e'

lemma Expr.Approx.Param.cong_save {e₁ e₂ e₁' e₂' env env' name name'} :
  (env ⊢ e₁↓ → env' ⊢ e₁'↓) →
  (∀ a a', env ⊢ e₁ ↦ a → env' ⊢ e₁' ↦ a' → e₂ ≲⟨a ∷ env, a' ∷ env'⟩ e₂') →
  Expr.save name e₁ e₂ ≲⟨env, env'⟩ Expr.save name' e₁' e₂'

lemma Expr.Approx.Param.cong_branch {constr names names' e e' next next' a a' env env'} :
  a ≲ᵥ a' →
  (∀ args args', a = Value.constr_app constr args → a' = Value.constr_app constr args' →
    e ≲⟨args.map Object.value ++ env, args'.map Object.value ++ env'⟩ e') →
  next ≲⟨a ∷ env, a' ∷ env'⟩ next' →
  Expr.branch constr names e next ≲⟨a ∷ env, a' ∷ env'⟩ Expr.branch constr names' e' next'

lemma Expr.Approx.Param.cong_recur {e e' env env' name name'} :
  e ≲⟨Object.delayed env (Expr.recur name e) :: env, Object.delayed env' (Expr.recur name' e') :: env'⟩ e' →
  Expr.recur name e ≲⟨env, env'⟩ Expr.recur name' e'

lemma Expr.Approx.Param.cong_fail {e env env'} :
  Expr.fail ≲⟨env, env'⟩ e

lemma Eval.Indexed.monotone {n n' env e v} (h : env ⊢ e ↦(n) v) (h' : n ≤ n') : env ⊢ e ↦(n') v

lemma Eval.Indexed.toEval {n env e v} (h : env ⊢ e ↦(n) v) : env ⊢ e ↦ v

lemma Eval.toIndexed {env e v} (h : env ⊢ e ↦ v) : ∃ n, env ⊢ e ↦(n) v

lemma Value.Equiv.toApprox₁ {v₁ v₂} : v₁ ≈ᵥ v₂ → v₁ ≲ᵥ v₂

lemma Value.Equiv.toApprox₂ {v₁ v₂} : v₁ ≈ᵥ v₂ → v₂ ≲ᵥ v₁

lemma Value.Approx.toEquiv {v₁ v₂} : v₁ ≲ᵥ v₂ → v₂ ≲ᵥ v₁ → v₁ ≈ᵥ v₂

@[refl]
lemma Value.Equiv.refl {v} : v ≈ᵥ v

@[symm]
lemma Value.Equiv.symm {v₁ v₂} : v₁ ≈ᵥ v₂ → v₂ ≈ᵥ v₁

@[trans]
lemma Value.Equiv.trans {v₁ v₂ v₃} : v₁ ≈ᵥ v₂ → v₂ ≈ᵥ v₃ → v₁ ≈ᵥ v₃

lemma Object.Equiv.toApprox {o₁ o₂} : o₁ ≈ₒ o₂ → o₁ ≲ₒ o₂

lemma Object.Equiv.toApprox' {o₁ o₂} : o₁ ≈ₒ o₂ → o₂ ≲ₒ o₁

lemma Object.Approx.toEquiv {o₁ o₂} : o₁ ≲ₒ o₂ → o₂ ≲ₒ o₁ → o₁ ≈ₒ o₂

@[refl]
lemma Object.Equiv.refl {o} : o ≈ₒ o

@[symm]
lemma Object.Equiv.symm {o₁ o₂} : o₁ ≈ₒ o₂ → o₂ ≈ₒ o₁

@[trans]
lemma Object.Equiv.trans {o₁ o₂ o₃} : o₁ ≈ₒ o₂ → o₂ ≈ₒ o₃ → o₁ ≈ₒ o₃

lemma Env.Equiv.toApprox₁ {env₁ env₂} : env₁ ≈ₑ env₂ → env₁ ≲ₑ env₂

lemma Env.Equiv.toApprox₂ {env₁ env₂} : env₁ ≈ₑ env₂ → env₂ ≲ₑ env₁

lemma Env.Equiv.toApprox {env₁ env₂} : env₁ ≈ₑ env₂ → env₁ ≲ₑ env₂ ∧ env₂ ≲ₑ env₁

lemma Env.Approx.toEquiv {env₁ env₂} : env₁ ≲ₑ env₂ → env₂ ≲ₑ env₁ → env₁ ≈ₑ env₂

@[refl]
lemma Env.Equiv.refl {env} : env ≈ₑ env

@[symm]
lemma Env.Equiv.symm {env₁ env₂} : env₁ ≈ₑ env₂ → env₂ ≈ₑ env₁

@[trans]
lemma Env.Equiv.trans {env₁ env₂ env₃} : env₁ ≈ₑ env₂ → env₂ ≈ₑ env₃ → env₁ ≈ₑ env₃

lemma Expr.Equiv.toParam {e₁ e₂ env₁ env₂} : e₁ ≈ e₂ → env₁ ≈ₑ env₂ → e₁ ≈⟨env₁, env₂⟩ e₂

lemma Expr.Equiv.fromParam {e₁ e₂} : (∀ env₁ env₂, env₁ ≈ₑ env₂ → e₁ ≈⟨env₁, env₂⟩ e₂) → e₁ ≈ e₂

lemma Expr.Equiv.toApprox₁ {e₁ e₂} : e₁ ≈ e₂ → e₁ ≲ e₂

lemma Expr.Equiv.toApprox₂ {e₁ e₂} : e₁ ≈ e₂ → e₂ ≲ e₁

lemma Expr.Equiv.toApprox {e₁ e₂} : e₁ ≈ e₂ → e₁ ≲ e₂ ∧ e₂ ≲ e₁

lemma Expr.Approx.toEquiv {e₁ e₂} : e₁ ≲ e₂ → e₂ ≲ e₁ → e₁ ≈ e₂

lemma Expr.Equiv.Approx.equiv {e₁ e₂} : e₁ ≈ e₂ ↔ e₁ ≲ e₂ ∧ e₂ ≲ e₁

@[refl]
lemma Expr.Equiv.refl {e} : e ≈ e

@[trans]
lemma Expr.Equiv.trans {e₁ e₂ e₃} : e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃

@[symm]
lemma Expr.Equiv.symm {e₁ e₂} : e₁ ≈ e₂ → e₂ ≈ e₁

lemma Expr.Equiv.const {c₁ c₂} :
  Expr.const c₁ ≈ Expr.const c₂ →
  c₁ = c₂

lemma Expr.Equiv.eval_const {op a₁ a₂ i₁ i₂ i₃} :
  a₁ ≈ Expr.const (Constant.int i₁) →
  a₂ ≈ Expr.const (Constant.int i₂) →
  i₃ = eval_binop_int op i₁ i₂ →
  Expr.binop op a₁ a₂ ≈
    Expr.const (Constant.int i₃)

@[refl]
lemma Value.Approx.refl v : v ≲ᵥ v

@[simp]
lemma Value.Approx.unit_left {v} : v ≲ᵥ Value.unit ↔ v = Value.unit

@[simp]
lemma Value.Approx.unit_right {v} : Value.unit ≲ᵥ v ↔ v = Value.unit

@[simp]
lemma Value.Approx.const_left {v c} : v ≲ᵥ Value.const c ↔ v = Value.const c

@[simp]
lemma Value.Approx.const_right {v c} : Value.const c ≲ᵥ v ↔ v = Value.const c

@[aesop unsafe apply]
lemma Value.Approx.constr_app {ctr_name args_rev args_rev'} :
  args_rev ≲ₐ args_rev' →
  Value.constr_app ctr_name args_rev ≲ᵥ Value.constr_app ctr_name args_rev'

@[aesop safe destruct]
lemma Value.Approx.constr_app_inv {ctr_name args_rev args_rev'} :
  Value.constr_app ctr_name args_rev ≲ᵥ Value.constr_app ctr_name args_rev' →
  args_rev ≲ₐ args_rev'

lemma Value.Approx.constr_app_inv_length {ctr_name args_rev args_rev'} :
  Value.constr_app ctr_name args_rev ≲ᵥ Value.constr_app ctr_name args_rev' →
  args_rev.length = args_rev'.length

@[aesop unsafe 90% destruct]
lemma Value.Approx.constr_app_inv_left {ctr_name args_rev' v} :
  v ≲ᵥ Value.constr_app ctr_name args_rev' →
  ∃ args_rev,
    v = Value.constr_app ctr_name args_rev ∧
    args_rev ≲ₐ args_rev'

@[aesop unsafe 90% destruct]
lemma Value.Approx.constr_app_inv_right {ctr_name args_rev v} :
  Value.constr_app ctr_name args_rev ≲ᵥ v →
  ∃ args_rev',
    v = Value.constr_app ctr_name args_rev' ∧
    args_rev ≲ₐ args_rev'

lemma Value.Approx.closure_inv {env₁ body₁ env₂ body₂}
  (h : Value.closure env₁ body₁ ≲ᵥ Value.closure env₂ body₂) :
  ∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂

@[aesop unsafe 90% destruct]
lemma Value.Approx.closure_inv_left {env₂ body₂ v} :
  v ≲ᵥ Value.closure env₂ body₂ →
  ∃ env₁ body₁,
    v = Value.closure env₁ body₁ ∧
    (∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂)

@[aesop unsafe 90% destruct]
lemma Value.Approx.closure_inv_right {env₁ body₁ v} :
  Value.closure env₁ body₁ ≲ᵥ v →
  ∃ env₂ body₂,
    v = Value.closure env₂ body₂ ∧
    (∀ a₁ a₂, a₁ ≲ᵥ a₂ → body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂)

@[aesop unsafe destruct]
lemma Value.Approx.invert {v v'} :
  v ≲ᵥ v' →
  Value.Approx.Inversion v v'

@[trans]
lemma Value.Approx.Indexed.trans {n v₁ v₂ v₃} : v₁ ≲ᵥ(n) v₂ → v₂ ≲ᵥ v₃ → v₁ ≲ᵥ(n) v₃

@[trans]
lemma Value.Approx.trans {v₁ v₂ v₃} : v₁ ≲ᵥ v₂ → v₂ ≲ᵥ v₃ → v₁ ≲ᵥ v₃

@[refl]
lemma Expr.Approx.Param.refl {env} e : e ≲⟨env, env⟩ e

lemma Expr.Approx.Param.trans {env₁ env₂ env₃ e₁ e₂ e₃} :
  e₁ ≲⟨env₁, env₂⟩ e₂ → e₂ ≲⟨env₂, env₃⟩ e₃ → e₁ ≲⟨env₁, env₃⟩ e₃

@[refl]
lemma Object.Approx.refl {o} : o ≲ₒ o

@[trans]
lemma Object.Approx.trans {o₁ o₂ o₃} : o₁ ≲ₒ o₂ → o₂ ≲ₒ o₃ → o₁ ≲ₒ o₃

@[refl]
lemma Env.Approx.refl {env} : env ≲ₑ env

@[trans]
lemma Env.Approx.trans {env₁ env₂ env₃} :
  env₁ ≲ₑ env₂ → env₂ ≲ₑ env₃ → env₁ ≲ₑ env₃

lemma Env.Approx.cons {env₁ env₂ o₁ o₂} :
  o₁ ≲ₒ o₂ → env₁ ≲ₑ env₂ → (o₁ :: env₁) ≲ₑ (o₂ :: env₂)

lemma Env.Approx.cons_value {v₁ v₂ env} :
  v₁ ≲ᵥ v₂ → v₁ ∷ env ≲ₑ v₂ ∷ env

@[aesop unsafe apply]
lemma Value.Approx.closure {env₁ body₁ env₂ body₂} :
  (∀ a₁ a₂,
    a₁ ≲ᵥ a₂ →
    body₁ ≲⟨a₁ ∷ env₁, a₂ ∷ env₂⟩ body₂) →
  Value.closure env₁ body₁ ≲ᵥ Value.closure env₂ body₂

lemma Object.Approx.toIndexed {o₁ o₂} : o₁ ≲ₒ o₂ → ∀ n, o₁ ≲ₒ'(n) o₂

lemma Env.Approx.toIndexed {env₁ env₂} : env₁ ≲ₑ env₂ → ∀ n, env₁ ≲ₑ'(n) env₂

lemma Expr.Approx.toIndexed {e₁ e₂} : e₁ ≲ e₂ → ∀ n, e₁ ≲'(n) e₂

theorem Value.Approx.preserved :
  ∀ env env' e v,
    env ≲ₑ env' →
    env ⊢ e ↦ v →
    ∃ v', env' ⊢ e ↦ v' ∧ v ≲ᵥ v'

lemma Expr.Approx.Param.preserved {e e' env₁ env₂ env₃} :
  e ≲⟨env₁, env₂⟩ e' →
  env₂ ≲ₑ env₃ →
  e ≲⟨env₁, env₃⟩ e'

@[refl]
lemma Expr.Approx.relf {e} : e ≲ e

@[trans]
lemma Expr.Approx.trans {e₁ e₂ e₃} : e₁ ≲ e₂ → e₂ ≲ e₃ → e₁ ≲ e₃

lemma Expr.Approx.from_preservation {e₁ e₂}
  (h : ∀ env v₁, env ⊢ e₁ ↦ v₁ → ∃ v₂, env ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂)
  : e₁ ≲ e₂

lemma Expr.Approx.to_preservation {e₁ e₂} :
  e₁ ≲ e₂ →
  ∀ env v₁, env ⊢ e₁ ↦ v₁ → ∃ v₂, env ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂

lemma Expr.Approx.preservation {e₁ e₂} :
  e₁ ≲ e₂ ↔
  ∀ env v₁, env ⊢ e₁ ↦ v₁ → ∃ v₂, env ⊢ e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂

lemma Expr.Approx.const_left {c e env} :
  Expr.const c ≲ e →
  env ⊢ e ↦ Value.const c

lemma Expr.Approx.const_right {c e env v} :
  e ≲ Expr.const c →
  env ⊢ e ↦ v →
  v = Value.const c

lemma Expr.Approx.const {c₁ c₂} :
  Expr.const c₁ ≲ Expr.const c₂ →
  c₁ = c₂

lemma Expr.Approx.eval_const₁ {op a₁ a₂ i₁ i₂ i₃} :
  a₁ ≲ Expr.const (Constant.int i₁) →
  a₂ ≲ Expr.const (Constant.int i₂) →
  i₃ = eval_binop_int op i₁ i₂ →
  Expr.binop op a₁ a₂ ≲
    Expr.const (Constant.int i₃)

lemma Expr.Approx.eval_const₂ {op a₁ a₂ i₁ i₂ i₃} :
  Expr.const (Constant.int i₁) ≲ a₁ →
  Expr.const (Constant.int i₂) ≲ a₂ →
  i₃ = eval_binop_int op i₁ i₂ →
  Expr.const (Constant.int i₃) ≲
  Expr.binop op a₁ a₂

lemma Expr.Equiv.Context.preserved (e₁ e₂ : Expr) :
  e₁ ≈ e₂ →
  ∀ (C : Context) env₁ env₂ v₁,
  env₁ ≈ₑ env₂ → env₁ ⊢ C.subst e₁ ↦ v₁ →
  ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≈ᵥ v₂

theorem Expr.Equiv.soundness (e₁ e₂ : Expr) : e₁ ≈ e₂ → e₁ ≈ᶜ e₂

theorem forall₂_trans' {α} {P Q R : α → α → Prop} {l₁ l₂ l₃}
  (h : ∀ x y z, P x y → Q y z → R x z)
  (h₁ : List.Forall₂ P l₁ l₂)
  (h₂ : List.Forall₂ Q l₂ l₃)
  : List.Forall₂ R l₁ l₃

lemma Expr.Equiv.congruence {e₁ e₂} (C : Context) : e₁ ≈ e₂ → C.subst e₁ ≈ C.subst e₂

lemma Expr.Equiv.cong_app {e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.app e₁ e₂ ≈ Expr.app e₁' e₂'

lemma Expr.Equiv.cong_constr_app {e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.constr_app e₁ e₂ ≈ Expr.constr_app e₁' e₂'

lemma Expr.Equiv.cong_binop {op e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.binop op e₁ e₂ ≈ Expr.binop op e₁' e₂'

lemma Expr.Equiv.cong_lambda {name e₁ e₁'} : e₁ ≈ e₁' → Expr.lambda name e₁ ≈ Expr.lambda name e₁'

lemma Expr.Equiv.cong_save {name e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.save name e₁ e₂ ≈ Expr.save name e₁' e₂'

lemma Expr.Equiv.cong_branch {constr names e₁ e₂ e₁' e₂'} : e₁ ≈ e₁' → e₂ ≈ e₂' → Expr.branch constr names e₁ e₂ ≈ Expr.branch constr names e₁' e₂'

lemma Expr.Equiv.cong_recur {name e e'} : e ≈ e' → Expr.recur name e ≈ Expr.recur name e'

lemma Expr.Equiv.Param.cong_var {v v' x x' env env' name name'} :
  env[x]? = some (Object.value v) →
  env'[x']? = some (Object.value v') →
  v ≈ᵥ v' →
  Expr.var name x ≈⟨env, env'⟩ Expr.var name' x'

lemma Expr.Equiv.Param.cong_unit {env env'} :
  Expr.unit ≈⟨env, env'⟩ Expr.unit

lemma Expr.Equiv.Param.cong_const {c env env'} :
  Expr.const c ≈⟨env, env'⟩ Expr.const c

lemma Expr.Equiv.Param.cong_constr {name env env'} :
  Expr.constr name ≈⟨env, env'⟩ Expr.constr name

lemma Expr.Equiv.Param.cong_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≈⟨env, env'⟩ e₁' →
  e₂ ≈⟨env, env'⟩ e₂' →
  Expr.app e₁ e₂ ≈⟨env, env'⟩ Expr.app e₁' e₂'

lemma Expr.Equiv.Param.cong_constr_app {e₁ e₂ e₁' e₂' env env'} :
  e₁ ≈⟨env, env'⟩ e₁' →
  e₂ ≈⟨env, env'⟩ e₂' →
  Expr.constr_app e₁ e₂ ≈⟨env, env'⟩ Expr.constr_app e₁' e₂'

lemma Expr.Equiv.Param.cong_binop {op e₁ e₂ e₁' e₂' env env'} :
  e₁ ≈⟨env, env'⟩ e₁' →
  e₂ ≈⟨env, env'⟩ e₂' →
  Expr.binop op e₁ e₂ ≈⟨env, env'⟩ Expr.binop op e₁' e₂'

lemma Expr.Equiv.Param.cong_lambda {e₁ e₁' env env' name name'} :
  (∀ a₁ a₂, a₁ ≈ᵥ a₂ → e₁ ≈⟨a₁ ∷ env, a₂ ∷ env'⟩ e₁') →
  Expr.lambda name e₁ ≈⟨env, env'⟩ Expr.lambda name' e₁'

lemma Expr.Equiv.Param.cong_save {e₁ e₂ e₁' e₂' env env' name name'} :
  (env ⊢ e₁↓ → env' ⊢ e₁'↓) →
  (env' ⊢ e₁'↓ → env ⊢ e₁↓) →
  (∀ a a', env ⊢ e₁ ↦ a → env' ⊢ e₁' ↦ a' → e₂ ≈⟨a ∷ env, a' ∷ env'⟩ e₂') →
  Expr.save name e₁ e₂ ≈⟨env, env'⟩ Expr.save name' e₁' e₂'

lemma Expr.Equiv.Param.cong_branch {constr names₁ names₂ e₁ e₂ e₁' e₂' a a' env env'} :
  a ≈ᵥ a' →
  (∀ args args', a = Value.constr_app constr args → a' = Value.constr_app constr args' →
    e₁ ≈⟨args.map Object.value ++ env, args'.map Object.value ++ env'⟩ e₁') →
  e₂ ≈⟨a ∷ env, a' ∷ env'⟩ e₂' →
  Expr.branch constr names₁ e₁ e₂ ≈⟨a ∷ env, a' ∷ env'⟩ Expr.branch constr names₂ e₁' e₂'

lemma Expr.Equiv.Param.cong_recur {e e' env env' name name'} :
  e ≈⟨Object.delayed env (Expr.recur name e) :: env, Object.delayed env' (Expr.recur name' e') :: env'⟩ e' →
  Expr.recur name e ≈⟨env, env'⟩ Expr.recur name' e'

lemma Expr.Equiv.Param.cong_fail {env env'} :
  Expr.fail ≈⟨env, env'⟩ Expr.fail
</all_available_lemmas>

<local_ctx>
import Juvix.Core.Main.Semantics.Approx

import Juvix.Core.Main.Semantics.Approx.Contextual

namespace Juvix.Core.Main

def Context.Indexed.Preserved (k : Nat) : Prop :=
  ∀ n m,
    n + m < k →
    ∀ e₁ e₂,
      e₁ ≲'(n + m) e₂ → ∀ (C : Context) env₁ env₂ v₁,
      env₁ ≲ₑ'(n + m) env₂ →
      env₁ ⊢ C.subst e₁ ↦(n) v₁ →
      ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≲ᵥ(m) v₂
</local_ctx>

<target_theorem>
lemma Expr.Approx.Context.preserved (e₁ e₂ : Expr) :
  e₁ ≲ e₂ →
  ∀ (C : Context) env₁ env₂ v₁,
  env₁ ≲ₑ env₂ → env₁ ⊢ C.subst e₁ ↦ v₁ →
  ∃ v₂, env₂ ⊢ C.subst e₂ ↦ v₂ ∧ v₁ ≲ᵥ v₂ :=
</target_theorem>

