internlm/Lean-Github huggingface dataset:
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate <
    (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size
Tactic:
. simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref :=
          { gate := (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate,
            hgate := ?e_a.hright✝ } },
      assign⟧ =
    (~~~rhs).getLsb idx
Tactic:
simp only [RefStream.getRef_cast, Ref_cast', BitVec.getLsb_not, hidx, decide_True,
  Bool.true_and]
Proof state after:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((BVExpr.bitblast.blastNot aig input.rhs).stream.getRef idx hidx).gate, hgate := ⋯ } },
      assign⟧ =
    !rhs.getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((BVExpr.bitblast.blastNot aig input.rhs).stream.getRef idx hidx).gate, hgate := ⋯ } },
      assign⟧ =
    !rhs.getLsb idx
Tactic:
rw [BVExpr.bitblast.blastNot_eq_eval_getLsb]
Proof state after:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (!⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧) = !rhs.getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (!⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧) = !rhs.getLsb idx
Tactic:
congr 1
Proof state after:
case e_a.hright.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright.e_a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
Tactic:
apply hright
Proof state after:
no goals
Theorem: BVPred.mkUlt_denote_eq_eval_ult
Proof state before:
case e_a.hright
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefStream w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := input.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
idx : Nat
hidx : idx < w
⊢ (((BVExpr.bitblast.blastNot aig input.rhs).stream.cast ⋯).getRef idx hidx).gate <
    (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size
Tactic:
simp [Ref.hgate]
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__497
Proof state before:
⊢ ∀ (X C C2 : BitVec 64), (X ^^^ C2) >>> C = X >>> C ^^^ C2 >>> C
Tactic:
intros
Proof state after:
X✝ C✝ C2✝ : BitVec 64
⊢ (X✝ ^^^ C2✝) >>> C✝ = X✝ >>> C✝ ^^^ C2✝ >>> C✝
Theorem: bitvec_InstCombineShift__497
Proof state before:
X✝ C✝ C2✝ : BitVec 64
⊢ (X✝ ^^^ C2✝) >>> C✝ = X✝ >>> C✝ ^^^ C2✝ >>> C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.Assignment.toAIGAssignment_apply
Proof state before:
assign : Assignment
bit : BVBit
⊢ assign.toAIGAssignment bit = (assign.getD bit.var).bv.getLsb ↑bit.idx
Tactic:
rfl
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2243__B__C__A__B___B__A__C
Proof state before:
⊢ ∀ (A C B : BitVec 64), (B ||| C) &&& A ||| B = B ||| A &&& C
Tactic:
intros
Proof state after:
A✝ C✝ B✝ : BitVec 64
⊢ (B✝ ||| C✝) &&& A✝ ||| B✝ = B✝ ||| A✝ &&& C✝
Theorem: bitvec_AndOrXor_2243__B__C__A__B___B__A__C
Proof state before:
A✝ C✝ B✝ : BitVec 64
⊢ (B✝ ||| C✝) &&& A✝ ||| B✝ = B✝ ||| A✝ &&& C✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1295
Proof state before:
⊢ ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ (a✝ &&& b✝) + (a✝ ^^^ b✝) = a✝ ||| b✝
Theorem: bitvec_AddSub_1295
Proof state before:
a✝ b✝ : BitVec 64
⊢ (a✝ &&& b✝) + (a✝ ^^^ b✝) = a✝ ||| b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_239
Proof state before:
⊢ ∀ (Y X : BitVec 64), (0 - X) * (0 - Y) = X * Y
Tactic:
intros
Proof state after:
Y✝ X✝ : BitVec 64
⊢ (0 - X✝) * (0 - Y✝) = X✝ * Y✝
Theorem: bitvec_239
Proof state before:
Y✝ X✝ : BitVec 64
⊢ (0 - X✝) * (0 - Y✝) = X✝ * Y✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AddSub_1176
Proof state before:
⊢ ∀ (a b : BitVec 64), a + (0 - b) = a - b
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ a✝ + (0 - b✝) = a✝ - b✝
Theorem: bitvec_AddSub_1176
Proof state before:
a✝ b✝ : BitVec 64
⊢ a✝ + (0 - b✝) = a✝ - b✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_InstCombineShift__351
Proof state before:
⊢ ∀ (X C1 C2 : BitVec 7), (X * C1) <<< C2 = X * C1 <<< C2
Tactic:
intros
Proof state after:
X✝ C1✝ C2✝ : BitVec 7
⊢ (X✝ * C1✝) <<< C2✝ = X✝ * C1✝ <<< C2✝
Theorem: bitvec_InstCombineShift__351
Proof state before:
X✝ C1✝ C2✝ : BitVec 7
⊢ (X✝ * C1✝) <<< C2✝ = X✝ * C1✝ <<< C2✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVDecide.Normalize.BitVec.eq_to_beq
Proof state before:
w : Nat
a b : BitVec w
⊢ (a = b) = ((a == b) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.BitVec.ne_to_beq
Proof state before:
w : Nat
a b : BitVec w
⊢ (a ≠ b) = ((!a == b) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.eq_to_beq
Proof state before:
a b : Bool
⊢ (a = b) = ((a == b) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.BitVec.bne_to_beq
Proof state before:
w : Nat
a b : BitVec w
⊢ (a != b) = !a == b
Tactic:
simp [bne]
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.bne_to_beq
Proof state before:
a b : Bool
⊢ (a != b) = !a == b
Tactic:
simp [bne]
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.eq_false_to_beq
Proof state before:
a : Bool
⊢ (a = false) = ((!a) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.neg_to_not
Proof state before:
a : Bool
⊢ (¬a = true) = ((!a) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.ne_to_beq
Proof state before:
a b : Bool
⊢ (a ≠ b) = ((!a == b) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.imp_to_or
Proof state before:
a b : Bool
⊢ (a = true → b = true) = ((!a || b) = true)
Tactic:
revert a b
Proof state after:
⊢ ∀ (a b : Bool), (a = true → b = true) = ((!a || b) = true)
Theorem: BVDecide.Normalize.Bool.imp_to_or
Proof state before:
⊢ ∀ (a b : Bool), (a = true → b = true) = ((!a || b) = true)
Tactic:
decide
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.or_to_or
Proof state before:
a b : Bool
⊢ (a = true ∨ b = true) = ((a || b) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.and_to_and
Proof state before:
a b : Bool
⊢ (a = true ∧ b = true) = ((a && b) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.iff_to_or
Proof state before:
a b : Bool
⊢ (a = true ↔ b = true) = (((!a || b) && (!b || a)) = true)
Tactic:
revert a b
Proof state after:
⊢ ∀ (a b : Bool), (a = true ↔ b = true) = (((!a || b) && (!b || a)) = true)
Theorem: BVDecide.Normalize.Bool.iff_to_or
Proof state before:
⊢ ∀ (a b : Bool), (a = true ↔ b = true) = (((!a || b) && (!b || a)) = true)
Tactic:
decide
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.eq_false
Proof state before:
a : Bool
⊢ ((a = true) = False) = ((!a) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.decide_eq_true
Proof state before:
a : Bool
⊢ decide (a = true) = a
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.eq_true_eq_true_eq
Proof state before:
x y : Bool
⊢ ((x = true) = (y = true)) = (x = y)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.BitVec.lt_ult
Proof state before:
w : Nat
x y : BitVec w
⊢ (x < y) = (x.ult y = true)
Tactic:
rw [BitVec.ult]
Proof state after:
w : Nat
x y : BitVec w
⊢ (x < y) = (decide (x.toNat < y.toNat) = true)
Theorem: BVDecide.Normalize.BitVec.lt_ult
Proof state before:
w : Nat
x y : BitVec w
⊢ (x < y) = (decide (x.toNat < y.toNat) = true)
Tactic:
rw [LT.lt]
Proof state after:
w : Nat
x y : BitVec w
⊢ BitVec.instLT.1 x y = (decide (x.toNat < y.toNat) = true)
Theorem: BVDecide.Normalize.BitVec.lt_ult
Proof state before:
w : Nat
x y : BitVec w
⊢ BitVec.instLT.1 x y = (decide (x.toNat < y.toNat) = true)
Tactic:
rw [BitVec.instLT]
Proof state after:
w : Nat
x y : BitVec w
⊢ { lt := fun x x_1 => x.toNat < x_1.toNat }.1 x y = (decide (x.toNat < y.toNat) = true)
Theorem: BVDecide.Normalize.BitVec.lt_ult
Proof state before:
w : Nat
x y : BitVec w
⊢ { lt := fun x x_1 => x.toNat < x_1.toNat }.1 x y = (decide (x.toNat < y.toNat) = true)
Tactic:
simp
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.and_eq_and
Proof state before:
x y : Bool
⊢ x.and y = (x && y)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.or_eq_or
Proof state before:
x y : Bool
⊢ x.or y = (x || y)
Tactic:
rfl
Proof state after:
no goals
Theorem: BVDecide.Normalize.Bool.no_eq_not
Proof state before:
x : Bool
⊢ x.not = !x
Tactic:
rfl
Proof state after:
no goals
Theorem: bitvec_AddSub_1560
Proof state before:
⊢ ∀ (a : BitVec 64), -1 - a = a ^^^ -1
Tactic:
intros
Proof state after:
a✝ : BitVec 64
⊢ -1 - a✝ = a✝ ^^^ -1
Theorem: bitvec_AddSub_1560
Proof state before:
a✝ : BitVec 64
⊢ -1 - a✝ = a✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2123___A__B__A__B___A__B
Proof state before:
⊢ ∀ (A B : BitVec 64), A &&& (B ^^^ -1) ||| A ^^^ B = A ^^^ B
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ &&& (B✝ ^^^ -1) ||| A✝ ^^^ B✝ = A✝ ^^^ B✝
Theorem: bitvec_AndOrXor_2123___A__B__A__B___A__B
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ &&& (B✝ ^^^ -1) ||| A✝ ^^^ B✝ = A✝ ^^^ B✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go input distance curr hcurr s).getRef idx ⋯ = s.getRef idx hidx
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (go input distance curr hcurr s).getRef idx ⋯ = s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (go input distance curr hcurr s).getRef idx ⋯ = s.getRef idx hidx
Tactic:
unfold go
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (if hcurr1 : curr < w then
          if hcurr2 : curr < w - distance % w then
            let ref := input.getRef (distance % w + curr) ⋯;
            let s := s.pushRef ref;
            go input distance (curr + 1) ⋯ s
          else
            let ref := input.getRef (curr - (w - distance % w)) ⋯;
            let s := s.pushRef ref;
            go input distance (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ (if hcurr1 : curr < w then
          if hcurr2 : curr < w - distance % w then
            let ref := input.getRef (distance % w + curr) ⋯;
            let s := s.pushRef ref;
            go input distance (curr + 1) ⋯ s
          else
            let ref := input.getRef (curr - (w - distance % w)) ⋯;
            let s := s.pushRef ref;
            go input distance (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
split
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < w
⊢ (if hcurr2 : curr < w - distance % w then
          let ref := input.getRef (distance % w + curr) ⋯;
          let s := s.pushRef ref;
          go input distance (curr + 1) ⋯ s
        else
          let ref := input.getRef (curr - (w - distance % w)) ⋯;
          let s := s.pushRef ref;
          go input distance (curr + 1) ⋯ s).getRef
      idx ⋯ =
    s.getRef idx hidx

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < w
⊢ (if hcurr2 : curr < w - distance % w then
          let ref := input.getRef (distance % w + curr) ⋯;
          let s := s.pushRef ref;
          go input distance (curr + 1) ⋯ s
        else
          let ref := input.getRef (curr - (w - distance % w)) ⋯;
          let s := s.pushRef ref;
          go input distance (curr + 1) ⋯ s).getRef
      idx ⋯ =
    s.getRef idx hidx

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
. dsimp
  split
  . rw [go_getRef_aux]
    rw [AIG.RefStream.getRef_push_ref_lt]
  . rw [go_getRef_aux]
    rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : ¬curr < w
⊢ (let_fun hcurr := ⋯;
        hcurr ▸ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
. dsimp
  simp only [RefStream.getRef, Ref.mk.injEq]
  congr
  . omega
  . simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < w
⊢ (if hcurr2 : curr < w - distance % w then
          let ref := input.getRef (distance % w + curr) ⋯;
          let s := s.pushRef ref;
          go input distance (curr + 1) ⋯ s
        else
          let ref := input.getRef (curr - (w - distance % w)) ⋯;
          let s := s.pushRef ref;
          go input distance (curr + 1) ⋯ s).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
dsimp
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < w
⊢ (if hcurr2 : curr < w - distance % w then
          go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance % w + curr) ⋯))
        else go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef
      idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝ : curr < w
⊢ (if hcurr2 : curr < w - distance % w then
          go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance % w + curr) ⋯))
        else go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef
      idx ⋯ =
    s.getRef idx hidx
Tactic:
split
Proof state after:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance % w + curr) ⋯))).getRef idx ⋯ = s.getRef idx hidx

case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
case isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance % w + curr) ⋯))).getRef idx ⋯ = s.getRef idx hidx

case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx ⋯ =
    s.getRef idx hidx
Tactic:
. rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx ⋯ =
    s.getRef idx hidx
Theorem: BVExpr.bitblast.blastRotateRight.go_getRef_aux
Proof state before:
case isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
distance : Nat
input : aig.RefStream w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
h✝¹ : curr < w
h✝ : ¬curr < w - distance % w
⊢ (go input distance (curr + 1) ⋯ (s.pushRef (input.getRef (curr - (w - distance % w)) ⋯))).getRef idx ⋯ =
    s.getRef idx hidx
Tactic:
. rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
no goals