Documentation

Pdl.Syntax

Syntax (Section 2.1) #

inductive Formula :
Instances For
    def instDecidableEqProgram.decEq_1 (x✝ x✝¹ : Formula) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      def instDecidableEqFormula.decEq_2 (x✝ x✝¹ : Program) :
      Decidable (x✝ = x✝¹)
      Equations
      Instances For
        def instDecidableEqFormula.decEq_1 (x✝ x✝¹ : Formula) :
        Decidable (x✝ = x✝¹)
        Equations
        Instances For
          def instDecidableEqProgram.decEq_2 (x✝ x✝¹ : Program) :
          Decidable (x✝ = x✝¹)
          Equations
          Instances For
            inductive Program :
            Instances For

              Abbreviations and Notation #

              Equations
              Instances For

                □(αs,φ)

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

                      A basic formula is of the form ¬⊥, p, ¬p, [a]_ or ¬[a]_. Note: in the article also is basic, but not here because we want to apply OneSidedLocalRule.bot to it.

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

                            Tools for Box Formulas #

                            @[simp]
                            theorem Formula.boxes_nil {φ : Formula} :
                            @[simp]
                            theorem Formula.boxes_cons {β : Program} {δ : List Program} {φ : Formula} :
                            theorem boxes_last {δ : List Program} {α : Program} {φ : Formula} :
                            Equations
                            Instances For
                              theorem def_of_boxesOf_def {φ : Formula} {αs : List Program} {ψ : Formula} (h : boxesOf φ = (αs, ψ)) :
                              φ = ⌈⌈αs⌉⌉ψ
                              Equations
                              Instances For
                                theorem boxesOf_def_of_def_of_nonBox {φ : Formula} {αs : List Program} {ψ : Formula} (h : φ = ⌈⌈αs⌉⌉ψ) (nonBox : ¬ψ.isBox) :
                                boxesOf φ = (αs, ψ)

                                Loaded Formulas #

                                inductive AnyFormula :
                                Instances For
                                  def instDecidableEqAnyFormula.decEq_2 (x✝ x✝¹ : LoadFormula) :
                                  Decidable (x✝ = x✝¹)
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def instDecidableEqLoadFormula.decEq_2 (x✝ x✝¹ : LoadFormula) :
                                    Decidable (x✝ = x✝¹)
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      inductive LoadFormula :
                                      Instances For
                                        inductive AnyNegFormula :
                                        Instances For
                                          Equations
                                          Instances For
                                            @[simp]
                                            @[simp]
                                            theorem loadMulti_cons {β : Program} {δ : List Program} {α : Program} {φ : Formula} :
                                            loadMulti (β :: δ) α φ = βAnyFormula.loaded (loadMulti δ α φ)
                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem unload_loadMulti {δ : List Program} {α : Program} {φ : Formula} :
                                              inductive NegLoadFormula :
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  Instances For
                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        Equations
                                                        Instances For
                                                          @[simp]

                                                          Load a possibly already loaded formula χ with a sequence δ of boxes. The result is loaded iff δ≠[] or χ was loaded.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            @[simp]
                                                            theorem AnyFormula.loadBoxes_cons {α : Program} {γ : List Program} {ξ : AnyFormula} :
                                                            loadBoxes (α :: γ) ξ = loaded (αloadBoxes γ ξ)
                                                            theorem AnyFormula.loadBoxes_append {as bs : List Program} {φ : AnyFormula} :
                                                            loadBoxes (as ++ bs) φ = loadBoxes as (loadBoxes bs φ)

                                                            Spliting of loaded formulas #

                                                            Split any formula into the list of loaded boxes and the free formula.

                                                            Equations
                                                            Instances For

                                                              Split a loaded formula into the list of loaded boxes and the free formula.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem loadMulti_nonEmpty_box {δ : List Program} {α : Program} {h' : α :: δ []} {φ : Formula} (h : δ []) :
                                                                  theorem LoadFormula.split_eq_loadMulti_nonEmpty' {δ : List Program} {φ : Formula} (lf : LoadFormula) (h : δ []) (h2 : lf.split = (δ, φ)) :
                                                                  theorem loadMulti_nonEmpty_eq_loadMulti {δ : List Program} {α : Program} {h : δ ++ [α] []} {φ : Formula} :
                                                                  loadMulti_nonEmpty (δ ++ [α]) h φ = loadMulti δ α φ
                                                                  theorem LoadFormula.split_eq_loadMulti (lf : LoadFormula) {δ : List Program} {α : Program} {φ : Formula} (h : lf.split = (δ ++ [α], φ)) :
                                                                  lf = loadMulti δ α φ
                                                                  theorem loadMulti_eq_of_some {d : Program} {δ : List Program} {β : Program} {φ : Formula} (h : δ.head? = some d) :

                                                                  splitLast #

                                                                  def splitLast {α : Type u_1} :
                                                                  List αOption (List α × α)

                                                                  Helper function for YsetLoad' to get last list element.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem splitLast_nil {α : Type u_1} :
                                                                    theorem splitLast_cons_eq_some {α : Type u_1} (x : α) (xs : List α) :
                                                                    splitLast (x :: xs) = some ((x :: xs).dropLast, (x :: xs).getLast )
                                                                    @[simp]
                                                                    theorem splitLast_append_singleton {α✝ : Type u_1} {xs : List α✝} {x : α✝} :
                                                                    splitLast (xs ++ [x]) = some (xs, x)
                                                                    theorem splitLast_inj {α✝ : Type u_1} {αs βs : List α✝} (h : splitLast αs = splitLast βs) :
                                                                    αs = βs
                                                                    theorem splitLast_undo_of_some {α✝ : Type u_1} {αs : List α✝} {βs_b : List α✝ × α✝} (h : splitLast αs = some βs_b) :
                                                                    βs_b.fst ++ [βs_b.snd] = αs
                                                                    theorem loadMulti_of_splitLast_cons {α : Program} {αs βs : List Program} {β : Program} {φ : Formula} (h : splitLast (α :: αs) = some (βs, β)) :