diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
index d6f048d0f3..be3864b098 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Simproc.lean
@@ -111,10 +111,10 @@ builtin_simproc [bv_normalize] bv_udiv_of_two_pow (((_ : BitVec _) / (BitVec.ofN
   }
 
 builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec.ofNat _ _)) := fun e => do
-  let_expr BEq.beq α inst outerLhs rhs := e | return .continue
+  let_expr BEq.beq _ _ outerLhs rhs := e | return .continue
   let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue
   let_expr Complement.complement _ _ lhs := outerLhs | return .continue
-  let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst lhs (toExpr (~~~rhsVal))
+  let expr ← mkAppM ``BEq.beq #[lhs, toExpr (~~~rhsVal)]
   let proof :=
     mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm)
       (toExpr w)
@@ -123,10 +123,10 @@ builtin_simproc [bv_normalize] bv_equal_const_not (~~~(_ : BitVec _) == (BitVec.
   return .visit { expr := expr, proof? := some proof }
 
 builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_ : BitVec _)) := fun e => do
-  let_expr BEq.beq α inst lhs outerRhs := e | return .continue
+  let_expr BEq.beq _ _ lhs outerRhs := e | return .continue
   let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue
   let_expr Complement.complement _ _ rhs := outerRhs | return .continue
-  let expr := mkApp4 (mkConst ``BEq.beq [0]) α inst rhs (toExpr (~~~lhsVal))
+  let expr ← mkAppM ``BEq.beq #[rhs, toExpr (~~~lhsVal)]
   let proof :=
     mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.not_eq_comm')
       (toExpr w)
@@ -135,12 +135,12 @@ builtin_simproc [bv_normalize] bv_equal_const_not' ((BitVec.ofNat _ _) == ~~~(_
   return .visit { expr := expr, proof? := some proof }
 
 builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec _) == (BitVec.ofNat _ _)) := fun e => do
-  let_expr BEq.beq α instBEq outerLhs rhs := e | return .continue
+  let_expr BEq.beq _ _ outerLhs rhs := e | return .continue
   let some ⟨w, rhsVal⟩ ← getBitVecValue? rhs | return .continue
   if -1#w != rhsVal then return .continue
   let_expr HAnd.hAnd _ _ _ _ llhs lrhs := outerLhs | return .continue
-  let newLhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq llhs rhs
-  let newRhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq lrhs rhs
+  let newLhs ← mkAppM ``BEq.beq #[llhs, rhs]
+  let newRhs ← mkAppM ``BEq.beq #[lrhs, rhs]
   let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs
   let proof :=
     mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.and_eq_allOnes)
