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>
abbrev WithName (α : Sort u) (name : Lean.Name := default) := α

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

class LogicLift (l : outParam (Type u)) ( k : Type u) [CompleteLattice l] [CompleteLattice k] where
  [lift : MonadLift (Cont l) (Cont k)]
  lift_top {α : Type u} :
    monadLift (m := Cont l) (n := Cont k) (fun (_ : α -> l) => ⊤) = ⊤
  lift_bot {α : Type u} :
    monadLift (m := Cont l) (n := Cont k) (fun (_ : α -> l) => ⊥) = ⊥

PartialOrder in Mathlib.Order.Defs.PartialOrder

abbrev M := ReaderT Context TermElabM

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

Lean.Meta.Simp.mkContext in Lean.Meta.Tactic.Simp.Types

def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do
  let decl := doLetArrow[2]
  if decl.getKind == ``Parser.Term.doIdDecl then
    return #[getDoIdDeclVar decl]
  else if decl.getKind == ``Parser.Term.doPatDecl then
    getDoPatDeclVars decl
  else
    throwError "unexpected kind of `do` declaration"

Lean.Expr.lit in Lean.Expr

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]
  }

def AltExpr.vars (alt : AltExpr σ) : Array Var := Id.run do
  let mut vars := #[]
  if let some var := alt.var? then
    vars := vars.push var
  for pvar in alt.pvars do
    match pvar with
    | `(_) => pure ()
    | _ => vars := vars.push pvar
  return vars

instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] [CCPOBot m] [CCPOBotLawful m] : CCPOBotLawful (ExceptT ε m) where
  prop := CCPOBotLawful.prop (m := m)

Auto.Embedding.Lam.REntry.valid in Auto.Embedding.LamChecker

Function.comp in Init.Prelude

def hasReturn (c : Code) : Bool :=
  hasExitPointPred c fun
    | .return .. => true
    | _ => false

instance : LawfulMonad DivM :=

CompleteLattice in Mathlib.Order.CompleteLattice.Defs

Lean.Parser.Term.letrec in Lean.Parser.Term

def z3.target := s!"{arch}-{platform}"

def cvc5.arch := if System.Platform.target.startsWith "x86_64" then "x86_64" else "arm64"

System.FilePath.mk in Init.System.FilePath

Pure in Init.Prelude

termDepIfThenElse in Init.Notation

def mkDiscrTreeExtension [Inhabited α] [BEq α] (name : Name := by admit /- proof elided -/
) :
  IO (DiscrTreeExtension α) :=
  registerSimplePersistentEnvExtension {
    name          := name,
    addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insertCore k v) s) DiscrTree.empty,
    addEntryFn    := fun s n => s.insertCore n.1 n.2 ,
  }

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

private def _root_.Lean.EnvExtension.get [Inhabited σ] (ext : EnvExtension σ)
  [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)

instance (σ : Type u) (l : Type u) (m : Type u -> Type v)
  [CompleteLattice l]
  [Monad m] [LawfulMonad m] [inst: MAlgOrdered m l] [inst': MAlgDet m l]
   : MAlgDet (ReaderT σ m) (σ -> l) where
    angelic := by admit /- proof elided -/

macro "⌜" p:term "⌝" : term => `(LE.pure $p)

Lean.Parser.Term.doDbgTrace in Lean.Parser.Do

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

abbrev MProdWithNames.mk' {α β : Type u} (a : α) (b : β)
  (αName : Lean.Name := default) : MProdWithNames α β αName :=
  @MProdWithNames.mk _ _ αName a b

instance : ToString SmtResult where
  toString
    | SmtResult.Sat none => "sat"
    | SmtResult.Sat (some m) => s!"sat\n{m}"
    | SmtResult.Unsat => s!"unsat"
    | SmtResult.Unknown none => s!"unknown"
    | SmtResult.Unknown (some r) => s!"unknown ({r})"
    | SmtResult.Failure none => "failure"
    | SmtResult.Failure (some r) => s!"failure ({r})"

instance {l} [CompleteLattice l] : LogicLiftT l l where
  lift_top := by admit /- proof elided -/

Lean.Order.CCPO in Init.Internal.Order.Basic

def VelvetM.extract {α : Type} (x : VelvetM α)
  [∀ α, Lean.Order.CCPO (DivM α)] [Lean.Order.MonoBind DivM] [Inhabited α] : α :=
  x.run.run

termIfThenElse in Init.Notation

instance EffectObservationOfMAlg (l : Type u) {m : Type u -> Type v} [Monad m] [LawfulMonad m] [MAlg m l] : LawfulMonadLiftT m (Cont l) where
  monadLift_pure := by admit /- proof elided -/

def mkReturn (ref : Syntax) (val : Syntax) : CodeBlock :=
  { code := .return ref val }

List.sum in Init.Data.List.Basic

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

