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 Ty
  | bool
  | nat
  | pow : Ty → Ty → Ty

inductive Cx
  | nil
  | cons : Cx -> Ty -> Cx

inductive Var : Cx → Ty → Type
  | z : ∀ {Γ : Cx}, Var (Γ ∷ τ) τ
  | s : ∀ {Γ : Cx} {υ : Ty} τ, Var Γ τ → Var (Γ ∷ υ) τ

inductive Tm : Cx → Ty → Type
  | var : ∀ τ, Γ ∋ τ → Tm Γ τ
  | true : Tm Γ .bool
  | false : Tm Γ .bool
  | zero : Tm Γ .nat
  | succ : Tm Γ .nat → Tm Γ .nat
  | pred : Tm Γ .nat → Tm Γ .nat
  | zero? : Tm Γ .nat → Tm Γ .bool
  | cond : Tm Γ .bool → Tm Γ τ → Tm Γ τ → Tm Γ τ
  | fn : Tm (Γ ∷ τ) υ → Tm Γ (τ ⇒ υ)
  | app : Tm Γ (τ ⇒ υ) → Tm Γ τ → Tm Γ υ
  | fix : Tm Γ (τ ⇒ τ) → Tm Γ τ

inductive Tm.IsValue : Γ ⊢ τ → Type
  | true : true.IsValue
  | false : false.IsValue
  | zero : zero.IsValue
  | succ {v : Tm ..} : v.IsValue → v.succ.IsValue
  | fn {e : Tm ..} : e.fn.IsValue

inductive Ty.IsGround : Ty → Type
  | bool : bool.IsGround
  | nat : nat.IsGround

def Ty.IsGround.repr : Ty.IsGround τ → Type
  | .bool => Bool
  | .nat => Nat

def Tm.from_bool : Bool → Γ ⊢ .bool
  | .true => .true
  | .false => .false

def Tm.from_nat : Nat → Γ ⊢ .nat
  | .zero => .zero
  | .succ n => .succ (Tm.from_nat n)

def Tm.IsValue.extract_bool : {v : nil ⊢ .bool} → v.IsValue → (n : Bool) ×' v = from_bool n
  | .true, .true => ⟨.true, rfl⟩
  | .false, .false => ⟨.false, rfl⟩

def Tm.IsValue.extract_nat : {v : nil ⊢ .nat} → v.IsValue → (n : Nat) ×' v = from_nat n
  | .zero, .zero => ⟨.zero, rfl⟩
  | .succ _, .succ v' => let Φ := Tm.IsValue.extract_nat v'; ⟨Φ.fst.succ, congrArg Tm.succ Φ.snd⟩

def Tm.from_nat_is_value : ∀ n, (Tm.from_nat n : Γ ⊢ .nat).IsValue
  | .zero   => .zero
  | .succ n => .succ (from_nat_is_value n)

def Cx.append (Γ : Cx) : Cx → Cx
  | .nil => Γ
  | .cons Δ τ => (Γ.append Δ) ∷ τ

instance : Append Cx where
  append := Cx.append

def Var.tm (x : Γ ∋ τ) : Γ ⊢ τ := Tm.var τ x

def Var.succ (x : Γ ∋ τ) {υ : Ty} : (Γ ∷ υ) ∋ τ := s τ x

class Order (α) where
  R : α → α → Prop
  refl {x} : R x x
  trans {x y z} : R x y → R y z → R x z
  anti {x y} : R x y → R y x → x = y

instance [o : Order α] : Trans o.R o.R o.R where
  trans := o.trans

instance : Order Nat where
  R := Nat.le
  refl := Nat.le_refl _
  trans := Nat.le_trans
  anti := Nat.le_antisymm

instance [Order α] [Order β] : Order (α → β) where
  R := fun f g ↦ ∀ x, f x ⊑ g x
  refl := by admit /- proof elided -/

def is_monotone [Order α] [Order β] (f : α → β) := ∀ {x y : α}, x ⊑ y → f x ⊑ f y

def increasing_implies_monotone [Order α] (f : Nat → α) : (∀ n, f n ⊑ f n.succ) → is_monotone f :=

structure Mono (α) (β) [Order α] [Order β] where
  act : α → β
  act' : is_monotone act

instance [Order α] [Order β] : CoeFun (Mono α β) (fun _ => α → β) where
  coe f := f.act

instance [Order α] [Order β] : Order (Mono α β) where
  R := fun x y ↦ x.act ⊑ y.act
  refl := by admit /- proof elided -/

def Mono.const [Order α] [Order β] (b : β) : Mono α β := ⟨fun _ ↦ b, fun _ ↦ ⋆⟩

def Mono.id [Order α] : Mono α α
  := ⟨Function.id, Function.id⟩

def Mono.comp' [Order α] [Order β]  [Order γ] (f : Mono β γ) (g : Mono α β) : Mono α γ where
  act := f.act ∘ g.act
  act' := fun x_y ↦ f • (g • x_y)

def Mono.succ : Mono Nat Nat := ⟨Nat.succ, Nat.succ_le_succ⟩

def Chain (α : Type i) [Order α] := Mono Nat α

instance [Order α] : Order (Chain α) := inferInstanceAs (Order (Mono ..))

instance [Order α] : CoeFun (Chain α) (fun _ => Nat → α) where
  coe f := f.act

instance [Order α] [Order β] : Order (α × β) where
  R := fun ⟨a₀, b₀⟩ ⟨a₁, b₁⟩ ↦ a₀ ⊑ a₁ ∧ b₀ ⊑ b₁
  refl := ⟨⋆, ⋆⟩
  trans := fun ⟨p₀, p₁⟩ ⟨q₀, q₁⟩ ↦ ⟨p₀ ⬝ q₀, p₁ ⬝ q₁⟩
  anti := fun ⟨p₀, p₁⟩ ⟨q₀, q₁⟩ ↦ Prod.ext (p₀ ⇄! q₀) (p₁ ⇄! q₁)

def Chain.fst [Order α] [Order β] (c : Chain (α × β)) : Chain α :=
  ⟨fun n ↦ (c n).fst, fun p ↦ by admit /- proof elided -/
  ⟩

def Chain.snd [Order α] [Order β] (c : Chain (α × β)) : Chain β :=
  ⟨fun n ↦ (c n).snd, fun p ↦ by admit /- proof elided -/
  ⟩

def Mono.pair [Order α] [Order β] [Order γ]
  (f : Mono γ α) (g : Mono γ β) : Mono γ (α × β) :=
    ⟨fun c ↦ ⟨f c, g c⟩, fun p ↦ ⟨f • p, g • p⟩⟩

def Mono.swap [Order α] [Order β] : Mono (α × β) (β × α) := ⟨
    fun p ↦ ⟨p.snd, p.fst⟩,
    fun ⟨a', b'⟩ ↦ ⟨b', a'⟩
  ⟩

def Mono.assoc_swap_assoc {α : Type i} {β : Type j}
  [Order α] [Order β] [Order γ] : Mono ((α × β) × γ) ((α × γ) × β) := ⟨
    fun p ↦ ⟨⟨p.fst.fst, p.snd⟩, p.fst.snd⟩,
    fun ⟨⟨a', b'⟩, c'⟩ ↦ ⟨⟨a', c'⟩, b'⟩
  ⟩

def Mono.comp {α : Type i} {β : Type j} {γ : Type k} [Order α] [Order β] [Order γ]
  : Mono (Mono β γ × Mono α β) (Mono α γ) := ⟨
    fun h ↦ ⟨fun x ↦ h.fst (h.snd x), fun x_y ↦ h.fst • (h.snd • x_y)⟩,
    fun {h₀ h₁} h a ↦ (h₀.fst • h.right a) ⬝ (h.left (h₁.snd a))
  ⟩

