Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Extract.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ExtractTarget aig newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦{ aig := (blastExtract aig target).aig, ref := (blastExtract aig target).stream.getRef idx hidx }, assign⟧ =
      if h : target.lo + idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef (target.lo + idx) h }, assign⟧
      else false
Tactic:
intro idx hidx
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ExtractTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦{ aig := (blastExtract aig target).aig, ref := (blastExtract aig target).stream.getRef idx hidx }, assign⟧ =
    if h : target.lo + idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef (target.lo + idx) h }, assign⟧
    else false

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ExtractTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦{ aig := (blastExtract aig target).aig, ref := (blastExtract aig target).stream.getRef idx hidx }, assign⟧ =
    if h : target.lo + idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef (target.lo + idx) h }, assign⟧
    else false
Tactic:
generalize hextract : blastExtract aig target = res
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ExtractTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hextract : blastExtract aig target = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : target.lo + idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef (target.lo + idx) h }, assign⟧
    else false

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ExtractTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
hextract : blastExtract aig target = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : target.lo + idx < target.w then ⟦{ aig := aig, ref := target.stream.getRef (target.lo + idx) h }, assign⟧
    else false
Tactic:
rcases target with ⟨input, hi, lo, hnew⟩
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : (ExtractTarget.mk input hi lo hnew).lo + idx < (ExtractTarget.mk input hi lo hnew).w then
      ⟦{ aig := aig,
          ref := (ExtractTarget.mk input hi lo hnew).stream.getRef ((ExtractTarget.mk input hi lo hnew).lo + idx) h },
        assign⟧
    else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : (ExtractTarget.mk input hi lo hnew).lo + idx < (ExtractTarget.mk input hi lo hnew).w then
      ⟦{ aig := aig,
          ref := (ExtractTarget.mk input hi lo hnew).stream.getRef ((ExtractTarget.mk input hi lo hnew).lo + idx) h },
        assign⟧
    else false
Tactic:
dsimp
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract : blastExtract aig (ExtractTarget.mk input hi lo hnew) = res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
unfold blastExtract at hextract
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (match ExtractTarget.mk input hi lo hnew with
    | ExtractTarget.mk input hi lo hnew =>
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let falseRef := res.ref;
      let input := input.cast ⋯;
      if h : lo ≤ hi then { aig := aig_1, stream := blastExtract.go input lo 0 ⋯ falseRef RefStream.empty }
      else
        let_fun this := ⋯;
        let base := RefStream.empty;
        let base := base.pushRef (input.getRefD lo falseRef);
        { aig := aig_1, stream := this ▸ base }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (match ExtractTarget.mk input hi lo hnew with
    | ExtractTarget.mk input hi lo hnew =>
      let res := aig.mkConstCached false;
      let aig_1 := res.aig;
      let falseRef := res.ref;
      let input := input.cast ⋯;
      if h : lo ≤ hi then { aig := aig_1, stream := blastExtract.go input lo 0 ⋯ falseRef RefStream.empty }
      else
        let_fun this := ⋯;
        let base := RefStream.empty;
        let base := base.pushRef (input.getRefD lo falseRef);
        { aig := aig_1, stream := this ▸ base }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
dsimp at hextract
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (if h : lo ≤ hi then
      { aig := (aig.mkConstCached false).aig,
        stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }
    else
      { aig := (aig.mkConstCached false).aig,
        stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
hextract :
  (if h : lo ≤ hi then
      { aig := (aig.mkConstCached false).aig,
        stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }
    else
      { aig := (aig.mkConstCached false).aig,
        stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }) =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
split at hextract
State after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
. rw [← hextract]
  rw [blastExtract.go_getRef]
  . dsimp
    split
    . rw [RefStream.getRef_in_bound]
      rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
      . congr 1
      . assumption
    . rw [RefStream.getRef_out_bound]
      . simp
      . omega
  . omega
State after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
. have : idx = 0 := by omega
  simp only [this]
  have : 1 = newWidth := by omega
  subst this
  rw [← hextract]
  split
  . rw [RefStream.getRef_in_bound]
    dsimp
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    . congr 2
    . omega
  . rw [RefStream.getRef_out_bound]
    . simp
    . omega
State after:
no goals

State before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
rw [← hextract]
State after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.stream.getRef
            idx hidx },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
rw [blastExtract.go_getRef]
State after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx

State before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Tactic:
. dsimp
  split
  . rw [RefStream.getRef_in_bound]
    rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
    . congr 1
    . assumption
  . rw [RefStream.getRef_out_bound]
    . simp
    . omega
State after:
case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx

State before:
case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Tactic:
. omega
State after:
no goals

State before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty }.aig,
        ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
dsimp
State after:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
split
State after:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false

State before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_in_bound]
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  . congr 1
  . assumption
State after:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false

State before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_out_bound]
  . simp
  . omega
