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 Γ τ

def Var.tm (x : Γ ∋ τ) : Γ ⊢ τ := Tm.var τ 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

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

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

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

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

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

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)⟩

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

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

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

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

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

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 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⟩

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 Mono.sup_cont [Order α] [Order β] [Domain α] [Domain β] (c : Chain (Cont α β)) : Mono α β
  := ⟨
    fun a ↦ ⨆ (c.apply a),
    by admit /- proof elided -/
  ⟩

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

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

def Sb.push (σ : Sb Γ Δ) {υ : Ty} (a : Δ ⊢ υ) : Sb (Γ ∷ υ) Δ :=
  fun _ x => match x with
  | .z     => a
  | .s _ 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 Sb.Approx.id : Ev.nil ◃ Sb.id :=

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

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

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

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

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

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

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

id in Init.Prelude

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

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

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 Tm.from_bool : Bool → Γ ⊢ .bool
  | .true => .true
  | .false => .false

cond in Init.Prelude

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

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

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

And in Init.Prelude

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

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

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 por_test_left_true : (⟦(Var.z.tm.app .true).app loop⟧) (Ev.nil.push por_curry) = Flat.some true :=

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

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

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

Trans in Init.Prelude

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

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

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

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

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

bool in Init.Control.Basic

Append in Init.Prelude

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

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

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

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

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

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]

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

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)

Nat in Init.Prelude

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

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

Coe in Init.Coe

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 Sb Γ Δ := ∀ τ, Γ ∋ τ → Δ ⊢ τ

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

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

Nat.le in Init.Prelude

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

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

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

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)

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)

Trans.trans in Init.Prelude

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

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

Nat.zero in Init.Prelude

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₂) :=

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 -/
    ))

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

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

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

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

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)

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 -/

Bool in Init.Prelude

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

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

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

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

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 Sb.keeps (σ : Sb Γ₀ Γ₁) : (Δ : Cx) → Sb (Γ₀ ++ Δ) (Γ₁ ++ Δ)
  | .nil      => σ
  | .cons Δ τ => (σ.keeps Δ).keep τ

CoeFun in Init.Coe

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

inferInstanceAs in Init.Prelude

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

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

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

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

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

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

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

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

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

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

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 -/
  ⟩

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 loop_den_eq : (⟦(loop : _ ⊢ τ)⟧) ρ = ⊥ :=

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₂) :=

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

CoeFun.coe in Init.Coe

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 compositionality {t₀ t₁ : Δ ⊢ ν} (p : ⟦t₀⟧ = ⟦t₁⟧) : ∀ (C : Con Δ ν Γ τ), ⟦C t₀⟧ = ⟦C t₁⟧ :=

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

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

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

instance : Append Cx where
  append := Cx.append

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

Prod.snd in Init.Prelude

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

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

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⟩

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

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

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

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

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

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

Prod in Init.Prelude

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

Nat.succ in Init.Prelude

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

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

Eq in Init.Prelude

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 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 Tm.sub_id_eq {t : Γ ⊢ τ} : t.sub (Sb.id) = t :=

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

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

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 :=

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

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

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) :=

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

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

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

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

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

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

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

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

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

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

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₂)

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

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

Decidable in Init.Prelude

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

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

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

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

Cont in Mathlib.Control.Monad.Cont

Con in Mathlib.GroupTheory.Congruence.Defs

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

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

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

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 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 Δ) ∷ τ

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

DecidableEq in Init.Prelude

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

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

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

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

Prod.fst 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 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₁')

@[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

theorem Flat.chain_some {c : Chain (Flat _)} {a b : α}
  (p : ∃ k, c.act k = .some a) (q : ∃ k, c.act k = .some b) : a = b

theorem Cont.flat_id : Cont.flat (Function.id : α → α) = Cont.id

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

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

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

theorem Nat.partial_pred_converse {a : Flat Nat} (p : partial_pred a ≠ .none) : (a ≠ .none)

theorem Cont.pred_flat_succ_eq_id : Cont.pred ∘' Cont.flat (Nat.succ) = Cont.id

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

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

theorem Cont.flat_comp (f : β → γ) (g : α → β) : Cont.flat (f ∘ g) = Cont.flat f ∘' Cont.flat g

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

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

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

theorem Flat.some_leq {a : α} : (Flat.some a) ⊑ b → Flat.some a = b

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

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 ((σ ∷ₛ τ') ++ₛ Δ)

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

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

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

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

theorem full_abstraction_fails : ¬FullAbstraction

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)

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

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

theorem Flat.under_eq {x : Flat α} : x ⊑ .some a → x ⊑ .some b → a ≠ b → x = .none

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

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

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_lift_converse {f : α → β} {a : Flat α} (p : lift_flat f a ≠ .none) : (a ≠ .none)

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

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₂')

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

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

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

theorem Flat.leq_none {a : Flat α} : a ⊑ .none → a = .none
</all_available_lemmas>

<local_ctx>
import «PCF».Flat

import «PCF».Context

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

notation:max "⟦" τ " ty⟧" => Ty.den τ

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

notation:max "⟦" Γ " cx⟧" => Ev Γ

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

notation:100 "⟦" t "⟧" => Tm.den t

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⟩

notation:100 "⟦" r "⟧" => Ren.den r

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

notation:100 "⟦" σ "⟧" => Sb.den σ

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

notation:100 "⟦" C " con⟧" => Con.den C
</local_ctx>

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

