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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ s.getRefD idx alt = alt
Tactic:
unfold getRefD
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ (if hidx : idx < len then s.getRef idx hidx else alt) = alt

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
⊢ (if hidx : idx < len then s.getRef idx hidx else alt) = alt
Tactic:
split
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.getRef idx h✝ = alt

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.getRef idx h✝ = alt

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Tactic:
. omega
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Tactic:
. rfl
State after:
no goals

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : idx < len
⊢ s.getRef idx h✝ = alt
Tactic:
omega
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefStream len
idx : Nat
alt : aig.Ref
hidx : len ≤ idx
h✝ : ¬idx < len
⊢ alt = alt
Tactic:
rfl
State after:
no goals