State after:
no goals

State before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧
Tactic:
rw [RefStream.getRef_in_bound]
State after:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

State before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := aig,
        ref := { gate := ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate, hgate := ?mk.isTrue.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate < aig.decls.size

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

State before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := aig,
        ref := { gate := ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate, hgate := ?mk.isTrue.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate < aig.decls.size

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
. congr 1
State after:
case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

State before:
case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
. assumption
State after:
no goals

State before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := aig,
        ref := { gate := ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate, hgate := ?mk.isTrue.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧
Tactic:
congr 1
State after:
no goals

State before:
case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
assumption
State after:
no goals

State before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Tactic:
rw [RefStream.getRef_out_bound]
State after:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false

case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx

State before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false

case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
. simp
State after:
case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx

State before:
case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
. omega
State after:
no goals

State before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false
Tactic:
simp
State after:
no goals

State before:
case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
omega
State after:
no goals

State before:
case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Tactic:
omega
State after:
no goals

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
have : idx = 0 := by omega
State after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
simp only [this]
State after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
have : 1 = newWidth := by omega
State after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this✝ : idx = 0
this : 1 = newWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this✝ : idx = 0
this : 1 = newWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
subst this
State after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
rw [← hextract]
State after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false

State before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
split
State after:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧

case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false

State before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧

case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_in_bound]
  dsimp
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  . congr 2
  . omega
State after:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false

State before:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_out_bound]
  . simp
  . omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ idx = 0
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ 1 = newWidth
Tactic:
omega
State after:
no goals

State before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧
Tactic:
rw [RefStream.getRef_in_bound]
State after:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

State before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝
Tactic:
dsimp
State after:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig,
        ref := (RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef lo ⋯ }, assign⟧

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

State before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig,
        ref := (RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef lo ⋯ }, assign⟧

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝
Tactic:
rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
State after:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{ aig := aig,
        ref :=
          { gate := ((RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯).gate,
            hgate := ?mk.isFalse.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef lo ⋯ }, assign⟧

case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ((RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯).gate < aig.decls.size

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

State before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{ aig := aig,
        ref :=
          { gate := ((RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯).gate,
            hgate := ?mk.isFalse.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef lo ⋯ }, assign⟧

case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ((RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯).gate < aig.decls.size

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝
Tactic:
. congr 2
State after:
case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

State before:
case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝

case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝
Tactic:
. omega
State after:
no goals

State before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{ aig := aig,
        ref :=
          { gate := ((RefStream.empty.pushRef ((input.cast ⋯).getRef lo ?mk.isFalse.isTrue.hidx)).getRef 0 ⋯).gate,
            hgate := ?mk.isFalse.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef lo ⋯ }, assign⟧
Tactic:
congr 2
State after:
no goals

State before:
case mk.isFalse.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ lo < w✝
Tactic:
omega
State after:
no goals

State before:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Tactic:
rw [RefStream.getRef_out_bound]
State after:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false

case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo

State before:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false

case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Tactic:
. simp
State after:
case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo

State before:
case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Tactic:
. omega
State after:
no goals

State before:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream := ⋯ ▸ RefStream.empty.pushRef (aig.mkConstCached false).ref }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Tactic:
simp
State after:
no goals

State before:
case mk.isFalse.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ w✝ ≤ lo
Tactic:
omega
State after:
no goals