Theorem: BVExpr.bitblast.blastVar.go_denote_mem_prefix (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Var.lean)

State before:
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ start < (go w aig idx s a hidx).aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
State after:
case a
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go w aig idx s a hidx).aig.decls.size

case m
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ Nat

State before:
case a
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go w aig idx s a hidx).aig.decls.size

case m
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ Nat
Tactic:
exact hstart
State after:
case a
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size

State before:
case a
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size
Tactic:
apply go_le_size
State after:
no goals

State before:
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ ⟦{ aig := (go w aig idx s a hidx).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧
Tactic:
apply denote.eq_of_aig_eq (entry := ⟨aig, start,hstart⟩)
State after:
case hprefix
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go w aig idx s a hidx).aig.decls

State before:
case hprefix
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go w aig idx s a hidx).aig.decls
Tactic:
apply IsPrefix.of
State after:
case hprefix.idx_eq
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx_1 : Nat) (h : idx_1 < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go w aig idx s a hidx).aig.decls[idx_1] =
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx_1]

case hprefix.size_le
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size

State before:
case hprefix.idx_eq
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx_1 : Nat) (h : idx_1 < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go w aig idx s a hidx).aig.decls[idx_1] =
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx_1]

case hprefix.size_le
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size
Tactic:
. intros
  apply go_decl_eq
State after:
case hprefix.size_le
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size

State before:
case hprefix.size_le
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size
Tactic:
. intros
  apply go_le_size
State after:
no goals

State before:
case hprefix.idx_eq
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ ∀ (idx_1 : Nat) (h : idx_1 < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size),
    (go w aig idx s a hidx).aig.decls[idx_1] =
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx_1]
Tactic:
intros
State after:
case hprefix.idx_eq
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
idx✝ : Nat
h✝ : idx✝ < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size
⊢ (go w aig idx s a hidx).aig.decls[idx✝] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx✝]

State before:
case hprefix.idx_eq
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
idx✝ : Nat
h✝ : idx✝ < { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size
⊢ (go w aig idx s a hidx).aig.decls[idx✝] = { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls[idx✝]
Tactic:
apply go_decl_eq
State after:
no goals

State before:
case hprefix.size_le
w : Nat
assign : BVBit → Bool
aig : AIG BVBit
idx : Nat
hidx : idx ≤ w
s : aig.RefStream idx
a start : Nat
hstart : start < aig.decls.size
⊢ { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls.size ≤ (go w aig idx s a hidx).aig.decls.size
Tactic:
apply go_le_size
State after:
no goals