internlm/Lean-Github huggingface dataset:
Theorem: BoolExprNat.eval_if
Proof state before:
case w
x✝ : BoolExprNat
f : List Bool
g : Gate
x y : BoolExprNat
i : Nat
h : i < x.toBoolExpr.vars
⊢ f.getD i false = true → i < max x.toBoolExpr.vars y.toBoolExpr.vars
Tactic:
omega
Proof state after:
no goals
Theorem: BoolExprNat.sat_iff
Proof state before:
x : BoolExprNat
f : List Bool
⊢ x.sat f ↔ x.toBoolExpr.sat fun x => f.getD x false
Tactic:
simp [sat, BoolExpr.sat]
Proof state after:
no goals
Theorem: BoolExprNat.unsat_iff
Proof state before:
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.unsat
Tactic:
rw [← BoolExpr.attach_unsat]
Proof state after:
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.attach.unsat
Theorem: BoolExprNat.unsat_iff
Proof state before:
x : BoolExprNat
⊢ x.unsat ↔ x.toBoolExpr.attach.unsat
Tactic:
simp only [unsat, BoolExpr.unsat]
Proof state after:
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) ↔
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
Theorem: BoolExprNat.unsat_iff
Proof state before:
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) ↔
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
constructor
Proof state after:
case mp
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) →
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false

case mpr
x : BoolExprNat
⊢ (∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false) →
    ∀ (f : List Bool), eval f x = false
Theorem: BoolExprNat.unsat_iff
Proof state before:
case mp
x : BoolExprNat
⊢ (∀ (f : List Bool), eval f x = false) →
    ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
intro h f
Proof state after:
case mp
x : BoolExprNat
h : ∀ (f : List Bool), eval f x = false
f : Fin x.toBoolExpr.vars → Bool
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
Theorem: BoolExprNat.unsat_iff
Proof state before:
case mp
x : BoolExprNat
h : ∀ (f : List Bool), eval f x = false
f : Fin x.toBoolExpr.vars → Bool
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
specialize h (List.ofFn f)
Proof state after:
case mp
x : BoolExprNat
f : Fin x.toBoolExpr.vars → Bool
h : eval (List.ofFn f) x = false
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
Theorem: BoolExprNat.unsat_iff
Proof state before:
case mp
x : BoolExprNat
f : Fin x.toBoolExpr.vars → Bool
h : eval (List.ofFn f) x = false
⊢ BoolExpr.eval f x.toBoolExpr.attach = false
Tactic:
simpa using h
Proof state after:
no goals
Theorem: BoolExprNat.unsat_iff
Proof state before:
case mpr
x : BoolExprNat
⊢ (∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false) →
    ∀ (f : List Bool), eval f x = false