@@ -150,12 +150,12 @@ builtin_simproc [bv_normalize] bv_and_eq_allOnes ((_ : BitVec _) &&& (_ : BitVec
   return .visit { expr := expr, proof? := some proof }
 
 builtin_simproc [bv_normalize] bv_allOnes_eq_and ((BitVec.ofNat _ _) == (_ : BitVec _) &&& (_ : BitVec _)) := fun e => do
-  let_expr BEq.beq α instBEq lhs outerRhs := e | return .continue
+  let_expr BEq.beq _ _ lhs outerRhs := e | return .continue
   let some ⟨w, lhsVal⟩ ← getBitVecValue? lhs | return .continue
   if -1#w != lhsVal then return .continue
   let_expr HAnd.hAnd _ _ _ _ rlhs rrhs := outerRhs | return .continue
-  let newLhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq rlhs lhs
-  let newRhs := mkApp4 (mkConst ``BEq.beq [0]) α instBEq rrhs lhs
+  let newLhs ← mkAppM ``BEq.beq #[rlhs, lhs]
+  let newRhs ← mkAppM ``BEq.beq #[rrhs, lhs]
   let expr := mkApp2 (mkConst ``Bool.and) newLhs newRhs
   let proof :=
     mkApp3 (mkConst ``Std.Tactic.BVDecide.Frontend.Normalize.BitVec.allOnes_eq_and)
diff --git a/src/Std/Sat/AIG/Basic.lean b/src/Std/Sat/AIG/Basic.lean
index b7e47b7e06..5fed87fcf2 100644
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -224,21 +224,36 @@ instance : Membership α (AIG α) where
   mem := Mem
 
 /--
-A reference to a node within an AIG. This is the `AIG` analog of `Bool`.
+A reference to a node within an AIG.
 -/
 structure Ref (aig : AIG α) where
   gate : Nat
+  invert : Bool
   hgate : gate < aig.decls.size
 
 /--
 A `Ref` into `aig1` is also valid for `aig2` if `aig1` is smaller than `aig2`.
 -/
 @[inline]
-def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1)
-    (h : aig1.decls.size ≤ aig2.decls.size) :
+def Ref.cast {aig1 aig2 : AIG α} (ref : Ref aig1) (h : aig1.decls.size ≤ aig2.decls.size) :
     Ref aig2 :=
   { ref with hgate := by have := ref.hgate; omega }
 
+
+/--
+Flip the polarity of `Ref` if `inv` is set.
+-/
+@[inline]
+def Ref.flip {aig : AIG α} (ref : Ref aig) (inv : Bool) : Ref aig :=
+  { ref with invert := inv ^^ ref.invert }
+
+/--
+Flip the polarity of `Ref`.
+-/
+@[inline]
+def Ref.not {aig : AIG α} (ref : Ref aig) : Ref aig :=
+  ref.flip true
+
 /--
 A pair of `Ref`s, useful for `LawfulOperator`s that act on two `Ref`s at a time.
 -/
@@ -255,6 +270,14 @@ def BinaryInput.cast {aig1 aig2 : AIG α} (input : BinaryInput aig1)
     BinaryInput aig2 :=
   { input with lhs := input.lhs.cast h, rhs := input.rhs.cast h }
 
+/--
+Flip the current inverter settings of the `BinaryInput` if `linv` or `rinv` is set respectively.
+-/
+@[inline]
+def BinaryInput.invert {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
+    BinaryInput aig :=
+  { input with lhs := input.lhs.flip linv, rhs := input.rhs.flip rinv }
+
 /--
 A collection of 3 of `Ref`s, useful for `LawfulOperator`s that act on three `Ref`s at a time,
 in particular multiplexer style functions.
@@ -292,14 +315,14 @@ Transform an `Entrypoint` into a graphviz string. Useful for debugging purposes.
 -/
 def toGraphviz {α : Type} [DecidableEq α] [ToString α] [Hashable α] (entry : Entrypoint α) :
     String :=
-  let ⟨⟨decls, _, hinv⟩, ⟨idx, h⟩⟩ := entry
+  let ⟨⟨decls, _, hinv⟩, ⟨idx, invert, h⟩⟩ := entry
   let (dag, s) := go "" decls hinv idx h |>.run ∅
   let nodes := s.fold (fun x y ↦ x ++ toGraphvizString decls y) ""
   "Digraph AIG {" ++ nodes ++ dag ++ "}"
 where
   go {α : Type} [DecidableEq α] [ToString α] [Hashable α] (acc : String) (decls : Array (Decl α))
-      (hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size)
-        : StateM (HashSet (Fin decls.size)) String := do
+      (hinv : IsDAG α decls) (idx : Nat) (hidx : idx < decls.size) :
+      StateM (HashSet (Fin decls.size)) String := do
     let fidx : Fin decls.size := Fin.mk idx hidx
     if (← get).contains fidx then
       return acc
@@ -325,9 +348,9 @@ where
 A vector of references into `aig`. This is the `AIG` analog of `BitVec`.
 -/
 structure RefVec (aig : AIG α) (w : Nat) where
-  refs : Array Nat
+  refs : Array (Nat × Bool)
   hlen : refs.size = w
-  hrefs : ∀ (h : i < w), refs[i] < aig.decls.size
+  hrefs : ∀ (h : i < w), refs[i].1 < aig.decls.size
 
 /--
 A sequence of references bundled with their AIG.
@@ -362,7 +385,7 @@ structure ExtendTarget (aig : AIG α) (newWidth : Nat) where
 Evaluate an `AIG.Entrypoint` using some assignment for atoms.
 -/
 def denote (assign : α → Bool) (entry : Entrypoint α) : Bool :=
-  go entry.ref.gate entry.aig.decls assign entry.ref.hgate entry.aig.invariant
+  go entry.ref.gate entry.aig.decls assign entry.ref.hgate entry.aig.invariant ^^ entry.ref.invert
 where
   go (x : Nat) (decls : Array (Decl α)) (assign : α → Bool) (h1 : x < decls.size)
       (h2 : IsDAG α decls) :
@@ -400,61 +423,23 @@ def unexpandDenote : Lean.PrettyPrinter.Unexpander
 /--
 The denotation of the sub-DAG in the `aig` at node `start` is false for all assignments.
 -/
-def UnsatAt (aig : AIG α) (start : Nat) (h : start < aig.decls.size) : Prop :=
-  ∀ assign, ⟦aig, ⟨start, h⟩, assign⟧ = false
+def UnsatAt (aig : AIG α) (start : Nat) (invert : Bool) (h : start < aig.decls.size) : Prop :=
+  ∀ assign, ⟦aig, ⟨start, invert, h⟩, assign⟧ = false
 
 /--
 The denotation of the `Entrypoint` is false for all assignments.
 -/
 def Entrypoint.Unsat (entry : Entrypoint α) : Prop :=
-  entry.aig.UnsatAt entry.ref.gate entry.ref.hgate
-
-/--
-An input to an AIG gate.
--/
-structure Fanin (aig : AIG α) where
-  /--
-  The node we are referring to.
-  -/
-  ref : Ref aig
-  /--
-  Whether the node is inverted
-  -/
-  inv : Bool
-
-/--
-The `Ref.cast` equivalent for `Fanin`.
--/
-@[inline]
-def Fanin.cast {aig1 aig2 : AIG α} (fanin : Fanin aig1)
-    (h : aig1.decls.size ≤ aig2.decls.size) :
-    Fanin aig2 :=
-  { fanin with ref := fanin.ref.cast h }
-
-/--
-The input type for creating AIG and gates.
--/
-structure GateInput (aig : AIG α) where
-  lhs : Fanin aig
-  rhs : Fanin aig
-
-/--
-The `Ref.cast` equivalent for `GateInput`.
--/
-@[inline]
-def GateInput.cast {aig1 aig2 : AIG α} (input : GateInput aig1)
-    (h : aig1.decls.size ≤ aig2.decls.size) :
-    GateInput aig2 :=
-  { input with lhs := input.lhs.cast h, rhs := input.rhs.cast h }
+  entry.aig.UnsatAt entry.ref.gate entry.ref.invert entry.ref.hgate
 
 /--
 Add a new and inverter gate to the AIG in `aig`. Note that this version is only meant for proving,
 for production purposes use `AIG.mkGateCached` and equality theorems to this one.
 -/
-def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
+def mkGate (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
   let g := aig.decls.size
   let decls :=
-    aig.decls.push <| .gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv
+    aig.decls.push <| .gate input.lhs.gate input.rhs.gate input.lhs.invert input.rhs.invert
   let cache := aig.cache.noUpdate
   have invariant := by
     intro i lhs' rhs' linv' rinv' h1 h2
@@ -462,10 +447,10 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · injections
-      have := input.lhs.ref.hgate
-      have := input.rhs.ref.hgate
+      have := input.lhs.hgate
+      have := input.rhs.hgate
       omega
-  ⟨{ aig with decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
+  ⟨{ aig with decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩
 
 /--
 Add a new input node to the AIG in `aig`. Note that this version is only meant for proving,
@@ -481,7 +466,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
-  ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
+  ⟨{ decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩
 
 /--
 Add a new constant node to `aig`. Note that this version is only meant for proving,
@@ -497,17 +482,17 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
     split at h2
     · apply aig.invariant <;> assumption
     · contradiction
-  ⟨{ decls, invariant, cache }, ⟨g, by simp [g, decls]⟩⟩
+  ⟨{ decls, invariant, cache }, ⟨g, false, by simp [g, decls]⟩⟩
 
 
 /--
 Determine whether `ref` is a `Decl.const` with value `b`.
 -/
 def isConstant (aig : AIG α) (ref : Ref aig) (b : Bool) : Bool :=
-  let ⟨gate, hgate⟩ := ref
+  let ⟨gate, invert, hgate⟩ := ref
   let decl := aig.decls[gate]'hgate
   match decl with
-  | .const val => b = val
+  | .const val => (invert ^^ b) = val
   | _ => false
 
 end AIG
diff --git a/src/Std/Sat/AIG/CNF.lean b/src/Std/Sat/AIG/CNF.lean
index b43ced351d..d1810717e2 100644
--- a/src/Std/Sat/AIG/CNF.lean
+++ b/src/Std/Sat/AIG/CNF.lean
@@ -121,7 +121,7 @@ Tseitin transformation. This is done by combining the atom assignment with an as
 auxiliary variables, that just evaluates the AIG at the corresponding node.
 -/
 def cnfSatAssignment (aig : AIG Nat) (assign1 : Nat → Bool) : CNFVar aig → Bool :=
-  mixAssigns assign1 (fun idx => ⟦aig, ⟨idx.val, idx.isLt⟩, assign1⟧)
+  mixAssigns assign1 (fun idx => ⟦aig, ⟨idx.val, false, idx.isLt⟩, assign1⟧)
 
 @[simp]
 theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x := by
@@ -129,7 +129,7 @@ theorem satAssignment_inl : (cnfSatAssignment aig assign1) (.inl x) = assign1 x
 
 @[simp]
 theorem satAssignment_inr :
-    (cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, x.isLt⟩, assign1⟧ := by
+    (cnfSatAssignment aig assign1) (.inr x) = ⟦aig, ⟨x.val, false, x.isLt⟩, assign1⟧ := by
   simp [cnfSatAssignment, mixAssigns]
 
 /--
@@ -156,7 +156,7 @@ structure Cache.Inv (cnf : CNF (CNFVar aig)) (marks : Array Bool) (hmarks : mark
   -/
   heval : ∀ (assign : CNFVar aig → Bool) (_heval : cnf.eval assign = true) (idx : Nat)
             (hbound : idx < aig.decls.size) (_hmark : marks[idx]'(by omega) = true),
-              ⟦aig, ⟨idx, hbound⟩, projectLeftAssign assign⟧ = (projectRightAssign assign) idx hbound
+              ⟦aig, ⟨idx, false, hbound⟩, projectLeftAssign assign⟧ = (projectRightAssign assign) idx hbound
 
 
 /--
@@ -287,7 +287,7 @@ def Cache.addConst (cache : Cache aig cnf) (idx : Nat) (h : idx < aig.decls.size
           · next heq =>
             simp only [heq, CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq]
               at htip heval
-            simp only [denote_idx_const htip, projectRightAssign_property, heval]
+            simp [denote_idx_const htip, projectRightAssign_property, heval]
           · next heq =>
             simp only [CNF.eval_append, Decl.constToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval
             have := cache.inv.heval assign heval.right idx hbound hmarked
@@ -376,7 +376,7 @@ def Cache.addGate (cache : Cache aig cnf) {hlb} {hrb} (idx : Nat) (h : idx < aig
               at htip heval
             have hleval := cache.inv.heval assign heval.right lhs (by omega) hl
             have hreval := cache.inv.heval assign heval.right rhs (by omega) hr
-            simp only [denote_idx_gate htip, hleval, projectRightAssign_property, hreval, heval]
+            cases linv <;> cases rinv <;> simp [denote_idx_gate htip, hleval, projectRightAssign_property, hreval, heval]
           · next heq =>
             simp only [CNF.eval_append, Decl.gateToCNF_eval, Bool.and_eq_true, beq_iff_eq] at heval
             have := cache.inv.heval assign heval.right idx hbound hmarked
@@ -439,7 +439,7 @@ theorem State.Inv_gateToCNF {aig : AIG Nat} {h}
         rinv)
     := by
   intro assign1
-  simp [CNF.sat_def, denote_idx_gate heq]
+  cases linv <;> cases rinv <;> simp [CNF.sat_def, denote_idx_gate heq]
 
 /--
 The state to accumulate CNF clauses as we run our Tseitin transformation on the AIG.
@@ -566,10 +566,12 @@ theorem State.unsat_def (state : State aig) :
   rfl
 
 @[simp]
-theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by simp [State.eval]
+theorem State.eval_eq : State.eval assign state = state.cnf.eval assign := by
+  simp [State.eval]
 
 @[simp]
-theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by simp [State.sat_def]
+theorem State.sat_iff : State.Sat assign state ↔ state.cnf.Sat assign := by
+  simp [State.sat_def]
 
 @[simp]
 theorem State.unsat_iff : State.Unsat state ↔ state.cnf.Unsat := by simp [State.unsat_def]
@@ -581,7 +583,7 @@ Convert an AIG into CNF, starting at some entry node.
 -/
 def toCNF (entry : Entrypoint Nat) : CNF Nat :=
   let ⟨state, _⟩ := go entry.aig entry.ref.gate entry.ref.hgate (toCNF.State.empty entry.aig)
-  let cnf : CNF (CNFVar entry.aig) := [(.inr ⟨entry.ref.gate, entry.ref.hgate⟩, true)] :: state.cnf
+  let cnf : CNF (CNFVar entry.aig) := [(.inr ⟨entry.ref.gate, entry.ref.hgate⟩, !entry.ref.invert)] :: state.cnf
   cnf.relabel inj
 where
   inj {aig : AIG Nat} (var : CNFVar aig) : Nat :=
@@ -664,8 +666,8 @@ theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size)
   rw [State.sat_iff]
   simp [this]
 
-theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) :
-    ⟦aig, ⟨start, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by
+theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (inv) (h1) (assign1) :
+    ⟦aig, ⟨start, inv, h1⟩, assign1⟧ → (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1) := by
   have := go_sat aig start h1 assign1 (.empty aig)
   simp only [State.Sat, CNF.sat_def] at this
   simp [this]
@@ -674,26 +676,25 @@ theorem toCNF.go_as_denote' (aig : AIG Nat) (start) (h1) (assign1) :
 Connect SAT results about the CNF to SAT results about the AIG.
 -/
 theorem toCNF.go_as_denote (aig : AIG Nat) (start) (h1) (assign1) :
-    ((⟦aig, ⟨start, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?)
+    ((⟦aig, ⟨start, inv, h1⟩, assign1⟧ && (go aig start h1 (.empty aig)).val.eval (cnfSatAssignment aig assign1)) = sat?)
       →
-    (⟦aig, ⟨start, h1⟩, assign1⟧ = sat?) := by
-  have := go_as_denote' aig start h1 assign1
+    (⟦aig, ⟨start, inv, h1⟩, assign1⟧ = sat?) := by
+  have := go_as_denote' aig start inv h1 assign1
   by_cases CNF.eval (cnfSatAssignment aig assign1) (go aig start h1 (State.empty aig)).val.cnf <;> simp_all
 
 /--
 Connect SAT results about the AIG to SAT results about the CNF.
 -/
-theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool}:
-    (⟦aig, ⟨start, h1⟩, projectLeftAssign assign⟧ = false)
+theorem toCNF.denote_as_go {assign : AIG.CNFVar aig → Bool} :
+    (⟦aig, ⟨start, inv, h1⟩, projectLeftAssign assign⟧ = false)
       →
-    CNF.eval assign (([(.inr ⟨start, h1⟩, true)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by
+    CNF.eval assign (([(.inr ⟨start, h1⟩, !inv)] :: (go aig start h1 (.empty aig)).val.cnf)) = false := by
   intro h
   match heval1:(go aig start h1 (State.empty aig)).val.cnf.eval assign with
   | true =>
     have heval2 := (go aig start h1 (.empty aig)).val.cache.inv.heval
     specialize heval2 assign heval1 start h1 go_marks
-    simp only [h, projectRightAssign_property, Bool.false_eq] at heval2
-    simp [heval2]
+    cases inv <;> simp_all
   | false =>
     simp [heval1]
 
@@ -707,7 +708,7 @@ theorem toCNF_equisat (entry : Entrypoint Nat) : (toCNF entry).Unsat ↔ entry.U
     · intro h assign1
       apply toCNF.go_as_denote
       specialize h (toCNF.cnfSatAssignment entry.aig assign1)
-      simpa using h
+      rcases entry with ⟨_, ⟨_, _ | _, _⟩⟩ <;> simpa using h
     · intro h assign
       apply toCNF.denote_as_go
       specialize h (toCNF.projectLeftAssign assign)
diff --git a/src/Std/Sat/AIG/Cached.lean b/src/Std/Sat/AIG/Cached.lean
index 8537c6f07c..0627ba521c 100644
--- a/src/Std/Sat/AIG/Cached.lean
+++ b/src/Std/Sat/AIG/Cached.lean
@@ -29,7 +29,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
   let decl := .atom n
   match cache.get? decl with
   | some hit =>
-    ⟨⟨decls, cache, inv⟩ , hit.idx, hit.hbound⟩
+    ⟨⟨decls, cache, inv⟩ , hit.idx, false, hit.hbound⟩
   | none =>
     let g := decls.size
     let cache := cache.insert decls decl
@@ -40,7 +40,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
       split at h2
       · apply inv <;> assumption
       · contradiction
-  ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
+    ⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩
 
 /--
 A version of `AIG.mkConst` that uses the subterm cache in `AIG`. This version is meant for
@@ -51,7 +51,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
   let decl := .const val
   match cache.get? decl with
   | some hit =>
-    ⟨⟨decls, cache, inv⟩, hit.idx, hit.hbound⟩
+    ⟨⟨decls, cache, inv⟩, hit.idx, false, hit.hbound⟩
   | none =>
     let g := decls.size
     let cache := cache.insert decls decl
@@ -62,7 +62,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
       split at h2
       · apply inv <;> assumption
       · contradiction
-  ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
+    ⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩
 
 /--
 A version of `AIG.mkGate` that uses the subterm cache in `AIG`. This version is meant for
@@ -70,26 +70,26 @@ programming, for proving purposes use `AIG.mkGate` and equality theorems to this
 
 Beyond caching this function also implements a subset of the optimizations presented in:
 -/
-def mkGateCached (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
-  let lhs := input.lhs.ref.gate
-  let rhs := input.rhs.ref.gate
+def mkGateCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
+  let lhs := input.lhs.gate
+  let rhs := input.rhs.gate
   if lhs < rhs then
     go aig ⟨input.lhs, input.rhs⟩
   else
     go aig ⟨input.rhs, input.lhs⟩
 where
-  go (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
+  go (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
     let ⟨decls, cache, inv⟩ := aig
-    let lhs := input.lhs.ref.gate
-    let rhs := input.rhs.ref.gate
-    let linv := input.lhs.inv
-    let rinv := input.rhs.inv
-    have := input.lhs.ref.hgate
-    have := input.rhs.ref.hgate
+    let lhs := input.lhs.gate
+    let rhs := input.rhs.gate
+    let linv := input.lhs.invert
+    let rinv := input.rhs.invert
+    have := input.lhs.hgate
+    have := input.rhs.hgate
     let decl := .gate lhs rhs linv rinv
     match cache.get? decl with
     | some hit =>
-      ⟨⟨decls, cache, inv⟩, ⟨hit.idx, hit.hbound⟩⟩
+      ⟨⟨decls, cache, inv⟩, ⟨hit.idx, false, hit.hbound⟩⟩
     | none =>
       /-
       Here we implement the constant propagating subset of:
@@ -102,15 +102,15 @@ where
       | _, .const true, _, true | _, .const false, _, false =>
         mkConstCached ⟨decls, cache, inv⟩ false
       -- Left Neutrality
-      | .const true, _, false, false | .const false, _, true, false =>
-        ⟨⟨decls, cache, inv⟩, rhs, (by assumption)⟩
+      | .const true, _, false, _ | .const false, _, true, _ =>
+        ⟨⟨decls, cache, inv⟩, rhs, rinv, by assumption⟩
       -- Right Neutrality
-      | _, .const true, false, false | _, .const false, false, true =>
-        ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩
+      | _, .const true, _, false | _, .const false, _, true =>
+        ⟨⟨decls, cache, inv⟩, lhs, linv, by assumption⟩
       | _, _, _, _ =>
         if lhs == rhs && linv == false && rinv == false then
           -- Idempotency rule
-         ⟨⟨decls, cache, inv⟩, lhs, (by assumption)⟩
+         ⟨⟨decls, cache, inv⟩, lhs, false, by assumption⟩
         else if lhs == rhs && linv == !rinv then
           -- Contradiction rule
           mkConstCached ⟨decls, cache, inv⟩ false
@@ -125,7 +125,7 @@ where
             split at h2
             · apply inv <;> assumption
             · injections; omega
-          ⟨⟨decls, cache, inv⟩, ⟨g, by simp [g, decls]⟩⟩
+          ⟨⟨decls, cache, inv⟩, ⟨g, false, by simp [g, decls]⟩⟩
 
 end AIG
 
diff --git a/src/Std/Sat/AIG/CachedGates.lean b/src/Std/Sat/AIG/CachedGates.lean
index 5c4ed37724..40ceef0562 100644
--- a/src/Std/Sat/AIG/CachedGates.lean
+++ b/src/Std/Sat/AIG/CachedGates.lean
@@ -22,94 +22,43 @@ variable {α : Type} [Hashable α] [DecidableEq α]
 /--
 Create a not gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.
 -/
-def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α :=
-  -- ¬x = true && invert x
-  let res := aig.mkConstCached true
-  let aig := res.aig
-  let constRef := res.ref
-  aig.mkGateCached {
-    lhs := {
-      ref := constRef
-      inv := false
-    }
-    rhs := {
-      ref := gate.cast <| by
-        intros
-        apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
-        omega
-      inv := true
-    }
-  }
-
 @[inline]
-def BinaryInput.asGateInput {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
-    GateInput aig :=
-  { lhs := { ref := input.lhs, inv := linv }, rhs := { ref := input.rhs, inv := rinv } }
+def mkNotCached (aig : AIG α) (gate : Ref aig) : Entrypoint α :=
+  ⟨aig, gate.not⟩
 
 /--
 Create an and gate in the input AIG. This uses the builtin cache to enable automated subterm
 sharing.
 -/
+@[inline]
 def mkAndCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-  aig.mkGateCached <| input.asGateInput false false
+  aig.mkGateCached input
 
 /--
 Create an or gate in the input AIG. This uses the builtin cache to enable automated subterm sharing.
 -/
 def mkOrCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-  -- x or y = true && (invert (invert x && invert y))
-  let res := aig.mkGateCached <| input.asGateInput true true
+  -- x or y = invert (invert x && invert y)
+  let res := aig.mkGateCached <| input.invert true true
   let aig := res.aig
   let auxRef := res.ref
-  let res := aig.mkConstCached true
-  let aig := res.aig
-  let constRef := res.ref
-  aig.mkGateCached {
-      lhs := {
-        ref := constRef
-        inv := false
-      },
-      rhs := {
-        ref := auxRef.cast <| by
-          intros
-          simp +zetaDelta only
-          apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
-          omega
-        inv := true
-      }
-    }
+  ⟨aig, auxRef.not⟩
 
 /--
 Create an xor gate in the input AIG. This uses the builtin cache to enable automated subterm
 sharing.
 -/
 def mkXorCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-  -- x xor y = (invert (invert (x && y))) && (invert ((invert x) && (invert y)))
-  let res := aig.mkGateCached <| input.asGateInput false false
+  -- x xor y = (invert (x && y)) && (invert ((invert x) && (invert y)))
+  let res := aig.mkGateCached input
   let aig := res.aig
   let aux1Ref := res.ref
-  let rinput :=
-    (input.asGateInput true true).cast
-      (by
-        intros
-        apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
-        omega)
-  let res := aig.mkGateCached rinput
+  let input := input.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
+  let res := aig.mkGateCached (input.invert true true)
   let aig := res.aig
   let aux2Ref := res.ref
-  aig.mkGateCached {
-    lhs := {
-      ref := aux1Ref.cast <| by
-        simp +zetaDelta only
-        apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
-        omega
-      inv := true
-    },
-    rhs := {
-      ref := aux2Ref
-      inv := true
-    }
-  }
+  let aux1Ref := aux1Ref.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
+  aig.mkGateCached ⟨aux1Ref.not, aux2Ref.not⟩
 
 /--
 Create an equality gate in the input AIG. This uses the builtin cache to enable automated subterm
@@ -117,58 +66,26 @@ sharing.
 -/
 def mkBEqCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
   -- a == b = (invert (a && (invert b))) && (invert ((invert a) && b))
-  let res := aig.mkGateCached <| input.asGateInput false true
+  let res := aig.mkGateCached <| input.invert false true
   let aig := res.aig
   let aux1Ref := res.ref
-  let rinput :=
-    (input.asGateInput true false).cast
-      (by
-        intros
-        apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
-        omega)
-  let res := aig.mkGateCached rinput
+  let input := input.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
+  let res := aig.mkGateCached (input.invert true false)
   let aig := res.aig
   let aux2Ref := res.ref
-  aig.mkGateCached {
-    lhs := {
-      ref := aux1Ref.cast <| by
-        simp +zetaDelta only
-        apply LawfulOperator.le_size_of_le_aig_size (f := mkGateCached)
-        omega
-      inv := true
-    },
-    rhs := {
-      ref := aux2Ref
-      inv := true
-    }
-  }
+  let aux1Ref := aux1Ref.cast <| by apply LawfulOperator.le_size (f := mkGateCached)
+  aig.mkGateCached ⟨aux1Ref.not, aux2Ref.not⟩
 
 /--
 Create an implication gate in the input AIG. This uses the builtin cache to enable automated subterm
 sharing.
 -/
 def mkImpCached (aig : AIG α) (input : BinaryInput aig) : Entrypoint α :=
-  -- a -> b = true && (invert (a and (invert b)))
-  let res := aig.mkGateCached <| input.asGateInput false true
+  -- a -> b = (invert (a and (invert b)))
+  let res := aig.mkGateCached <| input.invert false true
   let aig := res.aig
   let auxRef := res.ref
-  let res := aig.mkConstCached true
-  let aig := res.aig
-  let constRef := res.ref
-  aig.mkGateCached {
-    lhs := {
-      ref := constRef
-      inv := false
-    },
-    rhs := {
-      ref := auxRef.cast <| by
-        intros
-        simp +zetaDelta only
-        apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
-        omega
-      inv := true
-    }
-  }
+  ⟨aig, auxRef.not⟩
 
 end AIG
 
diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean
index f17df1aa34..4f1b9afbd9 100644
--- a/src/Std/Sat/AIG/CachedGatesLemmas.lean
+++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean
@@ -18,12 +18,6 @@ namespace Sat
 
 namespace AIG
 
-/--
-Encoding of not as boolean expression in AIG form.
--/
-private theorem not_as_aig : ∀ (b : Bool), (true && !b) = !b := by
-  decide
-
 /--
 Encoding of or as boolean expression in AIG form.
 -/
@@ -50,27 +44,13 @@ private theorem imp_as_aig : ∀ (a b : Bool), (!(a && !b)) = (!a || b) := by
 
 variable {α : Type} [Hashable α] [DecidableEq α]
 
-@[simp]
-theorem BinaryInput_asGateInput_lhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
-    (input.asGateInput linv rinv).lhs = ⟨input.lhs, linv⟩ := rfl
-
-@[simp]
-theorem BinaryInput_asGateInput_rhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
-    (input.asGateInput linv rinv).rhs = ⟨input.rhs, rinv⟩ := rfl
-
 theorem mkNotCached_le_size (aig : AIG α) (gate : Ref aig) :
     aig.decls.size ≤ (aig.mkNotCached gate).aig.decls.size := by
-  simp only [mkNotCached]
-  apply LawfulOperator.le_size_of_le_aig_size
-  apply mkConstCached_le_size
+  simp [mkNotCached]
 
 theorem mkNotCached_decl_eq idx (aig : AIG α) (gate : Ref aig) {h : idx < aig.decls.size} {h2} :
-    (aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx] := by
-  simp only [mkNotCached]
-  rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
-  apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
-  assumption
+    (aig.mkNotCached gate).aig.decls[idx]'h2 = aig.decls[idx]'h := by
+  simp [mkNotCached]
 
 instance : LawfulOperator α Ref mkNotCached where
   le_size := mkNotCached_le_size
@@ -80,10 +60,7 @@ instance : LawfulOperator α Ref mkNotCached where
 
 @[simp]
 theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} :
-    ⟦aig.mkNotCached gate, assign⟧
-      =
-    !⟦aig, ⟨gate.gate, gate.hgate⟩, assign⟧ := by
-  rw [← not_as_aig]
+    ⟦aig.mkNotCached gate, assign⟧ = !⟦aig, gate, assign⟧ := by
   simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]
 
 theorem mkAndCached_le_size (aig : AIG α) (input : BinaryInput aig) :
@@ -104,33 +81,19 @@ instance : LawfulOperator α BinaryInput mkAndCached where
 
 @[simp]
 theorem denote_mkAndCached {aig : AIG α} {input : BinaryInput aig} :
-    ⟦aig.mkAndCached input, assign⟧
-      =
-    (⟦aig, input.lhs, assign⟧
-      &&
-    ⟦aig, input.rhs, assign⟧) := by
+    ⟦aig.mkAndCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by
   simp [mkAndCached]
 
 theorem mkOrCached_le_size (aig : AIG α) (input : BinaryInput aig) :
     aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size := by
   simp only [mkOrCached]
-  apply LawfulOperator.le_size_of_le_aig_size
-  apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
-  apply LawfulOperator.le_size_of_le_aig_size
-  omega
+  apply LawfulOperator.le_size
 
 theorem mkOrCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
     {h2} :
     (aig.mkOrCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
   simp only [mkOrCached]
   rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
-  · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-    apply LawfulOperator.lt_size_of_lt_aig_size
-    assumption
-  · apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
-    apply LawfulOperator.lt_size_of_lt_aig_size
-    assumption
 
 instance : LawfulOperator α BinaryInput mkOrCached where
   le_size := mkOrCached_le_size
@@ -138,11 +101,7 @@ instance : LawfulOperator α BinaryInput mkOrCached where
 
 @[simp]
 theorem denote_mkOrCached {aig : AIG α} {input : BinaryInput aig} :
-    ⟦aig.mkOrCached input, assign⟧
-      =
-    (⟦aig, input.lhs, assign⟧
-      ||
-     ⟦aig, input.rhs, assign⟧) := by
+    ⟦aig.mkOrCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
   rw [← or_as_aig]
   simp [mkOrCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
 
@@ -174,12 +133,7 @@ instance : LawfulOperator α BinaryInput mkXorCached where
 
 @[simp]
 theorem denote_mkXorCached {aig : AIG α} {input : BinaryInput aig} :
-    ⟦aig.mkXorCached input, assign⟧
-      =
-    xor
-      ⟦aig, input.lhs, assign⟧
-      ⟦aig, input.rhs, assign⟧
-    := by
+    ⟦aig.mkXorCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) := by
   rw [← xor_as_aig]
   simp [
     mkXorCached,
@@ -214,11 +168,7 @@ instance : LawfulOperator α BinaryInput mkBEqCached where
 
 @[simp]
 theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} :
-    ⟦aig.mkBEqCached input, assign⟧
-      =
-    (⟦aig, input.lhs, assign⟧
-       ==
-     ⟦aig, input.rhs, assign⟧) := by
+    ⟦aig.mkBEqCached input, assign⟧ = (⟦aig, input.lhs, assign⟧ == ⟦aig, input.rhs, assign⟧) := by
   rw [← beq_as_aig]
   simp [
     mkBEqCached,
@@ -229,23 +179,13 @@ theorem denote_mkBEqCached {aig : AIG α} {input : BinaryInput aig} :
 theorem mkImpCached_le_size (aig : AIG α) (input : BinaryInput aig) :
     aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size := by
   simp only [mkImpCached]
-  apply LawfulOperator.le_size_of_le_aig_size
-  apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
-  apply LawfulOperator.le_size_of_le_aig_size
-  omega
+  apply LawfulOperator.le_size
 
 theorem mkImpCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size}
     {h2} :
     (aig.mkImpCached input).aig.decls[idx]'h2 = aig.decls[idx] := by
   simp only [mkImpCached]
   rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-  rw [AIG.LawfulOperator.decl_eq (f := mkConstCached)]
-  · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-    apply LawfulOperator.lt_size_of_lt_aig_size
-    assumption
-  · apply LawfulOperator.lt_size_of_lt_aig_size (f := mkConstCached)
-    apply LawfulOperator.lt_size_of_lt_aig_size
-    assumption
 
 instance : LawfulOperator α BinaryInput mkImpCached where
   le_size := mkImpCached_le_size
@@ -253,13 +193,7 @@ instance : LawfulOperator α BinaryInput mkImpCached where
 
 @[simp]
 theorem denote_mkImpCached {aig : AIG α} {input : BinaryInput aig} :
-    ⟦aig.mkImpCached input, assign⟧
-      =
-    (
-      !⟦aig, ⟨input.lhs.gate, input.lhs.hgate⟩, assign⟧
-        ||
-      ⟦aig, ⟨input.rhs.gate, input.rhs.hgate⟩, assign⟧
-    ) := by
+    ⟦aig.mkImpCached input, assign⟧ = ( !⟦aig, input.lhs, assign⟧ || ⟦aig, input.rhs, assign⟧) := by
   rw [← imp_as_aig]
   simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
 
diff --git a/src/Std/Sat/AIG/CachedLemmas.lean b/src/Std/Sat/AIG/CachedLemmas.lean
index 311ad2a982..3254cbeaa6 100644
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -25,7 +25,7 @@ If we find a cached atom declaration in the AIG, denoting it is equivalent to de
 theorem denote_mkAtom_cached {aig : AIG α} {hit} :
     aig.cache.get? (.atom v) = some hit
       →
-    ⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkAtom v, assign⟧ := by
+    ⟦aig, ⟨hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkAtom v, assign⟧ := by
   have := hit.hvalid
   simp only [denote_mkAtom]
   unfold denote denote.go
@@ -98,7 +98,7 @@ If we find a cached const declaration in the AIG, denoting it is equivalent to d
 theorem denote_mkConst_cached {aig : AIG α} {hit} :
     aig.cache.get? (.const b) = some hit
       →
-    ⟦aig, ⟨hit.idx, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧ := by
+    ⟦aig, ⟨hit.idx, false, hit.hbound⟩, assign⟧ = ⟦aig.mkConst b, assign⟧ := by
   have := hit.hvalid
   simp only [denote_mkConst]
   unfold denote denote.go
@@ -171,9 +171,9 @@ theorem mkConstCached_eval_eq_mkConst_eval {aig : AIG α} :
 If we find a cached gate declaration in the AIG, denoting it is equivalent to denoting `AIG.mkGate`.
 -/
 theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
-    aig.cache.get? (.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = some hit
+    aig.cache.get? (.gate input.lhs.gate input.rhs.gate input.lhs.invert input.rhs.invert) = some hit
       →
-    ⟦⟨aig, hit.idx, hit.hbound⟩, assign⟧
+    ⟦⟨aig, hit.idx, false, hit.hbound⟩, assign⟧
       =
     ⟦aig.mkGate input, assign⟧ := by
   intros
@@ -184,27 +184,29 @@ theorem denote_mkGate_cached {aig : AIG α} {input} {hit} :
     unfold denote denote.go
   split <;> simp_all[denote]
 
-theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
+theorem mkGateCached.go_le_size (aig : AIG α) (input : BinaryInput aig) :
     aig.decls.size ≤ (go aig input).aig.decls.size := by
   dsimp only [go]
   split
   · simp
-  · split <;> try simp +arith [mkConstCached_le_size]
+  · split <;> try simp [mkConstCached_le_size]
     split
-    · simp +arith
-    · split <;> simp +arith [mkConstCached_le_size]
+    · simp
+    · split
+      · simp [mkConstCached_le_size]
+      · simp
 
 /--
 `AIG.mkGateCached` never shrinks the underlying AIG.
 -/
-theorem mkGateCached_le_size (aig : AIG α) (input : GateInput aig)
+theorem mkGateCached_le_size (aig : AIG α) (input : BinaryInput aig)
     : aig.decls.size ≤ (aig.mkGateCached input).aig.decls.size := by
   dsimp only [mkGateCached]
   split
   · apply mkGateCached.go_le_size
   · apply mkGateCached.go_le_size
 
-theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
+theorem mkGateCached.go_decl_eq (aig : AIG α) (input : BinaryInput aig) :
     ∀ (idx : Nat) (h1) (h2), (go aig input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
     generalize hres : go aig input = res
     unfold go at hres
@@ -256,7 +258,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
 The AIG produced by `AIG.mkGateCached` agrees with the input AIG on all indices that are valid for
 both.
 -/
-theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
+theorem mkGateCached_decl_eq (aig : AIG α) (input : BinaryInput aig) :
     ∀ (idx : Nat) (h1) (h2), (aig.mkGateCached input).aig.decls[idx]'h1 = aig.decls[idx]'h2 := by
     generalize hres : mkGateCached aig input = res
     unfold mkGateCached at hres
@@ -267,13 +269,13 @@ theorem mkGateCached_decl_eq (aig : AIG α) (input : GateInput aig) :
       intros
       rw [mkGateCached.go_decl_eq]
 
-instance : LawfulOperator α GateInput mkGateCached where
+instance : LawfulOperator α BinaryInput mkGateCached where
   le_size := mkGateCached_le_size
   decl_eq := by
     intros
     apply mkGateCached_decl_eq
 
-theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
+theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput aig} :
     ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by
   simp only [go]
   split
@@ -289,28 +291,27 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai
     · next heq _ _ _ =>
       simp_all [denote_idx_const heq]
     · next heq _ _ _ =>
+      rcases input with ⟨_, ⟨rhs, rinv, hrgate⟩⟩
       simp_all [denote_idx_const heq]
     · next heq _ _ _ =>
+      rcases input with ⟨_, ⟨rhs, rinv, hrgate⟩⟩
       simp_all [denote_idx_const heq]
-    · next heq _ _ _ _ =>
+    · next heq _ _ _ _ _ =>
+      rcases input with ⟨⟨lhs, linv, hlgate⟩, _⟩
       simp_all [denote_idx_const heq]
-    · next heq _ _ _ =>
+    · next heq _ _ _ _ _ =>
+      rcases input with ⟨⟨lhs, linv, hlgate⟩, _⟩
       simp_all [denote_idx_const heq]
-    · split
+    · rcases input with ⟨⟨lhs, linv, hlgate⟩, ⟨rhs, rinv, hrgate⟩⟩
+      split
       · next hif =>
         simp only [beq_false, Bool.and_eq_true, beq_iff_eq, Bool.not_eq_true'] at hif
         rcases hif with ⟨⟨hifeq, hlinv⟩, hrinv⟩
-        replace hifeq : input.lhs.ref = input.rhs.ref := by
-          rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩
-          simpa using hifeq
         simp [hlinv, hrinv, hifeq]
       · split
         · next hif =>
           simp only [Bool.and_eq_true, beq_iff_eq] at hif
           rcases hif with ⟨hifeq, hinv⟩
-          replace hifeq : input.lhs.ref = input.rhs.ref := by
-            rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩
-            simpa using hifeq
           simp [hifeq, hinv]
         · simp [mkGate, denote]
 
@@ -318,7 +319,7 @@ theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput ai
 The central equality theorem between `mkGateCached` and `mkGate`.
 -/
 @[simp]
-theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
+theorem mkGateCached_eval_eq_mkGate_eval {aig : AIG α} {input : BinaryInput aig} :
     ⟦aig.mkGateCached input, assign⟧ = ⟦aig.mkGate input, assign⟧ := by
   simp only [mkGateCached]
   split
diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean
index 649a7dde04..d37781ecc6 100644
--- a/src/Std/Sat/AIG/If.lean
+++ b/src/Std/Sat/AIG/If.lean
@@ -221,12 +221,12 @@ theorem go_denote_mem_prefix {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr
     (discr : Ref aig) (lhs rhs : RefVec aig w) (s : RefVec aig curr) (start : Nat) (hstart) :
     ⟦
       (go aig curr hcurr discr lhs rhs s).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Sat/AIG/LawfulOperator.lean b/src/Std/Sat/AIG/LawfulOperator.lean
index f7bd85297e..a26a40ba87 100644
--- a/src/Std/Sat/AIG/LawfulOperator.lean
+++ b/src/Std/Sat/AIG/LawfulOperator.lean
@@ -30,6 +30,13 @@ structure IsPrefix (decls1 decls2 : Array (Decl α)) : Prop where
     -/
     idx_eq : ∀ idx (h : idx < decls1.size), decls2[idx]'(by omega) = decls1[idx]'h
 
+@[simp]
+theorem IsPrefix_push {decls : Array (Decl α)} : IsPrefix decls (decls.push decl) := by
+  apply IsPrefix.of
+  · intro idx hidx
+    simp [hidx, Array.getElem_push]
+  · simp
+
 /--
 If `decls1` is a prefix of `decls2` and we start evaluating `decls2` at an
 index in bounds of `decls1` we can evaluate at `decls1`.
@@ -69,11 +76,12 @@ variable {α : Type} [Hashable α] [DecidableEq α]
 @[inherit_doc denote.go_eq_of_isPrefix]
 theorem denote.eq_of_isPrefix (entry : Entrypoint α) (newAIG : AIG α)
       (hprefix : IsPrefix entry.aig.decls newAIG.decls) :
-    ⟦newAIG, ⟨entry.ref.gate, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧
+    ⟦newAIG, ⟨entry.ref.gate, entry.ref.invert, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧
       =
     ⟦entry, assign⟧
     := by
   unfold denote
+  rw [Bool.bne_left_inj]
   apply denote.go_eq_of_isPrefix
   assumption
 
@@ -129,7 +137,7 @@ theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig) (h : x ≤ aig.de
 
 @[simp]
 theorem denote_input_entry (entry : Entrypoint α) {input} {h} :
-    ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign⟧
+    ⟦(f entry.aig input).aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧
       =
     ⟦entry, assign⟧ :=  by
   apply denote.eq_of_isPrefix
@@ -143,10 +151,10 @@ theorem denote_cast_entry (entry : Entrypoint α) {input} {h} :
   simp [Ref.cast]
 
 theorem denote_mem_prefix {aig : AIG α} {input} (h) :
-    ⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
+    ⟦(f aig input).aig, ⟨start, invert, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
       =
-    ⟦aig, ⟨start, h⟩, assign⟧ :=  by
-  rw [denote_input_entry ⟨aig, start, h⟩]
+    ⟦aig, ⟨start, invert, h⟩, assign⟧ :=  by
+  rw [denote_input_entry ⟨aig, start, invert, h⟩]
 
 end LawfulOperator
 
diff --git a/src/Std/Sat/AIG/LawfulVecOperator.lean b/src/Std/Sat/AIG/LawfulVecOperator.lean
index f0f02301dc..29bc7d0549 100644
--- a/src/Std/Sat/AIG/LawfulVecOperator.lean
+++ b/src/Std/Sat/AIG/LawfulVecOperator.lean
@@ -54,7 +54,7 @@ theorem le_size_of_le_aig_size (aig : AIG α) (input : β aig len) (h : x ≤ ai
 
 @[simp]
 theorem denote_input_entry (entry : Entrypoint α) {input : β entry.aig len} {h} :
-    ⟦(f entry.aig input).aig, ⟨entry.ref.gate, h⟩, assign ⟧
+    ⟦(f entry.aig input).aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign ⟧
       =
     ⟦entry, assign⟧ :=  by
   apply denote.eq_of_isPrefix
@@ -68,10 +68,10 @@ theorem denote_cast_entry (entry : Entrypoint α) {input : β entry.aig len} {h}
   simp [Ref.cast]
 
 theorem denote_mem_prefix {aig : AIG α} {input : β aig len} (h) :
-    ⟦(f aig input).aig, ⟨start, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
+    ⟦(f aig input).aig, ⟨start, inv, by apply lt_size_of_lt_aig_size; omega⟩, assign⟧
       =
-    ⟦aig, ⟨start, h⟩, assign⟧ :=  by
-  rw [denote_input_entry ⟨aig, start, h⟩]
+    ⟦aig, ⟨start, inv, h⟩, assign⟧ :=  by
+  rw [denote_input_entry ⟨aig, start, inv, h⟩]
 
 @[simp]
 theorem denote_input_vec (s : RefVecEntry α len) {input : β s.aig len} {hcast} :
diff --git a/src/Std/Sat/AIG/Lemmas.lean b/src/Std/Sat/AIG/Lemmas.lean
index 81d6ac58d2..f50b22c5a7 100644
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -27,25 +27,15 @@ theorem Ref.gate_cast {aig1 aig2 : AIG α} (ref : Ref aig1)
 @[simp]
 theorem Ref.cast_eq {aig1 aig2 : AIG α} (ref : Ref aig1)
     (h : aig1.decls.size ≤ aig2.decls.size) :
-    (ref.cast h) = ⟨ref.gate, by have := ref.hgate; omega⟩ := rfl
+    (ref.cast h) = ⟨ref.gate, ref.invert, by have := ref.hgate; omega⟩ := rfl
 
 @[simp]
-theorem Fanin.ref_cast {aig1 aig2 : AIG α} (fanin : Fanin aig1)
-    (h : aig1.decls.size ≤ aig2.decls.size) :
-    (fanin.cast h).ref = fanin.ref.cast h := rfl
-
-@[simp]
-theorem Fanin.inv_cast {aig1 aig2 : AIG α} (fanin : Fanin aig1)
-    (h : aig1.decls.size ≤ aig2.decls.size) :
-    (fanin.cast h).inv = fanin.inv := rfl
-
-@[simp]
-theorem GateInput.lhs_cast {aig1 aig2 : AIG α} (input : GateInput aig1)
+theorem BinaryInput.lhs_cast {aig1 aig2 : AIG α} (input : BinaryInput aig1)
     (h : aig1.decls.size ≤ aig2.decls.size) :
     (input.cast h).lhs = input.lhs.cast h := rfl
 
 @[simp]
-theorem GateInput.rhs_cast {aig1 aig2 : AIG α} (input : GateInput aig1)
+theorem BinaryInput.rhs_cast {aig1 aig2 : AIG α} (input : BinaryInput aig1)
     (h : aig1.decls.size ≤ aig2.decls.size) :
     (input.cast h).rhs = input.rhs.cast h := rfl
 
@@ -55,6 +45,16 @@ theorem BinaryInput.each_cast {aig1 aig2 : AIG α} (lhs rhs : Ref aig1)
     BinaryInput.mk (lhs.cast h1) (rhs.cast h2) = (BinaryInput.mk lhs rhs).cast h2 := by
   simp [BinaryInput.cast]
 
+@[simp]
+theorem BinaryInput_invert_lhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
+    (input.invert linv rinv).lhs = ⟨input.lhs.gate, linv ^^ input.lhs.invert, input.lhs.hgate⟩ := by
+  simp [BinaryInput.invert, Ref.flip]
+
+@[simp]
+theorem BinaryInput_invert_rhs {aig : AIG α} (input : BinaryInput aig) (linv rinv : Bool) :
+    (input.invert linv rinv).rhs = ⟨input.rhs.gate, rinv ^^ input.rhs.invert, input.rhs.hgate⟩ := by
+  simp [BinaryInput.invert, Ref.flip]
+
 @[simp]
 theorem denote_projected_entry {entry : Entrypoint α} :
     ⟦entry.aig, entry.ref, assign⟧ = ⟦entry, assign⟧ := by
@@ -62,20 +62,43 @@ theorem denote_projected_entry {entry : Entrypoint α} :
 
 @[simp]
 theorem denote_projected_entry' {entry : Entrypoint α} :
-    ⟦entry.aig, ⟨entry.ref.gate, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by
+    ⟦entry.aig, ⟨entry.ref.gate, entry.ref.invert, entry.ref.hgate⟩, assign⟧ = ⟦entry, assign⟧ := by
   cases entry; simp
 
+@[simp]
+theorem Ref.denote_flip {aig : AIG α} {ref : Ref aig} {inv : Bool} :
+    ⟦aig, ref.flip inv, assign⟧ = (⟦aig, ref, assign⟧ ^^ inv) := by
+  unfold denote
+  cases ref <;> cases inv <;> simp [Ref.flip] 
+
+@[simp]
+theorem Ref.denote_not {aig : AIG α} {ref : Ref aig} :
+    ⟦aig, ref.not, assign⟧ = !⟦aig, ref, assign⟧ := by
+  simp [Ref.not]
+
+@[simp]
+theorem denote_not_invert {aig : AIG α} {gate} {inv} {hgate} :
+    ⟦aig, ⟨gate, !inv, hgate⟩, assign⟧ = !⟦aig, ⟨gate, inv, hgate⟩, assign⟧ := by
+  unfold denote
+  simp
+
+@[simp]
+theorem denote_invert_true {aig : AIG α} {gate} {hgate} :
+    ⟦aig, ⟨gate, true, hgate⟩, assign⟧ = !⟦aig, ⟨gate, false, hgate⟩, assign⟧ := by
+  unfold denote
+  simp
+
 /--
 `AIG.mkGate` never shrinks the underlying AIG.
 -/
-theorem mkGate_le_size (aig : AIG α) (input : GateInput aig) :
+theorem mkGate_le_size (aig : AIG α) (input : BinaryInput aig) :
     aig.decls.size ≤ (aig.mkGate input).aig.decls.size := by
-  simp +arith [mkGate]
+  simp [mkGate]
 
 /--
 The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both.
 -/
-theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} :
+theorem mkGate_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : idx < aig.decls.size} :
     have := mkGate_le_size aig input
     (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by
   simp only [mkGate, Array.getElem_push]
@@ -83,17 +106,17 @@ theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig
   · rfl
   · contradiction
 
-instance : LawfulOperator α GateInput mkGate where
+instance : LawfulOperator α BinaryInput mkGate where
   le_size := mkGate_le_size
   decl_eq := by
     intros
     apply mkGate_decl_eq
 
 @[simp]
-theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
+theorem denote_mkGate {aig : AIG α} {input : BinaryInput aig} :
     ⟦aig.mkGate input, assign⟧
       =
-    ((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv)) := by
+    (⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧) := by
   conv =>
     lhs
     unfold denote denote.go
@@ -107,18 +130,12 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
   · next heq =>
     rw [mkGate, Array.getElem_push_eq] at heq
     injection heq with heq1 heq2 heq3 heq4
-    dsimp only
+    simp only [← heq1, mkGate, ← heq3, ← heq2, ← heq4, Bool.bne_false, denote]
     congr 2
-    · unfold denote
-      simp only [heq1]
-      apply denote.go_eq_of_isPrefix
-      apply LawfulOperator.isPrefix_aig
-    · simp [heq3]
-    · unfold denote
-      simp only [heq2]
-      apply denote.go_eq_of_isPrefix
-      apply LawfulOperator.isPrefix_aig
-    · simp [heq4]
+    · apply denote.go_eq_of_isPrefix
+      simp
+    · apply denote.go_eq_of_isPrefix
+      simp
 
 /--
 `AIG.mkAtom` never shrinks the underlying AIG.
@@ -154,7 +171,7 @@ theorem denote_mkAtom {aig : AIG α} :
   · next heq =>
     rw [mkAtom, Array.getElem_push_eq] at heq
     injection heq with heq
-    rw [heq]
+    simp [heq, mkAtom]
   · next heq =>
     rw [mkAtom, Array.getElem_push_eq] at heq
     contradiction
@@ -190,7 +207,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
   · next heq =>
     rw [mkConst, Array.getElem_push_eq] at heq
     injection heq with heq
-    rw [heq]
+    simp [heq, mkConst]
   · next heq =>
     rw [mkConst, Array.getElem_push_eq] at heq
     contradiction
@@ -202,7 +219,7 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
 If an index contains a `Decl.const` we know how to denote it.
 -/
 theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart = .const b) :
-    ⟦aig, ⟨start, hstart⟩, assign⟧ = b := by
+    ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = (b ^^ invert) := by
   unfold denote denote.go
   split <;> simp_all
 
@@ -210,7 +227,7 @@ theorem denote_idx_const {aig : AIG α} {hstart} (h : aig.decls[start]'hstart =
 If an index contains a `Decl.atom` we know how to denote it.
 -/
 theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a) :
-    ⟦aig, ⟨start, hstart⟩, assign⟧ = assign a := by
+    ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = (assign a ^^ invert) := by
   unfold denote denote.go
   split <;> simp_all
 
@@ -218,13 +235,13 @@ theorem denote_idx_atom {aig : AIG α} {hstart} (h : aig.decls[start] = .atom a)
 If an index contains a `Decl.gate` we know how to denote it.
 -/
 theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lhs rhs linv rinv) :
-    ⟦aig, ⟨start, hstart⟩, assign⟧
+    ⟦aig, ⟨start, invert, hstart⟩, assign⟧
       =
-    (
-      (⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv)
+    ((
+      (⟦aig, ⟨lhs, linv, by have := aig.invariant hstart h; omega⟩, assign⟧)
         &&
-      (⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv)
-    ) := by
+      (⟦aig, ⟨rhs, rinv, by have := aig.invariant hstart h; omega⟩, assign⟧)
+    ) ^^ invert) := by
   unfold denote
   conv =>
     lhs
@@ -247,15 +264,15 @@ theorem idx_trichotomy (aig : AIG α) (hstart : start < aig.decls.size) {prop :
   | .gate lhs rhs linv rinv => apply hgate; assumption
 
 theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size}
-    (hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, hstart⟩, assign⟧ = res)
-    (hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, hstart⟩, assign⟧ = res)
+    (hconst : ∀ b, aig.decls[start]'hstart = .const b → ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res)
+    (hatom : ∀ a, aig.decls[start]'hstart = .atom a → ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res)
     (hgate :
       ∀ lhs rhs linv rinv,
         aig.decls[start]'hstart = .gate lhs rhs linv rinv
           →
-        ⟦aig, ⟨start, hstart⟩, assign⟧ = res
+        ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res
     ) :
-    ⟦aig, ⟨start, hstart⟩, assign⟧ = res := by
+    ⟦aig, ⟨start, invert, hstart⟩, assign⟧ = res := by
   apply idx_trichotomy aig hstart
   · exact hconst
   · exact hatom
@@ -264,32 +281,32 @@ theorem denote_idx_trichotomy {aig : AIG α} {hstart : start < aig.decls.size}
 theorem mem_def {aig : AIG α} {a : α} : (a ∈ aig) ↔ ((.atom a) ∈ aig.decls) := by
   simp [Membership.mem, Mem]
 
-theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat)
+theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat) (invert : Bool)
     (hidx : idx < aig.decls.size) (h : ∀ a, a ∈ aig → assign1 a = assign2 a) :
-    ⟦aig, ⟨idx, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, hidx⟩, assign2⟧ := by
+    ⟦aig, ⟨idx, invert, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, invert, hidx⟩, assign2⟧ := by
   apply denote_idx_trichotomy
   · intro b heq
     simp [denote_idx_const heq]
   · intro a heq
-    simp only [denote_idx_atom heq]
+    simp only [denote_idx_atom heq, Bool.bne_left_inj]
     apply h
-    rw [mem_def, ← heq, Array.mem_def]
-    apply Array.getElem_mem_toList
+    simp [mem_def, ← heq]
   · intro lhs rhs linv rinv heq
     simp only [denote_idx_gate heq]
     have := aig.invariant hidx heq
-    rw [denote_congr assign1 assign2 aig lhs (by omega) h]
-    rw [denote_congr assign1 assign2 aig rhs (by omega) h]
+    rw [denote_congr assign1 assign2 aig lhs _ (by omega) h]
+    rw [denote_congr assign1 assign2 aig rhs _ (by omega) h]
 
 theorem of_isConstant {aig : AIG α} {assign : α → Bool} {ref : Ref aig} {b : Bool} :
     aig.isConstant ref b → ⟦aig, ref, assign⟧ = b := by
-  rcases ref with ⟨gate, hgate⟩
+  rcases ref with ⟨gate, invert, hgate⟩
   intro h
   unfold isConstant at h
   dsimp only at h
   split at h
-  · rw [denote_idx_const]
-    simp_all
+  · next heq =>
+    rw [denote_idx_const (h := heq)]
+    cases invert <;> simp_all
   · contradiction
 
 end AIG
diff --git a/src/Std/Sat/AIG/RefVec.lean b/src/Std/Sat/AIG/RefVec.lean
index ca3b2b907a..3ff1f769a4 100644
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -33,8 +33,8 @@ theorem emptyWithCapacity_eq : emptyWithCapacity (aig := aig) c = empty := by
 @[inline]
 def cast' {aig1 aig2 : AIG α} (s : RefVec aig1 len)
     (h :
-      (∀ {i : Nat} (h : i < len), s.refs[i]'(by have := s.hlen; omega) < aig1.decls.size)
-        → ∀ {i : Nat} (h : i < len), s.refs[i]'(by have := s.hlen; omega) < aig2.decls.size) :
+      (∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig1.decls.size)
+        → ∀ {i : Nat} (h : i < len), (s.refs[i]'(by have := s.hlen; omega)).1 < aig2.decls.size) :
     RefVec aig2 len :=
   { s with
     hrefs := by
@@ -58,13 +58,13 @@ def cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (h : aig1.decls.size ≤ aig
 def get (s : RefVec aig len) (idx : Nat) (hidx : idx < len) : Ref aig :=
   let ⟨refs, hlen, hrefs⟩ := s
   let ref := refs[idx]'(by rw [hlen]; assumption)
-  ⟨ref, by apply hrefs; assumption⟩
+  ⟨ref.1, ref.2, by apply hrefs; assumption⟩
 
 @[inline]
 def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
   let ⟨refs, hlen, hrefs⟩ := s
   ⟨
-    refs.push ref.gate,
+    refs.push (ref.gate, ref.invert),
     by simp [hlen],
     by
       intro i hi
@@ -75,6 +75,11 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
       · apply AIG.Ref.hgate
   ⟩
 
+@[simp]
+theorem cast_cast {aig1 aig2 aig3 : AIG α} (s : RefVec aig1 len)
+    (h1 : aig1.decls.size ≤ aig2.decls.size) (h2 : aig2.decls.size ≤ aig3.decls.size) :
+    (s.cast h1).cast h2 = s.cast (Nat.le_trans h1 h2) := by rfl
+
 @[simp]
 theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) :
     (s.push ref).get len (by omega) = ref := by
@@ -95,6 +100,8 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
   cases ref
   simp only [Ref.mk.injEq]
   rw [Array.getElem_push_lt]
+  · simp
+  · simp [hlen, hidx]
 
 @[simp]
 theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)
@@ -135,6 +142,9 @@ theorem get_append (lhs : RefVec aig lw) (rhs : RefVec aig rw) (idx : Nat)
   split
   · simp [Ref.mk.injEq]
     rw [Array.getElem_append_left]
+    · simp
+    · rw [lhs.hlen]
+      assumption
   · simp only [Ref.mk.injEq]
     rw [Array.getElem_append_right]
     · simp [lhs.hlen]
@@ -162,7 +172,7 @@ theorem get_out_bound (s : RefVec aig len) (idx : Nat) (alt : Ref aig) (hidx : l
 
 def countKnown [Inhabited α] (aig : AIG α) (s : RefVec aig len) : Nat := Id.run do
   let folder acc ref :=
-    let decl := aig.decls[ref]!
+    let decl := aig.decls[ref.1]!
     match decl with
     | .const .. => acc + 1
     | _ => acc
diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean
index 0f60aa90ad..fd7922be31 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Map.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean
@@ -36,7 +36,7 @@ theorem denote_prefix_cast_ref {aig : AIG α} {input1 input2 : Ref aig}
 instance : LawfulMapOperator α mkNotCached where
   chainable := by
     intros
-    simp only [Ref.gate_cast, denote_mkNotCached]
+    simp only [Ref.cast_eq, denote_mkNotCached, Bool.not_eq_eq_eq_not, Bool.not_not]
     rw [LawfulOperator.denote_mem_prefix (f := mkNotCached)]
 
 end LawfulMapOperator
@@ -156,7 +156,7 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe
     simp only [Nat.le_refl, get, Ref.cast_eq, Ref.mk.injEq, true_implies]
     have : curr = len := by omega
     subst this
-    rfl
+    simp
 termination_by len - curr
 
 theorem go_get {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec aig curr)
@@ -175,12 +175,12 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
     (start : Nat) (hstart) :
     ⟦
       (go aig curr hcurr s input f).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
index a8dd69ae91..d9f4f36d7a 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
@@ -202,12 +202,12 @@ theorem go_denote_mem_prefix {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len)
     [chainable : LawfulZipOperator α f] (start : Nat) (hstart) :
     ⟦
       (go aig curr s hcurr lhs rhs f).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Sat/AIG/Relabel.lean b/src/Std/Sat/AIG/Relabel.lean
index ae33a83460..8c082ac585 100644
--- a/src/Std/Sat/AIG/Relabel.lean
+++ b/src/Std/Sat/AIG/Relabel.lean
@@ -98,9 +98,9 @@ theorem relabel_gate {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig
 @[simp]
 theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx}
     (assign : β → Bool) :
-    ⟦aig.relabel r, ⟨start, hidx⟩, assign⟧
+    ⟦aig.relabel r, ⟨start, invert, hidx⟩, assign⟧
       =
-    ⟦aig, ⟨start, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by
+    ⟦aig, ⟨start, invert, by rw [← relabel_size_eq_size (r := r)]; omega⟩, (assign ∘ r)⟧ := by
   apply denote_idx_trichotomy
   · intro b heq1
     have heq2 := relabel_const heq1
@@ -121,14 +121,14 @@ theorem denote_relabel (aig : AIG α) (r : α → β) (start : Nat) {hidx}
     rw [denote_relabel aig r rhs assign]
 
 theorem unsat_relabel {aig : AIG α} (r : α → β) {hidx} :
-    aig.UnsatAt idx hidx → (aig.relabel r).UnsatAt idx (by simp [hidx]) := by
+    aig.UnsatAt idx invert hidx → (aig.relabel r).UnsatAt idx invert (by simp [hidx]) := by
   intro h assign
   specialize h (assign ∘ r)
   simp [h]
 
 theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
     (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
-    (aig.relabel r).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by
+    (aig.relabel r).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
   constructor
   · intro h assign
     let g : β → α := fun b =>
diff --git a/src/Std/Sat/AIG/RelabelNat.lean b/src/Std/Sat/AIG/RelabelNat.lean
index bc78f4cc57..8d66f738e4 100644
--- a/src/Std/Sat/AIG/RelabelNat.lean
+++ b/src/Std/Sat/AIG/RelabelNat.lean
@@ -329,7 +329,7 @@ theorem relabelNat_size_eq_size {aig : AIG α} : aig.relabelNat.decls.size = aig
 `relabelNat` preserves unsatisfiablility.
 -/
 theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
-    (aig.relabelNat).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2 := by
+    (aig.relabelNat).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2 := by
   dsimp only [relabelNat, relabelNat']
   rw [relabel_unsat_iff]
   intro x y hx hy heq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
index 429c30a85c..6032ccd160 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
@@ -197,6 +197,8 @@ theorem go_le_size (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
   dsimp only
   split
   · refine Nat.le_trans ?_ (by apply go_le_size)
+    unfold mkFullAdder
+    dsimp only
     apply AIG.LawfulOperator.le_size_of_le_aig_size (f := mkFullAdderCarry)
     apply AIG.LawfulOperator.le_size (f := mkFullAdderOut)
   · simp
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
index bbff7b66ad..4ffd685bdf 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
@@ -64,12 +64,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (idx : Nat) (hidx)
     (s : AIG.RefVec aig idx) (c : BitVec w) (start : Nat) (hstart) :
     ⟦
       (go aig c idx s hidx).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 099483892a..8a960a50ef 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -42,12 +42,12 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (expr : BVExpr w) (assign : Assig
     (hstart) :
     ⟦
       (go aig expr).val.aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply (go aig expr).property⟩,
       assign.toAIGAssignment
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign.toAIGAssignment⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign.toAIGAssignment⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
index 77b1485094..3998f3a2b3 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
@@ -63,11 +63,11 @@ theorem mkFullAdder_denote_mem_prefix (aig : AIG α) (input : FullAdderInput aig
     (hstart) :
     ⟦
       (mkFullAdder aig input).aig,
-      ⟨start, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩,
+      ⟨start, inv, Nat.lt_of_lt_of_le hstart (FullAdderOutput.hle _)⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
   unfold mkFullAdder
   dsimp only
   rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
@@ -77,12 +77,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (c
     (s : AIG.RefVec aig curr) (lhs rhs : AIG.RefVec aig w) (start : Nat) (hstart) :
     ⟦
       (go aig lhs rhs curr hcurr cin s).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
index e05ec1ac91..fc445e2d5c 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Neg.lean
@@ -39,9 +39,8 @@ theorem denote_blastNeg (aig : AIG α) (value : BitVec w) (target : RefVec aig w
   rw [denote_blastAdd]
   · intro idx hidx
     rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastConst)]
-    · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true,
-        Bool.true_and]
-      rw [denote_blastNot, htarget]
+    · simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
+      rw [denote_blastNot, htarget, BitVec.getLsbD_eq_getElem]
     · simp [Ref.hgate]
   · simp
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
index e7145d2efa..dceb5be1a6 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
@@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (distance : Nat) (input : AIG.RefVec
     (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) (start : Nat) (hstart) :
     ⟦
       (go aig input distance curr hcurr s).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
index 807103acf0..8b6202681b 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
@@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (distance : Nat) (input : AIG.RefVec
     (curr : Nat) (hcurr : curr ≤ w) (s : AIG.RefVec aig curr) (start : Nat) (hstart) :
     ⟦
       (go aig input distance curr hcurr s).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
index d939f530c3..983792eff1 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
@@ -61,12 +61,12 @@ theorem blastDivSubtractShift_denote_mem_prefix (aig : AIG α) (falseRef trueRef
     (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
     ⟦
       (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply blastDivSubtractShift_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply blastDivSubtractShift_decl_eq
@@ -95,58 +95,60 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
   unfold blastDivSubtractShift BitVec.divSubtractShift
   dsimp only
   rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)]
-  . simp only [RefVec.get_cast, Ref.gate_cast]
+  . simp only [Ref.cast_eq, RefVec.cast_cast, RefVec.get_cast]
     rw [AIG.RefVec.denote_ite]
-    rw [BVPred.mkUlt_denote_eq (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)]
-    · split
-      · next hdiscr =>
-        rw [← Normalize.BitVec.lt_ult] at hdiscr
-        simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast, hdiscr, ↓reduceIte]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
+    conv =>
+      rhs
+      rw [apply_ite (f := BitVec.DivModState.q)]
+      rw [apply_ite (f := (BitVec.getLsbD · idx))]
+    apply ite_congr
+    · rw [BVPred.mkUlt_denote_eq (assign := assign) (lhs := rbv.shiftConcat (lhs.getLsbD (wn - 1))) (rhs := rhs)]
+      · simp [Std.Tactic.BVDecide.Normalize.BitVec.lt_ult]
+      · intro idx hidx
+        simp only [RefVec.get_cast, Ref.cast_eq]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         rw [denote_blastShiftConcat_eq_shiftConcat]
-        · intro idx hidx
-          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-          · simp [hq]
-          · simp [Ref.hgate]
-        · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        · simp [hr]
+        · rw [BVPred.denote_getD_eq_getLsbD]
+          · simp [hleft]
           · simp [hfalse]
-          · simp [Ref.hgate]
-      · next hdiscr =>
-        rw [← Normalize.BitVec.lt_ult] at hdiscr
-        simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast, hdiscr, ↓reduceIte]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
+      · intro idx hidx
+        simp only [RefVec.get_cast, Ref.cast_eq]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-        rw [denote_blastShiftConcat_eq_shiftConcat]
-        · intro idx hidx
-          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-          · simp [hq]
-          · simp [Ref.hgate]
-        · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-          rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-          · simp [htrue]
-          · simp [Ref.hgate]
-    · intro idx hidx
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        · simp [hright]
+        · simp [Ref.hgate]
+    · intro h
+      simp only [RefVec.get_cast, Ref.cast_eq]
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-      . simp only [Ref.cast_eq, id_eq, Int.reduceNeg, RefVec.get_cast]
-        rw [denote_blastShiftConcat_eq_shiftConcat]
-        . simp [hr]
-        . dsimp only
-          rw [BVPred.denote_getD_eq_getLsbD]
-          · exact hleft
-          · exact hfalse
-      . simp [Ref.hgate]
-    · intro idx hidx
+      rw [denote_blastShiftConcat_eq_shiftConcat]
+      · intro idx hidx
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        · simp [hq]
+        · simp [Ref.hgate]
+      · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        · simp [hfalse]
+        · simp [Ref.hgate]
+    · intro h
+      simp only [RefVec.get_cast, Ref.cast_eq]
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
       rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-      . simp [hright]
-      . simp [Ref.hgate]
+      rw [denote_blastShiftConcat_eq_shiftConcat]
+      · intro idx hidx
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        · simp [hq]
+        · simp [Ref.hgate]
+      · rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        · simp [htrue]
+        · simp [Ref.hgate]
   . simp [Ref.hgate]
 
 theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lhs rhs : BitVec w)
@@ -378,12 +380,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (falseRef trueRef : AIG
     (n d q r : AIG.RefVec aig w) (wn wr : Nat) (start : Nat) (hstart) :
     ⟦
       (go aig curr falseRef trueRef n d wn wr q r).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
index 8ea81d4847..8fdafbee0f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
@@ -26,7 +26,7 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
     (assign : α → Bool)
     (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
     (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, input.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
-    ⟦(mkUlt aig input).aig, (mkUlt aig input).ref, assign⟧ = BitVec.ult lhs rhs := by
+    ⟦mkUlt aig input, assign⟧ = BitVec.ult lhs rhs := by
   rw [BitVec.ult_eq_not_carry]
   unfold mkUlt
   simp only [denote_projected_entry, denote_mkNotCached, denote_projected_entry']
@@ -42,11 +42,8 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
   · dsimp only
     intro idx hidx
     rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]
-    · simp only [RefVec.get_cast, Ref.gate_cast, BitVec.getLsbD_not, hidx, decide_true,
-        Bool.true_and]
-      rw [BVExpr.bitblast.denote_blastNot]
-      congr 1
-      apply hright
+    · simp only [RefVec.get_cast, Ref.cast_eq, hidx, BitVec.getLsbD_eq_getElem, BitVec.getElem_not]
+      rw [BVExpr.bitblast.denote_blastNot, hright, BitVec.getLsbD_eq_getElem]
     · simp [Ref.hgate]
 
 end BVPred
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
index 1e38916934..c148dd8a20 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
@@ -69,12 +69,12 @@ theorem go_denote_mem_prefix (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w)
     (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) (start : Nat) (hstart) :
     ⟦
       (go aig w input newWidth curr hcurr s).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
index 66cdb77688..dc8bd5e0b0 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
@@ -62,12 +62,12 @@ theorem go_denote_mem_prefix (aig : AIG BVBit) (idx : Nat) (hidx) (s : AIG.RefVe
     (a : Nat) (start : Nat) (hstart) :
     ⟦
       (go aig w a idx s hidx).aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply IsPrefix.of
   · intros
     apply go_decl_eq
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
index 6edda27913..6dce59215f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
@@ -141,17 +141,19 @@ theorem go_isPrefix_aig {aig : AIG β} :
 theorem go_denote_mem_prefix :
     ⟦
       (go aig expr atomHandler).val.aig,
-      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
+      ⟨start, inv, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
       assign
     ⟧
       =
-    ⟦aig, ⟨start, hstart⟩, assign⟧ := by
-  apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)
+    ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
+  apply denote.eq_of_isPrefix (entry := ⟨aig, start, inv, hstart⟩)
   apply go_isPrefix_aig
 
 @[simp]
 theorem go_denote_entry (entry : Entrypoint β) {h} :
-    ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, h⟩, assign⟧ = ⟦entry, assign⟧ := by
+    ⟦(go entry.aig expr atomHandler).val.aig, ⟨entry.ref.gate, entry.ref.invert, h⟩, assign⟧
+      =
+    ⟦entry, assign⟧ := by
   apply denote.eq_of_isPrefix
   apply ofBoolExprCached.go_isPrefix_aig
 
diff --git a/tests/lean/run/bv_counterexample.lean b/tests/lean/run/bv_counterexample.lean
index 445235db68..c3081bd7ea 100644
--- a/tests/lean/run/bv_counterexample.lean
+++ b/tests/lean/run/bv_counterexample.lean
@@ -12,7 +12,7 @@ example (x : BitVec 64) : x < x + 1 := by
 
 /--
 error: The prover found a counterexample, consider the following assignment:
-x = 511#64
+x = 0#64
 -/
 #guard_msgs in
 example (x : BitVec 64) (h : x < 512) : x ^^^ x ≠ 0 := by