Documentation

Foundation.Modal.Formula.NNFormula

source
inductive LO.Modal.NNFormula (α : Type u) :
Type u
Instances For
    source
    instance LO.Modal.instDecidableEqNNFormula {α✝ : Type u_1} [DecidableEq α✝] :
    DecidableEq (NNFormula α✝)
    Equations
    source
    def LO.Modal.instDecidableEqNNFormula.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : NNFormula α✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      def LO.Modal.NNFormula.neg {α : Type u} :
      NNFormula α → NNFormula α
      Equations
      Instances For
        source
        def LO.Modal.NNFormula.imp {α : Type u} (φ ψ : NNFormula α) :
        NNFormula α
        Equations
        Instances For
          source
          instance LO.Modal.NNFormula.instBasicModalLogicalConnective {α : Type u} :
          BasicModalLogicalConnective (NNFormula α)
          Equations
          • One or more equations did not get rendered due to their size.
          source
          theorem LO.Modal.NNFormula.or_eq {α : Type u} {φ ψ : NNFormula α} :
          φ.or ψ = φ ⋎ ψ
          source
          theorem LO.Modal.NNFormula.and_eq {α : Type u} {φ ψ : NNFormula α} :
          φ.and ψ = φ ⋏ ψ
          source
          theorem LO.Modal.NNFormula.imp_eq {α : Type u} {φ ψ : NNFormula α} :
          φ.imp ψ = φ ➝ ψ
          source
          theorem LO.Modal.NNFormula.box_eq {α : Type u} {φ : NNFormula α} :
          φ.box = □φ
          source
          theorem LO.Modal.NNFormula.dia_eq {α : Type u} {φ : NNFormula α} :
          φ.dia = ◇φ
          source
          @[simp]
          theorem LO.Modal.NNFormula.imp_eq' {α : Type u} {φ ψ : NNFormula α} :
          φ ➝ ψ = ∼φ ⋎ ψ
          source
          @[simp]
          theorem LO.Modal.NNFormula.iff_eq {α : Type u} {φ ψ : NNFormula α} :
          φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)
          source
          theorem LO.Modal.NNFormula.falsum_eq {α : Type u} :
          falsum = ⊥
          source
          theorem LO.Modal.NNFormula.verum_eq {α : Type u} :
          verum = ⊤
          source
          @[simp]
          theorem LO.Modal.NNFormula.and_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
          φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
          source
          @[simp]
          theorem LO.Modal.NNFormula.or_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
          φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
          source
          @[simp]
          theorem LO.Modal.NNFormula.imp_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
          φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
          source
          @[simp]
          theorem LO.Modal.NNFormula.neg_inj {α : Type u} (φ ψ : Formula α) :
          ∼φ = ∼ψ ↔ φ = ψ
          source
          theorem LO.Modal.NNFormula.neg_eq {α : Type u} {φ : NNFormula α} :
          φ.neg = ∼φ
          source
          @[simp]
          theorem LO.Modal.NNFormula.neg_atom {α : Type u} (a : α) :
          ∼atom a = natom a
          source
          @[simp]
          theorem LO.Modal.NNFormula.neg_natom {α : Type u} (a : α) :
          ∼natom a = atom a
          source
          theorem LO.Modal.NNFormula.negneg {α : Type u} {φ : NNFormula α} :
          ∼∼φ = φ
          source
          instance LO.Modal.NNFormula.instModalDeMorgan {α : Type u} :
          ModalDeMorgan (NNFormula α)
          source
          instance LO.Modal.NNFormula.instNegInvolutive {α : Type u} :
          NegInvolutive (NNFormula α)
          source
          def LO.Modal.NNFormula.toStr {α : Type u} [ToString α] :
          NNFormula α → String
          Equations
          Instances For
            source
            instance LO.Modal.NNFormula.instRepr {α : Type u} [ToString α] :
            Repr (NNFormula α)
            Equations
            source
            def LO.Modal.NNFormula.toFormula {α : Type u} :
            NNFormula α → Formula α
            Equations
            Instances For
              source
              instance LO.Modal.NNFormula.instCoeFormula {α : Type u} :
              Coe (NNFormula α) (Formula α)
              Equations
              source
              @[simp]
              theorem LO.Modal.NNFormula.toFormula_atom {α : Type u} (a : α) :
              (atom a).toFormula = Formula.atom a
              source
              @[simp]
              theorem LO.Modal.NNFormula.toFormula_natom {α : Type u} (a : α) :
              (natom a).toFormula = ∼Formula.atom a
              source
              @[simp]
              theorem LO.Modal.NNFormula.toFormula_falsum {α : Type u} :
              ⊥.toFormula = ⊥
              source
              @[simp]
              theorem LO.Modal.NNFormula.toFormula_verum {α : Type u} :
              ⊤.toFormula = ⊤
              source
              def LO.Modal.NNFormula.cases' {α : Type u} {C : NNFormula α → Sort v} (hAtom : (a : α) → C (atom a)) (hNatom : (a : α) → C (natom a)) (hFalsum : C ⊥) (hVerum : C ⊤) (hOr : (φ ψ : NNFormula α) → C (φ ⋎ ψ)) (hAnd : (φ ψ : NNFormula α) → C (φ ⋏ ψ)) (hBox : (φ : NNFormula α) → C (□φ)) (hDia : (φ : NNFormula α) → C (◇φ)) (φ : NNFormula α) :
              C φ
              Equations
              Instances For
                source
                def LO.Modal.NNFormula.rec' {α : Type u} {C : NNFormula α → Sort v} (hAtom : (a : α) → C (atom a)) (hNatom : (a : α) → C (natom a)) (hFalsum : C ⊥) (hVerum : C ⊤) (hOr : (φ ψ : NNFormula α) → C φ → C ψ → C (φ ⋎ ψ)) (hAnd : (φ ψ : NNFormula α) → C φ → C ψ → C (φ ⋏ ψ)) (hBox : (φ : NNFormula α) → C φ → C (□φ)) (hDia : (φ : NNFormula α) → C φ → C (◇φ)) (φ : NNFormula α) :
                C φ
                Equations
                Instances For
                  source
                  def LO.Modal.NNFormula.toNat {α : Type u} [Encodable α] :
                  NNFormula α → ℕ
                  Equations
                  Instances For
                    source
                    @[irreducible]
                    def LO.Modal.NNFormula.ofNat {α : Type u} [Encodable α] :
                    ℕ → Option (NNFormula α)
                    Equations
                    Instances For
                      source
                      instance LO.Modal.NNFormula.instEncodable {α : Type u} [Encodable α] :
                      Encodable (NNFormula α)
                      Equations
                      source
                      def LO.Modal.NNFormula.isPrebox {α : Type u} :
                      NNFormula α → Prop
                      Equations
                      Instances For
                        source
                        theorem LO.Modal.NNFormula.exists_isPrebox {α : Type u} {φ : NNFormula α} (hφ : φ.isPrebox) :
                        ∃ (ψ : NNFormula α), φ = □ψ
                        source
                        def LO.Modal.NNFormula.isPredia {α : Type u} :
                        NNFormula α → Prop
                        Equations
                        Instances For
                          source
                          theorem LO.Modal.NNFormula.exists_isPredia {α : Type u} {φ : NNFormula α} (hφ : φ.isPredia) :
                          ∃ (ψ : NNFormula α), φ = ◇ψ
                          source
                          def LO.Modal.NNFormula.degree {α : Type u} :
                          NNFormula α → ℕ
                          Equations
                          Instances For
                            source
                            @[reducible, inline]
                            abbrev LO.Modal.NNFormula.isModalCNFPart {α : Type u} (φ : NNFormula α) :
                            Prop
                            Equations
                            Instances For
                              source
                              theorem LO.Modal.NNFormula.isModalCNFPart.def_atom {α : Type u} {a : α} :
                              (atom a).isModalCNFPart
                              source
                              theorem LO.Modal.NNFormula.isModalCNFPart.def_natom {α : Type u} {a : α} :
                              (natom a).isModalCNFPart
                              source
                              theorem LO.Modal.NNFormula.isModalCNFPart.def_verum {α : Type u} :
                              ⊤.isModalCNFPart
                              source
                              theorem LO.Modal.NNFormula.isModalCNFPart.def_falsum {α : Type u} :
                              ⊥.isModalCNFPart
                              source
                              theorem LO.Modal.NNFormula.isModalCNFPart.def_box {α : Type u} {φ : NNFormula α} :
                              (□φ).isModalCNFPart
                              source
                              theorem LO.Modal.NNFormula.isModalCNFPart.def_dia {α : Type u} {φ : NNFormula α} :
                              (◇φ).isModalCNFPart
                              source
                              def LO.Modal.NNFormula.isModalCNF {α : Type u} (φ : NNFormula α) :
                              Prop
                              Equations
                              Instances For
                                source
                                @[simp]
                                theorem LO.Modal.NNFormula.isModalCNF.def_atom {α : Type u} {a : α} :
                                (atom a).isModalCNF
                                source
                                @[simp]
                                theorem LO.Modal.NNFormula.isModalCNF.def_natom {α : Type u} {a : α} :
                                (natom a).isModalCNF
                                source
                                @[simp]
                                theorem LO.Modal.NNFormula.isModalCNF.def_falsum {α : Type u} :
                                ⊥.isModalCNF
                                source
                                @[simp]
                                theorem LO.Modal.NNFormula.isModalCNF.def_verum {α : Type u} :
                                ⊤.isModalCNF
                                source
                                @[simp]
                                theorem LO.Modal.NNFormula.isModalCNF.def_box {α : Type u} {φ : NNFormula α} :
                                (□φ).isModalCNF
                                source
                                @[simp]
                                theorem LO.Modal.NNFormula.isModalCNF.def_dia {α : Type u} {φ : NNFormula α} :
                                (◇φ).isModalCNF
                                source
                                def LO.Modal.NNFormula.isModalDNFPart {α : Type u} :
                                NNFormula α → Prop
                                Equations
                                Instances For
                                  source
                                  theorem LO.Modal.NNFormula.isModalDNFPart.of_degree_zero {α : Type u} {φ : NNFormula α} (h : φ.degree = 0) :
                                  φ.isModalDNFPart
                                  source
                                  def LO.Modal.NNFormula.isModalDNF {α : Type u} :
                                  NNFormula α → Prop
                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem LO.Modal.NNFormula.isModalDNF.def_atom {α : Type u} {a : α} :
                                    (atom a).isModalDNF
                                    source
                                    @[simp]
                                    theorem LO.Modal.NNFormula.isModalDNF.def_natom {α : Type u} {a : α} :
                                    (natom a).isModalDNF
                                    source
                                    @[simp]
                                    theorem LO.Modal.NNFormula.isModalDNF.def_falsum {α : Type u} :
                                    ⊥.isModalDNF
                                    source
                                    @[simp]
                                    theorem LO.Modal.NNFormula.isModalDNF.def_verum {α : Type u} :
                                    ⊤.isModalDNF
                                    source
                                    @[simp]
                                    theorem LO.Modal.NNFormula.isModalDNF.def_box {α : Type u} {φ : NNFormula α} :
                                    (□φ).isModalDNF
                                    source
                                    @[simp]
                                    theorem LO.Modal.NNFormula.isModalDNF.def_dia {α : Type u} {φ : NNFormula α} :
                                    (◇φ).isModalDNF
                                    source
                                    def LO.Modal.Formula.toNNFormula {α : Type u} :
                                    Formula α → NNFormula α
                                    Equations
                                    Instances For
                                      source
                                      instance LO.Modal.Formula.instCoeNNFormula {α : Type u} :
                                      Coe (Formula α) (NNFormula α)
                                      Equations
                                      source
                                      @[simp]
                                      theorem LO.Modal.Formula.toNNFormula_atom {α : Type u} (a : α) :
                                      (atom a).toNNFormula = NNFormula.atom a
                                      source
                                      @[simp]
                                      theorem LO.Modal.Formula.toNNFormula_falsum {α : Type u} :
                                      ⊥.toNNFormula = ⊥