Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (match c.reduce acc.fst with
    | encounteredBoth => (acc.fst, acc.2.fst, true, false)
    | reducedToEmpty => (acc.fst, acc.2.fst, true, false)
    | reducedToUnit (l, b) =>
      if hasAssignment b acc.fst[l.val]! = true then (acc.fst, acc.2.fst, false, false)
      else (acc.fst.modify l.val (addAssignment b), (l, b) :: acc.2.fst, false, false)
    | reducedToNonunit => (acc.fst, acc.2.fst, false, true))
Tactic:
split
Proof state after:
case h_1
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = encounteredBoth
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_2
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToEmpty
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, true, false)

case h_3
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
l✝ : PosFin n
b✝ : Bool
heq✝ : c.reduce acc.fst = reducedToUnit (l✝, b✝)
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1)
    (if hasAssignment b✝ acc.fst[l✝.val]! = true then (acc.fst, acc.2.fst, false, false)
    else (acc.fst.modify l✝.val (addAssignment b✝), (l✝, b✝) :: acc.2.fst, false, false))

case h_4
n : Nat
f : DefaultFormula n
rupHints : Array Nat
idx : Fin rupHints.size
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
h1 : limplies (PosFin n) f acc.fst
h2 : acc.snd.snd.fst = true → incompatible (PosFin n) acc.fst f
acc2_eq_false : acc.2.2.snd = false ∧ acc.2.2.fst = false
x✝¹ : Option (Option (DefaultClause n))
c : DefaultClause n
hc : f.clauses[rupHints[↑idx]]? = some (some c)
c_in_f : c ∈ f.toList
x✝ : ReduceResult (PosFin n)
heq✝ : c.reduce acc.fst = reducedToNonunit
⊢ f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (acc.fst, acc.2.fst, false, true)