internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_fc : c' = c ∨ c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
rcases c'_in_fc with c'_eq_c | c'_in_f
Proof state after:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'

case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
. rw [c'_eq_c]
  exact confirmRupHint_of_insertRat_fold_entails_hsat f hf c rupHints p pf performRupCheck_success
Proof state after:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
. simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
  exact pf c' c'_in_f
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c'
Tactic:
rw [c'_eq_c]
Proof state after:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
case inl
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_eq_c : c' = c
⊢ p ⊨ c
Tactic:
exact confirmRupHint_of_insertRat_fold_entails_hsat f hf c rupHints p pf performRupCheck_success
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
pf : p ⊨ f
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
⊢ p ⊨ c'
Tactic:
simp only [formulaHSat_def, List.all_eq_true, decide_eq_true_eq] at pf
Proof state after:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'
Theorem: LRAT.DefaultFormula.performRupCheck_of_insertRat_entails_safe_insert
Proof state before:
case inr
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
rupHints : Array Nat
p : PosFin n → Bool
performRupCheck_success :
  (Array.foldl (confirmRupHint (f.insertRatUnits c.negate).1.clauses)
            ((f.insertRatUnits c.negate).1.assignments, [], false, false) rupHints 0).2.snd.fst =
    true
c' : DefaultClause n
c'_in_f : c' ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → p ⊨ x
⊢ p ⊨ c'
Tactic:
exact pf c' c'_in_f
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.assignments_invariant
Tactic:
simp only [performRupCheck, Prod.mk.eta]
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Tactic:
let motive := confirmRupHint_fold_entails_hsat_motive f
Proof state after:
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
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
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
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Tactic:
have h_base : motive 0 (f.assignments, [], false, false) := by
  simp only [confirmRupHint_fold_entails_hsat_motive, f_assignments_invariant.1, false_implies, and_true, true_and,
    assignments_invariant_entails_limplies f f_assignments_invariant, motive]
Proof state after:
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)
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
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)
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Tactic:
have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (ih : motive idx.1 acc) :=
  confirmRupHint_preserves_motive f rupHints idx acc ih
Proof state after:
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])
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Theorem: LRAT.DefaultFormula.performRupCheck_preserves_assignments_invariant
Proof state before:
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])
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Tactic:
rcases Array.foldl_induction motive h_base h_inductive with ⟨hsize, h1, _⟩
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
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
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
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
Tactic:
apply Exists.intro hsize
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),
    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)
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
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)
Tactic:
simp only at h
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 (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[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)
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
h :
  hasAssignment b (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[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)
Tactic:
specialize h1 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
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 (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints 0).fst[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 }
h1 : p ⊨ (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst
⊢ p ⊨ (i, b)