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
AList in Mathlib.Data.List.AList
Option in Init.Prelude
StateT in Init.Control.State
Unit in Init.Prelude
AList.insert in Mathlib.Data.List.AList
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
Valuation.map in Mathlib.RingTheory.Valuation.Basic
Set in Mathlib.Data.Set.Defs
Set.Subset in Mathlib.Data.Set.Defs
List.Subset in Init.Data.List.Basic
StateT.bind in Init.Control.State
liftM in Init.Prelude
Iff in Init.Core
IsEmpty in Mathlib.Logic.IsEmpty
reduceCtorEq in Lean.Meta.Tactic.Simp.BuiltinSimprocs.Core

abbrev Mapping (Γ Δ : Ctxt Ty) : Type :=
  @AList (Σ t, Var Γ t) (fun x => Var Δ x.1)

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 }

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

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 }

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

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

@[elab_as_elim]
def appendCases
    {motive : (Γ ++ Δ).Var t → Sort u}
    (left : (v : Var Γ t) → motive (appendInl v))
    (right : (v : Var Δ t) → motive (appendInr v)) :
    (v : (Γ ++ Δ).Var t) → motive v
  | ⟨idx, h⟩ =>
    if hv : idx < Γ.length then
      left ⟨idx, by admit /- proof elided -/
      ⟩
    else
      let v' : Var _ _ := ⟨idx - Γ.length, by admit /- proof elided -/
      ⟩
      have eq : v'.appendInr = ⟨idx, h⟩ := by admit /- proof elided -/

@[match_pattern]
def last (Γ : Ctxt Ty) (t : Ty) : Ctxt.Var (Ctxt.cons t Γ) t :=
  ⟨0, by admit /- proof elided -/
  ⟩

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

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

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

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

Lean.Meta.Simp.Step in Lean.Meta.Tactic.Simp.Types

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

