Documentation

Pdl.Syntax

Syntax (Section 2.1) #

inductive Formula :
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_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.
                            @[simp]
                            theorem Formula.boxes_nil {φ : Formula} :
                            @[simp]
                            theorem Formula.boxes_cons {β : Program} {δ : List Program} {φ : Formula} :
                            theorem boxes_last {δ : List Program} {α : Program} {φ : Formula} :

                            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, β)) :