private def openScope (ident : Name) : CommandElabM Unit := do
  let openDecls ← elabOpenDecl <| <- `(openDecl|$(mkIdent ident):ident)
  modifyScope fun scope => { scope with openDecls := openDecls }

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

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

def returnToTerm (val : Syntax) : M Syntax := do
  let ctx ← read
  let u ← mkUVarTuple
  match ctx.kind with
  | .regular         => if ctx.uvars.isEmpty then ``(Pure.pure $val) else ``(Pure.pure (MProdWithNames.mk $val $u))
  | .forIn           => ``(Pure.pure (ForInStep.done $u))
  | .forInWithReturn => ``(Pure.pure (ForInStep.done (MProdWithNames.mk (some $val) $u)))
  | .nestedBC        => unreachable!
  | .nestedPR        => ``(Pure.pure (DoResultPR.«return» $val $u))
  | .nestedSBC       => ``(Pure.pure (DoResultSBC.«pureReturn» $val $u))
  | .nestedPRBC      => ``(Pure.pure (DoResultPRBC.«return» $val $u))

Lean.Parser.Term.doSeqIndent in Lean.Parser.Do

Lean.MVarId in Lean.Expr

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

IO.FS.createDirAll in Init.System.IO

def withNewMutableVars {α} (newVars : Array Var) (mutable : Bool) (x : M α) : M α :=
  withReader (fun ctx => if mutable then { ctx with mutableVars := insertVars ctx.mutableVars newVars } else ctx) x

@[instance high]
instance [md : Monad m] [ccpo : ∀ α, CCPO (m α)] [mono : MonoBind m] : ForIn m Lean.Loop Unit where
  forIn {β} _ := @Loop.forIn m β md ccpo mono

iSup in Mathlib.Order.SetNotation

def cvc5Path := buildDir / "cvc5"

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

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

MonadExceptOf in Init.Prelude

Lean.addDecl in Lean.AddDecl

def spv_dot (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ): Int :=
  if (spv1.size) ≤ pnt1 ∨ (spv2.size) ≤ pnt2 then
    0
  else
    if (spv1.ind)[pnt1]! = (spv2.ind)[pnt2]! then
      (spv1.val)[pnt1]! * (spv2.val)[pnt2]! + spv_dot spv1 spv2 (pnt1 + 1) (pnt2 + 1)
    else
      if (spv1.ind)[pnt1]! < (spv2.ind)[pnt2]! then
        spv_dot spv1 spv2 (pnt1 + 1) pnt2
      else
        spv_dot spv1 spv2 pnt1 (pnt2 + 1)
  termination_by ((spv1.size) + (spv2.size) - pnt1 - pnt2)

private def liftMethodDelimiter (k : SyntaxNodeKind) : Bool :=
  k == ``Parser.Term.do ||
  k == ``Parser.Term.doSeqIndent ||
  k == ``Parser.Term.doSeqBracketed ||
  k == ``Parser.Term.termReturn ||
  k == ``Parser.Term.termUnless ||
  k == ``Parser.Term.termTry ||
  k == ``Parser.Term.termFor

Lean.Parser.Tactic.tacticSeq in Lean.Parser.Term.Basic

Lake.LogIO in Lake.Util.Log

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

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

Finset in Mathlib.Data.Finset.Defs

class WeakFindable {α : Type u} (p : α -> Prop) where
  find : Unit -> Option α
  find_some_p : find () = some x -> p x

List.head! in Init.Data.List.BasicAux

instance [Monad m] [inst : ∀ α, Lean.Order.CCPO (m α)] : Lean.Order.CCPO (ReaderT ε m α) :=

private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool :=
  let k := letDeclArg.getKind
  if k == ``Parser.Term.letPatDecl then
    false
  else if k == ``Parser.Term.letEqnsDecl then
    true
  else if k == ``Parser.Term.letIdDecl then
    
    let binders := letDeclArg[1]
    binders.getNumArgs > 0
  else
    false

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

partial def querySolver (goalQuery : String) (withTimeout : Nat) (forceSolver : Option SmtSolver := none) (retryOnUnknown : Bool := false) : MetaM (SmtResult × SmtSolver):= do
  let opts ← getOptions
  let solverName :=
    match forceSolver with
    | some s => s
    | none => loom.solver.smt.default.get opts
  try
  trace[loom.smt.debug] "solver: {solverName}"
  let solver ← createSolver solverName withTimeout
  emitCommandStr solver goalQuery
  emitCommand solver .checkSat
  let stdout ← solver.stdout.getLine
  trace[loom.smt.debug] "[checkSat] stdout: {stdout}"
  let (checkSatResponse, _) ← Auto.Solver.SMT.getSexp stdout
  match checkSatResponse with
  | .atom (.symb "sat") =>
    trace[loom.smt.result] "{solverName} says Sat"
    emitCommand solver .getModel
    let (_, solver) ← solver.takeStdin
    let stdout ← solver.stdout.readToEnd
    let stderr ← solver.stderr.readToEnd
    trace[loom.smt.debug] "stdout: {stdout}"
    trace[loom.smt.debug] "stderr: {stderr}"
    let (model, _) ← Auto.Solver.SMT.getSexp stdout
    solver.kill
    return (SmtResult.Sat s!"{model}", solverName)

Lean.indentD in Lean.Message

class PreOrderFunctor where preord : (α : Type u) -> Preorder (w α)

Lean.Parser.Term.termBeforeDo in Lean.Parser.Do

Lean.registerSimplePersistentEnvExtension in Lean.EnvExtension

abbrev Except.getD {ε α} (default : ε -> α)  : Except ε α -> α
  | Except.ok p => p
  | Except.error e => default e

Id.run in Init.Control.Id

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

Except.error in Init.Prelude

Unit.unit in Init.Prelude

def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Var) :=
  getPatternVars pattern <|>
  Quotation.getPatternVars pattern

Lean.AttrM in Lean.Attributes

partial def Lean.Expr.getNamesProp (tp : Expr) : MetaM (Option (List Name)) := do
  match_expr tp with
  | WithName _ n₁ => return some [<- n₁.getName]
  | MProdWithNames _ tr n₁ =>
    let n₁ <- n₁.getName
    let some ns <- tr.getNamesProp
      | return none
    return some $ n₁ :: ns
  | _ =>
    let .some typeWithNameExpr := tp.find? (fun e => e.isAppOf ``typeWithName)
      | return none
    let nname := typeWithNameExpr.getAppArgs[2]!
    return some [<- nname.getName]

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

Lean.throwErrorAt in Lean.Exception

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

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 simpleAddThm (n : Name) (tp : Expr) (pf : Expr)
  (attr : Array Attribute := #[]) : TermElabM Unit := do
  addDecl <|
    Declaration.thmDecl <|
      mkTheoremValEx n [] tp pf []
  applyAttributes n attr

instance : CCPOBotLawful DivM where
  prop := by admit /- proof elided -/

def isMutableLet (doElem : Syntax) : Bool :=
  let kind := doElem.getKind
  (kind == ``doLetArrow || kind == ``doLet || kind == ``doLetElse)
  &&
  !doElem[1].isNone

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

Lean.Parser.Term.letRecDecls in Lean.Parser.Term

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)

abbrev typeWithName {α : Type u} (β : α) (name : Lean.Name := default) := β

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

List.take in Init.Data.List.Basic

BooleanAlgebra in Mathlib.Order.BooleanAlgebra.Defs

def getAssertionStx : TacticM (Option Term) := withMainContext do
  let goal <- getMainTarget
  let goalStx <- ppExpr goal
  let ⟨_, ss, ns, _⟩ <- loomAssertionsMap.get
  let .some withNameExpr := goal.find? (fun e => e.isAppOf ``WithName)
    | let .some typeWithNameExpr := goal.find? (fun e => e.isAppOf ``typeWithName)
        | throwError s!"Failed to parse an assertion without names: {goalStx}"
      let nname := typeWithNameExpr.getAppArgs[2]!
      let sname <- nname.getName
      let some id1 := ns[sname]?
        | throwError s!"typeWithName {sname} not registered: {typeWithNameExpr}"
      return some ss[id1]!
  match_expr withNameExpr with
  | WithName exp name =>
    let name <- name.getName
    let some id := ns[name]?
      | let .some typeWithNameExpr := exp.find? (fun e => e.isAppOf ``typeWithName)
          | throwError s!"Failed to prove assertion without names: {goalStx}"
        let nname := typeWithNameExpr.getAppArgs[2]!
        let sname <- nname.getName
        let some id1 := ns[sname]?
          | throwError s!"typeWithName {sname} not registered: {typeWithNameExpr}"
        return some ss[id1]!
    return some ss[id]!
  | _ => throwError s!"Failed to prove assertion which is not registered4: {goalStx}"

def mkMatch (ref : Syntax) (genParam : Syntax) (discrs : Syntax) (optMotive : Syntax) (alts : Array (Alt CodeBlock)) : TermElabM CodeBlock := do
  
  let ws := alts.foldl (union · ·.rhs.uvars) {}
  let alts ← alts.mapM fun alt => do
    let rhs ← extendUpdatedVars alt.rhs ws
    return { ref := alt.ref, vars := alt.vars, patterns := alt.patterns, rhs := rhs.code : Alt Code }
  return { code := .match ref genParam discrs optMotive alts, uvars := ws }

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

def NonDetT.pickSuchThat (τ : Type u) (p : τ → Prop) [Findable p] : NonDetT m τ :=
  NonDetT.pickCont τ p pure

Lean.Parser.Term.optIdent in Lean.Parser.Term.Basic

StateT.run in Init.Control.State

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

Lean.Parser.Term.doSeqItem in Lean.Parser.Do

Lean.Parser.Term.doIf in Lean.Parser.Do

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

def WPGen.forWithInvariantLoop {β}
  {init : β} {f : Unit -> β → NonDetT m (ForInStep β)}
  (inv : β → List l) (on_done' : β → l)
  (measure : β → Option ℕ)
  (wpg : ∀ b, WPGen (f () b)) :
    WPGen (forIn Lean.Loop.mk init (fun u b => do
        invariantGadget (inv b)
        onDoneGadget (on_done' b)
        decreasingGadget (measure b)
        f u b)) where
    get := ⌜∀ b, invariantSeq (inv b) <= (wpg b).get fun
      | .yield b' => invariantSeq <| inv b'
      | .done b'  => invariantSeq (inv b') ⊓ on_done' b'⌝
      ⊓ spec
      ((inv init).foldr (·⊓·) ⊤)
      (fun b => (inv b).foldr (·⊓·) ⊤ ⊓ on_done' b)
    prop := by admit /- proof elided -/

StateT.get in Init.Control.State

elab "type_with_name_prefix" lit:name inv:term : term => do
  let ⟨maxId, _, _, cntr⟩ <- loomAssertionsMap.get
  let newMaxId := maxId + 1
  let coreName := match (← Term.getDeclName?) with
    | some res => res
    | none => `nameless
  let localName := (Lean.Name.mkSimple (lit.getName.toString ++ "_" ++ coreName.toString))
  let cntrElem := match cntr.get? localName with
    | some resId => resId
    | none => 0
  let maxIdLocal := 1 + cntrElem
  let invName := lit.getName.toString ++ "_" ++ toString maxIdLocal.toNat |>.toName
  loomAssertionsMap.modify (fun res => {
      syntaxStore := res.syntaxStore.insert newMaxId inv
      nameStore := res.nameStore.insert invName newMaxId
      maxId := newMaxId
      nameCounter := res.nameCounter.insert localName maxIdLocal
      })
  Term.elabTerm (<- ``(typeWithName $inv $(Lean.quoteNameMk invName))) none

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

