Documentation

Std.Tactic.BVDecide.LRAT.Internal.Entails

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

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} [Entails α σ] (f : σ) :

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} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) :

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} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) :

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} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) :

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} [Entails α σ1] [Entails α σ2] (f1 : σ1) (f2 : σ2) :

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} [Entails α σ] (f : σ) :

Liff α f f

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

Liff α f1 f2 → Liff α f2 f1

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

Liff α f1 f2 → Liff α f2 f3 → Liff α f1 f3

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

Limplies α f f

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

Limplies α f1 f2 → Limplies α f2 f3 → Limplies α f1 f3

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

Liff α f1 f2 ↔ Limplies α f1 f2 ∧ Limplies α f2 f1

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

Unsatisfiable α f1 ↔ Unsatisfiable α f2

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

Unsatisfiable α f1 → Unsatisfiable α f2

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

Unsatisfiable α f1 → Incompatible α f1 f2

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

Limplies α f1 f2 → Incompatible α f1 f2 → Unsatisfiable α f1

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

Incompatible α f1 f2 ↔ Incompatible α f2 f1