Documentation

Bml.CompletenessViaPaths

Equations
Instances For
    Equations
    Instances For
      Equations
      Equations
      Instances For
        inductive Path :

        A Path ctn is a maximal path of consistent TNodes starting with ctn and connected by LocalRuleApps. This does not have to be a path in any particular LocalTableau.

        Instances For
          @[irreducible]
          def pathToFinset {L R : Finset Formula} {cons : Consistent (L, R)} :
          Path (L, R), consFinset Formula
          Equations
          Instances For
            @[simp]
            theorem LR_in_PathLR {L R : Finset Formula} {LR_cons : Consistent (L, R)} (path : Path (L, R), LR_cons) :
            @[irreducible]
            def endNodeOf {LR : TNode} {LR_cons : Consistent LR} :
            Path LR, LR_consConsTNode
            Equations
            Instances For
              theorem endNodeIsSimple {consLR consLR' : ConsTNode} (path : Path consLR) (eq : consLR' = endNodeOf path) :
              Simple consLR'
              theorem consistentThenConsistentChild {L R : Finset Formula} {C : List TNode} (lrApp : LocalRuleApp (L, R) C) :
              Consistent (L, R)cC, Consistent c
              theorem consThenProjectLCons {L : Finset Formula} {α : Formula} {R : Finset Formula} (α_in : ~(α) L) (LR_simple : Simple (L, R)) :
              theorem consThenProjectRCons {R : Finset Formula} {α : Formula} {L : Finset Formula} (α_in : ~(α) R) (LR_simple : Simple (L, R)) :
              theorem pathSaturated {consLR : ConsTNode} (path : Path consLR) :
              def botTableauL {LR : TNode} (bot_in : LR.1) :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def botTableauR {LR : TNode} (bot_in : LR.2) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def notTableauLL {LR : TNode} {pp : Char} (pp_in : (·pp) LR.1) (npp_in : (~·pp) LR.1) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def notTableauLR {LR : TNode} {pp : Char} (pp_in : (·pp) LR.1) (npp_in : (~·pp) LR.2) :
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      def notTableauRL {LR : TNode} {pp : Char} (pp_in : (·pp) LR.2) (npp_in : (~·pp) LR.1) :
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def notTableauRR {LR : TNode} {pp : Char} (pp_in : (·pp) LR.2) (npp_in : (~·pp) LR.2) :
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem pathConsistent {TN : ConsTNode} (path : Path TN) :
                          pathToFinset path ∀ (pp : Char), (·pp) pathToFinset path(~·pp)pathToFinset path
                          theorem pathProjection {consLR : ConsTNode} (path : Path consLR) :
                          theorem pathDiamond {consLR : ConsTNode} {α : Formula} (path : Path consLR) (α_in : ~(α) pathToFinset path) :
                          @[irreducible]
                          noncomputable def aPathOf (conLR : ConsTNode) :
                          Path conLR
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            noncomputable def toWorld (consLR : ConsTNode) :
                            Equations
                            Instances For
                              inductive M₀ (T0 : ConsTNode) :
                              Instances For
                                theorem modelExistence {L R : Finset Formula} :
                                Consistent (L, R)∃ (WS : Set (Finset Formula)) (x : ModelGraph WS) (W : WS), L R W