def Mono.eval {α : Type i} {β : Type j} [Order α] [Order β] : Mono (Mono α β × α) β :=
  ⟨fun x ↦ x.fst x.snd, fun {x y} p ↦ (x.fst • p.right) ⬝ (p.left y.snd)⟩

inductive Eval : (.nil ⊢ τ) → (.nil ⊢ τ) → Type
  | true : Eval .true .true
  | false : Eval .false .false
  | zero : Eval .zero .zero
  | succ : Eval t v → Eval (t.succ) (v.succ)
  | fn : Eval (.fn e) (e.fn)
  | pred : Tm.IsValue v → Eval t (v.succ) → Eval (t.pred) (v)
  | zero?_zero : Eval t (.zero) → Eval (t.zero?) .true
  | zero?_succ : Tm.IsValue v → Eval t (v.succ) → Eval (t.zero?) .false
  | cond_true {t ct cf vt} : Eval t (.true) → Eval ct vt → Eval (t.cond ct cf) vt
  | cond_false {t ct cf vf} : Eval t (.false) → Eval cf vf → Eval (t.cond ct cf) vf
  | app {e : Tm ..} : Eval f (e.fn) → Eval (e.sub (Sb.inst u)) v → Eval (f.app u) v
  | fix {f : Tm ..} : Eval (f.app f.fix) v → Eval (f.fix) v

def Eval.result_is_value : (t ⇓ v) → v.IsValue
  | .true | .false | .zero | .fn | .zero?_zero .. | .zero?_succ .. => by admit /- proof elided -/
  | succ e   => e.result_is_value.succ
  | pred v _ => v
  | .cond_true _ e | .cond_false _ e | .app _ e | .fix e => e.result_is_value

def Tm.IsValue.evaluates : v.IsValue → (v ⇓ v)
  | .true | .false | .zero | .fn => by admit /- proof elided -/
  | .succ n => .succ n.evaluates

def Ty.IsGround.test_con {v : Γ ⊢ γ} : (γ.IsGround) → (v.IsValue) → Con Δ γ Δ .bool
  | .bool, .true   => .id
  | .bool, .false  => Con.id.cond_s .false .true
  | .nat,  .zero   => Con.id.zero?
  | .nat,  .succ n => Con.id.pred.comp (IsGround.nat.test_con n)

noncomputable def Ty.IsGround.test_con_true_iff {v : _ ⊢ γ}
  (γ_is_ground : γ.IsGround) (v_is_value : v.IsValue) (t) :
  (γ_is_ground.test_con v_is_value).fill t ⇓ .true ⇔ t ⇓ v :=

noncomputable def ConPreord.from_fill
  : (∀ (C : Con ..), C t₀ ⇓ .true → C t₁ ⇓ .true) → t₀ ≤ᶜ t₁ :=

noncomputable def approx_implies_con_preord (t₀ t₁ : .nil ⊢ τ) : (((⟦t₀⟧) Ev.nil) ◃ t₁) → t₀ ≤ᶜ t₁ :=

inductive Con : Cx → Ty → Cx → Ty → Type
  | id     : Con Γ τ Γ τ
  | comp   : Con Γ₀ τ₀ Γ₁ τ₁   → Con Γ₁ τ₁ Γ₂ τ₂   → Con Γ₀ τ₀ Γ₂ τ₂
  | sub    : Con Δ ν Γ τ       → Sb Γ Γ'           → Con Δ ν Γ' τ
  | succ   : Con Δ ν Γ .nat    → Con Δ ν Γ .nat
  | pred   : Con Δ ν Γ .nat    → Con Δ ν Γ .nat
  | zero?  : Con Δ ν Γ .nat    → Con Δ ν Γ .bool
  | cond_s : Con Δ ν Γ .bool   → Γ ⊢ τ             → Γ ⊢ τ       → Con Δ ν Γ τ
  | cond_t : Γ ⊢ .bool         → Con Δ ν Γ τ       → Γ ⊢ τ       → Con Δ ν Γ τ
  | cond_f : Γ ⊢ .bool         → Γ ⊢ τ             → Con Δ ν Γ τ → Con Δ ν Γ τ
  | fn     : Con Δ ν (Γ ∷ υ) τ → Con Δ ν Γ (υ ⇒ τ)
  | app_f  : Con Δ ν Γ (υ ⇒ τ) → Γ ⊢ υ             → Con Δ ν Γ τ
  | app_a  : Γ ⊢ υ ⇒ τ         → Con Δ ν Γ υ       → Con Δ ν Γ τ
  | fix    : Con Δ ν Γ (τ ⇒ τ) → Con Δ ν Γ τ

def Con.fill : Con Δ υ Γ τ → Δ ⊢ υ → Γ ⊢ τ
  | id          , t => t
  | comp C C'   , f => C'.fill (C.fill f)
  | sub C σ     , f => (C.fill f).sub σ
  | succ C      , t => (C.fill t).succ
  | pred C      , t => (C.fill t).pred
  | zero? C     , t => (C.fill t).zero?
  | cond_s C t f, s => (C.fill s).cond t f
  | cond_t s C f, t => s.cond (C.fill t) f
  | cond_f s t C, f => s.cond t (C.fill f)
  | fn C        , t => (C.fill t).fn
  | app_f C a   , f => (C.fill f).app a
  | app_a f C   , a => f.app (C.fill a)
  | fix C       , f => (C.fill f).fix

instance : CoeFun (Con Δ υ Γ τ) (fun _ => Δ ⊢ υ → Γ ⊢ τ) where
  coe C := C.fill

def ConEquiv (t₀ t₁ : Δ ⊢ τ) : Type :=
  ∀ γ, γ.IsGround → ∀ (C : Con Δ τ .nil γ) v, (C t₀ ⇓ v) ⇔ (C t₁ ⇓ v)

def ConPreord (t₀ t₁ : Δ ⊢ τ) : Type :=
  ∀ γ, γ.IsGround → ∀ (C : Con Δ τ .nil γ) v, (C t₀ ⇓ v) → C t₁ ⇓ v

def ConEquiv.from_preord : t₀ ≤ᶜ t₁ → t₁ ≤ᶜ t₀ → t₀ ≅ᶜ t₁ :=

def FullAbstraction := ∀ {Γ τ} {t₀ t₁ : Γ ⊢ τ}, t₀ ≅ᶜ t₁ → ⟦t₀⟧ = ⟦t₁⟧

def por_fn : (Flat Bool × Flat Bool) → (Flat Bool)
  | (.some true, _)            => .some true
  | (_, .some true)            => .some true
  | (.some false, .some false) => .some false
  | _                          => .none

def Mono.por : Mono (Flat Bool × Flat Bool) (Flat Bool) := ⟨
  por_fn,
  by admit /- proof elided -/
⟩

def Cont.por : Cont (Flat Bool × Flat Bool) (Flat Bool) := Mono.por.promote_trivial

def loop {τ : Ty} : Γ ⊢ τ := Var.z.tm.fn.fix

def loop_den_eq : (⟦(loop : _ ⊢ τ)⟧) ρ = ⊥ :=

def por_test (b : Bool) : .nil ⊢ (.bool ⇒ .bool ⇒ .bool) ⇒ .bool :=
  (((Var.z.tm.app .true).app loop).cond
    (((Var.z.tm.app loop).app .true).cond
      (((Var.z.tm.app .false).app .false).cond
        loop
        (Tm.from_bool b))
      loop)
    loop).fn

def por_curry : ↑⟦.bool ⇒ .bool ⇒ .bool ty⟧ := Cont.por.curry

def por_test_left_true : (⟦(Var.z.tm.app .true).app loop⟧) (Ev.nil.push por_curry) = Flat.some true :=

def por_test_right_true : (⟦(Var.z.tm.app loop).app .true⟧) (Ev.nil.push por_curry) = Flat.some true :=

