Theorem: AIG.RefStream.getRef_push_ref_lt (LeanSAT/AIG/RefStream.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ idx < len + 1
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.pushRef ref).getRef idx ⋯ = s.getRef idx hidx
Tactic:
simp [getRef, pushRef]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.refs.push ref.gate)[idx] = s.refs[idx]

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
ref : aig.Ref
idx : Nat
hidx : idx < len
⊢ (s.refs.push ref.gate)[idx] = s.refs[idx]
Tactic:
cases ref
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push { gate := gate✝, hgate := hgate✝ }.gate)[idx] = s.refs[idx]

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push { gate := gate✝, hgate := hgate✝ }.gate)[idx] = s.refs[idx]
Tactic:
simp only [Ref.mk.injEq]
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push gate✝)[idx] = s.refs[idx]

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
hidx : idx < len
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
⊢ (s.refs.push gate✝)[idx] = s.refs[idx]
Tactic:
rw [Array.get_push_lt]
State after:
no goals