def and1_shl1_is_cmp_eq_0_multiuse_after := [llvm|
{
^0(%arg14 : i8):
  %0 = llvm.mlir.constant(1 : i8) : i8
  %1 = llvm.shl %0, %arg14 overflow<nuw> : i8
  %2 = llvm.and %1, %0 : i8
  %3 = llvm.add %1, %2 overflow<nuw> : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def in_constant_varx_mone_invmask_after := [llvm|
{
^0(%arg41 : i4, %arg42 : i4):
  %0 = llvm.or %arg41, %arg42 : i4
  "llvm.return"(%0) : (i4) -> ()
}
]

def positive_with_signbit_before := [llvm|
{
^0(%arg62 : i32):
  %0 = llvm.mlir.constant(-1 : i32) : i32
  %1 = llvm.mlir.constant(128 : i32) : i32
  %2 = llvm.mlir.constant(256 : i32) : i32
  %3 = llvm.icmp "sgt" %arg62, %0 : i32
  %4 = llvm.add %arg62, %1 : i32
  %5 = llvm.icmp "ult" %4, %2 : i32
  %6 = llvm.and %3, %5 : i1
  "llvm.return"(%6) : (i1) -> ()
}
]

@[simp]
def mkOutEqZeroCircuitN {arity : Type _}
  [DecidableEq arity]
  [Fintype arity]
  [Hashable arity]
  (p : FSM arity) (n : Nat) :
  Circuit (Vars p.α arity (n + 1)) :=
    
    
    Circuit.xor
      (Circuit.ofBool false)
      (Circuit.var true <| Vars.outputs ⟨n, by admit /- proof elided -/
      ⟩)

def test_before := [llvm|
{
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(2 : i32) : i32
  %2 = llvm.icmp "eq" %0, %1 : i32
  %3 = llvm.zext %2 : i1 to i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def shl_add_nuw_before := [llvm|
{
^0(%arg69 : i32):
  %0 = llvm.mlir.constant(5 : i32) : i32
  %1 = llvm.mlir.constant(6 : i32) : i32
  %2 = llvm.add %arg69, %0 overflow<nuw> : i32
  %3 = llvm.shl %1, %2 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def select_or_disjoint_or_before := [llvm|
{
^0(%arg14 : i32, %arg15 : i1):
  %0 = llvm.mlir.constant(0 : i32) : i32
  %1 = llvm.mlir.constant(4 : i32) : i32
  %2 = "llvm.select"(%arg15, %0, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %3 = llvm.shl %arg14, %1 : i32
  %4 = llvm.or disjoint %2, %3 : i32
  %5 = llvm.add %4, %1 : i32
  "llvm.return"(%5) : (i32) -> ()
}
]

def ugt_rem_zero_after := [llvm|
{
^0(%arg167 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.icmp "ugt" %arg167, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

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

@[simp_denote]
def shl_riscv_8 := [LV| {
  ^entry (%reg1: i8, %reg2: i8 ):
    %0 = "builtin.unrealized_conversion_cast"(%reg1) : (i8) -> (!i64)
    %1 = "builtin.unrealized_conversion_cast"(%reg2) : (i8) -> (!i64)
    %2 = sll %0, %1 : !i64
    %3 = "builtin.unrealized_conversion_cast"(%2) : (!i64) -> (i8)
    llvm.return %3 : i8
  }]

@[simp_denote]
def urem {Γ : Ctxt _} (w : ℕ) (l r : Nat)
    (lp : (Γ[l]? = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)))
      := by admit /- proof elided -/
      )
    (rp : (Γ[r]? = some (InstCombine.MTy.bitvec (ConcreteOrMVar.concrete w)))
      := by admit /- proof elided -/
      ) :
    Expr InstCombine.LLVM Γ .pure (LLVM.Ty.bitvec w) :=
  Expr.mk
    (op := InstCombine.MOp.urem w)
    (eff_le := by admit /- proof elided -/
    )
    (ty_eq := rfl)
    (args := .cons ⟨l, lp⟩ <| .cons ⟨r, rp⟩ .nil)
    (regArgs := .nil)

def test13_before := [llvm|
{
^0(%arg16 : i8, %arg17 : i8):
  %0 = llvm.icmp "ult" %arg16, %arg17 : i8
  %1 = llvm.icmp "ugt" %arg16, %arg17 : i8
  %2 = llvm.xor %0, %1 : i1
  "llvm.return"(%2) : (i1) -> ()
}
]

@[reducible]
instance : TyDenote ExTy where
  toType
    | .nat => Nat

def ashrslt_01_05_after := [llvm|
{
^0(%arg264 : i4):
  %0 = llvm.mlir.constant(true) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def shl_nsw_nuw_add_before := [llvm|
{
^0(%arg14 : i32):
  %0 = llvm.mlir.constant(1 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.shl %0, %arg14 overflow<nsw,nuw> : i32
  %3 = llvm.add %2, %1 : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def test_sext1_after := [llvm|
{
^0(%arg49 : i1, %arg50 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = "llvm.select"(%arg50, %arg49, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %2 = llvm.sext %1 : i1 to i32
  "llvm.return"(%2) : (i32) -> ()
}
]

def vec_to_streams {α : Type u} {n : Nat} (xv : Stream' (Vector α n)) : Vector (Stream' α) n :=
   
  Vector.ofFn (fun (k : Fin n) => fun (i : Nat) => (xv i).get k)

class DialectPrint (d : Dialect) where
   
  printOpName : d.Op → String
   
  printAttributes : d.Op → String

def BuilderM.isErr {α : Type} (x : BuilderM d α) : Bool :=
  match x.run [] with
  | Except.ok _ => true
  | Except.error _ => false

def tryFactorization_add_nuw_mul_nuw_mul_var_after := [llvm|
{
^0(%arg3 : i32, %arg4 : i32, %arg5 : i32):
  %0 = llvm.add %arg4, %arg5 : i32
  %1 = llvm.mul %arg3, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

@[simp_denote]
def udiv_llvm_no_exact_32 : Com  LLVMPlusRiscV ⟨[.llvm (.bitvec 32), .llvm (.bitvec 32)]⟩
  .pure (.llvm (.bitvec 32)) := [LV| {
  ^entry (%x: i32, %y: i32 ):
    %1 = llvm.udiv    %x, %y : i32
    llvm.return %1 : i32
  }]

def test9_before := [llvm|
{
^0(%arg87 : i32):
  %0 = llvm.mlir.constant(42 : i32) : i32
  %1 = llvm.and %arg87, %0 : i32
  %2 = llvm.trunc %1 : i32 to i8
  "llvm.return"(%2) : (i8) -> ()
}
]

def lshr_shl_pow2_const_overflow_before := [llvm|
{
^0(%arg57 : i16):
  %0 = llvm.mlir.constant(8192 : i16) : i16
  %1 = llvm.mlir.constant(6 : i16) : i16
  %2 = llvm.mlir.constant(32 : i16) : i16
  %3 = llvm.lshr %0, %arg57 : i16
  %4 = llvm.shl %3, %1 : i16
  %5 = llvm.and %4, %2 : i16
  "llvm.return"(%5) : (i16) -> ()
}
]

def test13_logical_after := [llvm|
{
^0(%arg286 : i32, %arg287 : i32):
  %0 = llvm.mlir.constant(false) : i1
  "llvm.return"(%0) : (i1) -> ()
}
]

def exampleSink := [DCxComb_com| {
  ^entry(%0: !TokenStream):
    %src = "DCxComb.sink" (%0) : (!TokenStream) -> (!TokenStream)
    "return" (%src) : (!TokenStream) -> ()
  }]

def positive_easyinvert_before := [llvm|
{
^0(%arg7 : i16, %arg8 : i8):
  %0 = llvm.mlir.constant(0 : i16) : i16
  %1 = llvm.mlir.constant(0 : i8) : i8
  %2 = llvm.mlir.constant(true) : i1
  %3 = llvm.icmp "slt" %arg7, %0 : i16
  %4 = llvm.icmp "slt" %arg8, %1 : i8
  %5 = llvm.xor %4, %3 : i1
  %6 = llvm.xor %5, %2 : i1
  "llvm.return"(%6) : (i1) -> ()
}
]

def t8_lshr_exact_flag_preservation_after := [llvm|
{
^0(%arg27 : i32, %arg28 : i32):
  %0 = llvm.mlir.constant(30 : i32) : i32
  %1 = llvm.lshr exact %arg27, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def bad_shl2_sub_i32_after := [llvm|
{
^0(%arg9 : i32):
  %0 = llvm.mlir.constant(-31 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.add %arg9, %0 : i32
  %3 = llvm.shl %1, %2 overflow<nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def test17_before := [llvm|
{
^0(%arg36 : i32, %arg37 : i32):
  %0 = llvm.mlir.constant(-1431655766 : i32) : i32
  %1 = llvm.mlir.constant(-1431655765 : i32) : i32
  %2 = llvm.and %arg36, %0 : i32
  %3 = llvm.xor %2, %1 : i32
  %4 = llvm.add %3, %arg37 overflow<nsw> : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def n2_after := [llvm|
{
^0(%arg0 : i8, %arg1 : i8):
  %0 = llvm.mlir.constant(-1 : i8) : i8
  %1 = llvm.mlir.constant(-2 : i8) : i8
  %2 = llvm.mlir.constant(0 : i8) : i8
  %3 = llvm.shl %0, %arg1 overflow<nsw> : i8
  %4 = llvm.xor %3, %1 : i8
  %5 = llvm.and %arg0, %4 : i8
  %6 = llvm.icmp "ne" %5, %2 : i8
  "llvm.return"(%6) : (i1) -> ()
}
]

def ofFin (i : Fin Γ.length) : Γ.Var (Γ[i]) :=
  ⟨i.val, by admit /- proof elided -/
  ⟩

def sub_ashr_and_i8_after := [llvm|
{
^0(%arg31 : i8, %arg32 : i8):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.icmp "slt" %arg32, %arg31 : i8
  %2 = "llvm.select"(%1, %arg31, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  "llvm.return"(%2) : (i8) -> ()
}
]

printReturn : List d.Ty → String
   
  printFunc : List d.Ty → String := fun _ => "^entry"

def test3_before := [llvm|
{
^0(%arg103 : i32):
  %0 = llvm.mlir.constant(8 : i32) : i32
  %1 = llvm.urem %arg103, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def slt_swap_or_not_max_commute_logical_after := [llvm|
{
^0(%arg48 : i8, %arg49 : i8):
  %0 = llvm.mlir.constant(127 : i8) : i8
  %1 = llvm.icmp "ne" %arg48, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

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

def ult_rem_zero_after := [llvm|
{
^0(%arg174 : i8):
  %0 = llvm.mlir.constant(3 : i8) : i8
  %1 = llvm.icmp "ult" %arg174, %0 : i8
  "llvm.return"(%1) : (i1) -> ()
}
]

def PR38781_before := [llvm|
{
^0(%arg4 : i32, %arg5 : i32):
  %0 = llvm.mlir.constant(31 : i32) : i32
  %1 = llvm.mlir.constant(1 : i32) : i32
  %2 = llvm.lshr %arg4, %0 : i32
  %3 = llvm.xor %2, %1 : i32
  %4 = llvm.lshr %arg5, %0 : i32
  %5 = llvm.xor %4, %1 : i32
  %6 = llvm.and %5, %3 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def or_and2_commuted_after := [llvm|
{
^0(%arg132 : i1, %arg133 : i1, %arg134 : i1):
  %0 = llvm.mlir.constant(false) : i1
  %1 = llvm.mlir.constant(true) : i1
  %2 = "llvm.select"(%arg134, %arg133, %0) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  %3 = "llvm.select"(%arg132, %1, %2) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

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

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

def test_after := [llvm|
{
^0(%arg0 : i26):
  "llvm.return"(%arg0) : (i26) -> ()
}
]

def test_and2_before := [llvm|
{
^0(%arg48 : i32, %arg49 : i32):
  %0 = llvm.mlir.constant(2147483647 : i32) : i32
  %1 = llvm.mlir.constant(-1 : i32) : i32
  %2 = llvm.and %arg49, %0 : i32
  %3 = llvm.icmp "sgt" %arg48, %1 : i32
  %4 = llvm.icmp "sle" %arg48, %2 : i32
  %5 = llvm.and %3, %4 : i1
  "llvm.return"(%5) : (i1) -> ()
}
]

def test23_after := [llvm|
{
^0(%arg172 : i32):
  %0 = llvm.mlir.constant(65535 : i32) : i32
  %1 = llvm.and %arg172, %0 : i32
  "llvm.return"(%1) : (i32) -> ()
}
]

def select_icmp_eq_and_32_0_xor_8_after := [llvm|
{
^0(%arg237 : i32, %arg238 : i32):
  %0 = llvm.mlir.constant(2 : i32) : i32
  %1 = llvm.mlir.constant(8 : i32) : i32
  %2 = llvm.lshr %arg237, %0 : i32
  %3 = llvm.and %2, %1 : i32
  %4 = llvm.xor %arg238, %3 : i32
  "llvm.return"(%4) : (i32) -> ()
}
]

def test_mul__nuw_is_safe_after := [llvm|
{
^0(%arg8 : i32):
  %0 = llvm.mlir.constant(268435457 : i32) : i32
  %1 = llvm.mlir.constant(9 : i32) : i32
  %2 = llvm.and %arg8, %0 : i32
  %3 = llvm.mul %2, %1 overflow<nuw> : i32
  "llvm.return"(%3) : (i32) -> ()
}
]

def accepts (M : NFA' n) : Set (BitVecs n) := dec '' M.accepts'

def masked_icmps_mask_notallzeros_bmask_mixed_negated_swapped_3b_logical_before := [llvm|
{
^0(%arg19 : i32):
  %0 = llvm.mlir.constant(15 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.mlir.constant(3 : i32) : i32
  %3 = llvm.mlir.constant(true) : i1
  %4 = llvm.and %arg19, %0 : i32
  %5 = llvm.icmp "eq" %4, %1 : i32
  %6 = llvm.and %arg19, %2 : i32
  %7 = llvm.icmp "ne" %6, %1 : i32
  %8 = "llvm.select"(%7, %3, %5) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%8) : (i1) -> ()
}
]

def no_shift_xor_multiuse_or_before := [llvm|
{
^0(%arg134 : i32, %arg135 : i32):
  %0 = llvm.mlir.constant(4096 : i32) : i32
  %1 = llvm.mlir.constant(0 : i32) : i32
  %2 = llvm.and %arg134, %0 : i32
  %3 = llvm.icmp "ne" %1, %2 : i32
  %4 = llvm.or %arg135, %0 : i32
  %5 = "llvm.select"(%3, %arg135, %4) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i32, i32) -> i32
  %6 = llvm.mul %5, %4 : i32
  "llvm.return"(%6) : (i32) -> ()
}
]

def a_true_implies_b_true_after := [llvm|
{
^0(%arg36 : i8, %arg37 : i1, %arg38 : i1):
  %0 = llvm.mlir.constant(20 : i8) : i8
  %1 = llvm.mlir.constant(false) : i1
  %2 = llvm.icmp "ugt" %arg36, %0 : i8
  %3 = "llvm.select"(%2, %arg37, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i1, i1) -> i1
  "llvm.return"(%3) : (i1) -> ()
}
]

if defeqAttr.hasTag (← getEnv) id then
    attrs := attrs.push m!"defeq"

def test47_after := [llvm|
{
^0(%arg139 : i8):
  %0 = llvm.mlir.constant(42 : i8) : i8
  %1 = llvm.or %arg139, %0 : i8
  %2 = llvm.sext %1 : i8 to i32
  %3 = llvm.zext %2 : i32 to i64
  "llvm.return"(%3) : (i64) -> ()
}
]

def negate_select_of_op_vs_negated_op_nsw_after := [llvm|
{
^0(%arg21 : i8, %arg22 : i8, %arg23 : i1):
  %0 = llvm.mlir.constant(0 : i8) : i8
  %1 = llvm.sub %0, %arg21 : i8
  %2 = "llvm.select"(%arg23, %arg21, %1) <{"fastmathFlags" = #llvm.fastmath<none>}> : (i1, i8, i8) -> i8
  %3 = llvm.add %2, %arg22 : i8
  "llvm.return"(%3) : (i8) -> ()
}
]

def test85_after := [llvm|
{
^0(%arg60 : i32):
  %0 = llvm.mlir.constant(2130706432 : i32) : i32
  %1 = llvm.mlir.constant(23 : i32) : i32
  %2 = llvm.add %arg60, %0 : i32
  %3 = llvm.lshr %2, %1 : i32
  %4 = llvm.trunc %3 : i32 to i8
  "llvm.return"(%4) : (i8) -> ()
}
]

def exact_ashr_eq_both_equal_before := [llvm|
{
^0(%arg168 : i8):
  %0 = llvm.mlir.constant(-128 : i8) : i8
  %1 = llvm.ashr exact %0, %arg168 : i8
  %2 = llvm.icmp "eq" %1, %0 : i8
  "llvm.return"(%2) : (i1) -> ()
}
]

def or_xor_common_op_commute6_before := [llvm|
{
^0(%arg117 : i8, %arg118 : i8, %arg119 : i8):
  %0 = llvm.or %arg117, %arg118 : i8
  %1 = llvm.xor %arg119, %arg117 : i8
  %2 = llvm.or %1, %0 : i8
  "llvm.return"(%2) : (i8) -> ()
}
]

abbrev WidthExpr := Expr

pure pruned
</all_available_defs>

<all_available_lemmas>
Option.bind_eq_some_iff in Init.Data.Option.Lemmas
AList.entries_insert_of_notMem in Mathlib.Data.List.AList
AList.lookup_eq_none in Mathlib.Data.List.AList
List.subset_cons_of_subset in Init.Data.List.Sublist
Option.mem_def in Init.Data.Option.Instances
IsEmpty.forall_iff in Mathlib.Logic.IsEmpty
forall_eq' in Init.PropLemmas
iff_true in Init.SimpLemmas
implies_true in Init.SimpLemmas

@[simp] theorem appendCases_appendInl (v : Γ.Var t) :
    appendCases (motive := motive) left right v.appendInl = (left v)

theorem main3e_like_logical_thm.extracted_1._12 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 &&& x_1 == 0#32) = 1#1 →
    ¬ofBool (x_2 &&& x_1 != 0#32) = 1#1 → ¬0#1 = 1#1 → 1#32 = zeroExtend 32 (ofBool (x_2 &&& x != 0#32))

theorem e_857 :
    4 *  ~~~z + 3 *  ~~~(z &&&  ~~~t) + 1 *  ~~~(z ^^^ t) - 7 * (z |||  ~~~t) - 1 *  ~~~(z ||| t) + 7 * (z &&&  ~~~t) =  - 3 * (z &&& t) + 7 *  ~~~(z |||  ~~~t)

theorem main4f_like_logical_thm.extracted_1._11 : ∀ (x x_1 x_2 : BitVec 32),
  ¬ofBool (x_2 &&& x_1 != x_1) = 1#1 →
    ¬ofBool (x_2 &&& x_1 == x_1) = 1#1 → ofBool (x_2 &&& x != x) = 1#1 → 0#32 = zeroExtend 32 0#1

theorem src_is_notmask_lshr_shl_proof : src_is_notmask_lshr_shl_before ⊑ src_is_notmask_lshr_shl_after

theorem main4f_like_proof : main4f_like_before ⊑ main4f_like_after

theorem scalar_i16_shl_and_signbit_eq_thm.extracted_1._1 : ∀ (x x_1 : BitVec 16),
  ¬x ≥ ↑16 → ofBool (x_1 <<< x &&& BitVec.ofInt 16 (-32768) == 0#16) = ofBool (-1#16 <ₛ x_1 <<< x)

theorem smear_set_bit_different_dest_type_wider_dst_proof : smear_set_bit_different_dest_type_wider_dst_before ⊑ smear_set_bit_different_dest_type_wider_dst_after

theorem e_1369 :
    2 * (z |||  ~~~t) + 3 *  ~~~t - 1 * (z ||| t) - 6 *  ~~~(z &&&  ~~~z) - 2 * t - 5 * (z ^^^ t) + 2 *  ~~~(z &&& t) + 12 *  ~~~(z |||  ~~~t) + 5 * (z &&&  ~~~t) + 8 * (z &&& t) = 1 *  ~~~(z ^^^ t)

theorem e_334 :
     - 3 *  ~~~(x &&&  ~~~y) + 1 * x + 3 *  ~~~(x &&&  ~~~x) + 1 *  ~~~(x &&& y) + 5 * (x |||  ~~~y) + 1 *  ~~~(x |||  ~~~y) - 10 * (x &&&  ~~~y) - 4 * (x &&& y) = 2 * y + 6 *  ~~~(x ||| y)

theorem test_lshr__exact_is_unsafe_thm.extracted_1._4 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬ofBool (x_1 &&& 63#32 == 0#32) = 1#1 →
    ¬(2#32 ≥ ↑32 ∨ zeroExtend 64 ((x_1 &&& 63#32) >>> 2#32) ≥ ↑64) →
      ¬(2#32 ≥ ↑32 ∨ True ∧ (x_1 >>> 2#32 &&& 15#32).msb = true ∨ zeroExtend 64 (x_1 >>> 2#32 &&& 15#32) ≥ ↑64) →
        x.sshiftRight' (zeroExtend 64 ((x_1 &&& 63#32) >>> 2#32)) =
          x.sshiftRight' (zeroExtend 64 (x_1 >>> 2#32 &&& 15#32))

theorem add_or_sub_comb_i128_commuted3_nuw_nsw_proof : add_or_sub_comb_i128_commuted3_nuw_nsw_before ⊑ add_or_sub_comb_i128_commuted3_nuw_nsw_after

theorem test19_proof : test19_before ⊑ test19_after

theorem icmp_ne_sext_ne_allones_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (signExtend 32 (ofBool (x != -1#32)) != x) = 1#1

theorem positive_biggerlshr_shlnuwnsw_lshrexact_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ x >>> 6#8 <<< 6#8 ≠ x ∨
        6#8 ≥ ↑8 ∨
          True ∧ (x >>> 6#8 <<< 3#8).sshiftRight' 3#8 ≠ x >>> 6#8 ∨
            True ∧ x >>> 6#8 <<< 3#8 >>> 3#8 ≠ x >>> 6#8 ∨ 3#8 ≥ ↑8) →
    True ∧ x >>> 3#8 <<< 3#8 ≠ x ∨ 3#8 ≥ ↑8 → False

@[simp] theorem Com.changeDialect_rets (f : DialectMorphism d d') (vs) :
    Com.changeDialect f (Com.rets vs : Com d Γ eff t)
    = Com.rets (vs.map' f.mapTy (fun _ v => v.toMap))

theorem e_325 :
     - 1 *  ~~~(x &&&  ~~~y) - 2 *  ~~~(x &&& y) + 11 * (x ||| y) + 3 *  ~~~(x ||| y) - 8 *  ~~~(x |||  ~~~y) - 16 * (x &&&  ~~~y) - 17 * (x &&& y) =  - 7 * x

theorem neg_mask1_lshr_proof : neg_mask1_lshr_before ⊑ neg_mask1_lshr_after

theorem or_logic_or_logic_and_1_thm.extracted_1._5 : ∀ (x x_1 x_2 : BitVec 1),
  ¬x_2 ||

theorem shl_nuw_add_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ¬(True ∧ 1#32 <<< x >>> x ≠ 1#32 ∨ x ≥ ↑32) →
    ¬(True ∧ ((-1#32) <<< x).sshiftRight' x ≠ -1#32 ∨ x ≥ ↑32) → 1#32 <<< x + -1#32 = (-1#32) <<< x ^^^ -1#32

theorem src_x_and_nmask_slt_fail_maybe_z_thm.extracted_1._1 : ∀ (x : BitVec 8) (x_1 : BitVec 1) (x_2 : BitVec 8),
  x_1 = 1#1 → ¬x ≥ ↑8 → True ∧ ((-1#8) <<< x).sshiftRight' x ≠ -1#8 ∨ x ≥ ↑8 → False

theorem e_768 :
     - 7 *  ~~~(z &&&  ~~~t) + 5 * z + 7 *  ~~~(z ||| t) + 7 * (z &&& t) =  - 12 *  ~~~(z |||  ~~~t) + 5 * (z ||| t)

theorem demorganize_constant2_thm (e : IntW 32) :
  LLVM.xor (LLVM.or e (const? 32 15)) (const? 32 (-1)) ⊑
    LLVM.xor (LLVM.and e (const? 32 (-16))) (const? 32 (-16))

theorem test_logical_or_eq_a_b_proof : test_logical_or_eq_a_b_before ⊑ test_logical_or_eq_a_b_after

theorem main4_logical_thm.extracted_1._2 : ∀ (x : BitVec 32),
  ofBool (x &&& 7#32 == 7#32) = 1#1 →
    ¬ofBool (x &&& 48#32 == 48#32) = 1#1 → 1#32 = zeroExtend 32 (ofBool (x &&& 55#32 != 55#32))

theorem cmpeq_xor_cst3_proof : cmpeq_xor_cst3_before ⊑ cmpeq_xor_cst3_after

theorem main5e_like_proof : main5e_like_before ⊑ main5e_like_after

theorem main15_logical_thm.extracted_1._1 : ∀ (x : BitVec 32),
  ofBool (0#16 ≤ₛ truncate 16 x) = 1#1 → ofBool (x &&& 32896#32 == 32896#32) = 1#1 → True → 2#32 = 1#32

theorem test25_proof : test25_before ⊑ test25_after

theorem lshrugt_03_00_exact_proof : lshrugt_03_00_exact_before ⊑ lshrugt_03_00_exact_after

theorem e_2119 :
    2 * (e ^^^ (d &&& f)) - 2 *  ~~~( ~~~d &&& (e ||| f)) + 1 * (f ^^^  ~~~(d &&& (e ||| f))) + 1 * (e ^^^ f) + 7 * (f ^^^  ~~~(d ||| ( ~~~e &&& f))) - 1 * ((d &&&  ~~~e) ||| (e ^^^ f)) + 1 * (e ^^^  ~~~(d &&&  ~~~f)) + 11 * ( ~~~f &&& (d ^^^ e)) - 11 * (f ^^^  ~~~( ~~~d ||| ( ~~~e &&& f))) - 7 * ((d &&&  ~~~e) ||| (d ^^^ (e ^^^ f))) - 11 * (e ^^^ ( ~~~d ||| (e ^^^ f))) + 5 * (d ||| ( ~~~e &&& f)) + 1 * ( ~~~d ||| ( ~~~e ||| f)) - 2 * (f ^^^ (d ||| ( ~~~e ||| f))) + 11 * ( ~~~(d &&&  ~~~e) &&& (e ^^^ f)) + 3 * ((d &&& f) ^^^ (d ^^^ (e &&& f))) - 1 * (f &&&  ~~~(d &&&  ~~~e)) - 3 * (f ^^^  ~~~(d ||| (e &&& f))) + 1 * (e ^^^  ~~~(d ||| (e ^^^ f))) + 4 * ( ~~~e |||  ~~~(d ^^^ f)) - 1 *  ~~~(d ||| ( ~~~e &&& f)) - 2 * (e ^^^ ( ~~~d &&& (e ||| f))) + 2 *  ~~~(d &&&  ~~~f) + 4 * (e |||  ~~~(d |||  ~~~f)) + 1 * (f &&&  ~~~(d &&& e)) - 2 * (f ||| (d ^^^ e)) - 5 * ( ~~~(d &&&  ~~~e) &&&  ~~~(d ^^^ (e ^^^ f))) - 1 * d - 1 * (f ^^^  ~~~(d ||| e)) - 2 * (d ||| e) - 1 * ((d &&& f) ^^^  ~~~(d ^^^ (e &&& f))) - 3 * ((d |||  ~~~e) &&& (d ^^^ (e ^^^ f))) - 2 *  ~~~(d &&& f) - 1 * ( ~~~(d &&& e) &&&  ~~~(d ^^^ (e ^^^ f))) - 7 * (f ^^^ (d &&& e)) - 1 * (f ^^^  ~~~( ~~~d &&& (e &&& f))) + 4 *  ~~~( ~~~d &&& (e ^^^ f)) + 1 * (e ^^^ (d |||  ~~~f)) + 8 *  ~~~(d ||| (e ||| f)) - 28 *  ~~~(d ||| ( ~~~e ||| f)) + 1 *  ~~~( ~~~d ||| (e ||| f)) + 4 *  ~~~( ~~~d ||| ( ~~~e ||| f)) + 8 * ( ~~~d &&& ( ~~~e &&& f)) + 19 * ( ~~~d &&& (e &&& f)) + 20 * (d &&& ( ~~~e &&& f)) =  - 3 * (d ^^^ (e ^^^ f))

theorem ashr_exact_add_negative_shift_negative_thm (e : IntW 32) :
  ashr (const? 32 (-2)) (add e (const? 32 (-1))) { «exact» := true } ⊑
    ashr (const? 32 (-4)) e { «exact» := true }

theorem PR38781_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬(31#32 ≥ ↑32 ∨ 31#32 ≥ ↑32) →
    (x_1 >>> 31#32 ^^^ 1#32) &&& (x >>> 31#32 ^^^ 1#32) = zeroExtend 32 (ofBool (-1#32 <ₛ x_1 ||| x))

theorem sext_diff_i1_xor_sub_proof : sext_diff_i1_xor_sub_before ⊑ sext_diff_i1_xor_sub_after

theorem t6_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(True ∧ (0#8).ssubOverflow x = true) → ofBool (0#8 - x <ᵤ x) = ofBool (x <ₛ 0#8)

theorem select_ashr_icmp_bad_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ofBool (x_1 == 1#32) = 1#1 → ¬x_1 ≥ ↑32 → 1#32 ≥ ↑32 → False

theorem PR32830_thm (e e_1 e_2 : IntW 64) :
  LLVM.and (LLVM.or (LLVM.xor e_2 (const? 64 (-1))) e_1) (LLVM.or (LLVM.xor e_1 (const? 64 (-1))) e) ⊑
    LLVM.and (LLVM.or e_1 (LLVM.xor e_2 (const? 64 (-1)))) (LLVM.or e (LLVM.xor e_1 (const? 64 (-1))))

theorem bv_AndOrXor_2264 :
    ∀ (e e_1 : LLVM.IntW w),
      LLVM.or e (LLVM.xor (LLVM.xor e (LLVM.const? w (-1))) e_1) ⊑ LLVM.or e (LLVM.xor e_1 (LLVM.const? w (-1)))

theorem test12_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32),
  ¬zeroExtend 128 x &&& 31#128 ≥ ↑128 → True ∧ (x &&& 31#32).msb = true ∨ zeroExtend 64 (x &&& 31#32) ≥ ↑64 → False

theorem multiuse_select_thm.extracted_1._1 : ∀ (x : BitVec 1), x = 1#1 → 64#64 * (64#64 - zeroExtend 64 x) = 4032#64

theorem fold_sext_to_and_wrong6_proof : fold_sext_to_and_wrong6_before ⊑ fold_sext_to_and_wrong6_after

theorem test35_with_trunc_thm.extracted_1._1 : ∀ (x : BitVec 64),
  ofBool (0#32 ≤ₛ truncate 32 x) = 1#1 → ¬ofBool (x &&& 2147483648#64 == 0#64) = 1#1 → 60#32 = 100#32

theorem sgt_smax4_proof : sgt_smax4_before ⊑ sgt_smax4_after

theorem neg_slt_1_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ofBool (0#8 - x <ₛ 1#8) = ofBool (x <ᵤ BitVec.ofInt 8 (-127))

theorem t10_constants_thm.extracted_1._1 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ¬(12#32 ≥ ↑32 ∨ 14#64 ≥ ↑64) → 26#32 ≥ ↑32 → False

theorem e_428 :
    11 *  ~~~(x ^^^ y) - 1 *  ~~~y + 1 *  ~~~(x &&& y) + 5 * (x |||  ~~~y) + 1 * (x ^^^ y) - 16 *  ~~~(x ||| y) - 2 *  ~~~(x |||  ~~~y) - 6 * (x &&&  ~~~y) = 16 * (x &&& y)

theorem demorgan_and_zext_proof : demorgan_and_zext_before ⊑ demorgan_and_zext_after

@[simp]
theorem Lets.denote_var_pure [TyDenote d.Ty] [DialectDenote d] [Monad d.m] [LawfulMonad d.m]
  {Γstart Γ : Ctxt d.Ty}
  {lets : Lets d Γstart .pure Γ}
  (e : Expr d Γ .pure α)
  (V : Ctxt.Valuation Γstart) :
  (lets.var e).denote V
  = (e.pdenoteOp (lets.denote V) ++ lets.denotePure V)

theorem udiv_exact_ne_0_thm (e e_1 : IntW 8) :
  icmp IntPred.ne (LLVM.udiv e_1 e { «exact» := true }) (const? 8 0) ⊑
    icmp IntPred.ne e_1 (const? 8 0)

theorem lshrult_02_15_exact_proof : lshrult_02_15_exact_before ⊑ lshrult_02_15_exact_after

theorem main3_logical_thm.extracted_1._4 : ∀ (x : BitVec 32),
  ¬ofBool (x &&& 7#32 == 0#32) = 1#1 → ¬0#1 = 1#1 → 1#32 = zeroExtend 32 (ofBool (x &&& 55#32 != 0#32))

theorem shl_mul_mask_wrong_mul_const_proof : shl_mul_mask_wrong_mul_const_before ⊑ shl_mul_mask_wrong_mul_const_after

theorem a_or_b_const_proof : a_or_b_const_before ⊑ a_or_b_const_after

theorem icmp_ne_mul_nsw_nonequal_proof : icmp_ne_mul_nsw_nonequal_before ⊑ icmp_ne_mul_nsw_nonequal_after

theorem test_shl_nsw__nuw_is_safe_thm.extracted_1._2 : ∀ (x : BitVec 64) (x_1 : BitVec 32),
  ofBool (x_1 &&& 1073741822#32 == 0#32) = 1#1 →
    ¬(2#32 ≥ ↑32 ∨
          True ∧ (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)).msb = true ∨
            zeroExtend 64 (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)) ≥ ↑64) →
      x = x.sshiftRight' (zeroExtend 64 (x_1 <<< 2#32 &&& BitVec.ofInt 32 (-8)))

theorem lshrugt_03_13_exact_thm (e : IntW 4) :
  icmp IntPred.ugt (lshr e (const? 4 3) { «exact» := true }) (const? 4 (-3)) ⊑ const? 1 0

theorem ashr_and_thm.extracted_1._1 : ∀ (x : BitVec 8), ¬(x ≥ ↑8 ∨ x + 1#8 ≥ ↑8) → x ≥ ↑8 → False

theorem test16_proof : test16_before ⊑ test16_after

theorem demo4 (x y : BitVec 32) : (x ^^^ y) &&& 1#32 ||

theorem land_bor_left2_thm.extracted_1._2 : ∀ (x x_1 : BitVec 1), ¬x_1 = 1#1 → 0#1 ||

theorem e_1940 :
     - 7 *  ~~~(a &&& (b &&& c)) - 11 * ((a &&& b) ||| (a ^^^ (b ^^^ c))) + 1 * (c ^^^  ~~~(a &&& (b &&& c))) + 5 * (c ^^^  ~~~(a &&&  ~~~b)) - 3 * (b ^^^ ( ~~~a ||| (b &&& c))) - 1 * ((a |||  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) + 2 * (c ^^^ (a &&&  ~~~b)) - 1 * (a ||| ( ~~~b &&& c)) - 2 * ( ~~~c |||  ~~~(a ^^^ b)) + 7 * ( ~~~(a &&& b) &&& (a ^^^ (b ^^^ c))) - 1 * (c &&&  ~~~(a &&& b)) + 11 * ((a &&& c) ^^^  ~~~(b &&&  ~~~c)) - 1 *  ~~~(a ^^^ (b ^^^ c)) - 7 * (a &&& ( ~~~b ||| c)) - 5 * ((a &&& b) |||  ~~~(b ^^^ c)) - 1 * ((a |||  ~~~b) &&& (b ^^^ c)) - 7 * (b ^^^  ~~~( ~~~a ||| (b &&& c))) + 1 * ((a ||| b) &&& (b ^^^ c)) - 2 * (b ^^^ ( ~~~a ||| ( ~~~b ||| c))) - 1 * (a |||  ~~~b) + 1 * (a ^^^ ( ~~~b &&& c)) - 2 * ((a ^^^ b) &&&  ~~~(a ^^^ c)) - 2 * (c ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) + 4 * (b |||  ~~~c) - 2 * (a ||| c) - 1 * ((a &&& b) ^^^  ~~~(a ^^^ (b &&& c))) - 2 * ((a &&& b) ||| (b ^^^ c)) - 7 *  ~~~( ~~~a ||| (b &&& c)) + 5 *  ~~~(a ||| c) - 6 * (b ^^^ ( ~~~a &&& ( ~~~b ||| c))) - 11 * ( ~~~(a &&&  ~~~b) &&&  ~~~(b ^^^ c)) + 1 *  ~~~(a ||| b) + 2 * (b ^^^  ~~~(a &&& (b &&& c))) + 2 * ((a |||  ~~~b) &&&  ~~~(b ^^^ c)) - 6 *  ~~~( ~~~a &&& (b ||| c)) - 2 * ( ~~~a ||| (b &&& c)) + 2 * (b ^^^  ~~~(a ||| (b &&& c))) + 4 *  ~~~(a ^^^ ( ~~~b &&& c)) - 1 * (c ||| (a &&&  ~~~b)) - 2 * ((a &&&  ~~~b) |||  ~~~(b ^^^ c)) + 3 * (b ^^^ ( ~~~a ||| ( ~~~b &&& c))) + 5 * (b ^^^  ~~~(a ||| (b ^^^ c))) - 1 * (b ||| (a ^^^ c)) - 5 * (b ^^^ c) + 3 * (c ||| (a &&& b)) + 5 *  ~~~(a ||| (b ||| c)) + 16 *  ~~~(a ||| ( ~~~b ||| c)) + 32 *  ~~~( ~~~a ||| (b ||| c)) + 35 *  ~~~( ~~~a ||| ( ~~~b ||| c)) + 19 * ( ~~~a &&& ( ~~~b &&& c)) + 9 * ( ~~~a &&& (b &&& c)) + 36 * (a &&& ( ~~~b &&& c)) + 37 * (a &&& (b &&& c)) =  - 5 * (b &&& (a ||| c)) - 2 * ((b &&& c) ^^^  ~~~( ~~~a &&& (b ^^^ c)))

theorem positive_sameconst_shlnuw_thm.extracted_1._1 : ∀ (x : BitVec 8),
  ¬(3#8 ≥ ↑8 ∨ True ∧ x.sshiftRight' 3#8 <<< 3#8 >>> 3#8 ≠ x.sshiftRight' 3#8 ∨ 3#8 ≥ ↑8) →
    x.sshiftRight' 3#8 <<< 3#8 = x &&& BitVec.ofInt 8 (-8)

theorem e_1796 :
     - 11 * (b ^^^  ~~~(a ||| (b &&& c))) + 5 *  ~~~(a &&& (b ||| c)) - 7 * (c ^^^ ( ~~~a ||| (b ||| c))) + 3 * ( ~~~(a &&&  ~~~b) &&& (b ^^^ c)) - 2 * (b ^^^ ( ~~~a ||| (b &&& c))) - 2 *  ~~~( ~~~a &&& (b &&& c)) + 11 *  ~~~(a &&& c) - 1 * (b &&&  ~~~(a ^^^ c)) - 11 * (b ^^^ (a |||  ~~~c)) - 7 * (b ||| (a ^^^ c)) - 2 * (c ^^^ (a &&&  ~~~b)) + 3 * ( ~~~(a ||| b) ||| (a ^^^ (b ^^^ c))) + 2 * (c ^^^  ~~~(a |||  ~~~b)) - 5 * (c ^^^  ~~~( ~~~a &&& (b &&& c))) - 11 * (c &&& (a ||| b)) - 11 * (b &&&  ~~~c) - 7 * ((a |||  ~~~b) &&&  ~~~(a ^^^ (b ^^^ c))) + 11 * (b ^^^ ( ~~~a ||| (b ^^^ c))) - 2 * ((a ||| b) &&& (b ^^^ c)) - 6 *  ~~~b - 6 * ((a &&& b) ^^^  ~~~(a ^^^ ( ~~~b ||| c))) + 3 *  ~~~( ~~~a ||| (b ^^^ c)) + 2 * ( ~~~(a ||| b) |||  ~~~(b ^^^ c)) - 11 * ((a ^^^ b) |||  ~~~(a ^^^ c)) + 7 *  ~~~(a &&& (b &&& c)) + 7 * (c ^^^ (a ||| (b &&& c))) + 5 * ((b &&& c) ^^^  ~~~( ~~~a &&& (b ^^^ c))) - 5 *  ~~~(a &&& b) - 2 * (b ^^^ (a ||| (b ^^^ c))) - 1 * (b &&&  ~~~(a &&& c)) - 2 * (c ^^^  ~~~(a &&& (b &&& c))) + 26 *  ~~~(a ||| (b ||| c)) + 30 *  ~~~(a ||| ( ~~~b ||| c)) + 16 *  ~~~( ~~~a ||| (b ||| c)) + 31 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 13 * ( ~~~a &&& ( ~~~b &&& c)) + 42 * ( ~~~a &&& (b &&& c)) + 38 * (a &&& ( ~~~b &&& c)) + 27 * (a &&& (b &&& c)) = 1 *  ~~~(a &&&  ~~~b)

theorem ashrsgt_03_14_exact_proof : ashrsgt_03_14_exact_before ⊑ ashrsgt_03_14_exact_after

@[simp] theorem Valuation.nil_append {V : Γ.Valuation} :
    HAppend.hAppend (α := Valuation no_index _) (γ := Valuation no_index _)
      (nil (Ty:=Ty)) V -- nil ++ V
    = V

theorem test1_proof : test1_before ⊑ test1_after

theorem icmp_eq_and_pow2_shl_pow2_negative3_thm (e : IntW 32) :
  zext 32 (icmp IntPred.eq (LLVM.and (shl (const? 32 32) e) (const? 32 16)) (const? 32 0)) ⊑ const? 32 1

theorem lshrult_02_05_exact_thm.extracted_1._1 : ∀ (x : BitVec 4),
  ¬(True ∧ x >>> 2#4 <<< 2#4 ≠ x ∨ 2#4 ≥ ↑4) → ofBool (x >>> 2#4 <ᵤ 5#4) = 1#1

theorem lshr_mul_times_3_div_2_proof : lshr_mul_times_3_div_2_before ⊑ lshr_mul_times_3_div_2_after

theorem shift_no_xor_multiuse_cmp_thm.extracted_1._8 : ∀ (x x_1 x_2 x_3 : BitVec 32),
  ¬ofBool (x_3 &&& 1#32 == 0#32) = 1#1 →
    ¬(True ∧ ((x_3 &&& 1#32) <<< 1#32).sshiftRight' 1#32 ≠ x_3 &&& 1#32 ∨
          True ∧ (x_3 &&& 1#32) <<< 1#32 >>> 1#32 ≠ x_3 &&& 1#32 ∨ 1#32 ≥ ↑32) →
      (x_2 ||| 2#32) * x = (x_2 ||| (x_3 &&& 1#32) <<< 1#32) * x

theorem logic_and_logic_or_1_thm (e e_1 e_2 : IntW 1) :
  select (select e_2 e_1 (const? 1 0)) (const? 1 1) (select e_2 e (const? 1 0)) ⊑
    select e_2 (select e_1 (const? 1 1) e) (const? 1 0)

theorem e_1833 :
    1 * ( ~~~(a |||  ~~~b) |||  ~~~(a ^^^ (b ^^^ c))) + 2 * ((b &&& c) ^^^  ~~~(a &&& (b ^^^ c))) - 3 * ( ~~~b |||  ~~~(a ^^^ c)) - 5 *  ~~~( ~~~a ||| (b &&& c)) + 2 * (b ||| (a ^^^ c)) + 4 * (b ^^^  ~~~(a ||| ( ~~~b &&& c))) - 2 * ( ~~~c &&& (a ^^^ b)) + 1 * ((a &&& b) ^^^  ~~~(a ^^^ ( ~~~b ||| c))) - 2 * c - 1 * (b ^^^  ~~~( ~~~a &&& (b ||| c))) + 11 * (a &&& c) - 2 * ((a |||  ~~~b) &&& (b ^^^ c)) + 1 * (c ||| (a &&& b)) - 5 * (c ^^^  ~~~(a ||| b)) + 11 * ( ~~~(a ^^^ b) |||  ~~~(a ^^^ c)) + 3 * (b ^^^ ( ~~~a ||| (b ^^^ c))) - 2 * (b ^^^ (a ||| (b &&& c))) + 4 * ( ~~~(a |||  ~~~b) ||| (b ^^^ c)) - 2 * ((a &&&  ~~~b) |||  ~~~(b ^^^ c)) + 7 * (b ^^^ (a &&& c)) + 2 * ( ~~~(a &&& b) &&& (b ^^^ c)) - 7 * ( ~~~a &&& ( ~~~b ||| c)) - 5 * ( ~~~(a &&&  ~~~b) &&&  ~~~(b ^^^ c)) + 4 * (c ^^^ (a ||| ( ~~~b &&& c))) - 2 *  ~~~(a ^^^ c) - 6 * (c ^^^ (a ||| ( ~~~b ||| c))) - 1 *  ~~~(a ||| b) + 11 * (b ^^^  ~~~( ~~~a &&& ( ~~~b &&& c))) + 11 * (b ^^^  ~~~(a &&&  ~~~c)) + 5 * (b ^^^  ~~~(a &&& ( ~~~b &&& c))) - 1 * (c ^^^  ~~~( ~~~a &&& (b &&& c))) + 7 * (b ^^^  ~~~(a |||  ~~~c)) + 7 * (b ^^^  ~~~(a ||| c)) - 6 * ( ~~~(a |||  ~~~b) |||  ~~~(b ^^^ c)) - 6 *  ~~~(b |||  ~~~c) + 5 * (c ^^^  ~~~(a |||  ~~~b)) - 16 *  ~~~(a ||| (b ||| c)) + 3 *  ~~~( ~~~a ||| (b ||| c)) - 46 *  ~~~( ~~~a ||| ( ~~~b ||| c)) - 30 * ( ~~~a &&& ( ~~~b &&& c)) + 3 * ( ~~~a &&& (b &&& c)) - 36 * (a &&& ( ~~~b &&& c)) - 24 * (a &&& (b &&& c)) = 2 * (c &&& (a |||  ~~~b)) + 25 *  ~~~(a ||| ( ~~~b ||| c))

theorem sgt_smin4_thm (e e_1 : IntW 32) :
  icmp IntPred.slt (add e_1 (const? 32 3))
      (select (icmp IntPred.slt e (add e_1 (const? 32 3))) e (add e_1 (const? 32 3))) ⊑
    const? 1 0

theorem test9_thm.extracted_1._1 : ∀ (x x_1 : BitVec 32), x_1 ||

theorem or_simplify_ugt_fail_proof : or_simplify_ugt_fail_before ⊑ or_simplify_ugt_fail_after

theorem lshrult_01_13_proof : lshrult_01_13_before ⊑ lshrult_01_13_after

theorem shift_no_xor_multiuse_cmp_with_xor_thm (e e_1 e_2 e_3 : IntW 32) :
  mul (select (icmp IntPred.eq (LLVM.and e_3 (const? 32 1)) (const? 32 0)) e_2 (LLVM.xor e_2 (const? 32 2)))
      (select (icmp IntPred.eq (LLVM.and e_3 (const? 32 1)) (const? 32 0)) e_1 e) ⊑
    mul (LLVM.xor e_2 (shl (LLVM.and e_3 (const? 32 1)) (const? 32 1) { «nsw» := true, «nuw» := true }))
      (select (icmp IntPred.eq (LLVM.and e_3 (const? 32 1)) (const? 32 0)) e_1 e)

@[ext]
theorem ext {x y : BitStream} (h : ∀ i, x i = y i) : x = y

theorem exact_lshr_ne_proof : exact_lshr_ne_before ⊑ exact_lshr_ne_after

theorem or_test2_thm (e : IntW 7) : LLVM.or (shl e (const? 7 6)) (const? 7 (-64)) ⊑ const? 7 (-64)
</all_available_lemmas>

<local_ctx>
import LeanMLIR.Framework

import LeanMLIR.Transforms.Rewrite.Mapping

open Ctxt (Var VarSet Valuation Hom)

variable {d} [DialectSignature d] [DecidableEq d.Ty]

variable {Γ : Ctxt d.Ty} {ty : d.Ty}

abbrev MatchVarM (Δ Γ : Ctxt d.Ty) := (StateT (Mapping Δ Γ) Option)

abbrev MatchVar (Δ Γ : Ctxt d.Ty)  := MatchVarM Δ Γ Unit

def MatchVarM.unifyVars {Δ Γ : Ctxt d.Ty} (v : Δ.Var t) (w : Γ.Var t) : MatchVar Δ Γ :=
  fun ma =>
    match ma.lookup ⟨_, v⟩ with
    | some v =>
      if v = w then
        some ((), ma)
      else
        none
    | none =>
      some ((), AList.insert ⟨_, v⟩ w ma)

open MatchVarM

variable [DecidableEq d.Op]

def matchArg [DecidableEq d.Op]
    (lets : Lets d Γ_in eff Γ_out) (matchLets : Lets d Δ_in .pure Δ_out) :
    {l : List d.Ty} → HVector (Var Γ_out) l → HVector (Var Δ_out) l →
    MatchVar Δ_in Γ_out
  | _, .nil, .nil => return
  | t::l, .cons vₗ vsₗ, .cons vᵣ vsᵣ => do
      matchVar (t := t) lets vₗ matchLets vᵣ
      matchArg lets matchLets vsₗ vsᵣ
  termination_by l => (sizeOf matchLets, l.length + 1)

def matchVar {Γ_in Γ_out Δ_in Δ_out : Ctxt d.Ty} {t : d.Ty} [DecidableEq d.Op]
    (lets : Lets d Γ_in eff Γ_out) (v : Var Γ_out t) :
    (matchLets : Lets d Δ_in .pure Δ_out) →
    (w : Var Δ_out t) →
    MatchVar Δ_in Γ_out
   
  | @Lets.var _ _ _ _ Δ_out ts matchLets matchExpr, w => by admit /- proof elided -/
      | right w =>
        exact matchVar lets v matchLets w
      | left w => exact do
        let ⟨ts', w', ie⟩ ← lets.getPureExpr v
        if hs : ∃ h : ie.op = matchExpr.op, ie.regArgs = (h ▸ matchExpr.regArgs) then
          have hts : Ctxt.ofList ts' = ts := by admit /- proof elided -/

end

section MatchVar

variable [DecidableEq d.Op] {Γ_in Γ_out Δ_in Δ_out t te}
          {lets : Lets d Γ_in eff Γ_out} {v : Var Γ_out t}
          {matchLets : Lets d Δ_in .pure Δ_out}
          {matchExpr : Expr d Δ_out .pure te}

variable (lets v matchLets w) (mapIn : Mapping _ _) in

variable (lets matchLets) {tys} (vs ws : HVector _ tys) (mapIn : Mapping _ _) in

namespace MatchVarResult

variable [TyDenote d.Ty] [∀ (t : d.Ty), Inhabited ⟦t⟧] in

section Left

variable {w : Δ_out.Var t}

variable {mapIn} (mapOut : MatchVarResult lets v (.var matchLets matchExpr) w.appendInr mapIn)

end Left

variable {w : Var ⟨te⟩ _} {mapIn}

end MatchVarResult

end MatchVar

section SubsetEntries

def MatchVar.IsMonotone (f : MatchVar Δ Γ) : Prop :=
    ∀ mapIn, ∀ mapOut ∈ f mapIn,
      mapIn.entries ⊆ mapOut.2.entries

open MatchVar

section UnifyVars

variable {Δ Γ : Ctxt d.Ty} {t} (w : Δ.Var t) (v : Γ.Var t)

end UnifyVars

variable [DecidableEq d.Op]
</local_ctx>

<target_theorem>
theorem isMonotone_matchVarArg_aux (lets : Lets d Γ_in eff Γ_out) :
    (
     ∀  (Δ_out : Ctxt d.Ty)
        (matchLets : Lets d Δ_in EffectKind.pure Δ_out) (l : List d.Ty)
        (argsl : HVector Γ_out.Var l) (argsr : HVector Δ_out.Var l),
        (matchArg lets matchLets argsl argsr).IsMonotone
    )
    ∧ (
      ∀ (Δ_out : Ctxt d.Ty) (t : d.Ty) (v : Γ_out.Var t)
        (matchLets : Lets d Δ_in EffectKind.pure Δ_out)
        (w : Var Δ_out t),
        (matchVar lets v matchLets w).IsMonotone
    ) :=
</target_theorem>

