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.

Instances

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

    Equations
      Instances For

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

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

            f is not true under any assignment.

            Equations
              Instances For
                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
                  Instances For
                    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
                      Instances For
                        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
                          Instances For
                            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
                              Instances For
                                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 f2Liff α 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 f2Liff α f2 f3Liff α 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 f2Limplies α f2 f3Limplies α 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) :
                                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) :
                                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 α f1Incompatible α 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 f2Incompatible α f1 f2Unsatisfiable α 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