exact assignments_invariant_entails_limplies fc.1 fc_satisfies_assignments_invariant
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
fc : DefaultFormula n × Bool := f.insertRatUnits c.negate
confirmRupHint_fold_res : Array Assignment × List (Literal (PosFin n)) × Bool × Bool :=
  Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints 0
confirmRupHint_success : confirmRupHint_fold_res.snd.snd.fst = true
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fc.fst.confirmRupHint_fold_entails_hsat_motive
fc_satisfies_assignments_invariant : fc.fst.assignments_invariant
⊢ limplies (PosFin n) (f.insertRatUnits c.negate).fst (f.insertRatUnits c.negate).fst.assignments
no goals