Documentation

Bml.Partitions

source
def Partition :
Type
Equations
Instances For
    source
    def isPartInterpolant (LR : TNode) (θ : Formula) :
    Prop
    Equations
    Instances For
      source
      def PartInterpolant (LR : TNode) :
      Type
      Equations
      Instances For
        source
        theorem choice_property_in_image {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Prop} (p_in_image : ∃ y ∈ List.map f l, p y) :
        ∃ x ∈ l, p (f x)
        source
        def InterpolantInductionStep {C : List TNode} (L R : Finset Formula) (ruleA : LocalRuleApp (L, R) C) (subθs : (c : TNode) → c ∈ C → PartInterpolant c) :
        PartInterpolant (L, R)
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem projection_reflects_unsat_L_L {θ : Formula} {LR : TNode} {φ : Formula} (nBoxφ_in_L : ~(□φ) ∈ LR.1) (notSatNotTheta : ¬HasSat.Satisfiable ((diamondProjectTNode (Sum.inl φ) LR).1 ∪ {~θ})) :
          ¬HasSat.Satisfiable (LR.1 ∪ {□~θ})
          source
          theorem projection_reflects_unsat_L_R {θ : Formula} {LR : TNode} {φ : Formula} (nBoxφ_in_L : ~(□φ) ∈ LR.1) (notSatNotTheta : ¬HasSat.Satisfiable ((diamondProjectTNode (Sum.inl φ) LR).2 ∪ {θ})) :
          ¬HasSat.Satisfiable (LR.2 ∪ {~(□~θ)})
          source
          theorem projection_reflects_unsat_R_L {θ : Formula} {LR : TNode} {φ : Formula} (nBoxφ_in_R : ~(□φ) ∈ LR.2) (notSatNotTheta : ¬HasSat.Satisfiable ((diamondProjectTNode (Sum.inr φ) LR).1 ∪ {~θ})) :
          ¬HasSat.Satisfiable (LR.1 ∪ {~(□θ)})
          source
          theorem projection_reflects_unsat_R_R {θ : Formula} {LR : TNode} {φ : Formula} (nBoxφ_in_R : ~(□φ) ∈ LR.2) (notSatNotTheta : ¬HasSat.Satisfiable ((diamondProjectTNode (Sum.inr φ) LR).2 ∪ {θ})) :
          ¬HasSat.Satisfiable (LR.2 ∪ {□θ})
          source
          def LocalTableau.length {LR : TNode} :
          LocalTableau LR → ℕ
          Equations
          Instances For
            source
            def ClosedTableau.length {LR : TNode} :
            ClosedTableau LR → ℕ
            Equations
            Instances For
              source
              theorem endNodeOfChildIsEndNode {C : List TNode} {x : TNode} {h : x ∈ C} {E LR : TNode} (lrApp : LocalRuleApp LR C) (subTabs : (c : TNode) → c ∈ C → LocalTableau c) (E_in : E ∈ endNodesOf ⟨x, subTabs x h⟩) :
              E ∈ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩
              source
              def childNext {C : List TNode} {LR : TNode} {lrApp : LocalRuleApp LR C} (subTabs : (c : TNode) → c ∈ C → LocalTableau c) (next : (Y : TNode) → Y ∈ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩ → ClosedTableau Y) (cLR : TNode) (c_in_C : cLR ∈ C) (Y : TNode) :
              Y ∈ endNodesOf ⟨cLR, subTabs cLR c_in_C⟩ → ClosedTableau Y
              Equations
              • childNext subTabs next cLR c_in_C Y Y_in = next Y ⋯
              Instances For
                source
                theorem childNext_eq {C : List TNode} {LR : TNode} {lrApp : LocalRuleApp LR C} (subTabs : (c : TNode) → c ∈ C → LocalTableau c) (next : (Y : TNode) → Y ∈ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩ → ClosedTableau Y) (cLR : TNode) (c_in_C : cLR ∈ C) (Y : TNode) (Y_in : Y ∈ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩) (Y_in_child : Y ∈ endNodesOf ⟨cLR, subTabs cLR c_in_C⟩) :
                childNext subTabs next cLR c_in_C Y Y_in_child = next Y Y_in
                source
                theorem elem_lt_map_sum {α : Type u_1} {x : α} {l : List α} (h : x ∈ l) (f : α → ℕ) :
                f x ≤ (List.map f l).sum
                source
                theorem endNodesOfChildAreEndNodes {C : List TNode} {cLR LR : TNode} (subTabs : (c : TNode) → c ∈ C → LocalTableau c) (c_in_C : cLR ∈ C) (lrApp : LocalRuleApp LR C) :
                endNodesOf ⟨cLR, subTabs cLR c_in_C⟩ ⊆ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩
                source
                theorem endNodesOfChildSublistEndNodes {C : List TNode} {cLR LR : TNode} (subTabs : (c : TNode) → c ∈ C → LocalTableau c) (c_in_C : cLR ∈ C) (lrApp : LocalRuleApp LR C) :
                (endNodesOf ⟨cLR, subTabs cLR c_in_C⟩).Sublist (endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩)
                source
                theorem Sublist.pmap {α : Type u_1} {β : Type u_2} {p p2 : α → Prop} {f : (a : α) → p a → β} {g : (a : α) → p2 a → β} {xs ys : List α} {H : ∀ a ∈ xs, p a} {H2 : ∀ a ∈ ys, p2 a} (h : xs.Sublist ys) (agree : ∀ (x : α) (h1 : p x) (h2 : p2 x), f x h1 = g x h2) :
                (List.pmap f xs H).Sublist (List.pmap g ys H2)
                source
                theorem map_sum_le_map_sum {α : Type u_1} (xs ys : List α) (h : xs.Sublist ys) (f : { x : α // x ∈ xs } → ℕ) (g : { x : α // x ∈ ys } → ℕ) (agree : ∀ x ∈ xs.attach, ∀ (x_in_ys : ↑x ∈ ys), f x = g ⟨↑x, x_in_ys⟩) :
                (List.map f xs.attach).sum ≤ (List.map g ys.attach).sum
                source
                theorem childNext_lt {C : List TNode} {LR : TNode} {lrApp : LocalRuleApp LR C} (subTabs : (c : TNode) → c ∈ C → LocalTableau c) (next : (Y : TNode) → Y ∈ endNodesOf ⟨LR, LocalTableau.fromRule lrApp subTabs⟩ → ClosedTableau Y) (cLR : TNode) (c_in_C : cLR ∈ C) :
                (ClosedTableau.loc (subTabs cLR c_in_C) (childNext subTabs next cLR c_in_C)).length < (ClosedTableau.loc (LocalTableau.fromRule lrApp subTabs) next).length
                source
                theorem simple_lt {LR cLR : TNode} (isSimple : Simple LR) (next : (Y : TNode) → Y ∈ endNodesOf ⟨LR, LocalTableau.fromSimple isSimple⟩ → ClosedTableau Y) (h : cLR ∈ endNodesOf ⟨LR, LocalTableau.fromSimple isSimple⟩) :
                (next cLR h).length < (ClosedTableau.loc (LocalTableau.fromSimple isSimple) next).length
                source
                @[irreducible]
                def tabToInt {LR : TNode} (tab : ClosedTableau LR) :
                PartInterpolant LR
                Equations
                Instances For