def WPGen.recMT1 {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
  {ls: mt1 γ}
  {ll : γ → m β}
  {el : m β}
  {nl : mt1 γ → mt1 γ → γ → m β → m β → m β}
  (wpgl : ∀ (a: γ), WPGen (ll a))
  (wpge : WPGen el)
  (wpgn : ∀ (l r: mt1 γ) (a: γ) (ml mr: m β), WPGen (nl l r a ml mr)):
  WPGen (mt1.recOn ls ll el nl : m β) where
  get := fun post =>
    (⨅ a, (wpgl a).get post) ⊓
    (wpge.get post) ⊓
    (⨅ l, ⨅ r, ⨅ a, ⨅ ml, ⨅ mr, (wpgn l r a ml mr).get post)
  prop := by admit /- proof elided -/

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

Lean.Parser.Term.doLetElse in Lean.Parser.Do

IO.Process.Child in Init.System.IO

Bind.bind in Init.Prelude

MonadExcept.tryCatch in Init.Prelude

def run (code : Code) (m : Syntax) (returnType : Syntax) (uvars : Array Var := #[]) (kind := Kind.regular) : MacroM Syntax :=
  toTerm code { m, returnType, kind, uvars }

Lean.Meta.reduceAll in Lean.Meta.Reduce

structure DoIfView where
  ref        : Syntax
  optIdent   : Syntax
  cond       : Syntax
  thenBranch : Syntax
  elseBranch : Syntax

def getLetIdVars (letId : Syntax) : Array Var :=
  assert! letId.isOfKind ``Parser.Term.letId
  
  if letId[0].isIdent then
    #[letId[0]]
  else if letId[0].isOfKind hygieneInfoKind then
    #[HygieneInfo.mkIdent letId[0] `this (canonical := true)]
  else
    #[]

instance [Monad m] [LawfulMonad m] : LawfulMonadLiftT m (ReaderT σ m) where
  monadLift_pure := by admit /- proof elided -/

Repr in Init.Data.Repr

def cvc5.os :=
  if System.Platform.isWindows then "Win64"
  else if System.Platform.isOSX then "macOS"
  else "Linux"

def List.nonEmpty (q : List α) : Prop :=
  ¬q.isEmpty

Lake.buildFileAfterDep in Lake.Build.Common

instance [Monad m] : LawfulMonadLiftT m m where
  monadLift_pure := by admit /- proof elided -/

instance [LawfulMonad m] : LawfulMonad (NonDetT m) :=

elab "invariants" invs:term : term => do
  let opts <- getOptions
  let invsIsEmpty := match invs with
    | `([]) => true
    | _ => false
  let warningsEnabled := opts.getBool (defVal := true) `loom.linter.warnings
  if invsIsEmpty && warningsEnabled then
    logWarningAt (<- getRef) "Invariant annotations are not specified, so the loop invariant is assumed to be just `True`.
To turn off this warning, use `set_option loom.linter.warnings false`."
  Term.elabTerm (<- `(invariantGadget $invs:term)) none

prove_correct calc_fact by
  loom_solve

LawfulMonad in Init.Control.Lawful.Basic

Lean.Elab.Term.getPatternsVars in Lean.Elab.PatternVar

let wpgenTypeBuilder x : MetaM Expr :=
    
    mkAppOptM ``WPGen #[.some mExpr, .some monadInstExpr, .some αExpr, .some lExpr, .none, .some omaInstExpr, .some x]
  let branchConds ← do
    pure <| Array.map (fun x => (x.1, x.2.1)) <| List.toArray <| getForallPremises partialMatcher
  let subMonadArgsWithInfo ← branchConds.mapM fun (nm, br) => do
    
    
    
    
    forallTelescope br fun xs body => do
      if xs.isEmpty then
        return ((0, MatcherArgCase.normal), (nm, mαExpr))
      let (case, xs') :=
        if xs[0]!.occurs body
        then (MatcherArgCase.normal, xs)
        else (MatcherArgCase.dropFirst, xs.drop 1)
      pure ((xs'.size, case), (nm, ← mkForallFVars xs' mαExpr))
  let (subMonadArgsInfo, subMonadArgs) := subMonadArgsWithInfo.unzip
  trace[Loom.debug] "subMonadArgs: {subMonadArgs.map Prod.snd}"
  withLocalDecls (← subMonadArgs.mapM fun (nm, t) => do
      let nm' ← mkFreshUserName nm
      pure (nm', BinderInfo.implicit, fun _ => pure t)) fun subMonadArgsFVars => do

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

Lean.TSyntaxArray in Init.Prelude

instance : Inhabited (SpV Int) where
  default :=
  { ind := #[],
    val := #[],
    size := 0,
    size_eq := (by admit /- proof elided -/
    ),
    inc := (fun i j h_i h_j i_lt_j => by admit /- proof elided -/
    ) }

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]!

instance : Lean.Order.MonoBind DivM where
  bind_mono_left := by admit /- proof elided -/

Lean.instantiateMVars in Lean.MetavarContext

Lean.Parser.Term.doLetRec in Lean.Parser.Do

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

IO.FS.removeDirAll in Init.System.IO

def mkForInBody  (_ : Syntax) (forInBody : CodeBlock) : M ToForInTermResult := do
  let ctx ← read
  let uvars := forInBody.uvars
  let uvars := varSetToArray uvars
  let term ← liftMacroM <| ToTerm.run forInBody.code ctx.m ctx.returnType uvars (if hasReturn forInBody.code then ToTerm.Kind.forInWithReturn else ToTerm.Kind.forIn)
  return ⟨uvars, term⟩

OrderTop in Mathlib.Order.BoundedOrder.Basic

Lean.Meta.abstractMVars in Lean.Meta.AbstractMVars

Lean.ReducibilityHints.regular in Lean.Declaration

inductive Kind where
  | regular
  | forIn
  | forInWithReturn
  | nestedBC
  | nestedPR
  | nestedSBC
  | nestedPRBC

@[instance high]
instance {p : α -> Prop} [FinEnum α] [DecidablePred p] : Findable p where
  find := fun _ => FinEnum.toList α |>.find? p
  find_none := by admit /- proof elided -/

Lean.Expr.getNumHeadForalls in Lean.Expr

def WPGen.recOption {l : Type u} {m : Type u -> Type v} [Monad m] [LawfulMonad m] [CompleteBooleanAlgebra l] [MAlgOrdered m l]
   {x : m β} {y : α → m β} {val: Option α}
  (wpgx : WPGen x) (wpgy : ∀ a, WPGen (y a)) :
  WPGen (Option.recOn val x y : m β) where
  get := fun post =>
    (wpgx.get post) ⊓ (⨅ a, (wpgy a).get post)
  prop := by admit /- proof elided -/

def assertGadget {l : Type u} (h : l) : m PUnit := pure .unit

Lean.Elab.Term.getPatternVars in Lean.Elab.PatternVar

Auto.Embedding.Lam.MutualIndInfo in Auto.Embedding.LamInductive

class LogicLiftT (l : (Type u)) ( k : Type u) [CompleteLattice l] [CompleteLattice k] where
  [lift : MonadLiftT (Cont l) (Cont k)]
  lift_top {α : Type u} :
    monadLift (m := Cont l) (n := Cont k) (fun (_ : α -> l) => ⊤) = ⊤
  lift_bot {α : Type u} :
    monadLift (m := Cont l) (n := Cont k) (fun (_ : α -> l) => ⊥) = ⊥

ULift in Init.Prelude

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
  [CompleteLattice l] [inst: MAlgOrdered m l] [IsHandler (fun (_ : ε) => True)]
  [inst': NoFailure m] : NoFailure (ExceptT ε m) where
  noFailure := by admit /- proof elided -/

def z3.baseUrl := "https://github.com/Z3Prover/z3/releases/download"

def failureGoalStr (solver : Option SmtSolver := none) : String := s!"{solverStr solver}solver invocation failed"

inferInstanceAs in Init.Prelude

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

Preorder in Mathlib.Order.Defs.PartialOrder

def constructWPGen (matcherName : Name) : TermElabM (Option MatcherWPGen) := do
  
  
  
  let some matcherInfo ← getMatcherInfo? matcherName | return none
  let constInfo ← getConstInfo matcherName
  
  let lvlMVars ← mkFreshLevelMVars constInfo.levelParams.length

measure in Init.WF

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

def Array.sumUpTo [Inhabited α] [AddCommMonoid β] (a : Array α) (f : ℕ -> α -> β) (bound : ℕ) : β :=
  ∑ i ∈ Finset.range bound, f i a[i]!

System.FilePath in Init.System.FilePath

ExceptT.bindCont in Init.Control.Except

private def recordOption (stx : Syntax) : CommandElabM Unit := do
  let options ← Elab.elabSetOption stx[1] stx[3]
  modify fun s => { s with maxRecDepth := maxRecDepth.get options }
  modifyScope fun scope => { scope with opts := options }

instance : ToString LoomSolver where
  toString
    | .cvc5 => "cvc5"
    | .smt .z3 => "z3"
    | .smt .cvc5 => "cvc5"
    | .grind => "grind"
    | .custom => "custom"

def MAlgExcept (ε : Type u) (df : ε -> Prop) (l : Type u) (m : Type u -> Type v)
  [CompleteLattice l]
  [Monad m] [LawfulMonad m] [inst: MAlgOrdered m l] : MAlgOrdered (ExceptT ε m) l where
  μ := fun e => inst.μ $ Except.getD (⌜df ·⌝) <$> e
  μ_ord_pure := by admit /- proof elided -/

DoResultPRBC in Init.Core

instance: GetElem (SpV Int) Nat Int fun _ _ => True where
  getElem inst i _ :=
    match (List.zip (inst.ind.toList) (inst.val.toList)).find? fun (j, _) => j = i with
    | some pr => pr.2
    | none => 0

Lean.Parser.Term.doReassign in Lean.Parser.Do

Lean.Parser.Term.doExpr in Lean.Parser.Do

Lean.MessageData.ofList in Lean.Message

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

Lean.Meta.mkFreshExprMVar in Lean.Meta.Basic

instance {p : α -> Prop} [Encodable α] [DecidablePred p] : Findable p where
  find := fun _ => find p
  find_none := find_none p
  find_some_p := find_some_p p _

Lean.hygieneInfoKind in Init.Prelude

Lean.Meta.simp in Lean.Meta.Tactic.Simp.Main

def attachJP (jpDecl : JPDecl) (k : Code) : Code :=
  Code.joinpoint jpDecl.name jpDecl.params jpDecl.body k

Lean.Parser.Term.doIfCond in Lean.Parser.Do

instance [NoFailure m] : NoFailure (NonDetT m) where
  noFailure := by admit /- proof elided -/

Lean.MessageData.joinSep in Lean.Message

partial def extendUpdatedVars (c : CodeBlock) (ws : VarSet) : TermElabM CodeBlock := do
  if ws.any fun x _ => !c.uvars.contains x then
    
    pure { code := (← extendUpdatedVarsAux c.code ws), uvars := ws }
  else
    pure { c with uvars := ws }

let subWPGenArgs ← subMonadArgs.mapIdxM fun i (nm, t) => do
    let nm' := nm.appendBefore "wpg"
    let ty ← forallTelescope t fun xs _ => do
      let tmp ← wpgenTypeBuilder <| mkAppN subMonadArgsFVars[i]! xs
      let motiveBody ← Expr.getForallBody <$> instantiateForall branchConds[i]!.2 xs
      let withEqs ← motiveBody.withApp fun _ args => do
        
        let eqs ← discrs.mapIdxM fun i lhs => mkEq lhs args[i]!
        mkArrowN eqs tmp
      
      
      mkForallFVars xs withEqs
    pure (nm', ty)
  trace[Loom.debug] "subWPGenArgs: {subWPGenArgs}"
  withLocalDeclsDND (← subWPGenArgs.mapM fun (nm, t) => do
      pure (← mkFreshUserName nm, t)) fun subWPGenArgsFVars => do

private def Array.andList (ts : Array (TSyntax `term)) : TermElabM (TSyntax `term) := do
  if ts.size = 0 then `(term| True) else
    let mut t := ts[0]!
    for t' in ts[1:] do
      t <- `(term| $t' ∧ $t)
    return t

Lean.Name.cmp in Lean.Data.Name

withLocalDecl (← mkFreshUserName `α) BinderInfo.implicit (← Expr.bindingDomain! <$> inferType mExpr) fun αExpr => do
  let mαExpr := mkApp mExpr αExpr

def mkSeq (action : Syntax) (c : CodeBlock) : CodeBlock :=
  { c with code := .seq action c.code }

structure Extractable (x : NonDetT m α) where
  cond : Cont l α
  prop : ∀ post, cond post <= x.prop post

def SpecAttr.find? (s : SpecAttr) (e : Expr) : MetaM (Array Loom.Spec) := do
  (s.ext.getState (← getEnv)).getMatch e

IO.FS.removeFile in Init.System.IO

StateT.bind in Init.Control.State

Lean.Parser.Term.matchAlts in Lean.Parser.Term

Auto.collectAllLemmas in Auto.Tactic

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

instance: GetElem (SpV Int) Nat Int fun _ _ => True where
  getElem inst i _ :=
    match (List.zip (inst.ind.toList) (inst.val.toList)).find? fun (j, _) => j = i with
    | some pr => pr.2
    | none => 0

Lean.Elab.Term.Quotation.getPatternsVars in Lean.Elab.Quotation.Util

private def letDeclHasBinders (letDecl : Syntax) : Bool :=
  letDeclArgHasBinders letDecl[0]

def CaseStudiesRoot : Array Glob :=
  #[`CaseStudies.Extension,
    `CaseStudies.Macro,
    `CaseStudies.Tactic,
    `CaseStudies.TestingUtil,
    `CaseStudies.Theory]

