soundness

(in-package "LRAT")

(include-book "lrat-checker")

(local (include-book "../list-based/soundness"))

(local (include-book "equiv"))

(defthm refutation-p-equiv
  (implies (and (formula-p formula)
      (refutation-p$ proof formula))
    (refutation-p proof formula)))

(defthm main-theorem-stobj-based
  (implies (and (formula-p formula)
      (refutation-p$ proof formula))
    (not (satisfiable formula)))
  :hints (("Goal" :in-theory '(refutation-p-equiv)
     :use main-theorem-list-based)))