def por_test_b_den_por_eq_b : ∀ {b}, (⟦por_test b⟧) Ev.nil por_curry = Flat.some b :=

def Ty.Magic : (τ : Ty) → ↑⟦τ ty⟧ → ↑⟦τ ty⟧ → ↑⟦τ ty⟧ → Prop
  | .bool | .nat => fun t₀ t₁ t₂ ↦ (t₀ = ⊥ ∨ t₁ = ⊥) ∨ (t₀ = t₂ ∧ t₁ = t₂)
  | .pow τ₀ τ₁   => fun t₀ t₁ t₂ ↦ ∀ a₀ a₁ a₂, τ₀.Magic a₀ a₁ a₂ → τ₁.Magic (t₀ a₀) (t₁ a₁) (t₂ a₂)

def Cx.Magic (Γ : Cx) (ρ₀ ρ₁ ρ₂ : ⟦Γ cx⟧) : Sort :=
  ∀ (τ : Ty) (x : Γ ∋ τ), τ.Magic (ρ₀ τ x) (ρ₁ τ x) (ρ₂ τ x)

def por_is_not_magical : ¬(.bool ⇒ .bool ⇒ .bool).Magic por_curry por_curry por_curry :=

def Ty.bottom_magic_left : (τ : Ty) → ∀ {a b}, τ.Magic ⊥ a b
  | .bool | .nat => by admit /- proof elided -/
  | .pow τ₀ τ₁   => by admit /- proof elided -/

def Ty.bottom_magic_right : (τ : Ty) → ∀ {a b}, τ.Magic a ⊥ b
  | .bool | .nat => by admit /- proof elided -/
  | .pow τ₀ τ₁   => by admit /- proof elided -/

noncomputable def Ty.supremum_magic : (τ : Ty) →  ∀ {c₀ c₁ c₂},
  (∀ n, τ.Magic (c₀ n) (c₁ n) (c₂ n)) → τ.Magic (⨆ c₀) (⨆ c₁) (⨆ c₂) :=

def Ty.Magic.succ : Ty.nat.Magic t₀ t₁ t₂
  → Ty.nat.Magic (Cont.flat (Nat.succ) t₀) (Cont.flat (Nat.succ) t₁) (Cont.flat (Nat.succ) t₂) :=

def Ty.Magic.pred : Ty.nat.Magic t₀ t₁ t₂ → Ty.nat.Magic (Cont.pred t₀) (Cont.pred t₁) (Cont.pred t₂) :=

def Ty.Magic.zero? : Ty.nat.Magic t₀ t₁ t₂
  → Ty.bool.Magic (Cont.flat (Nat.zero?) t₀) (Cont.flat (Nat.zero?) t₁) (Cont.flat (Nat.zero?) t₂) :=

def Ty.Magic.cond {τ : Ty} {t₀ t₁ t₂ f₀ f₁ f₂ : ↑⟦τ ty⟧}
  : Ty.bool.Magic s₀ s₁ s₂ → τ.Magic t₀ t₁ t₂ → τ.Magic f₀ f₁ f₂
  → τ.Magic (Cont.cond.uncurry (s₀, (t₀, f₀)))
    (Cont.cond.uncurry (s₁, (t₁, f₁))) (Cont.cond.uncurry (s₂, (t₂, f₂))) :=

