Theorem: LRAT.DefaultFormula.confirmRupHint_preserves_motive
Proof state before:
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)
Tactic:
. next heq =>
  simp only [confirmRupHint_fold_entails_hsat_motive, h1, imp_self, and_self, hsize,
    incompatible_of_unsat (PosFin n) acc.1 f (encounteredBoth_entails_unsat c acc.1 heq)]
Proof state after:
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)