Lean.Meta.ppExpr in Lean.Meta.Basic

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

LawfulMonadLift in Init.Control.Lawful.MonadLift.Basic

def breakToTerm : M Syntax := do
  let ctx ← read
  let u ← mkUVarTuple
  match ctx.kind with
  | .regular         => unreachable!
  | .forIn           => ``(Pure.pure (ForInStep.done $u))
  | .forInWithReturn => ``(Pure.pure (ForInStep.done (MProdWithNames.mk none $u)))
  | .nestedBC        => ``(Pure.pure (DoResultBC.«break» $u))
  | .nestedPR        => unreachable!
  | .nestedSBC       => ``(Pure.pure (DoResultSBC.«break» $u))
  | .nestedPRBC      => ``(Pure.pure (DoResultPRBC.«break» $u))

Bool in Init.Prelude

Auto.LamReif.preprocess in Auto.Translation.LamReif

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

Decidable in Init.Prelude

instance [Monad m] [LawfulMonad m] [_root_.CompleteLattice l]
  [inst: MAlgOrdered m l] :
  MAlgLift m l (NonDetT m) l where
    cl := by admit /- proof elided -/

instance [inst: (α : Type u) -> Preorder (w α)] : PreOrderFunctor w := ⟨inst⟩

Lean.MessageData in Lean.Message