Tactic:
intro h f
Proof state after:
case mpr
x : BoolExprNat
h : ∀ (f : Fin x.toBoolExpr.vars → Bool), BoolExpr.eval f x.toBoolExpr.attach = false
f : List Bool
⊢ eval f x = false
Theorem: BoolExprNat.unsat_iff
Proof state before:
case mpr
x : BoolExprNat
f : List Bool
h : BoolExpr.eval (fun x_1 => f.getD (↑x_1) false) x.toBoolExpr.attach = false
⊢ eval f x = false
Tactic:
simpa using h
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2581__BAB___A__B
Proof state before:
⊢ ∀ (a op1 : BitVec 64), (a ||| op1) ^^^ op1 = a &&& (op1 ^^^ -1)
Tactic:
intros
Proof state after:
a✝ op1✝ : BitVec 64
⊢ (a✝ ||| op1✝) ^^^ op1✝ = a✝ &&& (op1✝ ^^^ -1)
Theorem: bitvec_AndOrXor_2581__BAB___A__B
Proof state before:
a✝ op1✝ : BitVec 64
⊢ (a✝ ||| op1✝) ^^^ op1✝ = a✝ &&& (op1✝ ^^^ -1)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_135
Proof state before:
⊢ ∀ (X C1 C2 : BitVec 64), (X ^^^ C1) &&& C2 = X &&& C2 ^^^ C1 &&& C2
Tactic:
intros
Proof state after:
X✝ C1✝ C2✝ : BitVec 64
⊢ (X✝ ^^^ C1✝) &&& C2✝ = X✝ &&& C2✝ ^^^ C1✝ &&& C2✝
Theorem: bitvec_AndOrXor_135
Proof state before:
X✝ C1✝ C2✝ : BitVec 64
⊢ (X✝ ^^^ C1✝) &&& C2✝ = X✝ &&& C2✝ ^^^ C1✝ &&& C2✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: arith_unit_1
Proof state before:
x y : BitVec 64
⊢ x + y = y + x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: arith_unit_1'
Proof state before:
x y : BitVec 64
⊢ x.add y = y + x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: arith_unit_2
Proof state before:
x y : BitVec 64
⊢ x - y = -y + x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: arith_unit_2'
Proof state before:
x y : BitVec 64
⊢ x.sub y = y.neg + x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: arith_unit_3
Proof state before:
x y : BitVec 16
⊢ x - (x - y) = y
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2285
Proof state before:
⊢ ∀ (A B : BitVec 64), A ||| A ^^^ B ^^^ -1 = A ||| B ^^^ -1
Tactic:
intros
Proof state after:
A✝ B✝ : BitVec 64
⊢ A✝ ||| A✝ ^^^ B✝ ^^^ -1 = A✝ ||| B✝ ^^^ -1
Theorem: bitvec_AndOrXor_2285
Proof state before:
A✝ B✝ : BitVec 64
⊢ A✝ ||| A✝ ^^^ B✝ ^^^ -1 = A✝ ||| B✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_1
Proof state before:
x y : BitVec 64
⊢ x <<< 65 = y <<< 66
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_1'
Proof state before:
x y : BitVec 64
⊢ x.shiftLeft 65 = y >>> 66
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_2
Proof state before:
x y : BitVec 64
⊢ x >>> 65 = y >>> 66
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_2'
Proof state before:
x y : BitVec 64
⊢ x.ushiftRight 65 = y >>> 66
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_3
Proof state before:
x : BitVec 64
⊢ x <<< 32 <<< 32 = x >>> 32 >>> 32
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_5
Proof state before:
x y : BitVec 64
⊢ x <<< y + y = y + x <<< y
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_6
Proof state before:
x y : BitVec 64
⊢ x >>> y + y = y + x >>> y
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_1
Proof state before:
x : BitVec 64
⊢ x.rotateLeft 0 = x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_2
Proof state before:
x : BitVec 64
⊢ x.rotateLeft 64 = x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_3
Proof state before:
x : BitVec 64
⊢ x.rotateLeft 16 = (x.rotateLeft 6).rotateLeft 10
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_4
Proof state before:
x : BitVec 64
⊢ x.rotateLeft (64 + 16) = x.rotateLeft 16
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_5
Proof state before:
x : BitVec 64
⊢ x.rotateRight 0 = x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_6
Proof state before:
x : BitVec 64
⊢ x.rotateRight 64 = x
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_7
Proof state before:
x : BitVec 64
⊢ x.rotateRight 16 = (x.rotateRight 6).rotateRight 10
Tactic:
bv_decide
Proof state after:
no goals
Theorem: rotate_unit_8
Proof state before:
x : BitVec 64
⊢ x.rotateRight (64 + 16) = x.rotateRight 16
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_7
Proof state before:
x : BitVec 64
⊢ x.sshiftRight 65 = x.sshiftRight 66
Tactic:
bv_decide
Proof state after:
no goals
Theorem: shift_unit_8
Proof state before:
x : BitVec 64
h : BitVec.slt 0 x = true
⊢ x.sshiftRight 32 = x >>> 32
Tactic:
bv_decide
Proof state after:
no goals
Theorem: BVExpr.bitblast_le_size
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ aig.decls.size ≤ (bitblast aig expr).aig.decls.size
Tactic:
unfold bitblast
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ aig.decls.size ≤ (bitblast.go aig expr).val.aig.decls.size
Theorem: BVExpr.bitblast_le_size
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ aig.decls.size ≤ (bitblast.go aig expr).val.aig.decls.size
Tactic:
exact (bitblast.go aig expr).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr).val.aig.decls.size),
    (go aig expr).val.aig.decls[idx] = aig.decls[idx]
