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>
def main : IO Unit :=
  IO.println "Hello, World !"

inductive ArStep: (val: V -> Int) -> (ArExpr V) -> (ArExpr V) -> Prop where
    | getVarValue (var: V) :
        ArStep
            val
            (ArExpr.Var var)
            (ArExpr.Const (val var))
    | addConstConst(n₁ n₂: Int) :
        ArStep
            val
            (ArExpr.Add (ArExpr.Const n₁) (ArExpr.Const n₂))
            (ArExpr.Const (n₁ + n₂))
    | subConstConst(n₁ n₂: Int) :
        ArStep
            val
            (ArExpr.Sub (ArExpr.Const n₁) (ArExpr.Const n₂))
            (ArExpr.Const (n₁ - n₂))
    | mulConstConst(n₁ n₂: Int) :
        ArStep
            val
            (ArExpr.Mul (ArExpr.Const n₁) (ArExpr.Const n₂))
            (ArExpr.Const (n₁ * n₂))
    | addLeft (e₁ e₁' e₂) : ArStep val e₁ e₁' -> ArStep val (ArExpr.Add e₁ e₂) (ArExpr.Add e₁' e₂)

    | subLeft (e₁ e₁' e₂) : ArStep val e₁ e₁' -> ArStep val (ArExpr.Sub e₁ e₂) (ArExpr.Sub e₁' e₂)

    | mulLeft (e₁ e₁' e₂) : ArStep val e₁ e₁' -> ArStep val (ArExpr.Mul e₁ e₂) (ArExpr.Mul e₁' e₂)

    | addRight (n: Int) (e₂ e₂': ArExpr V) : ArStep val e₂ e₂' -> ArStep val (ArExpr.Add (ArExpr.Const n) e₂)  (ArExpr.Add (ArExpr.Const n) e₂')

    | subRight (n: Int) (e₂ e₂': ArExpr V) : ArStep val e₂ e₂' -> ArStep val (ArExpr.Sub (ArExpr.Const n) e₂)  (ArExpr.Sub (ArExpr.Const n) e₂')
    | mulRight (n: Int) (e₂ e₂': ArExpr V) : ArStep val e₂ e₂' -> ArStep val (ArExpr.Mul (ArExpr.Const n) e₂)  (ArExpr.Mul (ArExpr.Const n) e₂')

    | ifStep (e e': BoolExpr V) (a b : ArExpr V): BoolStep val e e' ->
        ArStep val (ArExpr.If e a b) (ArExpr.If e' a b)
    | ifCondTrue (a b: ArExpr V) : ArStep val (ArExpr.If (BoolExpr.Const true) a b) a
    | ifCondFalse (a b: ArExpr V) : ArStep val (ArExpr.If (BoolExpr.Const false) a b) b

inductive BoolStep: (val: V -> Int) -> (BoolExpr V) -> (BoolExpr V) -> Prop where
    | notIsBoolNot (b: Bool): BoolStep val
        (BoolExpr.Not (BoolExpr.Const b))
        (BoolExpr.Const !b)
    | andLeftTrue (e: BoolExpr V): BoolStep val
        (BoolExpr.And (BoolExpr.Const true) e)
        e
    | orLeftFalse (e: BoolExpr V): BoolStep val
        (BoolExpr.Or (BoolExpr.Const false) e)
        e
    | andLeftShortCircuit e : BoolStep val
        (BoolExpr.And (BoolExpr.Const false) e)
        (BoolExpr.Const false)
    | orLeftShortCircuit e : BoolStep val
        (BoolExpr.Or (BoolExpr.Const true) e)
        (BoolExpr.Const true)
    | lessConstConstTrue n₁ n₂ : n₁ < n₂ -> BoolStep val
        (BoolExpr.Less (ArExpr.Const n₁) (ArExpr.Const n₂))
        (BoolExpr.Const true)
    | lessConstConstFalse n₁ n₂ : n₁ >= n₂ -> BoolStep val
        (BoolExpr.Less (ArExpr.Const n₁) (ArExpr.Const n₂))
        (BoolExpr.Const false)
    | eqConstConstTrue n₁ n₂ : n₁ = n₂ -> BoolStep val
        (BoolExpr.Eq (ArExpr.Const n₁) (ArExpr.Const n₂))
        (BoolExpr.Const true)
    | eqConstConstFalse n₁ n₂ : n₁ != n₂ -> BoolStep val
        (BoolExpr.Eq (ArExpr.Const n₁) (ArExpr.Const n₂))
        (BoolExpr.Const false)
    | lessArStepLeft (e₁ e₁' e₂: ArExpr V):
        ArStep val e₁ e₁' ->
            BoolStep val
                (BoolExpr.Less e₁ e₂)
                (BoolExpr.Less e₁' e₂)
    | eqArStepLeft (e₁ e₁' e₂: ArExpr V):
        ArStep val e₁ e₁' ->
            BoolStep val
                (BoolExpr.Eq e₁ e₂)
                (BoolExpr.Eq e₁' e₂)
     | lessArStepRight (e₁ e₂ e₂': ArExpr V):
        ArStep val e₂ e₂' ->
            BoolStep val
                (BoolExpr.Less e₁ e₂)
                (BoolExpr.Less e₁ e₂')
    | eqArStepRight (e₁ e₂ e₂': ArExpr V):
        ArStep val e₂ e₂' ->
            BoolStep val
                (BoolExpr.Eq e₁ e₂)
                (BoolExpr.Eq e₁ e₂')
    | orStepLeft (e₁ e₁' e₂: BoolExpr V):
        BoolStep val e₁ e₁' ->
            BoolStep val
                (BoolExpr.Or e₁ e₂)
                (BoolExpr.Or e₁' e₂)
    | andStepLeft (e₁ e₁' e₂: BoolExpr V):
        BoolStep val e₁ e₁' ->
            BoolStep val
                (BoolExpr.And e₁ e₂)
                (BoolExpr.And e₁' e₂)
    | notStep (e e' : BoolExpr V):
        BoolStep val e e' -> BoolStep val
            (BoolExpr.Not e)
            (BoolExpr.Not e')

def ArStepStar (V: Type) := StepStar (Step := ArStep V) V

def ArStepStar.refl {V: Type} (val: V -> Int) := StepStar.refl (Step := ArStep V) val

def ArStepStar.trans {V: Type} {val: V -> Int} e₁ e₂ e₃ := StepStar.trans e₁ e₂ e₃ (Step := ArStep V) (val := val)

def BoolStepStar (V: Type) := StepStar (Step := BoolStep V) V

def BoolStepStar.refl {V: Type} (val: V -> Int) := StepStar.refl (Step := BoolStep V) val

def BoolStepStar.trans {V: Type} {val: V -> Int} e₁ e₂ e₃ := StepStar.trans e₁ e₂ e₃ (Step := BoolStep V) (val := val)

    inductive ArExpr: Type
        | Const: Int -> ArExpr
        | Add: ArExpr -> ArExpr -> ArExpr
        | Sub: ArExpr -> ArExpr -> ArExpr
        | Mul: ArExpr -> ArExpr -> ArExpr
        | Var: V -> ArExpr
        | If : BoolExpr -> ArExpr -> ArExpr -> ArExpr

    inductive BoolExpr : Type
        | Const: Bool -> BoolExpr
        | Less: ArExpr -> ArExpr -> BoolExpr
        | Eq: ArExpr -> ArExpr -> BoolExpr
        | Not : BoolExpr -> BoolExpr
        | And : BoolExpr -> BoolExpr -> BoolExpr
        | Or : BoolExpr -> BoolExpr -> BoolExpr

def StepKind (V: Type) (ExprType: Type):= (V -> Int) -> ExprType -> ExprType -> Prop

inductive StepStar {ExprType: Type} {Step: StepKind V ExprType} : (val: V -> Int) -> ExprType -> ExprType -> Prop where
        | refl val e : StepStar val e e
        | trans e₁ e₂ e₃ : Step val e₁ e₂ -> StepStar val e₂ e₃ -> StepStar val e₁ e₃

    def eval_bool (val: V -> Int) (e: BoolExpr V): Bool :=
        match e with
        | BoolExpr.Const b => b
        | BoolExpr.Less l r =>  (eval val l) < (eval val r)
        | BoolExpr.Eq l r => (eval val l) == (eval val r)
        | BoolExpr.Not e => not (eval_bool val e)
        | BoolExpr.And l r => if eval_bool val l then eval_bool val r else false
        | BoolExpr.Or l r => if eval_bool val l then true else eval_bool val r

    def eval (val: V -> Int) (e: ArExpr V) : Int :=
        match e with
            | ArExpr.Const x => x
            | ArExpr.Add lhs rhs => (eval val lhs) + (eval val rhs)
            | ArExpr.Sub lhs rhs => (eval val lhs) - (eval val rhs)
            | ArExpr.Mul lhs rhs => (eval val lhs) * (eval val rhs)
            | ArExpr.Var v => val v
            | ArExpr.If cond then_e else_e => if eval_bool val cond then eval val then_e else eval val else_e

IO in Init.System.IO

Unit in Init.Prelude

IO.println in Init.System.IO

Int in Init.Data.Int.Basic

Bool in Init.Prelude

Add in Init.Prelude

Mul in Init.Prelude

Sub in Init.Prelude

And in Init.Prelude

Eq in Init.Prelude

Not in Init.Prelude

Or in Init.Prelude
</all_available_defs>

<all_available_lemmas>
theorem eval_soundness (e: ArExpr V) (v: Int) :
    ArStepStar V val e (ArExpr.Const v) -> eval V val e = v

theorem eval_bool_soundness (e: BoolExpr V) (b: Bool) :
    BoolStepStar V val e (BoolExpr.Const b) -> eval_bool V val e = b

theorem chasles_step_star {ExprKind: Type} {Step: StepKind V ExprKind} {e₁ e₂ e₃: ExprKind}:
    StepStar (Step := Step) V val e₁ e₂  ->
        StepStar (Step := Step) V val e₂ e₃ ->
            StepStar (Step := Step) V val e₁ e₃

theorem step_to_stepstar {ExprKind: Type} {Step: StepKind V ExprKind} {e e': ExprKind}:
    Step val e e' -> StepStar (Step := Step) V val e e'
</all_available_lemmas>

<local_ctx>
import ExprEval.Expr

import ExprEval.Steps
</local_ctx>

<target_theorem>
theorem boolstep_preserves_eval_bool (e e': BoolExpr V):
        BoolStep V val e e' -> eval_bool V val e = eval_bool V val e' :=
</target_theorem>

