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>
DecidableEq in Init.Prelude
Lean.ToExpr in Lean.ToExpr
List in Init.Prelude
Repr in Init.Data.Repr
Nat in Init.Prelude
String in Init.Prelude
BEq in Init.Prelude
ite in Init.Prelude
Vector in Init.Data.Vector.Basic
Bool in Init.Prelude
Int in Init.Data.Int.Basic
bool in Init.Control.Basic
Computation in Mathlib.Data.Seq.Computation
Id in Init.Control.Id
List.map in Init.Prelude
PUnit in Init.Prelude
Pure in Init.Prelude
And in Init.Prelude
Prod in Init.Prelude
Prod.mk in Init.Prelude

macro "simp_peephole" loc:(location)? : tactic =>
  `(tactic|(
      
      first
      | rw [funext_iff (α := Ctxt.Valuation _)] $[$loc]?
      | change ∀ (_ : Ctxt.Valuation _), _ $[$loc]?
      | skip

simp (config := {failIfUnchanged := false}) only
        [Expr.denote_castPureToEff, simp_denote] $[$loc]?
      
      
      
  ))

@[match_pattern]
def cons (hd : Ty) : Ctxt Ty → Ctxt Ty
| ⟨tl⟩ => ⟨hd :: tl⟩

structure Ctxt (Ty : Type) : Type where
  ofList :: toList : List Ty
  
  deriving Repr, Lean.ToExpr, DecidableEq

def Var (Γ : Ctxt Ty) (t : Ty) : Type :=
  { i : Nat // Γ[i]? = some t }

protected instance Expr.decidableEq [DecidableEq d.Op] [DecidableEq d.Ty] :
    {Γ : Ctxt d.Ty} → {ty : List d.Ty} → DecidableEq (Expr d Γ eff ty)
  | Γ, _, .mk op₁ rfl eff_le₁ arg₁ regArgs₁, .mk op₂ eq eff_le₂ arg₂ regArgs₂ =>
    if ho : op₁ = op₂ then by
      subst ho
      letI := HVector.decidableEq arg₁ arg₂
      letI := HVector.decidableEqReg regArgs₁ regArgs₂
      exact decidable_of_iff (arg₁ = arg₂ ∧ regArgs₁ = regArgs₂) (by admit /- proof elided -/
      )
    else isFalse (by admit /- proof elided -/
    )

def Var (Γ : Context Ty) (ty : Ty) : Type := { v : VarName // Γ.hasType v ty }

protected instance HVector.decidableEqReg [DecidableEq d.Op] [DecidableEq d.Ty] :
    ∀ {l : RegionSignature d.Ty}, DecidableEq (HVector (fun t => Com d t.1 .impure t.2) l)
  | _, .nil, .nil => isTrue rfl
  | _, .cons x₁ v₁, .cons x₂ v₂ =>
    letI := HVector.decidableEqReg v₁ v₂
    letI := Com.decidableEq x₁ x₂
    decidable_of_iff (x₁ = x₂ ∧ v₁ = v₂) (by admit /- proof elided -/
    )

inductive Com : Ctxt d.Ty → EffectKind → List d.Ty → Type where
  | rets {Γ} {tys} {eff : EffectKind} (vs : HVector Γ.Var tys) : Com Γ eff tys
  | var (e : Expr Γ eff ty) (body : Com (ty ++ Γ) eff β) : Com Γ eff β

structure FlatCom (d : Dialect) [DialectSignature d]  (Γ_in : Ctxt d.Ty) (eff : EffectKind)
    (Γ_out : Ctxt d.Ty) (ts : List d.Ty) where
  lets : Lets d Γ_in eff Γ_out
  rets : HVector Γ_out.Var ts

inductive Lets (Γ_in : Ctxt d.Ty) (eff : EffectKind) :
    (Γ_out : Ctxt d.Ty) → Type where
  | nil : Lets Γ_in eff Γ_in
  | var (body : Lets Γ_in eff Γ_out) (e : Expr d Γ_out eff t) : Lets Γ_in eff e.outContext

inductive EffectKind
| pure 
| impure 
deriving Repr, DecidableEq, Lean.ToExpr

class DialectDenote (d : Dialect) [TyDenote d.Ty] [DialectSignature d] where
  denote : (op : d.Op) → HVector toType (DialectSignature.sig op) →
    (HVector (fun t : Ctxt d.Ty × List d.Ty =>
      t.1.Valuation
      → EffectKind.impure.toMonad d.m (HVector toType t.2))
            (DialectSignature.regSig op)) →
    ((DialectSignature.effectKind op).toMonad d.m
      (HVector toType <| DialectSignature.returnTypes op))

def sig          := Signature.sig ∘ s.signature

structure Signature (Ty : Type) where
  mkEffectful ::
  sig         : List Ty
  regSig      : RegionSignature Ty
  returnTypes : List Ty
  effectKind  : EffectKind := .pure

class DialectSignature (d : Dialect) where
  signature : d.Op → Signature d.Ty

def regSig       := Signature.regSig ∘ s.signature

abbrev RegionSignature Ty := List (Ctxt Ty × List Ty)

inductive Ty (q : Nat) (n : Nat)
  | index : Ty q n
  | integer : Ty q n
  | tensor : Ty q n
  | polynomialLike : Ty q n
  deriving DecidableEq, Repr

def effectKind   := Signature.effectKind ∘ s.signature

def returnTypes  := Signature.returnTypes ∘ s.signature

structure Dialect where
  (Op : Type)
  (Ty : Type)
  (m : Type → Type := Id)

inductive Op (q : Nat) (n : Nat)
  | add : Op q n
  | sub : Op q n
  | mul : Op q n
  | mul_constant : Op q n
    
    
  | leading_term : Op q n
  | monomial : Op q n
  | monomial_mul : Op q n
  | from_tensor : Op q n
  | to_tensor : Op q n
  | const (c : R q n) : Op q n
  | const_int (c : Int) : Op q n
  | const_idx (i : Nat) : Op q n

class TyDenote (β : Type) : Type 1 where
  toType : β → Type

@[simp]
instance Valuation.instAppendHVector (Γ : Ctxt Ty) (ts : List Ty) :
    HAppend (HVector toType ts) (Valuation Γ) (Valuation <| ⟨ts⟩ ++ Γ) where
  hAppend vals V :=
    (Valuation.ofHVector vals) ++ V

inductive Ty
  | int
   
  | int2
  deriving DecidableEq, Lean.ToExpr

inductive Op
  | noop
  | mkPair
  | unPair
  deriving Lean.ToExpr

def Com.ret {Γ : Ctxt d.Ty} {ty : d.Ty} {eff : EffectKind} : Γ.Var ty → Com d Γ eff [ty] :=
  (Com.rets [·]ₕ)

def Com.letPure (e : Expr d Γ .pure t) (body : Com d (e.outContext) eff u) : Com d Γ eff u :=
  body.var (e.castPureToEff eff)

abbrev Expr.outContext (_ : Expr d Γ eff ts) : Ctxt d.Ty :=
  ts ++ Γ

def Expr.castPureToEff (eff : EffectKind) : Expr d Γ .pure t → Expr d Γ eff t :=
  changeEffect (EffectKind.pure_le eff)

def Expr.changeEffect {eff₁ eff₂ : EffectKind} (h : eff₁ ≤ eff₂) :
    Expr d Γ eff₁ t → Expr d Γ eff₂ t
  | Expr.mk op ty_eq eff_le args regArgs =>
    have heff : DialectSignature.effectKind op ≤ eff₂ := by admit /- proof elided -/

def Expr.args {Γ ts} (e : Expr d Γ eff ts) :
    HVector (Var Γ) (DialectSignature.sig e.op) :=
  Expr.casesOn e (fun _ _ _ args _ => args)

def Expr.regArgs {Γ ts} (e : Expr d Γ eff ts) :
    Regions d (DialectSignature.regSig e.op) :=
  Expr.casesOn e (fun _ _ _ _ regArgs => regArgs)

abbrev Regions (regSig : RegionSignature d.Ty) : Type :=
  HVector (fun t => Com d t.1 .impure t.2) regSig

def Expr.op {Γ : Ctxt d.Ty} {eff : EffectKind} {ty} (e : Expr d Γ eff ty) : d.Op :=
  Expr.casesOn e (fun op _ _ _ _ => op)

def Com.denote : Com d Γ eff ty → (Γv : Valuation Γ) →
    eff.toMonad d.m (HVector toType ty)
  | .rets vs, Γv     => pure (vs.map Γv)
  | .var e body, V => e.denote V >>= body.denote

def Lets.denote [DialectSignature d] [DialectDenote d] {Γ₂}
    (lets : Lets d Γ₁ eff Γ₂) (V : Valuation Γ₁) : (eff.toMonad d.m <| Valuation Γ₂) :=
  match lets with
  | .nil          => return V
  | .var lets' e  => lets'.denote V >>= e.denote

def HVector.denote :
    {l : RegionSignature d.Ty} → (T : HVector (fun t => Com d t.1 .impure t.2) l) →
    HVector (fun t => t.1.Valuation → EffectKind.impure.toMonad d.m (HVector toType t.2)) l
  | _, .nil => HVector.nil
  | _, .cons v vs => HVector.cons (v.denote) (HVector.denote vs)

@[simp] abbrev FlatCom.denote [DialectDenote d]
    (flatCom : FlatCom d Γ eff Γ_out ts)
    (V : Γ.Valuation) : eff.toMonad d.m (HVector toType ts) :=
  flatCom.lets.denote V >>= (return flatCom.rets.map ·)

def RegionSignature.map (f : Ty → Ty') : RegionSignature Ty → RegionSignature Ty' :=
  List.map fun ⟨Γ, ty⟩ => (Γ.map f, ty.map f)

def Signature.map (f : Ty → Ty') : Signature Ty → Signature Ty' :=
  fun sig => {
    sig         := sig.sig.map f
    regSig      := sig.regSig.map f
    returnTypes := sig.returnTypes.map f
  }

def map (f : Ty₁ → Ty₂) : Ctxt Ty₁ → Ctxt Ty₂ :=
  ofList ∘ (List.map f) ∘ toList

def Expr.denote {ty} (e : Expr d Γ eff ty) (V : Valuation Γ) :
    eff.toMonad d.m (e.outContext.Valuation) :=
  match e with
  | ⟨op, ty_eq, heff, args, regArgs⟩ => do
      let argsDenote := args.map V
      let val ← EffectKind.liftEffect heff <| DialectDenote.denote op argsDenote regArgs.denote
      return (val ++ V).cast (by admit /- proof elided -/
      )

def Com.outContext {Γ} : Com d Γ eff ts → Ctxt d.Ty :=
  Com.rec' (motive := fun _ => Ctxt d.Ty)
    (@fun Γ _ => Γ) 
    (fun _ _ r => r)

def Com.rec' {Γ} (com : Com d Γ eff t) : motive com :=
   
  Com.rec
    (motive_1 := fun _ _ _ _ => PUnit)
    (motive_2 := fun _ eff' t' c =>
      (h₁ : eff = eff') → (h₂ : t = t') → motive (h₁ ▸ h₂ ▸ c))
    (motive_3 := fun _ _ => PUnit)
    (fun _ _ _ _ _ _ => ⟨⟩) 
    (fun v h₁ h₂ => 
      cast (by admit /- proof elided -/
      ) <| rets (h₂ ▸ v))
    (fun e' body' _ r' h₁ h₂ => 
      let e := h₁ ▸ e'
      let body : Com _ _ eff t := cast (by admit /- proof elided -/
      ) body'
      let r : motive body := cast (by admit /- proof elided -/
      ) (r' h₁ h₂)
      cast (by admit /- proof elided -/
      ) <| var e body r)
    ⟨⟩
    (fun _ _ _ _ => ⟨⟩)
    com
    rfl
    rfl

def Valuation.cast {Γ Δ : Ctxt Ty} (h : Γ = Δ) (V : Valuation Γ) : Valuation Δ :=
  fun _ v => V <| v.castCtxt h.symm

def liftEffect [Pure m] {e1 e2 : EffectKind} {α : Type}
    (hle : e1 ≤ e2) (v1 : e1.toMonad m α) : e2.toMonad m α :=
  match e1, e2, hle with
    | .pure, .pure, _ | .impure, .impure, _ => v1
    | .pure, .impure, _ => Pure.pure v1

def toMonad (e : EffectKind) (m : Type → Type) : Type → Type :=
  match e with
  | pure => Id
  | impure => m

def Valuation.nil : Ctxt.Valuation (∅ : Ctxt Ty) := fun _ v => v.emptyElim

def Valuation.cons {Γ : Ctxt Ty} {t : Ty} (x : toType t) (V : Γ.Valuation) :
    (Γ.cons t).Valuation :=

def Com.ty : Com d Γ eff [t] → d.Ty := fun _ => t

infixr:50 "::ₕ" => HVector.cons

notation "⟦" x "⟧" => TyDenote.toType x

infixr:67 "::ᵥ" => Valuation.cons

def add_mask_ashr28_i32_after := [llvm|
{
^0(%arg2 : i32):
  %0 = llvm.mlir.constant(28 : i32) : i32
  %1 = llvm.mlir.constant(7 : i32) : i32
  %2 = llvm.lshr %arg2, %0 : i32
  %3 = llvm.and %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

instance : DialectToExpr Comb where
  toExprM := .const ``Id [0]
  toExprDialect := .const ``Comb []

def icmp_ule_after := [llvm|
{
^0(%arg49 : i32, %arg50 : i32):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def or_basic_after := [llvm|
{
^0(%arg15 : i16):
  %0 = llvm.mlir.constant(17791 : i16) : i16
  %1 = llvm.icmp "ne" %arg15, %0 : i16
  "llvm.return"(%1) : (i1) -> ()
}
]

def logical_and_bitwise_and_icmps_before := [llvm|
{
^0(%arg220 : i8, %arg221 : i8, %arg222 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.mlir.constant(1 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.mlir.constant(false) : i1
  %4 = llvm.icmp "eq" %arg221, %0 : i8
  %5 = llvm.and %arg220, %1 : i8
  %6 = llvm.shl %1, %arg222 : i8
  %7 = llvm.and %arg220, %6 : i8
  %8 = llvm.icmp "ne" %5, %2 : i8
  %9 = llvm.icmp "ne" %7, %2 : i8
  %10 = llvm.and %4, %8 : i1
  %11 = "llvm.select"(%10, %9, %3) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%11) : (i1) -> ()
}
]

def ule_or_min_after := [llvm|
{
^0(%arg142 : i8, %arg143 : i8):
  %0 = llvm.icmp "ule" %arg142, %arg143 : i8
  "llvm.return"(%0) : (i1) -> ()
}
]

def neg_mask_after := [llvm|
{
^0(%arg1 : i32, %arg2 : i16):
  %0 = llvm.mlir.constant(0 : i16) : i16
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.sext %arg2 : i16 to i32
  %3 = llvm.sub %arg1, %2 overflow<nsw> : i32
  %4 = llvm.icmp "slt" %arg2, %0 : i16
  %5 = "llvm.select"(%4, %3, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def ashrslt_03_09_before := [llvm|
{
^0(%arg228 : i4):
  %0 = llvm.mlir.constant(3 : i4) : i4
  %1 = llvm.mlir.constant(-7 : i4) : i4
  %2 = llvm.ashr %arg228, %0 : i4
  %3 = llvm.icmp "slt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

def ashrsgt_01_02_after := [llvm|
{
^0(%arg315 : i4):
  %0 = llvm.mlir.constant(5 : i4) : i4
  %1 = llvm.icmp "sgt" %arg315, %0 : i4
  "llvm.return"(%1) : (i1) -> ()
}
]

def lshrugt_03_11_exact_after := [llvm|
{
^0(%arg178 : i4):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def PR42691_2_logical_after := [llvm|
{
^0(%arg340 : i32):
  %0 = llvm.mlir.constant(-2 : i32) : i32
  %1 = llvm.icmp "sgt" %arg340, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def add_nsw_poison_constant_fold_after := [llvm|
{
^0(%arg2 : i1, %arg3 : i8):
  %0 = llvm.mlir.constant(64 : i8) : i8
  %1 = llvm.mlir.constant(-127 : i8) : i8
  %2 = llvm.add %arg3, %0 overflow<nsw> : i8
  %3 = "llvm.select"(%arg2, %2, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def uaddo_commute8_after := [llvm|
{
^0(%arg10 : i32, %arg11 : i32, %arg12 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.xor %arg11, %0 : i32
  %2 = llvm.add %arg11, %arg10 : i32
  %3 = llvm.icmp "ugt" %arg10, %1 : i32
  %4 = "llvm.select"(%3, %2, %arg12) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def t4_ugt_slt_65536_before := [llvm|
{
^0(%arg54 : i32, %arg55 : i32, %arg56 : i32):
  %0 = llvm.mlir.constant(65536 : i32) : i32
  %1 = llvm.mlir.constant(65535 : i32) : i32
  %2 = llvm.icmp "slt" %arg54, %0 : i32
  %3 = "llvm.select"(%2, %arg55, %arg56) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %4 = llvm.icmp "ugt" %arg54, %1 : i32
  %5 = "llvm.select"(%4, %3, %arg54) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def trunc_lshr_zext_after := [llvm|
{
^0(%arg12 : i8):
  %0 = llvm.mlir.constant(6 : i8) : i8
  %1 = llvm.lshr %arg12, %0 : i8
  "llvm.return"(%1) : (i8) -> ()
}
]

def and_add_bool_no_fold_before := [llvm|
{
^0(%arg4 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.and %arg4, %0 : i32
  %3 = llvm.add %1, %2 : i32
  %4 = llvm.and %3, %arg4 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def add_nsw_mul_nsw_after := [llvm|
{
^0(%arg33 : i16):
  %0 = llvm.mlir.constant(3 : i16) : i16
  %1 = llvm.mul %arg33, %0 overflow<nsw> : i16
  "llvm.return"(%1) : (i16) -> ()
}
]

def t6_shl_before := [llvm|
{
^0(%arg31 : i32, %arg32 : i32):
  %0 = llvm.mlir.constant(32 : i32) : i32
  %1 = llvm.mlir.constant(-2 : i32) : i32
  %2 = llvm.sub %0, %arg32 : i32
  %3 = llvm.shl %arg31, %2 overflow<nuw> : i32
  %4 = llvm.add %arg32, %1 : i32
  %5 = llvm.shl %3, %4 overflow<nsw> : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def q : Nat := 42

def test_add_sub_const_lhs_RHS := [mod_arith q, hq| {
  ^bb0(%x : !R):
    %res0 = mod_arith.constant 4 : !R
    %res1 = mod_arith.sub %res0, %x : !R
    return %res1 : !R
}]

def main4f_like_logical_after := [llvm|
{
^0(%arg115 : i32, %arg116 : i32, %arg117 : i32):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.and %arg115, %arg116 : i32
  %2 = llvm.icmp "eq" %1, %arg116 : i32
  %3 = llvm.and %arg115, %arg117 : i32
  %4 = llvm.icmp "eq" %3, %arg117 : i32
  %5 = "llvm.select"(%2, %4, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %6 = llvm.zext %5 : i1 to i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def test13_after := [llvm|
{
^0(%arg10 : i79):
  %0 = llvm.mlir.constant(78 : i79) : i79
  %1 = llvm.ashr %arg10, %0 : i79
  "llvm.return"(%1) : (i79) -> ()
}
]

def negate_ashr_after := [llvm|
{
^0(%arg110 : i8, %arg111 : i8):
  %0 = llvm.mlir.constant(7 : i8) : i8
  %1 = llvm.lshr %arg111, %0 : i8
  %2 = llvm.add %1, %arg110 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def t4_c1_before := [llvm|
{
^0(%arg23 : i8, %arg24 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.sub %arg23, %0 : i8
  %2 = llvm.sub %1, %arg24 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def getOutputWidth (opStx : MLIR.AST.Op 0) :
    Except TransformError Nat := do
  match opStx.res with
  | res::[] =>
    match res.2 with
    | .int _ (.concrete w) => pure w
    | _ => throw <| .generic s!"The operation {opStx.name} must output an integer type"
  | _ => throw <| .generic s!"The operation {opStx.name} must have a single output"

def tryFactorization_add_nuw_mul_nuw_mul_nuw_var_after := [llvm|
{
^0(%arg9 : i32, %arg10 : i32, %arg11 : i32):
  %0 = llvm.add %arg10, %arg11 : i32
  %1 = llvm.mul %arg9, %0 overflow<nuw> : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def ule_swap_or_not_min_commute_logical_before := [llvm|
{
^0(%arg258 : i8, %arg259 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.mlir.constant(true) : i1
  %2 = llvm.icmp "uge" %arg259, %arg258 : i8
  %3 = llvm.icmp "ne" %arg258, %0 : i8
  %4 = "llvm.select"(%3, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%4) : (i1) -> ()
}
]

def test68_before := [llvm|
{
^0(%arg166 : i32, %arg167 : i32):
  %0 = llvm.mlir.constant(128 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(2 : i32) : i32
  %3 = llvm.and %arg166, %0 : i32
  %4 = llvm.icmp "eq" %3, %1 : i32
  %5 = llvm.or %arg167, %2 : i32
  %6 = "llvm.select"(%4, %arg167, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def masked_or_A_slightly_optimized_after := [llvm|
{
^0(%arg119 : i32):
  %0 = llvm.mlir.constant(-40 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.and %arg119, %0 : i32
  %3 = llvm.icmp "eq" %2, %1 : i32
  "llvm.return"(%3) : (i1) -> ()
}
]

def lshrult_02_06_exact_before := [llvm|
{
^0(%arg127 : i4):
  %0 = llvm.mlir.constant(2 : i4) : i4
  %1 = llvm.mlir.constant(6 : i4) : i4
  %2 = llvm.lshr exact %arg127, %0 : i4
  %3 = llvm.icmp "ult" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

instance [Monad m] : Monad (e.toMonad m) :=

def eq_umax1_before := [llvm|
{
^0(%arg60 : i32, %arg61 : i32):
  %0 = llvm.icmp "ugt" %arg60, %arg61 : i32
  %1 = "llvm.select"(%0, %arg60, %arg61) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %2 = llvm.icmp "eq" %1, %arg60 : i32
  "llvm.return"(%2) : (i1) -> ()
}
]

def t2_before := [llvm|
{
^0(%arg30 : i8):
  %0 = llvm.mlir.constant(15 : i8) : i8
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.mlir.constant(-16 : i8) : i8
  %3 = llvm.and %arg30, %0 : i8
  %4 = llvm.icmp "eq" %3, %1 : i8
  %5 = llvm.add %arg30, %0 : i8
  %6 = llvm.and %5, %2 : i8
  %7 = "llvm.select"(%4, %arg30, %6) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%7) : (i8) -> ()
}
]

@[simp_denote]
def sll_llvm_i64 := [LV| {
    ^entry (%a: i64, %b: i64):
    %0 = llvm.shl %a, %b : i64
    llvm.return %0 : i64
  }]

def positive_sameconst_shlnsw_ashrexact_after := [llvm|
{
^0(%arg36 : i8):
  "llvm.return"(%arg36) : (i8) -> ()
}
]

def test5_before := [llvm|
{
^0(%arg303 : i32):
  %0 = llvm.and %arg303, %arg303 : i32
  "llvm.return"(%0) : (i32) -> ()
}
]

def ashrsgt_03_06_after := [llvm|
{
^0(%arg279 : i4):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def or_xor_tree_0110_before := [llvm|
{
^0(%arg27 : i32, %arg28 : i32, %arg29 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.mul %arg27, %0 : i32
  %2 = llvm.mul %arg28, %0 : i32
  %3 = llvm.mul %arg29, %0 : i32
  %4 = llvm.xor %1, %2 : i32
  %5 = llvm.xor %3, %2 : i32
  %6 = llvm.xor %1, %5 : i32
  %7 = llvm.or %4, %6 : i32
  "llvm.return"(%7) : (i32) -> ()
}
]

def bigAnd (constraints : List (BoolExpr α)) : BoolExpr α :=
  foldConstraints (BoolExpr.const true) constraints Gate.and

instance : Monad SLLVM.m :=

def main6d_after := [llvm|
{
^0(%arg88 : i32):
  %0 = llvm.mlir.constant(23 : i32) : i32
  %1 = llvm.mlir.constant(19 : i32) : i32
  %2 = llvm.and %arg88, %0 : i32
  %3 = llvm.icmp "eq" %2, %1 : i32
  %4 = llvm.zext %3 : i1 to i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def land_land_right1_after := [llvm|
{
^0(%arg54 : i1, %arg55 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = "llvm.select"(%arg54, %arg55, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%1) : (i1) -> ()
}
]

def or_and_or_pat1_before := [llvm|
{
^0(%arg38 : i8, %arg39 : i8, %arg40 : i8, %arg41 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.udiv %0, %arg40 : i8
  %2 = llvm.and %arg38, %arg39 : i8
  %3 = llvm.and %arg38, %arg41 : i8
  %4 = llvm.or %1, %3 : i8
  %5 = llvm.or %2, %4 : i8
  "llvm.return"(%5) : (i8) -> ()
}
]

def two_inst_macro_proof (w : Nat) :
    two_inst_macro w ⊑ two_inst_macro w :=

def addMax (a : BitVec v) (b : BitVec w) : BitVec (max v w + 1) :=
   a.signExtend _ + b.signExtend _

def uge_swap_and_max_commute_before := [llvm|
{
^0(%arg226 : i8, %arg227 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.icmp "ule" %arg227, %arg226 : i8
  %2 = llvm.icmp "eq" %arg226, %0 : i8
  %3 = llvm.and %2, %1 : i1
  "llvm.return"(%3) : (i1) -> ()
}
]

def icmp_shl_nsw_sge1_after := [llvm|
{
^0(%arg28 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "sgt" %arg28, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def or_or_xor_commute1_before := [llvm|
{
^0(%arg103 : i4, %arg104 : i4, %arg105 : i4):
  %0 = llvm.or %arg103, %arg105 : i4
  %1 = llvm.or %arg105, %arg104 : i4
  %2 = llvm.xor %0, %1 : i4
  "llvm.return"(%2) : (i4) -> ()
}
]

def t7_before := [llvm|
{
^0(%arg6 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg6 overflow<nsw> : i8
  %2 = llvm.icmp "ule" %1, %arg6 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def test9a_after := [llvm|
{
^0(%arg297 : i32):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.icmp "slt" %arg297, %0 : i32
  "llvm.return"(%1) : (i1) -> ()
}
]

def lshrugt_02_09_before := [llvm|
{
^0(%arg390 : i4):
  %0 = llvm.mlir.constant(2 : i4) : i4
  %1 = llvm.mlir.constant(-7 : i4) : i4
  %2 = llvm.lshr %arg390, %0 : i4
  %3 = llvm.icmp "ugt" %2, %1 : i4
  "llvm.return"(%3) : (i1) -> ()
}
]

Std.Format.align in Init.Data.Format.Basic

Lean.crossEmoji in Lean.Util.Trace
</all_available_defs>

<all_available_lemmas>
Function.comp_apply in Init.Core
Function.iterate_succ in Mathlib.Logic.Function.Iterate
Nat.cast_add in Mathlib.Data.Nat.Cast.Defs
Nat.cast_one in Mathlib.Data.Nat.Cast.Defs
and_true in Init.SimpLemmas
Int.mul_comm in Init.Data.Int.Lemmas
add_left_iterate in Mathlib.Algebra.Group.Basic
nsmul_eq_mul in Mathlib.Algebra.Ring.Defs

theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) :\n(l₁ ++ l₂)[i] = l₁[i]

theorem test8_thm (e : IntW 32) :
  icmp IntPred.ugt (LLVM.udiv (const? 32 4) e) (const? 32 3) ⊑ icmp IntPred.ult e (const? 32 2)

theorem reduce_xor_common_op_commute0_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 4),
  x_2 ^^^ x_1 ^^^ x ||

theorem flip_masked_bit_proof : flip_masked_bit_before ⊑ flip_masked_bit_after

theorem and_two_ranges_to_mask_and_range_proof : and_two_ranges_to_mask_and_range_before ⊑ and_two_ranges_to_mask_and_range_after

theorem e_485 :
     - 1 * (x ^^^ y) + 1 * (x |||  ~~~y) - 1 * (x ||| y) + 1 *  ~~~(x ^^^ y) + 4 * y - 9 *  ~~~(x ||| y) - 9 *  ~~~(x |||  ~~~y) + 1 * (x &&&  ~~~y) - 5 * (x &&& y) =  - 7 *  ~~~x

theorem masked_icmps_mask_notallzeros_bmask_mixed_swapped_5_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (x &&& 15#32 == 8#32) &&& ofBool (x &&& 15#32 != 0#32) = ofBool (x &&& 15#32 == 8#32)

theorem sext_xor_sub_thm.extracted_1._2 : ∀ (x : BitVec 1) (x_1 : BitVec 64),
  ¬x = 1#1 → (x_1 ^^^ signExtend 64 x) - signExtend 64 x = x_1

theorem bools2_logical_commute1_thm.extracted_1._3 : ∀ (x x_1 : BitVec 1),
  x_1 = 1#1 → ¬x ^^^ 1#1 = 1#1 → x = 1#1 → 1#1 = x_1

theorem demo2 (x : BitVec 64) : BitVec.zeroExtend 64 (BitVec.truncate 32 x) = x &&& 4294967295#64

theorem bools_multi_uses1_logical_proof : bools_multi_uses1_logical_before ⊑ bools_multi_uses1_logical_after

theorem icmp_ne_zext_eq_non_boolean_proof : icmp_ne_zext_eq_non_boolean_before ⊑ icmp_ne_zext_eq_non_boolean_after

theorem icmp_eq_sext_eq_zero_proof : icmp_eq_sext_eq_zero_before ⊑ icmp_eq_sext_eq_zero_after

theorem test_sub__nsw_is_safe_proof : test_sub__nsw_is_safe_before ⊑ test_sub__nsw_is_safe_after

theorem t10_shl_nuw_flag_preservation_proof : t10_shl_nuw_flag_preservation_before ⊑ t10_shl_nuw_flag_preservation_after

theorem lshrugt_01_13_proof : lshrugt_01_13_before ⊑ lshrugt_01_13_after

theorem n0_proof : n0_before ⊑ n0_after

theorem ule_or_not_min_thm.extracted_1._1 : ∀ (x x_1 : BitVec 427), ofBool (x_1 ≤ᵤ x) ||

theorem ashrslt_02_12_exact_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬(True ∧ x >>> 2#4 <<< 2#4 ≠ x ∨ 2#4 ≥ ↑4) → ofBool (x.sshiftRight' 2#4 <ₛ BitVec.ofInt 4 (-4)) = 0#1

theorem sub_mask1_lshr_thm (e : IntW 8) :
  sub (const? 8 10) (LLVM.and (lshr e (const? 8 1)) (const? 8 1)) ⊑
    add (ashr (shl e (const? 8 6)) (const? 8 7)) (const? 8 10) { «nsw» := true, «nuw» := false }

theorem scalar_i16_shl_ult_const_thm.extracted_1._1 : ∀ (x : BitVec 16),
  ¬8#16 ≥ ↑16 → ofBool (x <<< 8#16 <ᵤ 1024#16) = ofBool (x &&& 252#16 == 0#16)

theorem ashrslt_01_11_exact_thm (e : IntW 4) :
  icmp IntPred.slt (ashr e (const? 4 1) { «exact» := true }) (const? 4 (-5)) ⊑ const? 1 0

theorem p_commutative4_proof : p_commutative4_before ⊑ p_commutative4_after

theorem e_537 :
    2 *  ~~~(x &&& y) - 7 * y + 4 * (x ^^^ y) - 11 *  ~~~x - 2 * x + 5 * (x ||| y) - 6 *  ~~~(x ^^^ y) + 15 *  ~~~(x ||| y) + 10 * (x &&& y) = 9 * (x &&&  ~~~y) - 7 *  ~~~(x |||  ~~~y)

@[simp] theorem Valuation.comap_cons_consRight {Γ Δ : Ctxt Ty} (Γv : Valuation Γ) (f : Hom Δ Γ) :
    comap (Γv.cons x) (f.consRight) = comap Γv f

theorem test_thm.extracted_1._2 : ∀ (x : BitVec 31),
  ¬15#32 ≥ ↑32 →
    ¬(True ∧ (zeroExtend 32 x).uaddOverflow 16384#32 = true ∨ 15#32 ≥ ↑32) →
      truncate 16 ((signExtend 32 x + 16384#32) >>> 15#32) = truncate 16 ((zeroExtend 32 x + 16384#32) >>> 15#32)

theorem and_zext_thm.extracted_1._2 : ∀ (x : BitVec 1) (x_1 : BitVec 32), ¬x = 1#1 → x_1 &&& zeroExtend 32 x = 0#32

theorem narrow_zext_xor_proof : narrow_zext_xor_before ⊑ narrow_zext_xor_after

theorem test_zext1_thm (e e_1 : IntW 1) :
  select e_1 (zext 32 e) (const? 32 0) ⊑ zext 32 (select e_1 e (const? 1 0))

theorem XorZextXor_thm.extracted_1._1 : ∀ (x : BitVec 3), zeroExtend 5 (x ^^^ 3#3) ^^^ 12#5 = zeroExtend 5 x ^^^ 15#5

theorem test1_thm.extracted_1._1 : ∀ (x x_1 : BitVec 8), truncate 8 (zeroExtend 64 x_1 + zeroExtend 64 x) = x_1 + x

theorem e_1531 :
    1 * ((a &&& b) |||  ~~~(b |||  ~~~c)) + 3 * (c ||| (a &&&  ~~~b)) + 2 * (b ^^^  ~~~(a ||| c)) - 1 * (a ^^^ (b ^^^ c)) + 1 *  ~~~(a ||| ( ~~~b ||| c)) - 2 *  ~~~( ~~~a ||| (b ||| c)) - 4 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 4 * ( ~~~a &&& ( ~~~b &&& c)) - 6 * ( ~~~a &&& (b &&& c)) - 4 * (a &&& ( ~~~b &&& c)) - 5 * (a &&& (b &&& c)) =  - 1 * (c ^^^ (a &&& (b ||| c))) + 2 *  ~~~(a ||| (b ||| c))

theorem eq_21_comm_eq_thm.extracted_1._2 : ∀ (x x_1 : BitVec 32),
  ¬(16#32 ≥ ↑32 ∨ 16#32 ≥ ↑32 ∨ 8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) →
    ¬(8#32 ≥ ↑32 ∨ 8#32 ≥ ↑32) →
      ofBool (truncate 8 (x_1 >>> 16#32) == truncate 8 (x >>> 16#32)) &&&
          ofBool (truncate 8 (x >>> 8#32) == truncate 8 (x_1 >>> 8#32)) =
        ofBool (truncate 16 (x_1 >>> 8#32) == truncate 16 (x >>> 8#32))

theorem select_1_thm.extracted_1._15 : ∀ (x x_1 : BitVec 8) (x_2 x_3 : BitVec 1),
  ¬x_3 = 1#1 → ¬x_2 = 1#1 → x ^^^ 123#8 ^^^ -1#8 = x ^^^ BitVec.ofInt 8 (-124)

theorem and_add_bool_to_select_thm.extracted_1._2 : ∀ (x : BitVec 32) (x_1 : BitVec 1),
  ¬x_1 = 1#1 → -1#32 + zeroExtend 32 x_1 &&& x = x

theorem self_EqualUpTo_ofBitVecZext_toBitVec (x : BitStream) :
  EqualUpTo w x (BitStream.ofBitVecZext (x.toBitVec w))

theorem ashrslt_01_09_exact_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬(True ∧ x >>> 1#4 <<< 1#4 ≠ x ∨ 1#4 ≥ ↑4) → ofBool (x.sshiftRight' 1#4 <ₛ BitVec.ofInt 4 (-7)) = 0#1

theorem sle_and_min_proof : sle_and_min_before ⊑ sle_and_min_after

theorem bv_Select_1105 :
    ∀ (e e_1 : LLVM.IntW w), LLVM.select (LLVM.const? 1 0) e_1 e ⊑ e

theorem negate_add_with_single_negatible_operand_proof : negate_add_with_single_negatible_operand_before ⊑ negate_add_with_single_negatible_operand_after

theorem e_2087 :
     - 11 * (e ^^^ (d &&& f)) - 3 * ( ~~~(d &&& e) &&&  ~~~(e ^^^ f)) - 1 * (d |||  ~~~f) + 5 *  ~~~(d ^^^ ( ~~~e ||| f)) + 7 * ( ~~~(d ^^^ e) &&& (d ^^^ f)) + 5 * (e ^^^ (d |||  ~~~f)) + 4 * (d ||| (e ||| f)) + 11 * (f ^^^ ( ~~~d ||| ( ~~~e ||| f))) - 11 *  ~~~(d &&& (e ||| f)) + 4 * (f ^^^ (d &&& (e ||| f))) - 1 * (e ^^^ ( ~~~d ||| (e ||| f))) + 4 * (e ^^^ (d ||| (e ||| f))) - 7 *  ~~~(d ^^^ (e ||| f)) - 2 * (f ^^^ ( ~~~d ||| ( ~~~e &&& f))) - 2 *  ~~~( ~~~d &&& (e ^^^ f)) + 5 * ( ~~~e &&& (d ^^^ f)) - 2 *  ~~~(d ||| (e ^^^ f)) + 1 * ((d &&&  ~~~e) |||  ~~~(e ^^^ f)) + 2 * (e |||  ~~~f) + 1 * (f ^^^  ~~~(d &&& (e ||| f))) - 3 * (d ^^^ f) - 2 *  ~~~(d ^^^ ( ~~~e &&& f)) - 11 * (f ^^^  ~~~(d ||| e)) + 1 * (f ^^^ ( ~~~d ||| (e &&& f))) + 4 * (e ^^^  ~~~(d ||| f)) + 2 * (e ^^^  ~~~( ~~~d &&& ( ~~~e ||| f))) + 4 * ((d ||| e) &&&  ~~~(d ^^^ (e ^^^ f))) - 3 * (f &&&  ~~~(d ^^^ e)) - 5 *  ~~~(d &&&  ~~~d) + 7 * ( ~~~(d |||  ~~~e) ||| (d ^^^ (e ^^^ f))) - 2 *  ~~~(d &&& f) - 6 * ( ~~~d ||| ( ~~~e &&& f)) - 2 * ( ~~~(d &&&  ~~~e) &&&  ~~~(e ^^^ f)) - 5 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) + 9 *  ~~~(d ||| ( ~~~e ||| f)) - 15 *  ~~~( ~~~d ||| (e ||| f)) + 10 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 5 * ( ~~~d &&& ( ~~~e &&& f)) + 32 * ( ~~~d &&& (e &&& f)) + 18 * (d &&& ( ~~~e &&& f)) + 8 * (d &&& (e &&& f)) =  - 1 * (d &&& (e ||| f)) - 37 *  ~~~(d ||| (e ||| f))

theorem bitwise_or_bitwise_or_icmps_comm2_proof : bitwise_or_bitwise_or_icmps_comm2_before ⊑ bitwise_or_bitwise_or_icmps_comm2_after

theorem icmp_ne_sext_slt_allones_nofold_thm (e : IntW 32) :
  icmp IntPred.ne (sext 32 (icmp IntPred.slt e (const? 32 (-1)))) e ⊑
    icmp IntPred.ne e (sext 32 (icmp IntPred.slt e (const? 32 (-1))))

theorem t0_thm.extracted_1._17 : ∀ (x x_1 x_2 : BitVec 8) (x_3 : BitVec 1),
  ¬x_3 ^^^ 1#1 = 1#1 → ¬x_3 = 1#1 → 0#1 = 1#1 → False

theorem ashrsgt_02_14_exact_thm (e : IntW 4) :
  icmp IntPred.sgt (ashr e (const? 4 2) { «exact» := true }) (const? 4 (-2)) ⊑
    icmp IntPred.ne e (const? 4 (-8))

theorem Factor.denote_eq_toNat_reflect {w : Nat} (xs : Env w) (f : Factor) :
  f.denote xs = (f.reflect xs |>.toNat)

theorem sge_to_ugt_proof : sge_to_ugt_before ⊑ sge_to_ugt_after

theorem e_1813 :
     - 3 *  ~~~(a &&&  ~~~b) - 7 *  ~~~(a ^^^ (b &&& c)) + 11 * ((b &&&  ~~~c) |||  ~~~(a ||| ( ~~~b &&& c))) - 3 * (b ^^^  ~~~( ~~~a ||| (b ^^^ c))) - 2 * (b ^^^  ~~~( ~~~a &&& (b &&& c))) + 2 * (c ^^^  ~~~(a ||| ( ~~~b &&& c))) + 2 * (b &&&  ~~~(a ^^^ c)) + 4 * ( ~~~b ||| (a ^^^ c)) + 1 * ( ~~~(a |||  ~~~b) ||| (a ^^^ (b ^^^ c))) - 7 * (b ^^^ (a &&& c)) - 5 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) + 3 * ( ~~~(a &&& b) &&& (b ^^^ c)) - 11 * (c ||| (a &&& b)) + 1 * ((a ^^^ b) &&& (a ^^^ c)) - 6 * (c ^^^ (a ||| (b ||| c))) + 1 * ((a &&& c) |||  ~~~(b ||| c)) + 1 *  ~~~(a ^^^ ( ~~~b &&& c)) + 3 * (b ^^^  ~~~(a &&& ( ~~~b &&& c))) - 1 * ( ~~~a &&& (b ^^^ c)) - 6 *  ~~~(a &&& b) - 2 * ((a &&& b) |||  ~~~(b ||| c)) + 1 * ( ~~~b &&& (a ^^^ c)) - 3 * (a &&& b) + 1 *  ~~~(a ^^^ (b ^^^ c)) - 11 * ((a &&& b) ^^^  ~~~(a ^^^ (b &&& c))) + 5 * (c ^^^ ( ~~~a ||| ( ~~~b ||| c))) - 5 * ( ~~~a ||| ( ~~~b ||| c)) - 1 * ( ~~~c ||| (a ^^^ b)) + 11 * (b ^^^  ~~~( ~~~a &&& (b ^^^ c))) - 6 * (c ^^^ ( ~~~a ||| (b ||| c))) - 2 * (b ^^^  ~~~(a &&& c)) + 1 * (c ^^^ ( ~~~a ||| (b &&& c))) - 1 * (a ||| (b ||| c)) + 10 *  ~~~(a ||| (b ||| c)) + 25 *  ~~~(a ||| ( ~~~b ||| c)) + 6 *  ~~~( ~~~a ||| (b ||| c)) + 38 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 36 * ( ~~~a &&& ( ~~~b &&& c)) + 25 * ( ~~~a &&& (b &&& c)) + 10 * (a &&& ( ~~~b &&& c)) + 33 * (a &&& (b &&& c)) = 1 *  ~~~(b |||  ~~~c)

theorem t4_ugt_slt_128_thm.extracted_1._13 : ∀ (x x_1 x_2 : BitVec 32),
  ofBool (143#32 <ᵤ x_2 + 16#32) = 1#1 →
    ¬ofBool (x_2 <ₛ 128#32) = 1#1 →
      ¬ofBool (127#32 <ₛ x_2) = 1#1 → ¬ofBool (x_2 <ₛ BitVec.ofInt 32 (-16)) = 1#1 → x = x_2

theorem add_shl_same_amount_thm.extracted_1._1 : ∀ (x x_1 x_2 : BitVec 6), ¬(x_1 ≥ ↑6 ∨ x_1 ≥ ↑6) → x_1 ≥ ↑6 → False

theorem positive_samevar_shlnuwnsw_proof : positive_samevar_shlnuwnsw_before ⊑ positive_samevar_shlnuwnsw_after

theorem Eqn.denoteFin_eq_add {w : Nat} (eqn : Eqn) (env : EnvFin (w + 1) eqn.numVars) :
    eqn.denoteFin env = 2 * eqn.denoteFin env.getNonLsbs + eqn.denoteFin env.getLsb

theorem lshr_xor_thm (e e_1 : IntW 8) :
  shl (LLVM.xor (lshr e_1 (const? 8 3)) (LLVM.srem e (const? 8 42))) (const? 8 3) ⊑
    LLVM.xor (LLVM.and e_1 (const? 8 (-8))) (shl (LLVM.srem e (const? 8 42)) (const? 8 3))

theorem t7_proof : t7_before ⊑ t7_after

theorem ashr_lshr_exact_ashr_only_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (-1#32 <ₛ x_1) = 1#1 → ¬x ≥ ↑32 → x_1 >>> x = x_1.sshiftRight' x

theorem icmp_eq_and_pow2_shl_pow2_negative1_proof : icmp_eq_and_pow2_shl_pow2_negative1_before ⊑ icmp_eq_and_pow2_shl_pow2_negative1_after

theorem test11b_proof : test11b_before ⊑ test11b_after

theorem sge_or_max_proof : sge_or_max_before ⊑ sge_or_max_after

theorem e_2073 :
     - 7 * (e &&& (d ^^^ f)) - 1 * (d ^^^ ( ~~~e &&& f)) - 6 *  ~~~( ~~~d ||| (e ^^^ f)) - 1 * (d ||| ( ~~~e ||| f)) + 2 * ( ~~~(d |||  ~~~e) |||  ~~~(d ^^^ (e ^^^ f))) + 4 *  ~~~(d &&&  ~~~d) + 7 * ((d &&& f) ^^^  ~~~(d ^^^ ( ~~~e &&& f))) + 11 * (f ^^^  ~~~( ~~~d ||| (e &&& f))) + 5 *  ~~~(d &&& f) - 3 * (f ^^^ ( ~~~d ||| (e ||| f))) + 2 *  ~~~(d &&& (e ||| f)) + 11 *  ~~~(d ||| (e &&& f)) + 3 * (e ^^^ (d ||| f)) - 3 * ( ~~~d ||| ( ~~~e &&& f)) - 2 * ((e &&& f) ^^^  ~~~( ~~~d &&& (e ^^^ f))) + 11 * ((d &&& f) ^^^ (e ||| f)) + 2 *  ~~~( ~~~d ||| ( ~~~e &&& f)) - 11 *  ~~~(d ^^^ (e &&& f)) + 1 * ( ~~~(d |||  ~~~e) ||| (e ^^^ f)) - 3 * ( ~~~(d ||| e) ||| (d ^^^ (e ^^^ f))) + 11 * (d &&& (e ||| f)) - 11 * (e ^^^ ( ~~~d &&& ( ~~~e ||| f))) + 1 * (f ^^^  ~~~(d ||| e)) + 1 * (e ^^^  ~~~( ~~~d ||| (e ^^^ f))) + 4 * (e ^^^ (d &&& (e ||| f))) - 1 * (e |||  ~~~f) - 6 * ( ~~~f &&&  ~~~(d ^^^ e)) - 1 * (f ^^^  ~~~( ~~~d &&& (e ||| f))) - 6 * (e ^^^  ~~~( ~~~d &&& (e &&& f))) + 1 *  ~~~(d &&& e) + 2 *  ~~~( ~~~d &&& (e ||| f)) - 1 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) - 1 * (e ||| (d &&& f)) + 14 *  ~~~(d ||| (e ||| f)) - 18 *  ~~~(d ||| ( ~~~e ||| f)) - 10 *  ~~~( ~~~d ||| (e ||| f)) - 16 *  ~~~( ~~~d ||| ( ~~~e ||| f)) - 11 * ( ~~~d &&& ( ~~~e &&& f)) - 22 * (d &&& ( ~~~e &&& f)) - 9 * (d &&& (e &&& f)) = 30 * ( ~~~d &&& (e &&& f)) - 7 * (d &&& f)

theorem slt_0_proof : slt_0_before ⊑ slt_0_after

theorem test3_thm.extracted_1._1 : ∀ (x : BitVec 1) (x_1 : BitVec 599),
  x = 1#1 → ¬70368744177664#599 = 0 → 46#599 ≥ ↑599 → False

theorem lshr_16_to_64_add_zext_basic_thm.extracted_1._1 : ∀ (x x_1 : BitVec 16),
  ¬16#64 ≥ ↑64 → (zeroExtend 64 x_1 + zeroExtend 64 x) >>> 16#64 = zeroExtend 64 (ofBool (x_1 ^^^ -1#16 <ᵤ x))

theorem p1_ugt_proof : p1_ugt_before ⊑ p1_ugt_after

theorem select_icmp_ne_0_and_1073741824_xor_8_proof : select_icmp_ne_0_and_1073741824_xor_8_before ⊑ select_icmp_ne_0_and_1073741824_xor_8_after

theorem e_1089 :
    3 *  ~~~(z &&&  ~~~z) + 1 *  ~~~z - 3 *  ~~~(z &&& t) - 2 * (z |||  ~~~t) - 1 *  ~~~(z &&&  ~~~t) + 7 *  ~~~(z ||| t) + 2 * (z &&&  ~~~t) + 5 * (z &&& t) = 5 *  ~~~(z ^^^ t)

theorem icmp_select_var_select_thm.extracted_1._13 : ∀ (x x_1 : BitVec 8) (x_2 : BitVec 1),
  ¬x_2 = 1#1 → ofBool (x_1 == 0#8) = 1#1 ∧ x_2 = 1#1 → ofBool (x_1 == 0#8) = 1#1 → ¬True → ofBool (x == x_1) = 1#1

theorem test4_proof : test4_before ⊑ test4_after

theorem test_logical_and_ne_a_b_proof : test_logical_and_ne_a_b_before ⊑ test_logical_and_ne_a_b_after

theorem not_and_and_or_not_or_or_commute1_proof : not_and_and_or_not_or_or_commute1_before ⊑ not_and_and_or_not_or_or_commute1_after

theorem or_basic_commuted_thm (e : IntW 16) :
  LLVM.or (icmp IntPred.ne (LLVM.and e (const? 16 (-256))) (const? 16 32512))
      (icmp IntPred.ne (trunc 8 e) (const? 8 69)) ⊑
    icmp IntPred.ne e (const? 16 32581)

theorem ashr_ult_exact_proof : ashr_ult_exact_before ⊑ ashr_ult_exact_after

theorem t_0_10_proof : t_0_10_before ⊑ t_0_10_after

theorem ashrslt_01_00_proof : ashrslt_01_00_before ⊑ ashrslt_01_00_after

theorem test_ashr__exact_is_safe_proof : test_ashr__exact_is_safe_before ⊑ test_ashr__exact_is_safe_after
</all_available_lemmas>

<local_ctx>
import Mathlib.Logic.Function.Iterate

import Mathlib.Tactic.Linarith

import LeanMLIR.Framework

import LeanMLIR.Tactic

import LeanMLIR.ErasedContext

import LeanMLIR.Util

open LeanMLIR

open Ctxt(Var)

namespace ScfFunctor

open TyDenote

class HasTy (d : Dialect) (DenotedTy : Type) [TyDenote d.Ty] [DialectSignature d] where
    ty : d.Ty
    denote_eq : toType ty = DenotedTy := by admit /- proof elided -/

inductive Scf.Op (Op' Ty' : Type) (m') [TyDenote Ty'] [DialectSignature ⟨Op', Ty', m'⟩]
    [DialectDenote ⟨Op', Ty', m'⟩] : Type _
  | coe (o : Op')
  | iterate (k : ℕ) 
  | run (inputty : Ty')  
  | if (inputty retty' : Ty')  
  | for (ty : Ty')
  deriving DecidableEq, Repr

def Scf (d : Dialect) [TyDenote d.Ty] [DialectSignature d] [DialectDenote d] : Dialect where
  Op := Scf.Op d.Op d.Ty d.m
  Ty := d.Ty
  m  := d.m

namespace Scf

section InheritedInstances

variable {d : Dialect} [TyDenote d.Ty] [DialectSignature d] [DialectDenote d]

end InheritedInstances

abbrev LoopBody (t : Type) : Type := Int → t → t

namespace LoopBody

def counterDecorator (δ : Int) (f : LoopBody α) : Int × α → Int × α :=
  fun (i, v) => (i + δ, f i v)

def atZero (f : LoopBody t) : t → t := fun v => f 0 v

end LoopBody

namespace LoopBody.IndexInvariant

end LoopBody.IndexInvariant

namespace LoopBody.counterDecorator

end LoopBody.counterDecorator

variable [TyDenote d.Ty] [DialectSignature d] [DialectDenote d]
  [B : HasBool d] [N : HasNat d] [Z : HasInt d]

open Ctxt (Valuation) in

end Scf

namespace Arith

inductive Ty
| int
| bool
| nat
 deriving DecidableEq, Repr

inductive Op
  | add : Op  
  | add_nat : Op  
  | axpy : Op  
  | neg : Op  
  | const : (val : ℤ) → Op
  | const_nat : (val : ℕ) → Op

abbrev Arith : Dialect := {Op, Ty}

end Arith

abbrev ScfArith := Scf Arith

open LeanMLIR.SingleReturnCompat (Com Expr)

@[simp_denote] def cst (n : ℤ) : Expr ScfArith Γ .pure .int  :=
  Expr.mk
    (op := .coe <| .const n)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .nil)
    (regArgs := .nil)

@[simp_denote] def add {Γ : Ctxt _} (e₁ e₂ : Var Γ .int) : Expr ScfArith Γ .pure .int :=
  Expr.mk
    (op := .coe <| .add)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons e₁ <| .cons e₂ .nil)
    (regArgs := .nil)

@[simp_denote] def add_nat (e₁ e₂ : Var Γ .nat) : Expr ScfArith Γ .pure .nat :=
  Expr.mk
    (op := .coe <| .add_nat)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons e₁ <| .cons e₂ .nil)
    (regArgs := .nil)

@[simp_denote] def axpy {Γ : Ctxt _} (a : Var Γ .int) (x : Var Γ .nat) (b: Var Γ .int) :
    Expr ScfArith Γ .pure .int :=
  Expr.mk
    (op := .coe <| .axpy)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons a <| .cons x <| .cons b .nil)
    (regArgs := .nil)

@[simp_denote] def neg {Γ : Ctxt _} (a : Var Γ .int) : Expr ScfArith Γ .pure .int :=
  Expr.mk
    (op := .coe <| .neg)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons a <| .nil)
    (regArgs := .nil)

@[simp_denote] def iterate {Γ : Ctxt _} (k : Nat) (input : Var Γ Arith.Ty.int)
    (body : Com ScfArith ⟨[.int]⟩ .impure .int) : Expr ScfArith Γ .impure .int :=
  Expr.mk
    (op := .iterate k)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons input .nil)
    (regArgs := HVector.cons body HVector.nil)

@[simp_denote]
def run {Γ : Ctxt _} {t : Arith.Ty} (v : Var Γ t) (body : Com ScfArith ⟨[t]⟩ .impure t) :
    Expr ScfArith Γ .impure t :=
  Expr.mk
    (op := .run t)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons v .nil)
    (regArgs := HVector.cons body <| HVector.nil)

@[simp_denote] def for_ {Γ : Ctxt Arith.Ty} {t : Arith.Ty}
    (start step : Var Γ Arith.Ty.int)
    (niter : Var Γ Arith.Ty.nat) (v : Var Γ t) (body : Com ScfArith ⟨[.int, t]⟩ .impure t) :
      Expr ScfArith Γ .impure t :=
  Expr.mk
    (op := .for t)
    (ty_eq := rfl)
    (eff_le := by admit /- proof elided -/
    )
    (args := .cons start <| .cons step <| .cons niter <| .cons v .nil)
    (regArgs := HVector.cons body <| HVector.nil)

namespace ForAddToMul

def lhs (vincrement : ℤ) : Com ScfArith ⟨[  .nat,   .int]⟩ .impure .int :=
    Com.letPure (cst 0) <|
    Com.letPure  (cst 1) <|
    Com.var (for_ (t := .int)
                        ⟨  1, rfl⟩
                        ⟨  0, rfl⟩
                        ⟨  2, rfl⟩
                        ⟨  3, rfl⟩ (
      Com.letPure (cst vincrement) <|
      Com.letPure (add ⟨0, rfl⟩ ⟨2, rfl⟩) 
      <| Com.ret ⟨0, rfl⟩)) <|
  Com.ret ⟨0, rfl⟩

def rhs (vincrement : ℤ) : Com ScfArith ⟨[  .nat,   .int]⟩ .pure .int :=
  Com.var (cst vincrement) <|
  Com.var (axpy ⟨0, rfl⟩ ⟨1, rfl⟩ ⟨2, rfl⟩) <|
  Com.ret ⟨0, rfl⟩

open Scf in

open Arith in
</local_ctx>

<target_theorem>
theorem correct : Com.denote (lhs v0) = Com.denote (rhs v0) :=
</target_theorem>