Tactic:
intros idx h1 h2
Proof state after:
w : Nat
aig : AIG BVBit
expr : BVExpr w
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig expr).val.aig.decls.size
⊢ (go aig expr).val.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case var
w idx w✝ idx✝ : Nat
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (var idx✝)).val.aig.decls.size
⊢ (go aig (var idx✝)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
case var
w idx w✝ idx✝ : Nat
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (var idx✝)).val.aig.decls.size
⊢ (blastVar aig { ident := idx✝ }).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case var
w idx w✝ idx✝ : Nat
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (var idx✝)).val.aig.decls.size
⊢ (blastVar aig { ident := idx✝ }).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastVar)]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case const
w idx w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (const val✝)).val.aig.decls.size
⊢ (go aig (const val✝)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
case const
w idx w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (const val✝)).val.aig.decls.size
⊢ (blastConst aig val✝).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case const
w idx w✝ : Nat
val✝ : BitVec w✝
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (const val✝)).val.aig.decls.size
⊢ (blastConst aig val✝).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := blastConst)]
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case bin
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin op rhs)).val.aig.decls.size
⊢ (go aig (lhs.bin op rhs)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
match op with
| .and | .or | .xor =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := AIG.RefStream.zip)]
  rw [rih, lih]
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (bitblast.go aig lhs).property
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . apply Nat.le_trans
      . exact (bitblast.go aig lhs).property
      . exact (go (go aig lhs).1.aig rhs).property
| .add =>
  dsimp [go]
  rw [AIG.LawfulStreamOperator.decl_eq (f := blastAdd)]
  rw [rih, lih]
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . exact (bitblast.go aig lhs).property
  . apply Nat.lt_of_lt_of_le
    . exact h1
    . apply Nat.le_trans
      . exact (bitblast.go aig lhs).property
      . exact (go (go aig lhs).1.aig rhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp [go]
Proof state after:
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ (AIG.RefStream.zip (go (go aig lhs).1.aig rhs).1.aig
            (AIG.RefStream.ZipTarget.mk
              { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }
              AIG.mkXorCached)).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ (AIG.RefStream.zip (go (go aig lhs).1.aig rhs).1.aig
            (AIG.RefStream.ZipTarget.mk
              { lhs := (go aig lhs).1.stream.cast ⋯, rhs := (go (go aig lhs).1.aig rhs).1.stream }
              AIG.mkXorCached)).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [AIG.LawfulStreamOperator.decl_eq (f := AIG.RefStream.zip)]
Proof state after:
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ (go (go aig lhs).1.aig rhs).1.aig.decls[idx] = aig.decls[idx]

case h1
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go (go aig lhs).1.aig rhs).1.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ (go (go aig lhs).1.aig rhs).1.aig.decls[idx] = aig.decls[idx]

case h1
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go (go aig lhs).1.aig rhs).1.aig.decls.size
Tactic:
rw [rih, lih]
Proof state after:
case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go aig lhs).val.aig.decls.size

case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go aig lhs).val.aig.decls.size

case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
. apply Nat.lt_of_lt_of_le
  . exact h1
  . exact (bitblast.go aig lhs).property
Proof state after:
case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go (go aig lhs).1.aig rhs).val.aig.decls.size
Tactic:
. apply Nat.lt_of_lt_of_le
  . exact h1
  . apply Nat.le_trans
    . exact (bitblast.go aig lhs).property
    . exact (go (go aig lhs).1.aig rhs).property
Proof state after:
no goals
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < (go aig lhs).val.aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case h2.a
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < ?h2.m

case h2.a
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ ?h2.m ≤ (go aig lhs).val.aig.decls.size

case h2.m
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ Nat
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ idx < ?h2.m

case h2.a
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ ?h2.m ≤ (go aig lhs).val.aig.decls.size

case h2.m
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ Nat
Tactic:
. exact h1
Proof state after:
case h2.a
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig lhs).val.aig.decls.size
Theorem: BVExpr.bitblast.go_decl_eq
Proof state before:
case h2.a
w idx w✝ : Nat
lhs : BVExpr w✝
op : BVBinOp
rhs : BVExpr w✝
lih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig lhs).val.aig.decls.size),
    (go aig lhs).val.aig.decls[idx] = aig.decls[idx]
rih :
  ∀ (aig : AIG BVBit) (h1 : idx < aig.decls.size) (h2 : idx < (go aig rhs).val.aig.decls.size),
    (go aig rhs).val.aig.decls[idx] = aig.decls[idx]
aig : AIG BVBit
h1 : idx < aig.decls.size
h2 : idx < (go aig (lhs.bin BVBinOp.xor rhs)).val.aig.decls.size
⊢ aig.decls.size ≤ (go aig lhs).val.aig.decls.size
Tactic:
. exact (bitblast.go aig lhs).property
Proof state after:
no goals