internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  (if hdist : distance + curr < w then
      let s := s.pushRef (input.getRef (distance + curr) ⋯);
      go aig input distance (curr + 1) ⋯ s
    else
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let zeroRef := res.ref;
      let_fun hfinal := ⋯;
      let s := s.cast hfinal;
      let input := input.cast hfinal;
      let s := s.pushRef zeroRef;
      go aig_1 input distance (curr + 1) ⋯ s) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

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
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. dsimp at hgo
  split at hgo
  . rw [← hgo]
    intro idx h1 h2
    rw [blastShiftRightConst.go_decl_eq]
  . rw [← hgo]
    intro idx h1 h2
    rw [blastShiftRightConst.go_decl_eq]
    rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
    apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
    assumption
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
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. simp [← hgo]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  (if hdist : distance + curr < w then
      let s := s.pushRef (input.getRef (distance + curr) ⋯);
      go aig input distance (curr + 1) ⋯ s
    else
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let zeroRef := res.ref;
      let_fun hfinal := ⋯;
      let s := s.cast hfinal;
      let input := input.cast hfinal;
      let s := s.pushRef zeroRef;
      go aig_1 input distance (curr + 1) ⋯ s) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp at hgo
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
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  (if hdist : distance + curr < w then go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))
    else
      go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
        ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  (if hdist : distance + curr < w then go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))
    else
      go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
        ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
split at hgo
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. rw [← hgo]
  intro idx h1 h2
  rw [blastShiftRightConst.go_decl_eq]
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. rw [← hgo]
  intro idx h1 h2
  rw [blastShiftRightConst.go_decl_eq]
  rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
  apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
  assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
rw [← hgo]
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls.size),
    (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls.size),
    (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls[idx] = aig.decls[idx]
Tactic:
intro idx h1 h2
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls.size
⊢ (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls[idx] = aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : distance + curr < w
hgo : go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯)) = res
idx : Nat
h1 : idx < aig.decls.size
h2 : idx < (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls.size
⊢ (go aig input distance (curr + 1) ⋯ (s.pushRef (input.getRef (distance + curr) ⋯))).aig.decls[idx] = aig.decls[idx]
Tactic:
rw [blastShiftRightConst.go_decl_eq]
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
rw [← hgo]
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
                ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size),
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
              ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls[idx] =
      aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
                ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size),
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
              ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls[idx] =
      aig.decls[idx]
Tactic:
intro idx h1 h2
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls[idx] =
    aig.decls[idx]
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls[idx] =
    aig.decls[idx]
Tactic:
rw [blastShiftRightConst.go_decl_eq]
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (aig.mkConstCached false).aig.decls[idx] = aig.decls[idx]

case isTrue.isFalse.h1
α : 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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ (aig.mkConstCached false).aig.decls[idx] = aig.decls[idx]

case isTrue.isFalse.h1
α : 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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := AIG.mkConstCached)]
Proof state after:
case isTrue.isFalse.h2
α : 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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
Proof state before:
case isTrue.isFalse.h2
α : 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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < (aig.mkConstCached false).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := AIG.mkConstCached)
Proof state after:
case isTrue.isFalse.h2.h
α : 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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < aig.decls.size
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
Proof state before:
case isTrue.isFalse.h2.h
α : 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
res : AIG.RefStreamEntry α w
h✝¹ : curr < w
h✝ : ¬distance + curr < w
hgo :
  go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
      ((s.cast ⋯).pushRef (aig.mkConstCached false).ref) =
    res
idx : Nat
h1 : idx < aig.decls.size
h2 :
  idx <
    (go (aig.mkConstCached false).aig (input.cast ⋯) distance (curr + 1) ⋯
            ((s.cast ⋯).pushRef (aig.mkConstCached false).ref)).aig.decls.size
⊢ idx < aig.decls.size
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastShiftRightConst.go_decl_eq
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
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
simp [← hgo]
Proof state after:
no goals
Theorem: bitvec_229
Proof state before:
⊢ ∀ (X C1 Op1 : BitVec 64), (X + C1) * Op1 = X * Op1 + C1 * Op1
Tactic:
intros
Proof state after:
X✝ C1✝ Op1✝ : BitVec 64
⊢ (X✝ + C1✝) * Op1✝ = X✝ * Op1✝ + C1✝ * Op1✝
Theorem: bitvec_229
Proof state before:
X✝ C1✝ Op1✝ : BitVec 64
⊢ (X✝ + C1✝) * Op1✝ = X✝ * Op1✝ + C1✝ * Op1✝
Tactic:
bv_decide
Proof state after:
no goals
Theorem: bitvec_AndOrXor_1683_1
Proof state before:
⊢ ∀ (a b : BitVec 64), ((decide (b < a) || a == b) = true) = (b ≤ a)
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ ((decide (b✝ < a✝) || a✝ == b✝) = true) = (b✝ ≤ a✝)
Theorem: bitvec_AndOrXor_1683_1
Proof state before:
a✝ b✝ : BitVec 64
⊢ ((decide (b✝ < a✝) || a✝ == b✝) = true) = (b✝ ≤ a✝)
Tactic:
bv_decide
Proof state after:
no goals
Theorem: LeanSAT.polarity_eq
Proof state before:
l₁ l₂ : ILit
⊢ polarity l₁ = polarity l₂ ↔ (0 < ↑l₁ ↔ 0 < ↑l₂)
Tactic:
simp [polarity]
Proof state after:
no goals
Theorem: LeanSAT.ILit.exists_succ_toVar
Proof state before:
l : ILit
⊢ ∃ n, ↑(toVar l) = n + 1
Tactic:
exact Nat.exists_eq_add_of_le' (toVar l).property
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_ne_of_var_ne
Proof state before:
l₁ l₂ : ILit
⊢ toVar l₁ ≠ toVar l₂ → ILit.index l₁ ≠ ILit.index l₂
Tactic:
intro hne hcon
Proof state after:
l₁ l₂ : ILit
hne : toVar l₁ ≠ toVar l₂
hcon : ILit.index l₁ = ILit.index l₂
⊢ False
Theorem: LeanSAT.ILit.index_ne_of_var_ne
Proof state before:
l₁ l₂ : ILit
hne : toVar l₁ ≠ toVar l₂
hcon : ILit.index l₁ = ILit.index l₂
⊢ False
Tactic:
rcases mkPos_or_mkNeg l₁ with (hl₁ | hl₁)
<;> rw [hl₁] at hcon
<;> rcases mkPos_or_mkNeg l₂ with (hl₂ | hl₂)
<;> rw [hl₂] at hcon
<;> simp at hcon
<;> contradiction
Proof state after:
no goals
Theorem: LeanSAT.ILit.index_eq_iff_eq_or_negate_eq
Proof state before:
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ ↔ l₁ = l₂ ∨ negate l₁ = l₂
Tactic:
constructor
Proof state after:
case mp
l₁ l₂ : ILit
⊢ ILit.index l₁ = ILit.index l₂ → l₁ = l₂ ∨ negate l₁ = l₂

case mpr
l₁ l₂ : ILit
⊢ l₁ = l₂ ∨ negate l₁ = l₂ → ILit.index l₁ = ILit.index l₂