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>
structure Context where
  ref         : Syntax
   
  m           : Syntax
   
  returnType  : Syntax
  mutableVars : VarSet := {}
  insideFor   : Bool := false

private def _root_.Lean.EnvExtension.get [Inhabited σ] (ext : EnvExtension σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimpleScopedEnvExtension.get [Inhabited σ] (ext : SimpleScopedEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimplePersistentEnvExtension.get [Inhabited σ] (ext : SimplePersistentEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

def findNat (p : Nat -> Prop) [DecidablePred p] : Option Nat :=
  let rec aux i :=
    if p i then
      some i
    else
      aux (i + 1)
  partial_fixpoint
  aux 0

def find [Encodable α] (p : α -> Prop) [DecidablePred p] : Option α :=
  findNat (fun x => (Encodable.decode x).any (p ·)) |>.bind Encodable.decode

class Findable {α : Type u} (p : α -> Prop) where
  find : Unit -> Option α
  find_none : (find ()).isNone -> ∀ x, ¬ p x
  find_some_p : find () = some x -> p x

def findNat (p : Nat -> Prop) [DecidablePred p] : Option Nat :=
  let rec aux i :=
    if p i then
      some i
    else
      aux (i + 1)
  partial_fixpoint
  aux 0

def find [Encodable α] (p : α -> Prop) [DecidablePred p] : Option α :=
  findNat (fun x => (Encodable.decode x).any (p ·)) |>.bind Encodable.decode

class Findable {α : Type u} (p : α -> Prop) where
  find : Unit -> Option α
  find_none : (find ()).isNone -> ∀ x, ¬ p x
  find_some_p : find () = some x -> p x

def wp (c : m α) (post : α -> l) : l := liftM (n := Cont l) c post

def triple (pre : l) (c : m α) (post : α -> l) : Prop :=
  pre ≤ wp c post

def spec (pre : l) (post : α -> l) : Cont l α :=
  fun p => pre ⊓ ⌜post ≤ p⌝

@[specialize, inline]
def Loop.forIn.loop {m : Type u -> Type v} [Monad m] [∀ α, CCPO (m α)] [MonoBind m] (f : Unit → β → m (ForInStep β)) (b : β) : m β := do
    match ← f () b with
      | ForInStep.done b  => pure b
      | ForInStep.yield b => loop f b
  partial_fixpoint

class CCPOBotLawful (m : Type u -> Type v) [∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] where
  prop {α} : CCPOBot.compBot (m := m) (α := α) = Lean.Order.bot

private def _root_.Lean.SimpleScopedEnvExtension.get [Inhabited σ] (ext : SimpleScopedEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimplePersistentEnvExtension.get [Inhabited σ] (ext : SimplePersistentEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimpleScopedEnvExtension.get [Inhabited σ] (ext : SimpleScopedEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimplePersistentEnvExtension.get [Inhabited σ] (ext : SimplePersistentEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

structure WPGen (x : m α) where
  get : Cont l α
  
  prop : ∀ post, get post <= wp x post

def WPGen.bind {x : m α} {f : α -> m β} (wpg : WPGen x) (wpgf : ∀ a, WPGen (f a)) :
  WPGen (x >>= f) where
  get := fun post => wpg.get (fun a => (wpgf a).get post)
  prop := by admit /- proof elided -/

def WPGen.assert {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l] (h : l) : WPGen (assertGadget (m := m) h) where
  get := fun post => h ⊓ (h ⇨ post .unit)
  prop := by admit /- proof elided -/

def WPGen.if {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
  {hd : Decidable h} {x y : m α}
  (wpgx : h → WPGen x) (wpgy : ¬h → WPGen y)
  : WPGen (if h then x else y) where
  get := fun post =>
    (⨅ hc : WithName h (Lean.Name.anonymous.mkStr "if_pos"), (wpgx hc).get post) ⊓
    (⨅ hc : WithName (¬h) (Lean.Name.anonymous.mkStr "if_neg"), (wpgy hc).get post)
  prop := by admit /- proof elided -/

noncomputable def LE.pure {l : Type u} [inst: LE l] [OrderTop l] [OrderBot l] : Prop -> l := fun p =>
  if p then ⊤ else ⊥

class MAlg [Monad m] (l : outParam (Type v)) where
  μ : m l -> l
  pure : ∀ l, μ (pure l) = l
  bind : ∀ {α : Type v} (x : m α) (f g : α -> m l),
    μ ∘ f = μ ∘ g ->
    μ (x >>= f) = μ (x >>= g)

abbrev MAlg.lift {m : Type u -> Type v} {l : Type u} [Monad m] [MAlg m l] :
  {α : Type u} -> m α -> Cont l α := fun x f => μ $ f <$> x

class MAlgOrdered (l : outParam (Type v)) [Monad m] [CompleteLattice l] where
  μ : m l -> l
  μ_ord_pure : ∀ l, μ (pure l) = l
  μ_ord_bind {α : Type v} :
    ∀ (f g : α -> m l), μ ∘ f ≤ μ ∘ g ->
      ∀ x : m α, μ (x >>= f) ≤ μ (x >>= g)

private def _root_.Lean.EnvExtension.get [Inhabited σ] (ext : EnvExtension σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimpleScopedEnvExtension.get [Inhabited σ] (ext : SimpleScopedEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

private def _root_.Lean.SimplePersistentEnvExtension.get [Inhabited σ] (ext : SimplePersistentEnvExtension α σ)
  [Monad m] [MonadEnv m] : m σ := do
  return ext.getState (<- getEnv)

scoped instance TotalHandler {ε} : IsHandler (ε := ε) fun _ => False where

Lean.SimpleScopedEnvExtension in Lean.ScopedEnvExtension

Lean.Elab.Term.elabTermEnsuringType in Lean.Elab.Term.TermElabM

Lean.Parser.Term.doHave in Lean.Parser.Do

def mkTerminalAction (action : Syntax) : CodeBlock :=
  { code := .action action }

List.tail in Init.Data.List.Basic

def addFreshJP (ps : Array (Var × Bool)) (body : Code) : StateRefT (Array JPDecl) TermElabM Name := do
  let jp ← mkFreshJP ps body
  modify fun (jps : Array JPDecl) => jps.push jp
  pure jp.name

instance OfMAlgPartialOrdered {m : Type u -> Type v} {l : Type u} [Monad m] [CompleteLattice l] [mprop : MAlgOrdered m l] : MAlg m l where
  μ := MAlgOrdered.μ
  pure := MAlgOrdered.μ_ord_pure
  bind := by admit /- proof elided -/

elab "decreasing" t:term : term => do
  let opts <- getOptions
  let semantics := opts.getString (defVal := "unspecified") `loom.semantics.termination
  if semantics = "unspecified" then
    throwError "First, you need to specify the termination semantics using `set_option loom.semantics.termination <partial/total>`"
  let decr <- `(decreasingGadget $t)
  let decrIsNone := match t with
    | `(none) => true
    | _ => false
  let errorsEnabled := opts.getBool (defVal := true) `loom.linter.errors
  let warningsEnabled := opts.getBool (defVal := true) `loom.linter.warnings
  if semantics = "total" && decrIsNone && errorsEnabled then
    throwError "Decreasing annotations are required in total correctness semantics
To turn off this error, use `set_option loom.linter.errors false`."
  if semantics = "partial" && !decrIsNone && warningsEnabled then
    logWarningAt (<- getRef) "Decreasing annotations are not checked in partial correctness semantics
To turn off this warning, use `set_option loom.linter.warnings false`."
  Term.elabTerm decr none

def Lake.unzip (file : FilePath) (dir : FilePath) : LogIO PUnit := do
  IO.FS.createDirAll dir
  proc (quiet := true) {
    cmd := "unzip"
    args := #["-d", dir.toString, file.toString]
  }

Lean.EnvExtension in Lean.Environment

Lean.Parser.Term.doNested in Lean.Parser.Do

abbrev Cont (t : Type v) (α : Type u) := (α -> t) -> t

partial def doTryToCode (doTry : Syntax) (doElems: List Syntax) : M CodeBlock := do
    let tryCode ← doSeqToCode (getDoSeqElems doTry[1])
    let optFinally := doTry[3]
    let catches ← doTry[2].getArgs.mapM fun catchStx : Syntax => do
      if catchStx.getKind == ``Parser.Term.doCatch then
        let x       := catchStx[1]
        if x.isIdent then
          withRef x <| checkNotShadowingMutable #[x]
        let optType := catchStx[2]
        let c ← doSeqToCode (getDoSeqElems catchStx[4])
        return { x := x, optType := optType, codeBlock := c : Catch }
      else if catchStx.getKind == ``Parser.Term.doCatchMatch then
        let matchAlts := catchStx[1]
        let x ← `(ex)
        let auxDo ← `(do match ex with $matchAlts)
        let c ← doSeqToCode (getDoSeqElems (getDoSeq auxDo))
        return { x := x, codeBlock := c, optType := mkNullNode : Catch }
      else
        throwError "unexpected kind of `catch`"
    let finallyCode? ← if optFinally.isNone then pure none else some <$> doSeqToCode (getDoSeqElems optFinally[0][1])
    if catches.isEmpty && finallyCode?.isNone then
      throwError "invalid `try`, it must have a `catch` or `finally`"
    let ctx ← read
    let ws    := getTryCatchUpdatedVars tryCode catches finallyCode?
    let uvars := varSetToArray ws
    let a     := tryCatchPred tryCode catches finallyCode? hasTerminalAction
    let r     := tryCatchPred tryCode catches finallyCode? hasReturn
    let bc    := tryCatchPred tryCode catches finallyCode? hasBreakContinue
    let toTerm (codeBlock : CodeBlock) : M Syntax := do
      let codeBlock ← liftM $ extendUpdatedVars codeBlock ws
      liftMacroM <| ToTerm.mkNestedTerm codeBlock.code ctx.m ctx.returnType uvars a r bc
    let term ← toTerm tryCode
    let term ← catches.foldlM (init := term) fun term «catch» => do
      let catchTerm ← toTerm «catch».codeBlock
      if catch.optType.isNone then
        annotate doTry (← ``(MonadExcept.tryCatch $term (fun $(«catch».x):ident => $catchTerm)))
      else
        let type := «catch».optType[1]
        annotate doTry (← ``(tryCatchThe $type $term (fun $(«catch».x):ident => $catchTerm)))
    let term ← match finallyCode? with
      | none             => pure term
      | some finallyCode => withRef optFinally do
        unless finallyCode.uvars.isEmpty do
          throwError "`finally` currently does not support reassignments"
        if hasBreakContinueReturn finallyCode.code then
          throwError "`finally` currently does `return`, `break`, nor `continue`"
        let finallyTerm ← liftMacroM <| ToTerm.run finallyCode.code ctx.m ctx.returnType {} ToTerm.Kind.regular
        annotate doTry (← ``(tryFinally $term $finallyTerm))
    let doElemsNew ← liftMacroM <| ToTerm.matchNestedTermResult term uvars a r bc
    doSeqToCode (doElemsNew ++ doElems)

def cvc5Path := buildDir / "cvc5"

def getModIds (stx : Array (TSyntax `leafny_binder)) : MetaM (Array (Nat × Ident)) := do
  let mut ids := #[]
  let mut pos := 0
  for b in stx do
    match b with
    | `(leafny_binder| (mut $id:ident : $_:term)) => do
      ids := ids.push (pos, id)
      pos := pos + 1
    | _ => pos := pos + 1
  return ids

private def _root_.Lean.SimpleScopedEnvExtension.modify
  (ext : SimpleScopedEnvExtension α σ) (s : σ -> σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.modifyEnv (ext.modifyState · s)

BooleanAlgebra in Mathlib.Order.BooleanAlgebra.Defs

Lean.mkDefinitionValEx in Lean.Declaration

Lean.Syntax in Init.Prelude

partial def toTerm (c : Code) : M Syntax := do
  let term ← go c
  if let some ref := c.getRef? then
    annotate ref term
  else
    return term
where
  go (c : Code) : M Syntax := do
    match c with
    | .return ref val     => withRef ref <| returnToTerm val
    | .continue ref       => withRef ref continueToTerm
    | .break ref          => withRef ref breakToTerm
    | .action e           => actionTerminalToTerm e
    | .joinpoint j ps b k => mkJoinPoint j ps (← toTerm b) (← toTerm k)
    | .jmp ref j args     => return mkJmp ref j args
    | .decl _ stx k       => declToTerm stx (← toTerm k)
    | .reassign _ stx k   => reassignToTerm stx (← toTerm k)
    | .seq stx k          => seqToTerm stx (← toTerm k)
    | .ite ref _ o c t e  => withRef ref <| do mkIte o c (← toTerm t) (← toTerm e)
    | .match ref genParam discrs optMotive alts =>
      let mut termAlts := #[]
      for alt in alts do
        let rhs ← toTerm alt.rhs
        let termAlt := mkNode ``Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", mkNullNode #[alt.patterns], mkAtomFrom alt.ref "=>", rhs]
        termAlts := termAlts.push termAlt
      let termMatchAlts := mkNode ``Parser.Term.matchAlts #[mkNullNode termAlts]
      return mkNode ``Parser.Term.«match» #[mkAtomFrom ref "match", genParam, optMotive, discrs, mkAtomFrom ref "with", termMatchAlts]
    | .matchExpr ref «meta» d alts elseBranch => withFreshMacroScope do
      let d' ← `(discr)
      let mut termAlts := #[]
      for alt in alts do
        let rhs ← `(($(← toTerm alt.rhs) : $((← read).m) _))
        let optVar := if let some var := alt.var? then mkNullNode #[var, mkAtomFrom var "@"] else mkNullNode #[]
        let pat := mkNode ``Parser.Term.matchExprPat #[optVar, alt.funName, mkNullNode alt.pvars]
        let termAlt := mkNode ``Parser.Term.matchExprAlt #[mkAtomFrom alt.ref "|", pat, mkAtomFrom alt.ref "=>", rhs]
        termAlts := termAlts.push termAlt
      let elseBranch := mkNode ``Parser.Term.matchExprElseAlt #[mkAtomFrom ref "|", mkHole ref, mkAtomFrom ref "=>", (← toTerm elseBranch)]
      let termMatchExprAlts := mkNode ``Parser.Term.matchExprAlts #[mkNullNode termAlts, elseBranch]
      let body := mkNode ``Parser.Term.matchExpr #[mkAtomFrom ref "match_expr", d', mkAtomFrom ref "with", termMatchExprAlts]
      if «meta» then
        `(Bind.bind (instantiateMVarsIfMVarApp $d) fun discr => $body)
      else
        `(let discr := $d; $body)

ULift in Init.Prelude

IO.Ref in Init.System.IO

MonadReaderOf in Init.Prelude

Lean.Parser.Term.doReturn in Lean.Parser.Do

instance (l : Type u) {m : Type u -> Type v} [Monad m] [MAlg m l] : MonadLiftT m (Cont l) where
  monadLift := MAlg.lift

def generateWPStep : TacticM (Bool × Expr) := withMainContext do
  let goalType <- getMainTarget
  let_expr WPGen _m _mInst _α _l _lInst _mPropInst x := goalType | throwError "{goalType} is not a WPGen"
  if let some app ← matchMatcherApp? x then
    let name := app.matcherName
    if let some res ← Loom.Matcher.constructWPGen name then
      
       
      withMainContext do
        let goal ← getMainGoal
        let tmp ← Loom.Matcher.partiallyInstantiateWPGen #[_α, _m, _mInst, _l] res app
        let goals ← goal.apply tmp
        replaceMainGoal goals
      return (true, x)
  let cs <- findSpec x
  for elem in cs do
    try
      match elem with
      | (spec, .wpgen) =>
        evalTactic $ <- `(tactic| apply $spec)
      | (spec, .triple) =>
        let info ← getConstInfo spec.getId
        let num_args := info.type.getNumHeadForalls
        let refine_part ←
          Array.foldlM
            (fun x li => `(term|$x $li))
            (←`(term| $spec))
            (Array.replicate num_args (←`(term|?_)))
        let refine_tac ← `(tactic|refine $refine_part)
        try
          evalTactic $ <- `(tactic|
          eapply $(mkIdent ``WPGen.spec_triple);
          apply $spec)
          return (true, x)
        catch _ =>
          evalTactic $ <- `(tactic|
          eapply $(mkIdent ``WPGen.spec_triple);
          $refine_tac)
          return (true, x)
      return (true, x)
    catch _ => continue
  let some ⟨rsx, _⟩ := x.getAppFn.const? | return (false, x)
  let rsxCorrect := (rsx.toString ++ "_correct").toName
  let some mainName ← getDeclName? | throwError s!"no lemma name found for goal:{goalType}"
  if mainName ≠ rsxCorrect then
    return (false, x)
  let mainNameIdent := mkIdent mainName
  try
    evalTactic $ <- `(tactic|
        wpgen_generate_size_conditions;
        eapply $(mkIdent ``WPGen.spec_triple);
        apply $mainNameIdent)
    return (true, x)
  catch _ =>
    return (false, x)

abbrev DiscrTreeKey := Array DiscrTree.Key

instance {l σ : Type u} [CompleteLattice l] : LogicLift l (σ -> l) where
  lift_top := by admit /- proof elided -/

elab "#reduce!" e:term : command => do
  liftTermElabM do
    let e ← ultimateReduce <| <- Term.elabTerm e none
    logInfoAt (<- getRef) e

Lean.throwError in Lean.Exception

ForInStep in Init.Core

Lean.Parser.Term.bracketedBinder in Lean.Parser.Term.Basic

def WPGen.default (x : m α) : WPGen x where
  get := wp x
  prop := by admit /- proof elided -/

Lean.Parser.ident in Lean.Parser.Extra

method SpVSpV
  (mut out: Array Int)
  (spv1: SpV Int)
  (spv2: SpV Int) return (u: Unit)
  ensures out.size = 1
  ensures out[0]! = spv_dot spv1 spv2 0 0
  do
    out := Array.replicate 1 0
    let mut pnt1 := 0
    let mut pnt2 := 0
    while pnt1 ≠ spv1.size ∧ pnt2 ≠ spv2.size
    invariant out.size = 1
    invariant pnt1 ≤ spv1.size ∧ pnt2 ≤ spv2.size
    invariant out[0]! + spv_dot spv1 spv2 pnt1 pnt2 = spv_dot spv1 spv2 0 0
    done_with pnt1 = spv1.size ∨ pnt2 = spv2.size
    do
      if (spv1.ind)[pnt1]! = (spv2.ind)[pnt2]! then
        out[0] += (spv1.val)[pnt1]! * (spv2.val)[pnt2]!
        pnt1 := pnt1 + 1
        pnt2 := pnt2 + 1
      else
        if (spv1.ind)[pnt1]! < (spv2.ind)[pnt2]! then
          pnt1 := pnt1 + 1
        else
          pnt2 := pnt2 + 1
    return

private def mkTuple (elems : Array Syntax) : MacroM Syntax := do
  if elems.size = 0 then
    mkUnit
  else if h : elems.size = 1 then
    ``(WithName.mk' $(elems[0]) $(Lean.quoteNameMk elems[0].getId))
  else
    let init <- ``(WithName.mk' $(elems.back!) $(Lean.quoteNameMk elems.back!.getId))
    elems.extract 0 (elems.size - 1) |>.foldrM (init := init) fun elem tuple => do
      let name := Lean.quoteNameMk elem.getId
      ``(MProdWithNames.mk' $elem $tuple $name)

Prod in Init.Prelude

Lean.Elab.Term.exprToSyntax in Lean.Elab.Term.TermElabM

inductive AccFrom (p : Nat -> Prop) : Nat -> Prop
    | now : p i -> AccFrom p i
    | later : ¬ p i -> AccFrom p (i + 1) -> AccFrom p i

Lean.addDecl in Lean.AddDecl

def termBeforeReqEnsDo := withForbidden "require" (withForbidden "ensures" Term.termBeforeDo)

semiOutParam in Init.Prelude

List.sum in Init.Data.List.Basic

Lean.ReducibilityHints in Lean.Declaration

def WPGen.recProd {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
  {pr: Prod α₁ α₂}
  {mkp : α₁ → α₂ → m β}
  (wpgf : ∀ (a: α₁) (b: α₂), WPGen (mkp a b)):
  WPGen (Prod.recOn pr mkp : m β) where
  get := fun post =>
    (⨅ a, ⨅ b, (wpgf a b).get post)
  prop := by admit /- proof elided -/

instance : Monad (NonDetT m) where
  pure := NonDetT.pure
  bind := NonDetT.bind

Encodable.decode in Mathlib.Logic.Encodable.Basic

instance ExtractNonDet.ForIn_list {xs : List α} {init : β} {f : α → β → NonDetT m (ForInStep β)}
  (_ : ∀ a b, ExtractNonDet findable (f a b)) :
  ExtractNonDet findable (forIn xs init f) :=

noncomputable instance : Lean.Order.CCPO (DivM α) := inferInstanceAs (Lean.Order.CCPO (Lean.Order.FlatOrder .div))

Lean.Parser.Term.termReturn in Lean.Parser.Do

instance {l : Type u} [CompleteLattice l] [MAlgOrdered m l] [LawfulMonad m] : MAlgOrdered (NonDetT m) l where
  μ := NonDetT.μ
  μ_ord_pure := by admit /- proof elided -/

prove_correct SimpleOption by
  cases x <;> loom_solve

instance {l : outParam (Type u)} [CompleteLattice l] [MAlgOrdered m l] [LawfulMonad m] : MAlgOrdered (NonDetT m) l where
  μ := NonDetT.μ
  μ_ord_pure := by admit /- proof elided -/

method SubstringSearch (s: Array Char) (p: Char -> Bool) return (res: SubstringResult)

Lake.logError in Lake.Util.Log

Lean.mkArrowN in Lean.CoreM

LawfulMonadLift in Init.Control.Lawful.MonadLift.Basic

let firstMonadArgPos := 1 + matcherInfo.numParams + implicitArgs.size
  pure <| .some {
    lvls := newLvls,
    wpgenExpr := wpgen,
    matcherInfo := matcherInfo,
    monadRetTypePos := 0,
    monadArgPos := 1 + matcherInfo.numParams,
    monadInstPos := 1 + matcherInfo.numParams + 1,
    omaTypePos := 1 + matcherInfo.numParams + 2,
    firstMonadArgPos := firstMonadArgPos,
    
    
  }

def findSpec (prog : Expr) : TacticM (Array (Ident × Loom.SpecType)) := do
  let specs ← specAttr.find? prog
  let grts := specs.qsort (compare · · |>.isGT) |>.map
    fun ⟨specType, specName, _⟩ => (mkIdent specName, specType)
  return grts

StateT.modifyGet in Init.Control.State

ForInStep.yield in Init.Core

def mkUnless (cond : Syntax) (c : CodeBlock) : MacroM CodeBlock := do
  let thenBranch ← mkPureUnitAction
  return { c with code := .ite (← getRef) none mkNullNode cond thenBranch.code c.code }

inductive NonDetT (m : Type u -> Type v) : (α : Type u) -> Type _ where
  | pure {α} (ret : α) : NonDetT m α
  | vis {α} {β} (x : m β) (f : β → NonDetT m α) : NonDetT m α
  | pickCont {α} (τ : Type u) (p : τ -> Prop) (f : τ → NonDetT m α) : NonDetT m α

Lean.Elab.Term.expandOptType in Lean.Elab.BindersUtil

Nat in Init.Prelude

partial def expandLeafnyDoSeqItem (modIds : Array Ident) (stx : doSeqItem) : TermElabM (Array doSeqItem) := do
  match stx with
  
  | `(Term.doSeqItem| $stx ;) => expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| $stx:doElem)
  | `(Term.doSeqItem| return) => expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| return ())
  | `(Term.doSeqItem| return $t) =>
    let ret <-
      if modIds.size = 0 then
      `(term| $t)
     else
       `(term| ($t, $[$modIds:term],*))
    return #[<-`(Term.doSeqItem| return $ret)]
  | `(Term.doSeqItem| pure $t) =>
    let ret <-
      if modIds.size = 0 then
      `(term| $t)
     else
       `(term| ($t, $[$modIds:term],*))
    return #[<-`(Term.doSeqItem| pure $ret)]
  | `(Term.doSeqItem| if $h:ident : $t:term then $thn:doSeq else $els:doSeq) =>
    let thn <- expandLeafnyDoSeq modIds thn
    let els <- expandLeafnyDoSeq modIds els
    let ret ← `(Term.doSeqItem| if $h:ident : $t then $thn* else $els*)
    return #[ret]
  | `(Term.doSeqItem| if $h:ident : $t:term then $thn) =>
    expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| if $h:ident : $t:term then $thn else pure ())
  | `(Term.doSeqItem| if $t:term then $thn:doSeq) =>
    expandLeafnyDoSeqItem modIds $ <- `(Term.doSeqItem| if $t then $thn:doSeq else pure ())
  | `(Term.doSeqItem| match $discrs:matchDiscr,* with $[$alts:matchAlt]*) =>
    let alts' ← alts.mapM fun (alt : TSyntax _) => do
      match alt with
      | `(doMatchAltExpr| | $a,* => $rhs:doSeq) =>
        let rhs' ← expandLeafnyDoSeq modIds rhs
        let alt' ← `(doMatchAltExpr| | $a,* => $rhs'*)
        pure ⟨alt'.raw⟩
      | _ =>
        pure alt
    let ret ← `(Term.doSeqItem| match $discrs:matchDiscr,* with $[$alts':matchAlt]*)
    return #[ret]
  | `(Term.doSeqItem| if $t:term then $thn:doSeq else $els:doSeq) =>
    let thn <- expandLeafnyDoSeq modIds thn
    let els <- expandLeafnyDoSeq modIds els
    let ret ← `(Term.doSeqItem| if $t then $thn* else $els*)
    return #[ret]
  | `(Term.doSeqItem| let $id <- $trm:term) | `(Term.doSeqItem| let $id : $_ <- $trm:term) =>
    let `($t:ident $args:term*) := trm | pure #[stx]
    
    let ctx <- globalMutVarsCtx.get
    let .some ids := ctx[t.getId]? | pure #[stx]
    let mut mods := #[]
    let mut modArgs := #[]
    for (pos, a) in ids do
      let .some arg := args[pos]? | throwErrorAt stx s!"{t} is not fully applied"
      
      let argName := arg.raw.getId
      if argName.isAnonymous then throwErrorAt arg s!"mutable argument {arg} is not a name"
      if argName ∈ modArgs then throwErrorAt arg s!"mutable arguments cannot alias"
      modArgs := modArgs.push argName
      mods := mods.push $ <- withRef arg `(Term.doSeqItem| $(mkIdent argName):ident := $a:ident)
    return #[<-`(Term.doSeqItem| let $id <- $trm:term)] ++ mods
  | `(Term.doSeqItem| $trm:term) =>
    let id := mkIdent <| <- mkFreshUserName `ret
    let `($t:ident $args:term*) := trm | pure #[stx]
    
    let ctx <- globalMutVarsCtx.get
    let .some ids := ctx[t.getId]? | pure #[stx]
    let mut mods := #[]
    let mut modArgs := #[]
    for (pos, a) in ids do
      let .some arg := args[pos]? | throwErrorAt stx s!"{t} is not fully applied"
      
      let argName := arg.raw.getId
      if argName.isAnonymous then throwErrorAt arg s!"mutable argument {arg} is not a name"
      if argName ∈ modArgs then throwErrorAt arg s!"mutable arguments cannot alias"
      modArgs := modArgs.push argName
      mods := mods.push $ <- withRef arg `(Term.doSeqItem| $(mkIdent argName):ident := $a:ident)
    let ret <- withRef trm `(Term.doSeqItem| pure $id)
    return #[<- withRef trm `(Term.doSeqItem| let ⟨$id, _⟩ <- $trm:term)] ++ mods.push ret
  | `(Term.doSeqItem| while_some $id :| $p:term $invs* $done do $doSeq:doSeq) =>
    let doSeq <- expandLeafnyDoSeq modIds doSeq
    return #[<-`(Term.doSeqItem| while_some $id :| $p:term $invs* $done do $doSeq*)]
  | stx => pure #[stx]

private def _root_.Lean.EnvExtension.set (ext : EnvExtension σ) (s : σ)
  [Monad m] [MonadEnv m] : m Unit := do
  Lean.setEnv $ ext.setState (<- getEnv) s

Lean.Meta.getZetaDeltaFVarIds in Lean.Meta.Basic

Lean.Syntax.node in Init.Prelude

Array.foldlM in Init.Data.Array.Basic

private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Syntax → StateT (List Syntax) M Syntax
  | stx@(Syntax.node i k args) =>
    if k == choiceKind then do
      
      let alts ← stx.getArgs.mapM (expandLiftMethodAux inQuot inBinder · |>.run [])
      let (_, lifts) := alts[0]!
      unless alts.all (·.2 == lifts) do
        throwErrorAt stx "cannot lift `(<- ...)` over inconsistent syntax variants, consider lifting out the binding manually"
      modify (· ++ lifts)
      return .node i k (alts.map (·.1))
    else if liftMethodDelimiter k then
      return stx
    
    else if h : args.size >= 2 ∧ (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
      let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]
      let args := args.set! 1 arg1
      return Syntax.node i k args
    else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
      if inBinder then
        throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`"
      let term := args[1]!
      let term ← expandLiftMethodAux inQuot inBinder term
      
      let id ← mkIdentFromRef (.num baseId (← get).length)
      let auxDoElem : Syntax ← `(doElem| let $id:ident ← $term:term)
      modify fun s => s ++ [auxDoElem]
      return id
    else do
      let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
      let inBinder   := inBinder || (!inQuot && liftMethodForbiddenBinder stx)
      let args ← args.mapM (expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder)
      return Syntax.node i k args
  | stx => return stx

Unit.unit in Init.Prelude

Lean.MessageData.ofSyntax in Lean.Message

Lean.Meta.MetaM in Lean.Meta.Basic

private def elabSimpTheorem (config : Meta.ConfigWithKey) (id : Origin) (stx : Syntax)
    (post : Bool) (inv : Bool) : TermElabM ElabSimpArgResult := do
  let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
    let e ← Term.elabTerm stx .none
    Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
    let e ← instantiateMVars e
    if e.hasSyntheticSorry then
      return .none
    let e := e.eta
    if e.hasMVar then
      let r ← abstractMVars e
      return some (r.paramNames, r.expr)
    else
      return some (#[], e)
  if let some (levelParams, proof) := thm? then
    let thms ← mkSimpTheoremFromExpr id levelParams proof (post := post) (inv := inv) (config := config)
    return .addEntries <| thms.map (SimpEntry.thm ·)
  else
    return .none

def Extractable.forIn (xs : List α) (init : β) (f : α -> β -> NonDetT m (ForInStep β))
  (ex: ∀ a b, Extractable (f a b)):
  Extractable (forIn xs init f) :=

partial def doForToCode (doFor : Syntax) (doElems : List Syntax) : M CodeBlock := do
    let doForDecls := doFor[1].getSepArgs
    if h : doForDecls.size > 1 then
       
      
      let doForDecl := doForDecls[1]!
      unless doForDecl[0].isNone do
        throwErrorAt doForDecl[0] "the proof annotation here has not been implemented yet"
      let y  := doForDecl[1]
      let ys := doForDecl[3]
      let doForDecls := doForDecls.eraseIdx 1
      let body := doFor[3]
      withFreshMacroScope do
         
        let toStreamApp ← withRef ys `(@toStream _ _ _ $ys)
        let auxDo ←
          `(do let mut s := $toStreamApp:term
               for $doForDecls:doForDecl,* do
                 match @Stream.next? _ _ _ s with
                 | none => break
                 | some ($y, s') =>
                   s := s'
                   do $body)
        doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
    else withRef doFor do
      let h?        := if doForDecls[0]![0].isNone then none else some doForDecls[0]![0][0]
      let x         := doForDecls[0]![1]
      withRef x <| checkNotShadowingMutable (← getPatternVarsEx x)
      let xs        := doForDecls[0]![3]
      let forElems  := getDoSeqElems doFor[3]
      let forInBodyCodeBlock ← withFor (doSeqToCode forElems)
      let ⟨uvars, forInBody⟩ ← mkForInBody x forInBodyCodeBlock
      let ctx ← read
      
      
      
      let uvars := uvars.map fun v => ctx.mutableVars.getD v.getId v
      let uvarsTuple ← liftMacroM do mkTuple uvars
      let uvarsTuplePat ← liftMacroM do mkTuplePat uvars

instance ExtractNonDet.assume' {p : Prop} [Decidable p] : ExtractNonDet findable (MonadNonDet.assume (m :=  NonDetT m) p) :=

Lean.Parser.Term.letIdDecl in Lean.Parser.Term

partial def Handle.readLineSkip (h : IO.FS.Handle) (skipLine : String := "\n") : IO String := do
  let rec loop := do
    let line ← h.getLine
    if line.isEmpty then
      return line
    if line == skipLine then
      loop
    else
      return line
  loop

instance WeakFindable.of_Findable {α : Type u} (p : α -> Prop) [Findable p] : WeakFindable p where
  find := Findable.find p
  find_some_p := Findable.find_some_p

private def mkPureUnit : MacroM Syntax :=
  ``(pure PUnit.unit)

Multiset in Mathlib.Data.Multiset.Defs

Lean.Meta.withTrackingZetaDeltaSet in Lean.Meta.Basic

method VSpV
  (mut out: Array Int)
  (arr: Array Int)
  (spv: SpV Int) return (u: Unit)
  ensures out.size = 1
  ensures out[0]! = sumUpTo spv arr (spv.size)
  do
    let mut ind := 0
    out := Array.replicate 1 0
    while ind ≠ spv.size
    invariant out.size = 1
    invariant ind ≤ spv.size
    invariant out[0]! = sumUpTo spv arr ind
    done_with ind = spv.size
    do
      out[0] += (spv.val)[ind]! * arr[(spv.ind)[ind]!]!
      ind := ind + 1
    return

Empty in Init.Prelude

StateT.run in Init.Control.State

instance {l : outParam (Type u)} [CompleteLattice l] [MAlgOrdered m l] [LawfulMonad m] : MAlgOrdered (NonDetT m) l where
  μ := NonDetT.μ
  μ_ord_pure := by admit /- proof elided -/

instance ExtractNonDet.if {p : Prop} {dec : Decidable p} {x y : NonDetT m α}
  (_ : ExtractNonDet findable x) (_ : ExtractNonDet findable y) :
  ExtractNonDet findable (if p then x else y) :=

structure SpV (valTyp : Type) where
  ind: Array Nat
  val: Array valTyp
  size: ℕ
  size_eq: ind.size = size ∧ val.size = size
  inc: ∀ (i j: Nat), i < size → j < size →  i < j → ind[i]! < ind[j]!

def annotate [Monad m] [MonadRef m] [MonadQuotation m] (ref : Syntax) (term : Syntax) : m Syntax :=
  withRef term <| `(with_annotate_term $ref $term)

Auto.LamReif.reifFacts in Auto.Translation.LamReif

Lake.Package in Lake.Config.Package

def getDoPatDeclVars (doPatDecl : Syntax) : TermElabM (Array Var) := do
  let pattern := doPatDecl[0]
  getPatternVarsEx pattern

instance : Lean.KVMap.Value SmtSolver where
  toDataValue n := toString n
  ofDataValue?
  | "z3"  => some .z3
  | "cvc5" => some .cvc5
  | _     => none

Lean.MonadQuotation in Init.Prelude

def getLetIdDeclVars (letIdDecl : Syntax) : Array Var :=
  assert! letIdDecl.isOfKind ``Parser.Term.letIdDecl
  
  
  getLetIdVars letIdDecl[0]

Lean.registerSimplePersistentEnvExtension in Lean.EnvExtension

Lean.Parser.Term.funBinder in Lean.Parser.Term

def cvc5.target := s!"{os}-{arch}-static"

instance MAlgLiftTRefl [Monad m] [CompleteLattice l] [LawfulMonad m] [MAlgOrdered m l] :
  MAlgLiftT m l m l where
    μ_lift := by admit /- proof elided -/

instance : MonadLift m (NonDetT m) where
  monadLift x := NonDetT.vis x pure

OrderTop in Mathlib.Order.BoundedOrder.Basic

abbrev Bal := Int

Stream.next? in Init.Data.Stream

abbrev iwp (c : m α) : Cont l α := Cont.inv (wp c)

private def resolveSimpIdTheorem? (simpArgTerm : Term) : TermElabM ResolveSimpIdResult := do
    let resolveExt (n : Name) : TermElabM ResolveSimpIdResult := do
      let ext₁? ← getSimpExtension? n
      let ext₂? ← Simp.getSimprocExtension? n
      if h : ext₁?.isSome || ext₂?.isSome then
        return .ext ext₁? ext₂? h
      else
        return .none
    match simpArgTerm with
    | `($id:ident) =>
      try
        if let some e ← Term.resolveId? simpArgTerm (withInfo := true) then
          if let some simprocDeclName ← isSimproc? e then
            return .simproc simprocDeclName
          else
            return .expr e
        else
          let name := id.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then
            return .simproc name
          else
            resolveExt name
      catch _ =>
        resolveExt id.getId.eraseMacroScopes
    | _ =>
      if let some e ← Term.elabCDotFunctionAlias? simpArgTerm then
        return .expr e
      else
        return .none
where
  isSimproc? (e : Expr) : MetaM (Option Name) := do
    let .const declName _ := e | return none
    unless (← Simp.isSimproc declName) do return none
    return some declName

Auto.runAuto in Auto.Tactic

Lean.Name.anonymous in Init.Prelude

macro "decidable_by_nat_upperbound" "[" tms:term,* "]" : term => do
  let res ← deriveDecidableNatUpperBound tms.getElems.toList
  `(term| by admit /- proof elided -/
  )

def createSolver (name : SmtSolver) (withTimeout : Nat) : MetaM SolverProc := do
  let tlim_sec := withTimeout
  let seed := loom.solver.smt.seed.get $ ← getOptions
  match name with
  | .z3   => createAux s!"{z3Path}" #["-in", "-smt2", s!"-t:{tlim_sec * 1000}", s!"sat.random_seed={seed}", s!"smt.random_seed={seed}"]
  | .cvc5 =>
      let mut args := #["
      let proc ← createAux s!"{cvc5Path}" args
      emitCommand proc (.setLogic "ALL")
      pure proc

abbrev Except.bind' {m : Type u -> Type v} {ε α β} [Monad m] : Except ε α -> (α -> ExceptT ε m β) -> ExceptT ε m β :=
  fun x f => bind (m := ExceptT ε m) (pure (f := m) x) f

inductive SmtResult
   
  | Sat (modelString : Option String)
  | Unsat
  | Unknown (reason : Option String)
  | Failure (reason : Option String)
deriving Inhabited

Lean.Meta.mkFreshExprMVar in Lean.Meta.Basic

Lake.buildFileAfterDep in Lake.Build.Common

Lean.Meta.Simp.Result in Lean.Meta.Tactic.Simp.Types

def Lean.Expr.runUnfold (e : Expr) (defs : List Name) : TermElabM Expr := do
  let mut eu := e
  for name in defs do eu := (<- unfold eu name).expr
  return eu

Pi.hasLe in Mathlib.Order.Basic

instance : Inhabited LoomSemanticsTermination := ⟨.unspecified⟩

Lean.Loop in Init.While

def decodeStrLeanList (encoded_str: List Encoding) : List Char :=
  match encoded_str with
  | List.nil => List.nil
  | List.cons hd tl => (List.replicate hd.cnt hd.c) ++ (decodeStrLeanList tl)

instance [Monad m] [∀ α, Lean.Order.CCPO (m α)] [Lean.Order.MonoBind m] : Lean.Order.MonoBind (StateT ε m) where
  bind_mono_left h₁₂ _ := by admit /- proof elided -/

def anyGoalsWithTag (tactic : MVarId → TacticM (Option (Name × α))) : TacticM (Array α) := do
  let mvarIds ← getGoals
  let mut res : Array α := #[]
  let mut mvarIdsNew : Array MVarId := #[]
  for mvarId in mvarIds do
    unless (← mvarId.isAssigned) do
      setGoals [mvarId]
      try
        let r ← tactic mvarId
        let goals <- getUnsolvedGoals
        if let some ⟨n, r⟩ := r then
          for goal in goals do
            goal.setTag n
          res := res.push r
          mvarIdsNew := mvarIdsNew ++ goals
      catch _ =>
        mvarIdsNew := mvarIdsNew.push mvarId
  setGoals mvarIdsNew.toList
  pure res

Finset.range in Mathlib.Data.Finset.Range

Lean.mkNode in Init.Prelude

partial def doMatchToCode (doMatch : Syntax) (doElems: List Syntax) : M CodeBlock := do
    let ref       := doMatch
    let genParam  := doMatch[1]
    let optMotive := doMatch[2]
    let discrs    := doMatch[3]
    let matchAlts := doMatch[5][0].getArgs 
    let matchAlts ← matchAlts.foldlM (init := #[]) fun result matchAlt => return result ++ (← liftMacroM <| expandMatchAlt matchAlt)
    let alts ←  matchAlts.mapM fun matchAlt => do
      let patterns := matchAlt[1][0]
      let vars ← getPatternsVarsEx patterns.getSepArgs
      withRef patterns <| checkNotShadowingMutable vars
      let rhs  := matchAlt[3]
      let rhs ← doSeqToCode (getDoSeqElems rhs)
      pure { ref := matchAlt, vars := vars, patterns := patterns, rhs := rhs : Alt CodeBlock }
    let matchCode ← mkMatch ref genParam discrs optMotive alts
    concatWith matchCode doElems

def getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Var) := do
  
  let pattern := letPatDecl[0]
  getPatternVarsEx pattern

class MAlgLift
  (m : semiOutParam (Type u -> Type v)) (l : semiOutParam (Type u)) [Monad m] [CompleteLattice l] [MAlgOrdered m l]
  (n : (Type u -> Type w)) (k : outParam (Type u)) [Monad n] [CompleteLattice k] [MAlgOrdered n k]
  [MonadLiftT m n]
  where
    [cl : LogicLift l k]
    μ_lift (x : m α) : MAlg.lift (liftM (n := n) x) f = liftM (n := Cont k) (MAlg.lift x) f

observing in Init.Control.Except

MonadReaderOf.read in Init.Prelude

def getIds (stx : Array (TSyntax `leafny_binder)) : MetaM (Array Ident) := do
  let mut ids := #[]
  for b in stx do
    match b with
    | `(leafny_binder| (mut $id:ident : $_:term)) => do
      let idOld := mkIdent <| id.getId.appendAfter "Old"
      ids := ids.push idOld
    | `(leafny_binder| ($id:ident : $_:term)) => do
      ids := ids.push id
    | _ => throwError "unexpected syntax in leafny binder: {b}"
  return ids

macro "assert" t:term : term => `(assertGadget $t)

def getModIds (stx : Array (TSyntax `leafny_binder)) : MetaM (Array (Nat × Ident)) := do
  let mut ids := #[]
  let mut pos := 0
  for b in stx do
    match b with
    | `(leafny_binder| (mut $id:ident : $_:term)) => do
      ids := ids.push (pos, id)
      pos := pos + 1
    | _ => pos := pos + 1
  return ids

Lean.indentD in Lean.Message

Lean.Expr.const in Lean.Expr

def WPGen.spec_triple (x : m α) (trp : triple pre x post) : WPGen x where
  get := spec pre post
  prop := by admit /- proof elided -/

structure CodeBlock where
  code  : Code
  uvars : VarSet := {}

instance : Ord Loom.Spec where
  compare a b := if a.prio < b.prio then .lt else if a.prio > b.prio then .gt else .eq

CompleteBooleanAlgebra in Mathlib.Order.CompleteBooleanAlgebra

System.Platform.isWindows in Init.System.Platform

Lean.ConstantInfo.type in Lean.Declaration

Lake.LogIO in Lake.Util.Log

def SpecAttr.getState (s : SpecAttr) : MetaM (DiscrTree Loom.Spec) := do
  return s.ext.getState (← getEnv)

instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l] [inst: MAlgOrdered m l] :
  MAlgLift m l (StateT σ m) (σ -> l) where
    μ_lift := by admit /- proof elided -/

Lean.Meta.Simp.isSimproc in Lean.Meta.Tactic.Simp.Simproc

Lean.quoteNameMk in Init.Meta.Defs

prove_correct SubstringSearch by
  loom_solve

def simpleAddThm (n : Name) (tp : Expr) (pf : Expr)
  (attr : Array Attribute := #[]) : TermElabM Unit := do
  addDecl <|
    Declaration.thmDecl <|
      mkTheoremValEx n [] tp pf []
  applyAttributes n attr

def hasExitPoint (c : Code) : Bool :=
  hasExitPointPred c fun _ => true

instance ExtractNonDet.pure' : ExtractNonDet findable (Pure.pure (f := NonDetT m) x) :=

Lean.Expr.getForallBody in Lean.Expr

kind in Auto.Parser.TPTP

Lean.Parser.Term.matchAlt in Lean.Parser.Term

Auto.lamFOL2SMT in Auto.Translation.LamFOL2SMT

Array.flatten in Init.Data.Array.Basic

Lean.MessageData.joinSep in Lean.Message

Lean.Elab.Term.TermElab in Lean.Elab.Term.TermElabM

List in Init.Prelude

def isDoExpr? (doElem : Syntax) : Option Syntax :=
  if doElem.getKind == ``Parser.Term.doExpr then
    some doElem[0]
  else
    none

Lean.MonadQuotation.addMacroScope in Init.Prelude

Lean.collectLevelParams in Lean.Util.CollectLevelParams

def elabDefiningDecidableInstancesForVelvetSpec (nameRaw : Ident)
    (pre? : Bool) (tac : Option (TSyntax `Lean.Parser.Tactic.tacticSeq)) : CommandElabM Unit := do
  let (ctx, name) ← obtainVelvetTestingCtx nameRaw
  let bindersIdents := ctx.binderIdents
  let (target, suffix, binders) :=
    if pre?
    then (ctx.pre, "PreDecidable", bindersIdents)
    else (ctx.post, "PostDecidable", bindersIdents ++ ctx.modBinders |>.push ⟨mkExplicitBinder ctx.retId ctx.retType⟩)
  let decidableInstName := name.appendAfter suffix
  
  let tac := tac.getD (← `(Lean.Parser.Tactic.tacticSeq| skip ))
  let proof := (← `(Lean.Parser.Tactic.tacticSeq|
    repeat' refine @instDecidableAnd _ _ ?_ ?_
    all_goals (try infer_instance)
    ($tac) ))
  let decidableInstDefCmd ← `(command|
    def $(mkIdent decidableInstName) $binders* :
      $(mkIdent ``Decidable) ($target) := by admit /- proof elided -/
      )
  elabCommand decidableInstDefCmd

def mkUVarTuple : M Syntax := do
  let ctx ← read
  mkTuple ctx.uvars

while i < input.size
    
    invariant ∀ pos len,
      (len > 0 ∧
       pos + len ≤ i ∧
       (∀ j, j < len → isDigit input[pos + j]!) ∧
       (pos = 0 ∨ ¬isDigit input[pos - 1]!) ∧
       (pos + len = i ∨ (pos + len < i ∧ ¬isDigit input[pos + len]!))) →
      len ≤ bestLen
  do
    let c := input[i]!

List.replicate in Init.Data.List.Basic

Lean.getConstInfo in Lean.MonadEnv

Ord in Init.Data.Ord.Basic
</all_available_defs>

<all_available_lemmas>
lemma meet_himp (x x' y z : l) :
  x = x' ->
  (x ⇨ y) ⊓ (x' ⇨ z) = x ⇨ (y ⊓ z)

lemma NonDetT.wp_mono  {l : Type u} [CompleteLattice l] [MAlgOrdered m l] [LawfulMonad m] {α : Type u} (x : NonDetT m α) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  NonDetT.wp x f <= NonDetT.wp x g

@[aesop safe]
lemma emp_sum (x: Bal) (h: 0 ≤ x) : ∃ h: List Nat, h.sum ≤ x

omit [LawfulMonad m] in
lemma WPGen.intro (x : m α) (wpg : WPGen x) :
  pre <= wpg.get post ->
  -- pre <= wpg.sideCond ->
  triple pre x post

theorem triple_forIn_deacreasing {β} {measure : β -> ℕ}
  {init : β} {f : β → m (ForInStep β)}
  (inv : β → l)
  (hstep : ∀ b,
    measure b <= measure init ->
    triple
      (inv b)
      (f b)
      (fun | .yield b' => inv b' ⊓ ⌜measure b' < measure b⌝ | .done b' => ⌜ measure b' = 0 ⌝ ⊓ inv b')) :
  triple (inv init) (forIn [0:measure init] init (fun _ => f)) (fun b => inv b ⊓ ⌜measure b = 0⌝)

@[simp]
lemma trueE (l : Type v) [inst: LE l] [OrderTop l] [OrderBot l] : ⌜True⌝ = (⊤ : l)

@[simp]
lemma falseE (l : Type v) [inst: LE l] [OrderTop l] [OrderBot l] : ⌜False⌝ = (⊥ : l)

lemma LE.pure_imp {l : Type u} [inst: LE l] [OrderTop l] [OrderBot l]
  (p₁ p₂ : Prop) : (p₁ -> p₂) -> ⌜p₁⌝ <= (⌜p₂⌝ : l)

@[simp]
lemma LE.pure_intro {l : Type u} [inst: LE l] [OrderTop l] [OrderBot l]
  (p : Prop) (h : l) : (⌜p⌝ <= h) = (p -> ⊤ <= h)

@[simp]
lemma pure_intro_l {l : Type u} [CompleteLattice l] (x y : l) :
  (x ⊓ ⌜ p ⌝ <= y) = (p -> x <= y)

@[simp]
lemma pure_intro_r {l : Type u} [CompleteLattice l] (x y : l) :
  (⌜ p ⌝ ⊓ x <= y) = (p -> x <= y)

lemma MAlgOrdered.bind {α : Type u} {m} {l : Type u} [Monad m] [CompleteLattice l] [MAlgOrdered m l] :
    ∀ (x : m α) (f g : α -> m l), μ ∘ f = μ ∘ g ->
     μ (x >>= f) = μ (x >>= g)

lemma Cont.monotone_lift {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l] :
  ∀ {α : Type u} (x : m α), MAlg.lift x |>.monotone

@[simp]
lemma MAlg.μ_eq {m l} [Monad m] [CompleteLattice l] [MAlgOrdered m l] : MAlg.μ (m := m) = MAlgOrdered.μ (m := m)

lemma MAlg.monadLift_bind {α β} {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteLattice l] [MAlgOrdered m l]
  (x : m α) (f g : α -> Cont l β) :
    f <= g ->
    (lift x >>= f) ≤ (lift x >>= g)

@[simp]
lemma lift_cont_eq {l σ : Type u} [CompleteLattice l] [CompleteLattice σ] (c : Cont l α) :
  liftM (m := Cont l) (n := Cont (σ -> l)) c = fun post s => c (post · s)

@[loomLogicSimp]
lemma leE (l : Type u) [PartialOrder l] (a b : α -> l) : a ≤ b ↔ ∀ x, a x ≤ b x

@[loomLogicSimp]
lemma lePropE (a b : Prop) : (a ≤ b) = (a → b)

@[loomLogicSimp]
lemma pureE (l : Type u) [CompleteLattice l] (a : Prop) : (⌜a⌝ : α -> l) = fun _ => ⌜a⌝

@[loomLogicSimp]
lemma purePropE  : (⌜a⌝ : Prop) = a

@[loomLogicSimp]
lemma infPropE (a b : Prop) : (a ⊓ b) = (a ∧ b)

@[loomLogicSimp]
lemma infE (l : Type u) [CompleteLattice l] (a b : α -> l) : (a ⊓ b) = fun x => a x ⊓ b x

@[loomLogicSimp]
lemma supE (l : Type u) [CompleteLattice l] (a b : α -> l) : (a ⊔ b) = fun x => a x ⊔ b x

@[loomLogicSimp]
lemma supPropE (a b : Prop) : (a ⊔ b) = (a ∨ b)

@[loomLogicSimp]
lemma iInfE (l : Type u) [CompleteLattice l] (a : ι -> α -> Prop) : (⨅ i, a i) = fun x => ⨅ i, a i x

@[loomLogicSimp]
lemma iSupE (l : Type u) [CompleteLattice l] (a : ι -> α -> Prop) : (⨆ i, a i) = fun x => ⨆ i, a i x

@[loomLogicSimp]
lemma himpE  (l : Type u) [CompleteBooleanAlgebra l] (a b : α -> l) :
  (a ⇨ b) = fun x => a x ⇨ b x

@[loomLogicSimp]
lemma himpPureE (a b : Prop) :
  (a ⇨ b) = (a -> b)

@[loomLogicSimp]
lemma topE (l : Type u) [CompleteLattice l] : (⊤ : α -> l) = fun _ => ⊤

@[loomLogicSimp]
lemma topPureE : (⊤ : Prop) = True

@[aesop safe]
theorem List.sum_lt (x: Bal) : x < y -> x < ([Int.toNat y]).sum

@[aesop safe]
theorem balance_lt (x: Bal) : x < x + 1

lemma Except.bind'_bind {m : Type u -> Type v} {ε α β} [Monad m] [LawfulMonad m] (i : m (Except ε α)) (f : α -> ExceptT ε m β) :
  (i >>= fun a => Except.bind' a f) = bind (m := ExceptT ε m) i f

lemma MAlg.lift_ExceptT ε (hd : ε -> Prop) [IsHandler hd] [CompleteLattice l] [inst: MAlgOrdered m l]
   (c : ExceptT ε m α) post :
  MAlg.lift c post = MAlg.lift (m := m) c (fun | .ok x => post x | .error e => ⌜hd e⌝)

lemma lift_map {α : Type u} {β : Type u} (f : α -> β) (x : m α)
  [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] [MonadLiftT m n] [LawfulMonadLiftT m n] :
  liftM (f <$> x) = f <$> liftM (n := n) x

@[aesop unsafe]
theorem tail_length : ∀ q : List Nat, q.nonEmpty → q.tail.length < q.length

@[aesop norm]
theorem tail_sum (q: List Nat) (hnemp: q.nonEmpty): q.sum = q.tail.sum + q.head!

@[aesop unsafe]
theorem non_zero_length (q: List Nat) (hnemp: q.nonEmpty): 0 < q.length

@[aesop norm]
theorem sum_zero : ∀ q : List Nat, ¬q.nonEmpty → q.sum = 0

lemma meet_himp (x x' y z : l) :
  x = x' ->
  (x ⇨ y) ⊓ (x' ⇨ z) = x ⇨ (y ⊓ z)

lemma NonDetT.wp_mono  {l : Type u} [CompleteLattice l] [MAlgOrdered m l] [LawfulMonad m] {α : Type u} (x : NonDetT m α) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  NonDetT.wp x f <= NonDetT.wp x g

@[ext]
lemma W_ext (t : Type v) (α : Type u) [Preorder t] (w w' : W t α) :
  w.wp = w'.wp → w = w'

lemma wp_top_wlp (c : m α) (post : α -> l) :
  wp c ⊤ ⊓ wlp c post = wp c post

@[simp]
lemma wp_bot :
  wp (bot : m α) = fun _ => (⊥ : l)

lemma find_none (p : α -> Prop) [DecidablePred p] [Encodable α] :
  (find p).isNone -> ∀ x, ¬ p x

lemma wp_top_iwp (c : m α) (post : α -> l) :
  wp c ⊥ = ⊥ ->
  wp c ⊤ ⊓ iwp c post = wp c post

theorem simp1 {l : Type u} [CompleteBooleanAlgebra l] {p : Prop} (proof : p) {a b : l} (h : a ≤ b) :
  ⌜p⌝ ⇨ a ≤ b

omit [LawfulMonad m] in
@[simp]
lemma wp_top (c : m α) [NoFailure m] :
  wp c (fun _ => ⊤) = ⊤

lemma wp_except_handler_eq ε (hd : ε -> Prop) [IsHandler hd] (c : ExceptT ε m α) post :
  wp c post = wp (m := m) c (fun | .ok x => post x | .error e => ⌜hd e⌝)

omit [CCPOBot m] [MAlgDet m l] [LawfulMonad m] in
lemma wp_bot [∀ α, CCPO (m α)] [MAlgPartial m]:
  wp (bot : m α) = fun _ => (⊤ : l)

lemma ExtractNonDet.extract_refines (pre : l) (s : NonDetT m α) :
  triple pre s post ->
  triple pre s.run post

lemma ExceptT.wp_lift_hd {hd : ε -> Prop} (c : m α) (post : α -> l) [IsHandler hd] :
  wp (liftM (n := ExceptT ε m) c) post = wp (m := m) c post

lemma ExtractNonDet.extract_refines (pre : l) (s : NonDetT m α) (inst : ExtractNonDet Findable s) :
  triple pre s post ->
  pre <= s.prop ⊤ ->
  triple pre s.extract post

lemma wp_bind {β} (x : m α) (f : α -> m β) (post : β -> l) :
    wp (x >>= f) post = wp x (fun x => wp (f x) post)

lemma find_some_p (p : α -> Prop) [DecidablePred p] [Encodable α] (x : α) :
  find p = some x -> p x

theorem spmv_correct_triple (out: Array Int) (arr: Array Int) (spm: Array (SpV Int)):
  triple
    (∀ i < spm.size, ∀ j < spm[i]!.size, spm[i]!.ind[j]! < arr.size)
    (spmv out arr spv spm)
    fun ⟨_, outNew⟩ =>
      (∀ j < outNew.size, outNew[j]! = ∑ i ∈ Finset.range (arr.size), spm[j]![i] * arr[i]!)

lemma AccFrom_findNat (p : Nat -> Prop) [DecidablePred p] (i : Nat) :
  AccFrom p i -> (findNat.aux p i).isSome

theorem VSpV_correct_triple (out: Array Int) (arr: Array Int) (spv: SpV Int):
  triple
    (∀ i < spv.size, spv.ind[i]! < arr.size)
    (VSpV out arr spv)
    fun ⟨_, outNew⟩ =>
      outNew[0]! = ∑ i ∈ Finset.range (arr.size), spv[i] * arr[i]!

lemma AccFrom_findNat (p : Nat -> Prop) [DecidablePred p] (i : Nat) :
  AccFrom p i -> (findNat.aux p i).isSome

lemma TotalCorrectness.DivM.wp_eq (α : Type) (x : DivM α) (post : α -> Prop) :
  wp x post =
    match x with

lemma SumDigits_unfold (n : Nat) (h : n > 0) :
  SumDigits n = (n % 10) + SumDigits (n / 10)

lemma MonadNonDet.wp_assume {as : Prop} post : _root_.wp (MonadNonDet.assume (m := NonDetT m) as) post = ⌜as⌝ ⊓ post .unit

omit [MAlgDet m l] in
lemma ExtractNonDet.extract_refines_wp_weak (s : NonDetT m α) (inst : ExtractNonDet WeakFindable s) :
  wp s.extractWeak post <= wp s post
</all_available_lemmas>

<local_ctx>
import Mathlib.Logic.Function.Basic

import Mathlib.Order.CompleteBooleanAlgebra

import Mathlib.Order.Lattice

import Mathlib.Order.Basic

import Loom.MonadAlgebras.WP.Basic

import Loom.MonadAlgebras.WP.Tactic

import Loom.MonadAlgebras.WP.Gen

import Loom.MonadAlgebras.NonDetT.Findable

section NonDeterministicTransformer

inductive NonDetT (m : Type u -> Type v) : (α : Type u) -> Type _ where
  | pure {α} (ret : α) : NonDetT m α
  | vis {α} {β} (x : m β) (f : β → NonDetT m α) : NonDetT m α
  | pickCont {α} (τ : Type u) (p : τ -> Prop) [Findable p] (f : τ → NonDetT m α) : NonDetT m α
  | repeatCont {α} {β} (init : β) (f : β -> NonDetT m (ForInStep β)) (cont : β -> NonDetT m α) : NonDetT m α

variable {m : Type u -> Type v} {α β : Type u} [Monad m]

def NonDetT.bind (x : NonDetT m α) (f : α → NonDetT m β) : NonDetT m β :=
  match x with
  | pure ret => f ret
  | vis x f' => vis x fun y => bind (f' y) f
  | pickCont τ p f' => pickCont τ p fun t => bind (f' t) f
  | repeatCont init f' cont => repeatCont init f' fun t => bind (cont t) f

variable [CompleteBooleanAlgebra l] [MAlgOrdered m l]

namespace PartialCorrectness

namespace DemonicChoice

/- WP for NonDetT -/
noncomputable

def NonDetT.wp {l : Type u} [CompleteLattice l] [MAlgOrdered m l] : {α : Type u} -> NonDetT m α -> Cont l α
  | _, .pure ret => pure ret
  | _, .vis x f => fun post => _root_.wp x fun a => wp (f a) post
  | _, @NonDetT.pickCont _ _ τ p _ f =>
  fun post =>
    let p : Set τ := p;
    ⨅ a ∈ (p : Set τ), wp (f a) post
  | _, @NonDetT.repeatCont _ _ β init f cont => fun post => ⨆ (inv : ForInStep β -> l),
      ⌜ ∀ b, (inv (ForInStep.yield b)) <= wp (f b) inv⌝ ⊓
      spec (inv (.yield init)) (fun b => inv (.done b)) (fun b => wp (cont b) post)

def NonDetT.μ  {l : Type u} [CompleteLattice l] [MAlgOrdered m l] : NonDetT m l -> l := fun x => NonDetT.wp x id

variable [LawfulMonad m]

/- Ordered Monad Algebra instance for NonDetT -/
noncomputable
scoped
</local_ctx>

<target_theorem>
@[simp]
lemma NonDetT.wp_pickCont {τ : Type u} p (f : τ → NonDetT m α) [Findable p] post :
  _root_.wp (NonDetT.pickCont τ p f) post =  ⨅ a, ⌜p a⌝ ⇨ _root_.wp (f a) post :=
</target_theorem>