Lean.MessageData.ofSyntax in Lean.Message

private def elabSimpArg (indexConfig : Meta.ConfigWithKey) (eraseLocal : Bool) (kind : SimpKind)
    (arg : Syntax) : TermElabM ElabSimpArgResult := withRef arg do
  try
     
    if arg.getKind == ``Lean.Parser.Tactic.simpErase then
      let fvar? ← if eraseLocal then Term.isLocalIdent? arg[1] else pure none
      if let some fvar := fvar? then
        
        return .erase (.fvar fvar.fvarId!)
      else
        let id := arg[1]
        if let .ok declName ← observing (realizeGlobalConstNoOverloadWithInfo id) then
          if (← Simp.isSimproc declName) then
            return .eraseSimproc declName
          else
            return .erase (.decl declName)
        else
          
          
          let name := id.getId.eraseMacroScopes
          if (← Simp.isBuiltinSimproc name) then
            return .eraseSimproc name
          else
            throwUnknownConstantAt id name
    else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
      let post :=
        if arg[0].isNone then
          true
        else
          arg[0][0].getKind == ``Parser.Tactic.simpPost
      let inv  := !arg[1].isNone
      let term := arg[2]
      match (← resolveSimpIdTheorem? ⟨term⟩) with
      | .expr e  =>
        let name ← mkFreshId
        elabDeclToUnfoldOrTheorem indexConfig (.stx name arg) e post inv kind
      | .simproc declName =>
        return .addSimproc declName post
      | .ext ext₁? ext₂? h =>
        return .ext ext₁? ext₂? h
      | .none    =>
        let name ← mkFreshId
        elabSimpTheorem indexConfig (.stx name arg) term post inv
    else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
      return .star
    else
      throwUnsupportedSyntax
  catch ex =>
    throw ex

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

