Documentation

LeanPool.PointwiseComposition.Foundation.FirstOrder.LJ.Head

Supporting results for pointwise provable equality.

First-order $\mathbf{LJ}$ #

source
@[reducible, inline]
abbrev PointwiseComposition.FFL.FirstOrder.Theoryᵢ (L : Language) :
Type u

The Theoryᵢ construction in FFL.FirstOrder.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev PointwiseComposition.FFL.FirstOrder.LJ.Sequent (L : Language) :
    Type u

    The Sequent construction in FFL.FirstOrder.LJ.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev PointwiseComposition.FFL.FirstOrder.LJ.Head (L : Language) :
      Type u

      The Head construction in FFL.FirstOrder.LJ.

      Equations
      Instances For
        source
        def PointwiseComposition.FFL.FirstOrder.LJ.Head.shift {L : Language} (Ξ : Head L) :
        Head L

        The shift construction in FFL.FirstOrder.LJ.Head.

        Equations
        Instances For
          source
          def PointwiseComposition.FFL.FirstOrder.LJ.Head.rewrite {L : Language} (f : ℕ → SyntacticTerm L) (Ξ : Head L) :
          Head L

          The rewrite construction in FFL.FirstOrder.LJ.Head.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem PointwiseComposition.FFL.FirstOrder.LJ.Head.shift_none {L : Language} :
            shift none = none
            source
            @[simp]
            theorem PointwiseComposition.FFL.FirstOrder.LJ.Head.shift_some {L : Language} (φ : Propositionᵢ L) :
            shift (some φ) = some (Rewriting.shift φ)
            source
            @[simp]
            theorem PointwiseComposition.FFL.FirstOrder.LJ.Head.rewrite_none {L : Language} (f : ℕ → SyntacticTerm L) :
            rewrite f none = none
            source
            @[simp]
            theorem PointwiseComposition.FFL.FirstOrder.LJ.Head.rewrite_some {L : Language} (f : ℕ → SyntacticTerm L) (φ : Propositionᵢ L) :
            rewrite f (some φ) = some ((Rewriting.app (Rew.rewrite f)) φ)