class Std.Tactic.BVDecide.LRAT.Internal.Entails (α : Type u) (β : Type v) : Type (max u v)

For variables of type α and formulas of type β, Entails.eval a f is meant to determine whether a formula f is true under assignment a.

• eval : (α → Bool) → β → Prop

Instances

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.instEntailsPosFinArray
• Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntails
• Std.Tactic.BVDecide.LRAT.Internal.Clause.instEntailsLiteral
• Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.instEntailsPosFin

def Std.Tactic.BVDecide.LRAT.Internal.«term_⊨_» : Lean.TrailingParserDescr

a ⊨ f reads formula f is true under assignment a.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.«term_⊭_» : Lean.TrailingParserDescr

a ⊭ f reads formula f is false under assignment a.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (α : Type u) {σ : Type v} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] (f : σ) : Prop

f is not true under any assignment.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f = ∀ (a : α → Bool), ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f

def Std.Tactic.BVDecide.LRAT.Internal.Liff (α : Type u) {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Prop

f1 and f2 are logically equivalent

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 = ∀ (a : α → Bool), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f1 ↔ Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f2

def Std.Tactic.BVDecide.LRAT.Internal.Limplies (α : Type u) {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Prop

f1 logically implies f2

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 = ∀ (a : α → Bool), Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f1 → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f2

def Std.Tactic.BVDecide.LRAT.Internal.Equisat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Prop

f1 is unsat iff f2 is unsat

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Equisat α f1 f2 = (Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 ↔ Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f2)

def Std.Tactic.BVDecide.LRAT.Internal.Incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Prop

For any given assignment f1 or f2 is not true.

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2 = ∀ (a : α → Bool), ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f1 ∨ ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a f2

theorem Std.Tactic.BVDecide.LRAT.Internal.Liff.refl {α : Type u} {σ : Type v} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] (f : σ) : Std.Tactic.BVDecide.LRAT.Internal.Liff α f f

theorem Std.Tactic.BVDecide.LRAT.Internal.Liff.symm {α : Type u} {σ1 : Type v} {σ2 : Type 2} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Liff α f2 f1

theorem Std.Tactic.BVDecide.LRAT.Internal.Liff.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Liff α f2 f3 → Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f3

theorem Std.Tactic.BVDecide.LRAT.Internal.Limplies.refl {α : Type u} {σ : Type v} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] (f : σ) : Std.Tactic.BVDecide.LRAT.Internal.Limplies α f f

theorem Std.Tactic.BVDecide.LRAT.Internal.Limplies.trans {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ3] (f1 : σ1) (f2 : σ2) (f3 : σ3) : Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Limplies α f2 f3 → Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f3

theorem Std.Tactic.BVDecide.LRAT.Internal.liff_iff_limplies_and_limplies {α : Type u} {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 ↔ Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 ∧ Std.Tactic.BVDecide.LRAT.Internal.Limplies α f2 f1

theorem Std.Tactic.BVDecide.LRAT.Internal.liff_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) (h : Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2) : Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 ↔ Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f2

theorem Std.Tactic.BVDecide.LRAT.Internal.limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) (h : Std.Tactic.BVDecide.LRAT.Internal.Limplies α f2 f1) : Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 → Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f2

theorem Std.Tactic.BVDecide.LRAT.Internal.incompatible_of_unsat (α : Type u) {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1 → Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2

theorem Std.Tactic.BVDecide.LRAT.Internal.unsat_of_limplies_and_incompatible (α : Type u) {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2 → Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f1

theorem Std.Tactic.BVDecide.LRAT.Internal.Incompatible.symm {α : Type u} {σ1 : Type v} {σ2 : Type w} [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1] [Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] (f1 : σ1) (f2 : σ2) : Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f1 f2 ↔ Std.Tactic.BVDecide.LRAT.Internal.Incompatible α f2 f1