let goal ← mkFreshExprMVar body
        let goals ← goal.mvarId!.casesRec fun localDecl => do
          return eqs.contains <| Expr.fvar localDecl.fvarId
        let goal := .mvar goals[0]!
        
        let goal' ← withinBranch i numBranches lExpr goal
        
        let dependencies := backup[i]!.toArray
        let (_, goal'') ← dependencies.foldlM (init := (0, goal')) fun (i, mainGoal) dep => do
          unless dep do
            let x := xs[i]!
            let xty ← inferType x
            let tmp ← mkAppOptM ``Loom.Matcher.simp1 #[.some lExpr, .none, .some xty, .some x]
            let goals ← mainGoal.mvarId!.apply tmp
            return (i.succ, .mvar goals[0]!)
          let (x, xty) ← match xs[i]? with
            | some x => pure (x, ← inferType x)
            | none =>
              let aa ← mkFreshExprMVar none
              let eq ← mkEq aa aa
              let rfl ← mkEqRefl aa
              pure (rfl, eq)
          let f ← mkFreshExprMVar (← mkArrow xty lExpr)
          let a ← mkFreshExprMVar lExpr
          let tmp ← mkAppOptM ``iInf_le_of_le #[.some lExpr, .some xty, .none,
            .some f   ,
            .some a, .some x]
          let goals ← mainGoal.mvarId!.apply tmp
          pure (i.succ, .mvar goals[0]!)
        
        let goal''' ←
          try
            let r ← goal''.mvarId!.rewrite (← goal''.mvarId!.getType) (← mkConstWithFreshMVarLevels matchEqnNames[i]!)
            let goal''' ← Expr.mvar <$> goal''.mvarId!.replaceTargetEq r.eNew r.eqProof
            for g in r.mvarIds do
              g.assumption
            pure goal'''
          catch _ => pure goal''
        
        let _ ← goal'''.mvarId!.applyConst ``WPGen.prop
        let res ← instantiateMVars goal
        mkLambdaFVars (xs ++ eqs) res
      trace[Loom.debug] "sub-proof for branch {i}: {br} ==> {res}"
      pure res
    let discrsRfls ← discrs.mapM (mkEqRefl ·)
    mkLambdaFVars #[postExpr] <| mkAppN partialSplitter (wpgenPostSubProofs ++ discrsRfls)

System.mkFilePath in Init.System.FilePath

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

structure VelvetObligation where
  binderIdents : TSyntaxArray `Lean.Parser.Term.bracketedBinder
  modIds : Array Ident
  ids : Array Ident
  retId : Ident
  ret : Term
  pre : Term
  post : Term
deriving Inhabited

instance (t : Type v) : Monad (Cont t) where
  pure x := fun f => f x
  bind x f := fun g => x (fun a => f a g)

Lean.mkNullNode in Init.Prelude

Lean.Elab.Term.expandMatchAlt in Lean.Elab.BindersUtil

MonadStateOf in Init.Prelude

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

ReaderT in Init.Prelude
</all_available_defs>

<all_available_lemmas>
lemma wp_cons (x : m α) (post post' : α -> l) :
  (∀ y, post y ≤ post' y) ->
  wp x post ≤ wp x post'

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

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

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

@[grind, solverHint]
lemma sumUpToSucc
  (spv : SpV Int)
  (v : Array Int) (bound : ℕ) :
  sumUpTo spv v (bound + 1) = (sumUpTo spv v bound) +
    ((spv.val)[bound]! * v[(spv.ind)[bound]!]!)

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

lemma MonadNonDet.wp_pick {τ : Type u} [Inhabited τ] post :
  _root_.wp (MonadNonDet.pick (m := NonDetT m) τ) post = iInf post

lemma Gen.wp_rand {α : Type} (c : Gen α) :
  triple ⊤ c (fun _ => ⊤)

lemma array_extract_split (arr : Array α) (i j : Nat) :
    i < j → j ≤ arr.size →
    arr.extract 0 j = (arr.extract 0 i) ++ (arr.extract i j)

lemma exists_findNat (p : Nat -> Prop) [DecidablePred p] :
  (∃ x, p x) ↔ (findNat p).isSome

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

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

@[simp]
lemma Array.replicate_get (n : ℕ) [Inhabited α] (a : α) (i : ℕ) (_ : i < n := by omega) :
  (Array.replicate n a)[i]! = a

lemma StateT.wp_lift (c : m α) (post : α -> σ -> l) :
  wp (liftM (n := StateT σ m) c) post = fun s => wp (m := m) c (post · s)

lemma adjacent_to_global_sorted (a : Array Int) :
    (∀ k, 0 ≤ k ∧ k < a.size - 1 → a[k]! ≤ a[k+1]!) →
    (∀ i j, 0 ≤ i ∧ i < j ∧ j < a.size → a[i]! ≤ a[j]!)

lemma TotalCorrectness.DivM.wlp_eq (α : Type) (x : DivM α) (post : α -> Prop) :
  (open TotalCorrectness in wlp x post) = (open PartialCorrectness in wp x post)

@[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 trueE (l : Type v) [inst: LE l] [OrderTop l] [OrderBot l] : ⌜True⌝ = (⊤ : l)

@[simp]
lemma NonDetT.wp_pickCont {τ : Type u} p (f : τ → NonDetT m α) post :
  _root_.wp (NonDetT.pickCont τ p f) post = ⨆ a, ⌜p a⌝ ⊓ _root_.wp (f a) 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

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

@[solverHint]
theorem spv_dot_gt
  (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ) (prev: Int) :
  prev + spv_dot spv1 spv2 pnt1 pnt2 = spv_dot spv1 spv2 0 0 →
  spv2.ind[pnt2]! ≤ spv1.ind[pnt1]! →
  spv1.ind[pnt1]! ≠ spv2.ind[pnt2]! →
  pnt1 < spv1.size → pnt2 < spv2.size →
    prev + spv_dot spv1 spv2 pnt1 (pnt2 + 1) = spv_dot spv1 spv2 0 0

omit [MonoBind m] [LawfulMonad m] in
lemma wp_csup (xc : Set (m α)) (post : α -> l) :
  Lean.Order.chain xc ->
  ⨅ c ∈ xc, wp c post ≤ wp (Lean.Order.CCPO.csup xc) post

lemma filter_sum_snoc (arr: Array Nat) (p: Nat → Bool) :
  forall i, i < arr.size →
      (Array.filter p (Array.extract arr 0 i)).sum + (if (p arr[i]!) then arr[i]! else 0)=
      (Array.filter p (Array.extract arr 0 (i + 1))).sum

lemma StateT.wp_get (post : σ -> σ -> l) :
  wp (get (m := StateT σ m)) post = fun s => post s s

lemma repeat_inv (f : Unit -> β -> m (ForInStep β))
  (inv : ForInStep β -> l) (measure : β -> Nat)
  init :
   (∀ b, triple (inv (.yield b)) (f () b) (fun | .yield b' => inv (.yield b') ⊓ ⌜ measure b' < measure b ⌝ | .done b' => inv (.done b'))) ->
   triple (inv (.yield init)) (Loop.forIn.loop f init) (fun b => inv (.done b))

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

lemma spec_mono {α : Type u} {l : Type u} [CompleteLattice l] (pre : l) (post : α -> l) (f g : α -> l) :
  (∀ a, f a <= g a) ->
  spec pre post f <= spec pre post g

@[simp]
lemma NonDetT.wp_vis {β : Type u} (x : m β) (f : β → NonDetT m α) post :
  _root_.wp (NonDetT.vis x f) post = _root_.wp x fun a => _root_.wp (f a) post

theorem SpVSpV_correct_triple (out: Array Int) (spv1 spv2: SpV Int) (n: ℕ):
  triple
    ((∀ i < spv1.size, spv1.ind[i]! < n) ∧ (∀ i < spv2.size, spv2.ind[i]! < n))
    (SpVSpV out spv1 spv2)
    fun ⟨_, outNew⟩ =>
      outNew[0]! = ∑ i ∈ Finset.range n, spv1[i]! * spv2[i]!

theorem triple_forIn_list {α β}
  {xs : List α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : List α → β → l)
  (hstep : ∀ hd tl b,
    triple
      (inv (hd :: tl) b)
      (f hd b)
      (fun | .yield b' => inv tl b' | .done b' => inv [] b')) :
  triple (inv xs init) (forIn xs init f) (inv [])

theorem finalCorrectnessTheorem (s : Array Char) (p : Char → Bool) :
  let res := SubstringSearch s p |>.extract
  (res.flag = false → ∀ i < s.size, p s[i]! = false) ∧
  (res.flag = true →
    (∀ l₁ r₁, CorrectSubstring s p l₁ r₁ →
  r₁ - l₁ + 1 = res.r - res.l + 1 ∧ res.r ≤ r₁ ∨
  r₁ - l₁ + 1 < res.r - res.l + 1)) ∧
  (res.flag = true → CorrectSubstring s p res.l res.r) ∧
  (0 < s.size → res.r < s.size) ∧
  (res.l ≤ res.r)

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

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

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

@[solverHint]
theorem spv_dot_exh
  (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ):
  pnt1 = spv1.size ∨ pnt2 = spv2.size → spv_dot spv1 spv2 pnt1 pnt2 = 0

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

lemma NonDetT.wp_eq_wp {α : Type u} (x : NonDetT m α) (post : α -> l) :
  _root_.wp x post = NonDetT.wp x post

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

omit [LawfulMonad m] [CCPOBot m] [MAlgDet m l] in
lemma NonDetT.prop_bind (x : NonDetT m α) (f : α -> NonDetT m β) :
  (x >>= f).prop = fun post => x.prop (fun a => (f a).prop post)

@[simp]
lemma NonDetT.wp_pure (x : α) post :
  _root_.wp (NonDetT.pure (m := m) x) post = post x

@[grind]
lemma get_cnt_sum_hd e l : get_cnt_sum (e::l) = e.cnt + get_cnt_sum l

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

omit [LawfulMonad m] in
lemma MAlgLift.wp_lift [Monad n] [CompleteLattice k] [MAlgOrdered n k] [MonadLiftT m n]
  -- [MonadLiftT (Cont l) (Cont k)]
  [mAlgLift : MAlgLiftT m l n k] (c : m α):
  wp (liftM (n := n) c) = fun (post : α -> k) => mAlgLift.cl.lift.monadLift (wp c) post

lemma wp_compl'  (c : m α) post (wp_bot : ∀ α (c : m α), wp c ⊥ = ⊥) :
  wp c post <= (wp c postᶜ)ᶜ

lemma MonadNonDet.wp_pick {τ : Type u} post :
  _root_.wp (MonadNonDet.pick (m := NonDetT m) τ) post = iInf post

@[grind, solverHint]
lemma sumUpTo0
  (spv : SpV Int) (v : Array Int) :
  sumUpTo spv v 0 = 0

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]!)

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

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 NonDetT.wp_bind [LawfulMonad m] {α β : Type u} {l : Type u} [CompleteLattice l] [MAlgOrdered m l] (x : NonDetT m α) (f : α -> NonDetT m β)
  (post : β -> l):
  NonDetT.wp (x.bind f) post = NonDetT.wp x (fun x => NonDetT.wp (f x) post)

lemma MonadNonDet.wp_repeat {α : Type u} (init : α) (f : α -> NonDetT m (ForInStep α)) post :
  _root_.wp (MonadNonDet.rep (m := NonDetT m) init f) post = ⨆ (inv : ForInStep _ -> l),
    ⌜ ∀ b, (inv (ForInStep.yield b)) <= wp (f b) inv⌝ ⊓
    spec (inv (.yield init)) (fun b => inv (.done b)) post

omit [CCPOBot m] [MAlgDet m l] in
lemma NonDetT.prop_mono (x : NonDetT m α) post post' :
  post <= post' -> x.prop post <= x.prop post'

lemma findNat_none (p : Nat -> Prop) [DecidablePred p] :
  (findNat p).isNone -> ∀ i, ¬ p i

lemma triple_pure (pre : l) (x : α) (post : α -> l) :
  triple pre (pure (f := m) x) post <-> pre ≤ (post x)

lemma wp_pure (x : α) (post : α -> l) : wp (m := m) (pure x) post = post x
</all_available_lemmas>

<local_ctx>
import Auto

import Lean

import Mathlib.Algebra.BigOperators.Intervals

import Mathlib.Algebra.Ring.Int.Defs

import Loom.MonadAlgebras.NonDetT.Extract

import Loom.MonadAlgebras.WP.Tactic

import Loom.MonadAlgebras.WP.DoNames'

import CaseStudies.Velvet.Std

section SpMV

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 spv_dot (spv1 spv2: SpV Int) (pnt1 pnt2: ℕ): Int :=
  if (spv1.size) ≤ pnt1 ∨ (spv2.size) ≤ pnt2 then
    0
  else
    if (spv1.ind)[pnt1]! = (spv2.ind)[pnt2]! then
      (spv1.val)[pnt1]! * (spv2.val)[pnt2]! + spv_dot spv1 spv2 (pnt1 + 1) (pnt2 + 1)
    else
      if (spv1.ind)[pnt1]! < (spv2.ind)[pnt2]! then
        spv_dot spv1 spv2 (pnt1 + 1) pnt2
      else
        spv_dot spv1 spv2 pnt1 (pnt2 + 1)
  termination_by ((spv1.size) + (spv2.size) - pnt1 - pnt2)


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


method SpMSpV
  (mut out: Array Int)
  (spm: Array (SpV Int))
  (spv: SpV Int) return (u: Unit)
  ensures out.size = spm.size
  ensures ∀ i < spm.size, out[i]! = spv_dot spm[i]! spv 0 0
  do
    out := Array.replicate spm.size 0
    let mut spmInd := Array.replicate spm.size 0
    let mut spvInd := Array.replicate spm.size 0
    while_some i :| i < spm.size ∧ spmInd[i]! < spm[i]!.size ∧ spvInd[i]! < spv.size
    invariant spvInd.size = spm.size
    invariant spmInd.size = spm.size
    invariant out.size = spm.size
    invariant ∀ i < spmInd.size, spmInd[i]! <= spm[i]!.size
    invariant ∀ i < spvInd.size, spvInd[i]! <= spv.size
    invariant ∀ i < spm.size, out[i]! + spv_dot spm[i]! spv spmInd[i]! spvInd[i]! = spv_dot spm[i]! spv 0 0
    done_with ∀ i < spm.size, spmInd[i]! = spm[i]!.size ∨ spvInd[i]! = spv.size
    do
      let ind_m := spmInd[i]!
      let ind_v := spvInd[i]!
      if spm[i]!.ind[ind_m]! = spv.ind[ind_v]! then
        out[i] += spm[i]!.val[ind_m]! * spv.val[ind_v]!
        spmInd[i] += 1
        spvInd[i] += 1
      else
        if spm[i]!.ind[ind_m]! < spv.ind[ind_v]! then
          spmInd[i] += 1
        else
          spvInd[i] += 1
    return
</local_ctx>

<target_theorem>
theorem SpMSpV_correct_triple
  (out: Array Int)
  (spm: Array (SpV Int))
  (spv: SpV Int)
  (n: ℕ):
  triple
    (∀ i < spm.size, (∀ j < spm[i]!.size, spm[i]!.ind[j]! < n) ∧ (∀ j < spv.size, spv.ind[j]! < n))
    (SpMSpV out spm spv)
    fun ⟨_, outNew⟩ =>
      outNew.size = spm.size ∧ ∀ i < spm.size, outNew[i]! = ∑ idx ∈ Finset.range n, spm[i]![idx]! * spv[idx]! :=
</target_theorem>