def Ty.Magic.fix  : (τ ⇒ τ).Magic t₀ t₁ t₂ → τ.Magic (Cont.fix' t₀) (Cont.fix' t₁) (Cont.fix' t₂) :=

def Cx.Magic.nil : Cx.nil.Magic Ev.nil Ev.nil Ev.nil :=

def Cx.Magic.push {Γ : Cx} {ρ₀ ρ₁ ρ₂} : Γ.Magic ρ₀ ρ₁ ρ₂ → τ.Magic d₀ d₁ d₂
  → (Γ ∷ τ).Magic (ρ₀.push d₀) (ρ₁.push d₁) (ρ₂.push d₂) :=

def Tm.magic (t : Γ ⊢ τ) : ∀ {ρ₀ ρ₁ ρ₂}, Γ.Magic ρ₀ ρ₁ ρ₂  → τ.Magic ((⟦t⟧) ρ₀) ((⟦t⟧) ρ₁) ((⟦t⟧) ρ₂) :=

def por_is_undefinable {f : .nil ⊢ .bool ⇒ .bool ⇒  .bool} : ¬(⟦f⟧) Ev.nil = por_curry :=

def por_test_some_den : (por_test k).app f ⇓ Tm.from_bool n → (⟦f⟧) Ev.nil = por_curry :=

noncomputable def por_test_con_equiv : por_test false ≅ᶜ por_test true :=

noncomputable def Ty.den : Ty → DomainType
  | .bool => ⟨Flat Bool, _, inferInstance⟩
  | .nat => ⟨Flat Nat, _, inferInstance⟩
  | .pow T₀ T₁ => by admit /- proof elided -/

instance (τ υ : Ty): CoeFun (⟦τ ⇒ υ ty⟧.carrier) (fun _ => ⟦τ ty⟧.carrier → ⟦υ ty⟧.carrier) where
  coe f := f.fn.act

noncomputable instance : TrivialDomain (⟦.bool ty⟧) := inferInstanceAs (TrivialDomain (Flat Bool))

noncomputable instance : TrivialDomain (⟦.nat ty⟧) := inferInstanceAs (TrivialDomain (Flat Nat))

def Ev (Γ : Cx) : Type := ∀ τ, Var Γ τ → ↑⟦τ ty⟧

noncomputable instance (Γ : Cx) : Order (⟦Γ cx⟧) where
  R := fun a b ↦ ∀ τ (x : Var Γ τ), a τ x ⊑ b τ x
  refl := fun _ _ ↦ ⋆
  trans := fun {_ _ _} p q {_} x ↦ p _ x ⬝ q _ x
  anti := fun p q ↦ funext fun _ ↦ (funext fun x ↦ p _ x ⇄! q _ x)

noncomputable instance (Γ : Cx) : Domain (⟦Γ cx⟧) where
  bot := fun _ _ ↦ ⊥
  sup := fun c _ x ↦ ⨆ ⟨fun n ↦ c.act n _ x, fun i_j ↦ c.act' i_j _ x⟩
  is_bot := fun _ _ ↦ Domain.is_bot
  is_bound := fun c {n} {_} x ↦ Domain.is_bound ⟨fun n ↦ c.act n _ x, fun i_j ↦ c.act' i_j _ x⟩ n
  is_least := fun c _ p {_} x ↦ Domain.is_least ⟨fun n ↦ c.act n _ x, fun i_j ↦ c.act' i_j _ x⟩
    (fun {_} ↦ p _ x)

def Ev.nil : ⟦Cx.nil cx⟧ :=

def Ev.push {Γ : Cx} (ρ : ⟦Γ cx⟧) {τ : Ty} (d : ↑⟦τ ty⟧) : ⟦Γ ∷ τ cx⟧ :=
  fun {τ} x ↦ match x with
  | .z => d
  | .s τ x => ρ τ x

def Ev.from {Γ : Cx} {τ : Ty} : Cont (⟦Γ cx⟧ × ⟦τ ty⟧) (⟦Γ ∷ τ cx⟧) := ⟨
  ⟨
    fun ⟨ρ, d⟩ υ x ↦ ρ.push d υ x,
    by admit /- proof elided -/
  ⟩,
  by admit /- proof elided -/
⟩

noncomputable def Tm.den : (Γ ⊢ τ) → Cont (⟦Γ cx⟧) (⟦τ ty⟧)
  | .var τ x => ⟨⟨fun ρ ↦ ρ τ x, fun ρ₀_ρ₁ ↦ ρ₀_ρ₁ τ x⟩, ⋆⟩
  | .true => Cont.const (.some .true)
  | .false => Cont.const (.some .false)
  | .zero => Cont.const (.some 0)
  | .succ e => Cont.flat (Nat.succ) ∘ e.den
  | .pred e => Cont.pred ∘ e.den
  | .zero? e => Cont.flat (Nat.zero?) ∘ e.den
  | .cond s t f  => Cont.uncurry (Cont.cond) ∘ Cont.pair s.den (Cont.pair t.den f.den)
  | .fn e  => Cont.curry (e.den ∘ Ev.from)
  | .app f e => Cont.eval ∘ (Cont.pair f.den e.den)
  | .fix f => Cont.fix' ∘ f.den

noncomputable def Ren.den (r : Ren Γ Δ) : Cont (⟦Δ cx⟧) (⟦Γ cx⟧) :=
  ⟨⟨fun ρ _ x ↦ (⟦(x.ren r).tm⟧) ρ, fun ρ' _ x ↦ (⟦(x.ren r).tm⟧) • ρ'⟩, fun _ x ↦ (⟦(x.ren r).tm⟧).sub⟩

noncomputable def Sb.den (σ : Sb Γ Δ) : Cont (⟦Δ cx⟧) (⟦Γ cx⟧) :=
  ⟨⟨fun ρ _ x ↦ (⟦x.sub σ⟧) ρ, fun ρ' _ x ↦ (⟦x.sub σ⟧) • ρ'⟩, fun _ x ↦ (⟦x.sub σ⟧).sub⟩

noncomputable def Con.den : Con Δ υ Γ τ → Cont (⟦Γ cx⟧ × Cont (⟦Δ cx⟧) (⟦υ ty⟧)) ⟦τ ty⟧
  | id         => Cont.uncurry Cont.id ∘' Cont.swap
  | comp C₀ C₁ => Cont.uncurry (Cont.curry (C₁.den ∘' Cont.swap)
                             ∘' Cont.curry (C₀.den ∘' Cont.swap)) ∘' Cont.swap
  | sub C σ => Cont.uncurry ((Cont.curry C.den) ∘' (⟦σ⟧))
  | succ C => Cont.flat (Nat.succ) ∘' C.den
  | pred C => Cont.pred ∘' C.den
  | zero? C => Cont.flat (Nat.zero?) ∘' C.den
  | fn C   => Cont.curry ((Cont.uncurry (Cont.curry C.den ∘' Ev.from)) ∘' Cont.assoc_swap_assoc)
  | cond_s C t f => Cont.uncurry (Cont.cond)
    ∘' Cont.pair C.den (Cont.pair ((⟦t⟧) ∘' Cont.fst) ((⟦f⟧) ∘' Cont.fst))
  | cond_t s C f => Cont.uncurry (Cont.cond)
    ∘' Cont.pair ((⟦s⟧) ∘' Cont.fst) (Cont.pair C.den ((⟦f⟧) ∘' Cont.fst))
  | cond_f s t C => Cont.uncurry (Cont.cond)
    ∘' Cont.pair ((⟦s⟧) ∘' Cont.fst) (Cont.pair ((⟦t⟧) ∘' Cont.fst) C.den)
  | app_f C a => Cont.eval ∘' (Cont.pair C.den ((⟦a⟧) ∘' Cont.fst))
  | app_a f C => Cont.eval ∘' (Cont.pair ((⟦f⟧) ∘' Cont.fst) C.den)
  | fix C => Cont.fix' ∘' C.den

def Con.fill_den_eq (C : Con Δ υ Γ τ) : ⟦C t⟧ = ((⟦C con⟧) ∘' Cont.swap).curry (⟦t⟧) :=

def Ren Γ Δ := ∀ τ, Γ ∋ τ → Δ ∋ τ

def Var.ren (v : Γ ∋ τ) (r : Ren Γ Δ) := r τ v

def Ren.id : Ren Γ Γ := fun _ ↦ Function.id

def Ren.comp (r₀₁ : Ren Γ₀ Γ₁) (r₁₂ : Ren Γ₁ Γ₂) : Ren Γ₀ Γ₂ :=
  fun _ x => (x.ren r₀₁).ren r₁₂

instance : Trans Ren Ren Ren where
  trans := Ren.comp

def Ren.keep (r : Ren Γ Δ) (τ  : Ty) : Ren (Γ ∷ τ) (Δ ∷ τ) :=
  fun υ v => match v with
  | .z     => .z
  | .s _ x => (x.ren r).succ

def Ren.keeps (r : Ren Γ₀ Γ₁) : (Δ : Cx) → Ren (Γ₀ ++ Δ) (Γ₁ ++ Δ)
  | .nil      => r
  | .cons Δ τ => (r.keeps Δ).keep τ

def Tm.ren (t : Γ ⊢ τ) (r : Ren Γ Δ) : Δ ⊢ τ :=
  match t with
  | .var τ x    => (x.ren r).tm
  | .true       => .true
  | .false      => .false
  | .zero       => .zero
  | .succ e     => (e.ren r).succ
  | .pred e     => (e.ren r).pred
  | .zero? e    => (e.ren r).zero?
  | .cond s t f => (s.ren r).cond (t.ren r) (f.ren r)
  | .fn e       => (e.ren (r ∷ᵣ _)).fn
  | .app f a    => (f.ren r).app (a.ren r)
  | .fix f      => (f.ren r).fix

def Tm.ren_id_eq {t : Γ ⊢ τ} : t.ren Ren.id = t :=

def Ren.weak {τ  : Ty} : Ren Γ (Γ ∷ τ) := Var.s

def Ren.weaks : (Δ : Cx) → Ren Γ (Γ ++ Δ)
  | .nil      => id
  | .cons Δ _ => fun υ x ↦ weak υ (weaks Δ υ x)

def Ren.cast : (Γ = Δ) → Ren Γ Δ :=

def Sb Γ Δ := ∀ τ, Γ ∋ τ → Δ ⊢ τ

def Var.sub (v : Γ ∋ τ) (σ : Sb Γ Δ) := σ τ v

def Sb.keep (σ : Sb Γ Δ) (τ : Ty) : Sb (Γ ∷ τ) (Δ ∷ τ) :=
  fun _ x => match x with
  | .z     => .var τ .z
  | .s _ x => (x.sub σ).ren .s

def Sb.keeps (σ : Sb Γ₀ Γ₁) : (Δ : Cx) → Sb (Γ₀ ++ Δ) (Γ₁ ++ Δ)
  | .nil      => σ
  | .cons Δ τ => (σ.keeps Δ).keep τ

def Tm.sub (t : Γ ⊢ τ) (σ : Sb Γ Δ) : Δ ⊢ τ :=
  match t with
  | .var _ x    => x.sub σ
  | .true       => .true
  | .false      => .false
  | .zero       => .zero
  | .succ t     => (t.sub σ).succ
  | .pred t     => (t.sub σ).pred
  | .zero? t    => (t.sub σ).zero?
  | .cond s t f => (s.sub σ).cond (t.sub σ) (f.sub σ)
  | .fn e       => (e.sub (σ ∷ₛ _)).fn
  | .app f a    => (f.sub σ).app (a.sub σ)
  | .fix f      => (f.sub σ).fix

def Sb.id : Sb Γ Γ := fun τ x => .var τ x

def Sb.comp (σ₀₁ : Sb Γ₀ Γ₁) (σ₁₂ : Sb Γ₁ Γ₂) : Sb Γ₀ Γ₂ :=
  fun _ x => (x.sub σ₀₁).sub σ₁₂

instance : Trans Sb Sb Sb where
  trans := Sb.comp

private def weak' {Γ} {τ} {Δ} : Ren (Γ ++ Δ) (Γ ∷ τ ++ Δ) := Ren.weak ++ᵣ Δ

private def sub_weak_exchange {t : Γ₀ ⊢ τ} {σ : Sb Γ₀ Γ₁}
  : (t.sub σ).ren Ren.weak = (t.ren Ren.weak).sub (σ ∷ₛ υ) :=

def Sb.keep_id : (@ Sb.id Γ) ∷ₛ τ = Sb.id :=

def Sb.keep_comp {σ₀₁ : Sb Γ₀ Γ₁} {σ₁₂ : Sb Γ₁ Γ₂}
  : (σ₀₁ ⬝ σ₁₂) ∷ₛ τ = (σ₀₁ ∷ₛ τ) ⬝ (σ₁₂ ∷ₛ τ) :=

def Tm.sub_id_eq {t : Γ ⊢ τ} : t.sub (Sb.id) = t :=

def Tm.sub_comp_eq {t : Γ₀ ⊢ τ}
  : ∀ {Γ₁ Γ₂} {σ₀₁ : Sb Γ₀ Γ₁} {σ₁₂ : Sb Γ₁ Γ₂}, t.sub (σ₀₁ ⬝ σ₁₂) = (t.sub σ₀₁).sub σ₁₂ :=

def Ren.then (r : Ren Γ₀ Γ₁) (σ : Sb Γ₁ Γ₂) : Sb Γ₀ Γ₂ :=
  fun _ x => (x.ren r).sub σ

instance : Trans Ren Sb Sb where
  trans := Ren.then

def Sb.keep_then_eq {r : Ren Γ₀ Γ₁} {σ : Sb Γ₁ Γ₂} : (r ⬝ σ) ∷ₛ τ = ((r ∷ᵣ τ) ⬝ (σ ∷ₛ τ)) :=

def Tm.sub_then_eq {t : Γ₀ ⊢ τ}
  : ∀ {Γ₁ Γ₂} {r : Ren Γ₀ Γ₁} {σ : Sb Γ₁ Γ₂}, t.sub (r ⬝ σ) = (t.ren r).sub σ :=

def Sb.inst : (t : Γ ⊢ τ) → Sb (Γ ∷ τ) Γ :=
  fun a _ x => match x with
  | .z     => a
  | .s _ x => x.tm

def Sb.weak_inst_eq : Ren.weak ⬝ (Sb.inst a) = Sb.id :=

def Tm.weak_inst_eq {t : Γ ⊢ τ} : (t.ren Ren.weak).sub (Sb.inst a) = t :=

def Sb.push (σ : Sb Γ Δ) {υ : Ty} (a : Δ ⊢ υ) : Sb (Γ ∷ υ) Δ :=
  fun _ x => match x with
  | .z     => a
  | .s _ x => x.sub σ

def Sb.push_eq {σ : Sb  Γ Δ} {υ : Ty} {a : Δ ⊢ υ} : σ.push a = (σ ∷ₛ υ) ⬝ Sb.inst a :=

inductive Flat (α : Type) : Type where
  | none : Flat α
  | some : α → Flat α

instance (a : Flat α) : Decidable (∃ k, a = .some k) :=
  match a with
  | .none => isFalse (fun p ↦ p.elim (fun _ y ↦ by admit /- proof elided -/
  ))
  | .some a => isTrue (.intro a rfl)

instance [DecidableEq α] : DecidableEq (Flat α) := fun a b ↦
  match a with
  | .none => match b with
    | .none => isTrue rfl
    | .some _ => isFalse Flat.noConfusion
  | .some a => match b with
    | .none => isFalse Flat.noConfusion
    | .some b => if p : a = b then isTrue (by admit /- proof elided -/
    ) else isFalse (fun q ↦ p (by admit /- proof elided -/
    ))

instance [DecidableEq α] : Order (Flat α) where
  R := fun x y ↦ (x ≠ .none) → x = y
  refl := fun _ ↦ rfl
  trans {x y z} p q :=
    if h : x = .none
    then fun a ↦ (a h).elim
    else fun a ↦ by rw [p h]; rw [p h] at h; rw [q h]
  anti {x y} p q :=
    if i : x = .none
    then if j : y = .none then by rw [i, j] else by rw [q j]
    else by rw [p i]

noncomputable def flat_sup (c : Chain (Flat α)) : Flat α :=
  if p : ∃ a n, c.act n = .some a then .some p.choose else .none

noncomputable instance : Domain (Flat α) where
  bot := .none
  sup := flat_sup
  is_bot := by admit /- proof elided -/

noncomputable instance (α) [DecidableEq α] : TrivialDomain (Flat α) where
  eventually_const := fun c ↦ by admit /- proof elided -/

def lift_flat (f : α → β) : Flat α → Flat β
| .none => .none
| .some x => .some (f x)

def Mono.flat (f : α → β) : (Mono (Flat α) (Flat β)) := ⟨
    lift_flat f,
    by admit /- proof elided -/
  ⟩

def Cont.flat (f : α → β) : (Cont (Flat α) (Flat β)) := (Mono.flat f).promote_trivial

def cond' [Order α] [Domain α] : Mono (Flat Bool) (Cont (α × α) α) := ⟨
  fun b ↦ (
    match b with
    | .none => Cont.const ⊥
    | .some true => Cont.fst
    | .some false => Cont.snd
  ),
  by admit /- proof elided -/
⟩

def Cont.cond [Order α] [Domain α] : Cont (Flat Bool) (Cont (α × α) α) := ⟨
  cond',
  by admit /- proof elided -/
⟩

def Nat.partial_pred : Flat Nat → Flat Nat :=
  fun n ↦ match n with
  | .some (.succ n) => .some n
  | _ => .none

def Mono.pred : Mono (Flat Nat) (Flat Nat) := ⟨
    Nat.partial_pred,
    by admit /- proof elided -/
  ⟩

def Cont.pred : Cont (Flat Nat) (Flat Nat) := Mono.pred.promote_trivial

def Tm.Approx : ∀ {τ}, (.nil ⊢ τ) → ↑⟦τ ty⟧ → Type
  | .bool   => fun t d ↦ ∀ n,   d = .some n → t ⇓ Tm.from_bool n
  | .nat    => fun t d ↦ ∀ n,   d = .some n → t ⇓ Tm.from_nat n
  | .pow .. => fun t d ↦ ∀ e s, Tm.Approx e s → Tm.Approx (t.app e) (d s)

def Sb.Approx {Γ : Cx} (ρ : ⟦Γ cx⟧) (σ : Sb Γ .nil) : Type :=
  ∀ τ x, ρ τ x ◃ x.sub σ

def Con.Approx (D: (Cont (Cont ⟦Δ cx⟧ ⟦υ ty⟧) (⟦τ ty⟧))) (C : Con Δ υ .nil τ) : Type :=
    ∀ (d : Cont ⟦Δ cx⟧ ⟦υ ty⟧) (t : Δ ⊢ υ),
      (∀ {ρ : ⟦Δ cx⟧} {σ}, (ρ ◃ σ) → (d ρ ◃ t.sub σ)) → D d ◃ C t

def bottom_approximates : ∀ {τ} {t : .nil ⊢ τ}, ⊥ ◃ t
  | .bool | .nat => fun _ p   ↦ Flat.noConfusion p
  | .pow ..      => fun _ _ _ ↦ bottom_approximates

noncomputable def supremum_approximates {τ} {t : .nil ⊢ τ} : ∀ {c}, (∀ n, c n ◃ t) → ⨆ c ◃ t :=

def same_eval_same_approx
  {τ : Ty} : ∀ {t₀ t₁ : .nil ⊢ τ}, (∀ {v}, t₀ ⇓ v → t₁ ⇓ v) → ∀ {d}, (d ◃ t₀) → (d ◃ t₁) :=

def fn_same_eval {e : _ ⊢ _} : (e.sub (σ.push t) ⇓ v) → (e.fn.sub σ).app t ⇓ v :=

def Tm.Approx.succ {t : Tm ..} {d} : (d ◃ t) → (Cont.flat Nat.succ d ◃ t.succ) :=

def Tm.Approx.pred {t : Tm ..} {d} : (d ◃ t) → (Cont.pred d ◃ t.pred) :=

def Tm.Approx.zero? {t : Tm ..} {d} : (d ◃ t) → (Cont.flat Nat.zero? d ◃ t.zero?) :=

noncomputable def Tm.Approx.fix {t : _ ⊢ τ ⇒ τ} {d} : (d ◃ t) → (Cont.fix d ◃ t.fix) :=

noncomputable def Tm.Approx.cond {s : .nil ⊢ .bool} {s'} {t f : .nil ⊢ τ} {t' f'}
  : (s' ◃ s) → (t' ◃ t) → (f' ◃ f) → Cont.cond.uncurry (s', (t', f')) ◃ s.cond t f :=

def Sb.Approx.id : Ev.nil ◃ Sb.id :=

def Sb.Approx.push {σ : Sb Γ .nil} {ρ : ⟦Γ cx⟧} (ρ_σ : ρ ◃ σ)
  {u : .nil ⊢ τ} {d : ↑⟦τ ty⟧} (d_u : d ◃ u) : ρ.push d ◃ σ.push u :=

noncomputable def Tm.approx (t : Γ ⊢ τ) {ρ : ⟦Γ cx⟧} {σ : Sb Γ .nil}
  : (ρ ◃ σ) → (⟦t⟧) ρ ◃ t.sub σ :=

noncomputable def Tm.approx' (t : .nil ⊢ τ) : (⟦t⟧) Ev.nil ◃ t :=

noncomputable def Sb.approx (σ' : Sb Γ' Γ) {ρ : ⟦Γ cx⟧} {σ : Sb Γ Cx.nil}
  : (ρ ◃ σ) → ((⟦σ'⟧) ρ ◃ σ' ⬝ σ) :=

noncomputable def Con.approx (C : Con Δ υ Γ τ) {ρ : ⟦Γ cx⟧} {σ : Sb Γ .nil}
  : (ρ ◃ σ) → ⟦C con⟧.curry ρ ◃ C.sub σ :=

def compositionality {t₀ t₁ : Δ ⊢ ν} (p : ⟦t₀⟧ = ⟦t₁⟧) : ∀ (C : Con Δ ν Γ τ), ⟦C t₀⟧ = ⟦C t₁⟧ :=

noncomputable def adequacy {t v : Cx.nil ⊢ τ} : τ.IsGround → v.IsValue → ⟦t⟧ = ⟦v⟧ → t ⇓ v :=

noncomputable def den_eq_implies_con_equiv {t₀ t₁ : Γ ⊢ τ} (eq : ⟦t₀⟧ = ⟦t₁⟧) : t₀ ≅ᶜ t₁ :=

structure LogicallyEquivalent (a : Sort i) (b : Sort j) : Sort max 1 i j where
  intro ::
  mp : a → b
  mpr : b → a

def Nat.zero? : Nat → Bool
| .zero => true
| _ => false

@[inline] def Function.id {α : Sort u} (a : α) : α := a

class Domain (α) [Order α] where
  bot : α
  sup : (c : Chain α) → α
  is_bot {x} : bot ⊑ x
  is_bound (c) (n): c.act n ⊑ sup c
  is_least (c) {d} : ({n : _} → c.act n ⊑ d) → sup c ⊑ d

structure DomainType : Type (i + 1) :=
  carrier : Type i
  order : Order carrier
  domain : Domain carrier

instance : Coe DomainType Type where
  coe D := D.carrier

instance (τ : DomainType) : Order (τ) := τ.order

instance (τ : DomainType) : Domain (τ) := τ.domain

def Mono.sup [Order α] [Domain α] : Mono (Chain α) α :=
  ⟨⨆, Domain.sup_is_mono⟩

def continuous [Order α] [Order β] [Domain α] [Domain β] (f : Mono α β) :=
  ∀ {c : Chain α}, f.act (⨆ c) ⊑ ⨆ (f ∘ c)

structure Cont (α) (β) [Order α] [Order β] [Domain α] [Domain β] where
  fn : Mono α β
  sub : ∀ {c : Chain α}, fn.act (⨆ c) ⊑ ⨆ (fn ∘ c)

instance [Order α] [Order β] [Domain α] [Domain β] : CoeFun (Cont α β) (fun _ => α → β) where
  coe f := f.fn.act

def Cont.id [Order α] [Domain α] : Cont α α := ⟨Mono.id, ⋆⟩

def Cont.comp' [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ] (f : Cont β γ) (g : Cont α β)
  : Cont α γ
  := ⟨
    ⟨fun x ↦ f (g x), fun x_y ↦ f • g • x_y⟩,
    by admit /- proof elided -/
  ⟩

def Domain.sup_of_const [Order α] [Domain α] (a : α) : ⨆ (Mono.const a) = a :=
  (by admit /- proof elided -/
  ) ⇄! (Domain.is_bound (Mono.const a) 0)

def sup_succ [Order α] [Domain α] {c : Chain α} : ⨆ (c ∘ Mono.succ) ⊑ ⨆ c :=

def Cont.const [Order α] [Order β] [Domain α] [Domain β] (b : β) : Cont α β := ⟨Mono.const b, fun {c} ↦ by admit /- proof elided -/
  ⟩

instance [Order α] [Order β] [Domain α] [Domain β] : Domain (α × β) where
  bot := ⟨⊥, ⊥⟩
  sup := fun c ↦ ⟨⨆ c.fst, ⨆ c.snd⟩
  is_bot := ⟨Domain.is_bot, Domain.is_bot⟩
  is_bound := fun c n ↦ ⟨Domain.is_bound c.fst n, Domain.is_bound c.snd n⟩
  is_least := fun c _ p ↦ ⟨Domain.is_least c.fst p.left, Domain.is_least c.snd p.right⟩

def Cont.fst [Order α] [Order β] [Domain α] [Domain β] : Cont (α × β) α :=
  ⟨⟨Prod.fst, And.left⟩, Domain.sup_is_mono (fun _ ↦ ⋆)⟩

def Cont.snd [Order α] [Order β] [Domain α] [Domain β] : Cont (α × β) β :=
  ⟨⟨Prod.snd, And.right⟩, Domain.sup_is_mono (fun _ ↦ ⋆)⟩

def Cont.pair [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ]
  (f : Cont γ α) (g : Cont γ β) : Cont γ (α × β) := ⟨
    ⟨fun c ↦ ⟨f c, g c⟩, fun p ↦ ⟨f • p, g • p⟩⟩,
    ⟨f.sub ⬝ Domain.sup_is_mono (fun _ ↦ ⋆), g.sub ⬝ Domain.sup_is_mono (fun _ ↦ ⋆)⟩
  ⟩

def Cont.swap [Order α] [Domain α] [Order β] [Domain β] : Cont (α × β) (β × α) := ⟨
  Mono.swap,
    by admit /- proof elided -/
  ⟩

def Cont.assoc_swap_assoc {α : Type i} {β : Type j}
  [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ] : Cont ((α × β) × γ) ((α × γ) × β) := ⟨
    Mono.assoc_swap_assoc,
    by admit /- proof elided -/
  ⟩

instance [Order α] [Order β] [Domain α] [Domain β] : Order (Cont α β) where
  R := fun x y ↦ x.fn.act ⊑ y.fn.act
  refl := fun _ ↦ ⋆
  trans := fun p q ↦ p ⬝ q
  anti := fun p q ↦ Cont.ext (p ⇄! q)

def Mono.apply [Order α] [Order β] [Domain α] [Domain β] (c : Mono Nat (Cont α β)) (a : α) : Chain β where
  act := fun n ↦ (c n) a
  act' := fun a_b ↦ (c • a_b) _

def Chain.apply [Order α] [Order β] [Domain α] [Domain β] (c : Chain (Cont α β)) (a : α) : Chain β
  := Mono.apply c a

def Chain.apply_monotone_in_a [Order α] [Order β] [Domain α] [Domain β] {x y : α} (c : Chain (Cont α β))
  (x_y : x ⊑ y) : c.apply x ⊑ c.apply y :=

def Mono.sup_cont [Order α] [Order β] [Domain α] [Domain β] (c : Chain (Cont α β)) : Mono α β
  := ⟨
    fun a ↦ ⨆ (c.apply a),
    by admit /- proof elided -/
  ⟩

instance [Order α] [Order β] [Domain α] [Domain β] : Domain (Cont α β) where
  bot := ⟨⟨fun _ ↦ ⊥, fun _ ↦ Domain.is_bot⟩, Domain.is_bot⟩
  sup := fun c ↦ ⟨Mono.sup_cont c, by admit /- proof elided -/
  ⟩
  is_bot := fun _ ↦ Domain.is_bot
  is_bound := by admit /- proof elided -/

def Mono.from_cont [Order α] [Order β] [Domain α] [Domain β] : Mono (Cont α β) (Mono α β) :=
  ⟨Cont.fn, fun p a ↦ p a⟩

def Cont.comp {α : Type i} {β : Type j} {γ : Type k}
  [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ] : Cont (Cont β γ × Cont α β) (Cont α γ)
  := ⟨⟨
      fun h ↦ Cont.comp' h.fst h.snd,
      fun {h₀ h₁} h a ↦ (h₀.fst • h.right a) ⬝ (h.left (h₁.snd a))
    ⟩,
    fun {c} a ↦ by admit /- proof elided -/
  ⟩

def Mono.eval_cont {α : Type i} {β : Type j} [Order α] [Order β] [Domain α] [Domain β]
  : Mono (Cont α β × α) β :=
  ⟨fun x ↦ x.fst x.snd, fun {x y} p ↦ (x.fst • p.right) ⬝ (p.left y.snd)⟩

def Cont.eval {α : Type i} {β : Type j} [Order α] [Order β] [Domain α] [Domain β]
  : Cont (Cont α β × α) β := ⟨
    Mono.eval_cont,
    by admit /- proof elided -/
  ⟩

def Cont.curry {α : Type i} {β : Type j}
  [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ]
  (f : Cont (α × β) γ) : Cont α (Cont β γ) := ⟨
    ⟨
      fun a ↦ ⟨
        ⟨
          fun b ↦ f (a, b),
          fun b' ↦ f • ⟨⋆, b'⟩
        ⟩,
        by admit /- proof elided -/
      ⟩,
      fun a' b ↦ f • ⟨a', ⋆⟩
    ⟩,
    by admit /- proof elided -/
  ⟩

def Mono.uncurry_cont {α : Type i} {β : Type j}
  [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ]
  (f : Cont α (Cont β γ)) : Mono (α × β) γ := ⟨
    fun ⟨a, b⟩ ↦ (f a) b,
    by admit /- proof elided -/
  ⟩

def Cont.uncurry {α : Type i} {β : Type j}
  [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ]
  (f : Cont α (Cont β γ)) : Cont (α × β) γ  := ⟨
    Mono.uncurry_cont f,
    by admit /- proof elided -/
  ⟩

def Cont.iter [Order α] [Domain α] : Nat → Cont α α → Cont α α
| 0 => fun _ ↦ Cont.id
| .succ n => fun f ↦ f ∘ iter n f

def Cont.iterations [Order α] [Domain α] (f : Cont α α) : Chain α := ⟨
    fun n ↦ Cont.iter n f ⊥,
    increasing_implies_monotone (fun n ↦ iter n f ⊥) (by admit /- proof elided -/
    )
  ⟩

def Cont.fix [Order α] [Domain α] (f : Cont α α) := ⨆ f.iterations

def is_prefixed [Order α] [Domain α] (f : Cont α α) (a : α) := f a ⊑ a

def fix_is_prefixed [Order α] [Domain α] (f : Cont α α) : is_prefixed f (⨆ f.iterations) :=

def fix_is_least_prefixed [Order α] [Domain α] (f : Cont α α) (a : α) (h : is_prefixed f a)
  : f.fix ⊑ a :=

def Cont.fix_is_fixed [Order α] [Domain α] (f : Cont α α) : f (f.fix) = f.fix :=

def Cont.fix_mono [Order α] [Domain α] : Mono (Cont α α) α := ⟨
    Cont.fix,
    by admit /- proof elided -/
  ⟩

def Cont.fix' [Order α] [Domain α] : Cont (Cont α α) α := ⟨
    fix_mono,
    by
      intro f
      apply fix_is_least_prefixed
      calc ⨆ f (⨆ (fix_mono ∘ f))
        _ = ⨆ (f.apply (⨆ (fix_mono ∘ f))) := rfl
        _ ⊑ ⨆ (Mono.sup ∘ Mono.comp ∘ Mono.pair (Mono.from_cont ∘ f) (Mono.const (fix_mono ∘ f))) :=

def scott [Order D] [Domain D] {φ : D → Sort u} {f : Cont D D}
  : φ ⊥ → (∀ {c}, (∀ n, φ (c n)) → φ (⨆ c)) → (∀ {d}, φ d → φ (f d)) → φ (f.fix) :=

def scott3 [Order D] [Domain D] {φ : D → D → D → Sort u} {f₀ : Cont D D} {f₁ : Cont D D} {f₂ : Cont D D}
  : φ ⊥ ⊥ ⊥
  → (∀ {c₀ c₁ c₂}, (∀ n, φ (c₀ n) (c₁ n) (c₂ n)) → φ (⨆ c₀) (⨆ c₁) (⨆ c₂))
  → (∀ {d₀ d₁ d₂}, φ d₀ d₁ d₂ → φ (f₀ d₀) (f₁ d₁) (f₂ d₂)) → φ (f₀.fix) (f₁.fix) (f₂.fix) :=

class TrivialDomain (α) [Order α] [Domain α] where
  eventually_const : (c : Chain α) → ∃ N, ∀ {n}, N ≤ n → c n ⊑ c N

def Domain.eventually_const_sup [Order α] [Domain α]
  {c : Chain α} : (∀ {n}, N ≤ n → c n ⊑ c N) → ⨆ c ⊑ c N :=

def Mono.promote_trivial [Order α] [Domain α] [TrivialDomain α] [Order β] [Domain β] [TrivialDomain β]
  (f : Mono α β) : Cont α β := ⟨
    f,
    by admit /- proof elided -/
  ⟩

instance (α β)  [Order α] [Domain α] [TrivialDomain α] [Order β] [Domain β] [TrivialDomain β] : TrivialDomain (α × β) where
  eventually_const := by admit /- proof elided -/

Bool in Init.Prelude

Cont in Mathlib.Control.Monad.Cont

bool in Init.Control.Basic

Nat in Init.Prelude

Trans.trans in Init.Prelude

Nat.succ in Init.Prelude

CoeFun in Init.Coe

CoeFun.coe in Init.Coe

Decidable in Init.Prelude

DecidableEq in Init.Prelude

Eq in Init.Prelude

Trans in Init.Prelude

Con in Mathlib.GroupTheory.Congruence.Defs

inferInstanceAs in Init.Prelude

Nat.le in Init.Prelude

Prod in Init.Prelude

id in Init.Prelude

cond in Init.Prelude

Append in Init.Prelude

Coe in Init.Coe

And in Init.Prelude

Prod.fst in Init.Prelude

Prod.snd in Init.Prelude

Nat.zero in Init.Prelude
</all_available_defs>

<all_available_lemmas>
@[ext] theorem Mono.ext [Order α] [Order β] {f g : Mono α β} (p : f.act = g.act) : f = g

theorem Eval.determinism : t ⇓ v₀ → t ⇓ v₁ → v₀ = v₁

theorem loop_diverges_at_bool {v : .nil ⊢ .bool} : loop ⇓ v → False

theorem por_test_den_unequal : ⟦por_test false⟧ ≠ ⟦por_test true⟧

theorem full_abstraction_fails : ¬FullAbstraction

theorem Tm.from_bool_den_eq : ∀ {n}, (⟦.from_bool n⟧) ρ = (.some n)

theorem Tm.from_nat_den_eq : (⟦.from_nat n⟧) ρ = (.some n)

theorem Tm.ren_den_eq (e : Γ ⊢ τ) : ∀ {Δ}, (r : Ren Γ Δ) → ⟦e.ren r⟧ = (⟦e⟧) ∘' (⟦r⟧)

theorem Ren.weak_den_eq : (⟦Ren.weak⟧) (Ev.from (ρ, d)) = ρ

theorem Tm.sub_den_eq (e : Γ ⊢ τ) : ∀ {Δ}, (σ : Sb Γ Δ) → ⟦e.sub σ⟧ = (⟦e⟧) ∘' (⟦σ⟧)

theorem Sb.inst_den_eq : (⟦Sb.inst a⟧) ρ = (Ev.from (ρ, (⟦a⟧) ρ))

theorem Ren.keep_id {Γ : Cx} (τ : Ty) : (@ Ren.id Γ) ∷ᵣ τ = Ren.id

theorem Ren.keep_comp {r₀₁ : Ren Γ₀ Γ₁} {r₁₂ : Ren Γ₁ Γ₂}
  : (r₀₁ ⬝ r₁₂) ∷ᵣ τ = (r₀₁ ∷ᵣ τ) ⬝ (r₁₂ ∷ᵣ τ)

theorem Ren.ren_comp_eq {t : Γ₀ ⊢ τ}
  : ∀ {Γ₁ Γ₂} {σ₀₁ : Ren Γ₀ Γ₁} {σ₁₂ : Ren Γ₁ Γ₂}, t.ren (σ₀₁ ⬝ σ₁₂) = (t.ren σ₀₁).ren σ₁₂

theorem Ren.ren_weak_exch {r : Ren Γ₀ Γ₁} : r ⬝ Ren.weak = Ren.weak ⬝ (r ∷ᵣ υ)

theorem Sb.keeps_keep_assoc (σ : Sb Γ₀ Γ₁) {Δ : Cx} (τ : Ty) : (σ ++ₛ Δ) ∷ₛ τ = σ ++ₛ (Δ ∷ τ)

private theorem cx_eq_cons {Γ Δ : Cx} (p : Γ = Δ) (υ : Ty) : Γ ∷ υ = Δ ∷ υ

private theorem cx_comp_eq_cx {Γ Δ : Cx} (h : Γ ∷ τ = Δ ∷ υ) : Γ = Δ

private theorem cx_comp_eq_ty {Γ Δ : Cx} (h : Γ ∷ τ = Δ ∷ υ) : τ = υ

private theorem Tm.ren_cast_rfl (t : Γ ⊢ τ) : t.ren (Ren.cast rfl) = t

private theorem Var.ren_cast_z (h : Γ ∷ υ = Δ ∷ υ) : (Var.z).ren (Ren.cast h) = Var.z

private theorem Var.ren_cast_s (h : Γ = Δ)
  : (Var.s τ x).ren (Ren.cast (cx_eq_cons h υ)) = Var.s τ (x.ren (Ren.cast h))

private theorem Ren.cast_keep_eq
  : (Ren.cast h ∷ᵣ υ : Ren (Γ ∷ υ) (Δ ∷ υ)) = Ren.cast (cx_eq_cons h υ)

private theorem sub_weak'_exchange_var {Δ} : ∀ {Γ} {Γ₀ Γ₁ : Cx} {σ : Sb Γ₀ Γ₁} {τ'}
  {h : Γ = Γ₀ ++ Δ} {ν} {x : Γ ∋ ν},
    (((x.ren (Ren.cast h)).ren (Ren.id ++ᵣ Δ)).sub (σ ++ₛ Δ)).ren weak'
  = (((x.ren (Ren.cast h)).ren (Ren.id ++ᵣ Δ)).ren weak').sub ((σ ∷ₛ τ') ++ₛ Δ)

private theorem sub_weak'_exchange_tm {t : Γ ⊢ τ} : ∀ Δ {Γ₀ Γ₁ : Cx}
  {h : Γ = Γ₀ ++ Δ} {σ : Sb Γ₀ Γ₁} {τ'},
    (((t.ren (Ren.cast h)).ren (Ren.id ++ᵣ Δ)).sub (σ ++ₛ Δ)).ren weak'
  = (((t.ren (Ren.cast h)).ren (Ren.id ++ᵣ Δ)).ren weak').sub ((σ ∷ₛ τ') ++ₛ Δ)

theorem Flat.invert {x : Flat α} (p : x ≠ .none) : ∃ k, x = .some k

theorem soundness {t v : Cx.nil ⊢ τ} : t ⇓ v → ⟦t⟧ = ⟦v⟧

theorem congrArg2
  {α₀ : Sort u₀} {α₁ : Sort u₁} {β : Sort v} {a₀ a₀' : α₀} {a₁ a₁' : α₁}
  (f : α₀ → α₁ → β) (h₀ : Eq a₀ a₀') (h₁ : Eq a₁ a₁') : Eq (f a₀ a₁) (f a₀' a₁')

theorem congrArg3
  {α₀ : Sort u₀} {α₁ : Sort u₁} {α₂ : Sort u₂} {β : Sort v} {a₀ a₀' : α₀} {a₁ a₁' : α₁} {a₂ a₂' : α₂}
  (f : α₀ → α₁ → α₂ → β) (h₀ : Eq a₀ a₀') (h₁ : Eq a₁ a₁') (h₂ : Eq a₂ a₂') : Eq (f a₀ a₁ a₂) (f a₀' a₁' a₂')

private theorem Domain.sup_is_mono [Order α] [Domain α] {c d : Chain α} (p : c ⊑ d) : ⨆ c ⊑ ⨆ d

@[ext] theorem Cont.ext [Order α] [Order β] [Domain α] [Domain β]
  {f g : Cont α β} (p : f.fn.act = g.fn.act) : f = g

theorem Cont.pair_after [Order α] [Domain α] [Order β] [Domain β] [Order γ] [Domain γ] [Order δ] [Domain δ]
  (f : Cont γ α) (g : Cont γ β) (h : Cont δ γ) : (f ∘' h).pair (g ∘' h) = (f.pair g) ∘' h

private theorem diagonalize_eval [Order α] [Order β] [Domain β] (c : Chain (Mono α β)) (d : Chain α)
  : ⨆ (Mono.sup ∘ Mono.comp ∘ (Mono.pair c (Mono.const d)))
  ⊑ ⨆ (Mono.eval ∘ Mono.pair c d)
</all_available_lemmas>

<local_ctx>
import «PCF».Domain

inductive Flat (α : Type) : Type where
  | none : Flat α
  | some : α → Flat α

open Classical

noncomputable def flat_sup (c : Chain (Flat α)) : Flat α :=
  if p : ∃ a n, c.act n = .some a then .some p.choose else .none
</local_ctx>

<target_theorem>
theorem Flat.sup_some {c : Chain _} {a : α} : (∃ k, c.act k = .some a) ↔ (flat_sup c = .some a) :=
</target_theorem>

