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