theorem Std.Tactic.BVDecide.LRAT.Internal.addEmptyCaseSound {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : Formula.ReadyForRupAdd f) (rupHints : Array Nat) (rupAddSuccess : (Formula.performRupAdd f Clause.empty rupHints).snd = true) : Unsatisfiable α f

theorem Std.Tactic.BVDecide.LRAT.Internal.addRupCaseSound {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : Formula.ReadyForRupAdd f) (f_readyForRatAdd : Formula.ReadyForRatAdd f) (c : β) (f' : σ) (rupHints : Array Nat) (heq : Formula.performRupAdd f c rupHints = (f', true)) (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) (ih : ∀ (f : σ), Formula.ReadyForRupAdd f → Formula.ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = Result.success → Unsatisfiable α f) (f'_success : lratChecker f' restPrf = Result.success) : Unsatisfiable α f

theorem Std.Tactic.BVDecide.LRAT.Internal.addRatCaseSound {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : Formula.ReadyForRupAdd f) (f_readyForRatAdd : Formula.ReadyForRatAdd f) (c : β) (pivot : Sat.Literal α) (f' : σ) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (pivot_limplies_c : Limplies α pivot c) (heq : Formula.performRatAdd f c pivot rupHints ratHints = (f', true)) (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) (ih : ∀ (f : σ), Formula.ReadyForRupAdd f → Formula.ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = Result.success → Unsatisfiable α f) (f'_success : lratChecker f' restPrf = Result.success) : Unsatisfiable α f

theorem Std.Tactic.BVDecide.LRAT.Internal.delCaseSound {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : Formula.ReadyForRupAdd f) (f_readyForRatAdd : Formula.ReadyForRatAdd f) (ids : Array Nat) (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) (ih : ∀ (f : σ), Formula.ReadyForRupAdd f → Formula.ReadyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → WellFormedAction a) → lratChecker f restPrf = Result.success → Unsatisfiable α f) (h : lratChecker (Formula.delete f ids) restPrf = Result.success) : Unsatisfiable α f

theorem Std.Tactic.BVDecide.LRAT.Internal.lratCheckerSound {α : Type u_1} {β : Type u_2} {σ : Type u_3} [DecidableEq α] [Clause α β] [Entails α σ] [Formula α β σ] (f : σ) (f_readyForRupAdd : Formula.ReadyForRupAdd f) (f_readyForRatAdd : Formula.ReadyForRatAdd f) (prf : List (Action β α)) (prfWellFormed : ∀ (a : Action β α), a ∈ prf → WellFormedAction a) : lratChecker f prf = Result.success → Unsatisfiable α f