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

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h : ¬idx < lw
⊢ idx - lw < rw
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ (lhs.append rhs).getRef idx hidx = if h : idx < lw then lhs.getRef idx h else rhs.getRef (idx - lw) ⋯
Tactic:
simp only [getRef, append]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } =
    if h : idx < lw then { gate := lhs.refs[idx], hgate := ⋯ } else { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
split
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
. simp [Ref.mk.injEq]
  rw [Array.get_append_left]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
. simp only [Ref.mk.injEq]
  rw [Array.get_append_right]
  . simp [lhs.hlen]
  . rw [lhs.hlen]
    omega
State after:
no goals

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := lhs.refs[idx], hgate := ⋯ }
Tactic:
simp [Ref.mk.injEq]
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = lhs.refs[idx]

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = lhs.refs[idx]
Tactic:
rw [Array.get_append_left]
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ { gate := (lhs.refs ++ rhs.refs)[idx], hgate := ⋯ } = { gate := rhs.refs[idx - lw], hgate := ⋯ }
Tactic:
simp only [Ref.mk.injEq]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = rhs.refs[idx - lw]

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ (lhs.refs ++ rhs.refs)[idx] = rhs.refs[idx - lw]
Tactic:
rw [Array.get_append_right]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Tactic:
. simp [lhs.hlen]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Tactic:
. rw [lhs.hlen]
  omega
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ rhs.refs[idx - lhs.refs.size] = rhs.refs[idx - lw]
Tactic:
simp [lhs.hlen]
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lhs.refs.size ≤ idx
Tactic:
rw [lhs.hlen]
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lw ≤ idx

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
lw rw : Nat
lhs : aig.RefStream lw
rhs : aig.RefStream rw
idx : Nat
hidx : idx < lw + rw
h✝ : ¬idx < lw
⊢ lw ≤ idx
Tactic:
omega
State after:
no goals