Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
case intro.intro
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h1 :
  limplies (PosFin n) f
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b
          { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                assignments :=
                  (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
                      0).fst }.assignments[i.val] =
        true →
      limplies (PosFin n)
        { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
          assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
        (i, b)
Tactic:
intro i b h p pf
Proof state after:
case intro.intro
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
hsize : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h1 :
  limplies (PosFin n) f
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst
right✝ :
  (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.snd.fst = true →
    incompatible (PosFin n)
      (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst f
i : PosFin n
b : Bool
h :
  hasAssignment b
      { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments :=
              (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
                  0).fst }.assignments[i.val] =
    true
p : PosFin n → Bool
pf :
  p ⊨
    { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst }
⊢ p ⊨ (i, b)