Theorem: LRAT.DefaultFormula.mem_of_insertRupUnits
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.ratUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.data → l ∈ f.rupUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.rupUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
hl : l ∈ acc.fst.data ∨ l = unit
⊢ l ∈ f.rupUnits.data ∨ l ∈ units
Tactic:
rcases hl with l_in_acc | l_eq_unit
Proof state after:
case isFalse.inl
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.ratUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.data → l ∈ f.rupUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.rupUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_in_acc : l ∈ acc.fst.data
⊢ l ∈ f.rupUnits.data ∨ l ∈ units

case isFalse.inr
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
h :
  some c ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ (List.foldl insertUnit (f.rupUnits, f.assignments, false) units).fst.data ∧
            LRAT.DefaultClause.unit (a, true) = c) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ LRAT.DefaultClause.unit (a, false) = c ∨
          (a, true) ∈ f.ratUnits.data ∧ LRAT.DefaultClause.unit (a, true) = c
hb : ∀ (l : Literal (PosFin n)), l ∈ (f.rupUnits, f.assignments, false).fst.data → l ∈ f.rupUnits.data ∨ l ∈ units
acc : Array (Literal (PosFin n)) × Array Assignment × Bool
ih : ∀ (l : Literal (PosFin n)), l ∈ acc.fst.data → l ∈ f.rupUnits.data ∨ l ∈ units
unit : Literal (PosFin n)
unit_in_units : unit ∈ units
l : Literal (PosFin n)
h✝ : ¬hasAssignment unit.snd acc.2.fst[unit.fst.val]! = true
l_eq_unit : l = unit
⊢ l ∈ f.rupUnits.data ∨ l ∈ units