logic: justification
system: tableau
name: J₀
description: |
    This system stays mostly faithful to the one described in Ghari 2016. The 
    CSr rule was not present in the original; it emulates closure upon
    encountering [F] φ on the branch for some φ ∊ CS.
rules:
    - name: "Te"
      consume: ["[T] T:A"]
      produce:
            - ["[T, e] T:A"]

    - name: "Fe"
      consume: ["[F] T:A"]
      produce:
          - ["[F, e] T:A"]

    - name: "F→"
      consume: ["[F] A → B"]
      produce: 
          - ["[T] A", "[F] B"]

    - name: "T→"
      consume: ["[T] A -> B"]
      produce:
          - ["[F] A"]
          - ["[T] B"]

    - name: "F+"
      consume: ["[F, e] T+S:A"]
      produce:
          - ["[F, e] T:A", "[F, e] S:A"]

    - name: "T·"
      consume: ["[T, e] S:(A → B)", "[T, e] T:A"]
      produce:
          - ["[T, e] (S * T) : B"]
      restrict:
          and:
              - match: "A → B"
                with: [subterms, formulas]
                in:
                    union: [root, assumptions]
              - match: "S * T"
                with: subterms
                in: root
    - name: "CSr"
      consume: []
      produce:
          - ["[T] A"]
      generate:
          match: "A"
          with: all
          in: assumptions
    - name: "PBe"
      consume: []
      produce:
          - ["[T, e] T:A"]
          - ["[F, e] T:A"]
      generate:
          and:
              - match: "A"
                with: [subterms, formulas]
                in: 
                    union: [root, assumptions]
              - match: "T"
                with: [subterms, justifications]
                in: root

    - name: "PBf"
      consume: []
      produce:
          - ["[T] A"]
          - ["[F] A"]
      generate:
          match: "A"
          with: [subterms, formulas]
          in: 
              union: [root, assumptions]