{
  "terms": {
    "name": "Judge_t",
    "types": [
      {
        "type_name": "Var_t",
        "constrs": [
          {
            "constr_name": "V",
            "args": [ { "arg_name": "v", "arg_type": [ "StringT" ] } ],
            "draw": [ [ "Arg", "v" ] ]
          }
        ]
      },
      {
        "type_name": "Term_t",
        "constrs": [
          {
            "constr_name": "Var",
            "args": [ { "arg_name": "v", "arg_type": [ "RecT", "Var_t" ] } ],
            "draw": [ [ "Arg", "v" ] ]
          },
          {
            "constr_name": "Arrow",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "Term_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "Term_t" ] }
            ],
            "draw": [
              [ "Str", " ( " ],
              [ "Arg", "t1" ],
              [ "Str", " -> " ],
              [ "Arg", "t2" ],
              [ "Str", " ) " ]
            ]
          },
          {
            "constr_name": "And",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "Term_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "Term_t" ] }
            ],
            "draw": [
              [ "Str", " ( " ],
              [ "Arg", "t1" ],
              [ "Str", " ^ " ],
              [ "Arg", "t2" ],
              [ "Str", " ) " ]
            ]
          },
          {
            "constr_name": "Or",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "Term_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "Term_t" ] }
            ],
            "draw": [
              [ "Str", " ( " ],
              [ "Arg", "t1" ],
              [ "Str", " ∨ " ],
              [ "Arg", "t2" ],
              [ "Str", " ) " ]
            ]
          }
        ]
      },
      {
        "type_name": "Env_t",
        "constrs": [
          {
            "constr_name": "Cons",
            "args": [
              { "arg_name": "term", "arg_type": [ "RecT", "Term_t" ] },
              { "arg_name": "env", "arg_type": [ "RecT", "Env_t" ] }
            ],
            "draw": [ [ "Arg", "term" ], [ "Str", " , " ], [ "Arg", "env" ] ]
          },
          {
            "constr_name": "Empty",
            "args": [],
            "draw": [ [ "Str", " []" ] ]
          }
        ]
      },
      {
        "type_name": "Judge_t",
        "constrs": [
          {
            "constr_name": "Judge",
            "args": [
              { "arg_name": "env", "arg_type": [ "RecT", "Env_t" ] },
              { "arg_name": "term", "arg_type": [ "RecT", "Term_t" ] }
            ],
            "draw": [
              [ "Arg", "env" ],
              [ "Str", " => " ],
              [ "Arg", "term" ]
            ]
          }
        ]
      }
    ]
  },
  "infers": [
    {
      "name": "->Intro",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [
              [ "M", "Env_t", "Γ " ],
              [
                "V",
                "Term_t",
                "Arrow",
                [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
              ]
            ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [
                  "V",
                  "Env_t",
                  "Cons",
                  [ [ "M", "Term_t", "φ" ], [ "M", "Env_t", "Γ " ] ]
                ],
                [ "M", "Term_t", "ψ" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "->Elim",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "ψ" ] ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "φ" ] ]
            ],
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [ "M", "Env_t", "Γ" ],
                [
                  "V",
                  "Term_t",
                  "Arrow",
                  [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "^Intro",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [
              [ "M", "Env_t", "Γ" ],
              [
                "V",
                "Term_t",
                "And",
                [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
              ]
            ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "φ" ] ]
            ],
            [
              "V",
              "Judge_t",
              "Judge",
              [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "ψ" ] ]
            ]
          ]
        }
      ]
    },
    {
      "name": "^ElimL",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "φ" ] ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [ "M", "Env_t", "Γ" ],
                [
                  "V",
                  "Term_t",
                  "And",
                  [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "^ElimR",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "ψ" ] ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [ "M", "Env_t", "Γ" ],
                [
                  "V",
                  "Term_t",
                  "And",
                  [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "∨IntroL",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [
              [ "M", "Env_t", "Γ" ],
              [
                "V",
                "Term_t",
                "Or",
                [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
              ]
            ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "φ" ] ]
            ]
          ]
        }
      ]
    },
    {
      "name": "∨IntroR",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [
              [ "M", "Env_t", "Γ" ],
              [
                "V",
                "Term_t",
                "Or",
                [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
              ]
            ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "ψ" ] ]
            ]
          ]
        }
      ]
    },
    {
      "name": "∨Elim",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "χ" ] ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [ "M", "Env_t", "Γ" ],
                [
                  "V",
                  "Term_t",
                  "Or",
                  [ [ "M", "Term_t", "φ" ], [ "M", "Term_t", "ψ" ] ]
                ]
              ]
            ],
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [
                  "V",
                  "Env_t",
                  "Cons",
                  [ [ "M", "Term_t", "φ" ], [ "M", "Env_t", "Γ" ] ]
                ],
                [ "M", "Term_t", "χ" ]
              ]
            ],
            [
              "V",
              "Judge_t",
              "Judge",
              [
                [
                  "V",
                  "Env_t",
                  "Cons",
                  [ [ "M", "Term_t", "ψ" ], [ "M", "Env_t", "Γ" ] ]
                ],
                [ "M", "Term_t", "χ" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "tvarsuc",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "Judge_t",
            "Judge",
            [
              [
                "V",
                "Env_t",
                "Cons",
                [ [ "M", "Term_t", "φ" ], [ "M", "Env_t", "Γ" ] ]
              ],
              [ "M", "Term_t", "ψ" ]
            ]
          ],
          "premises": [
            [
              "V",
              "Judge_t",
              "Judge",
              [ [ "M", "Env_t", "Γ" ], [ "M", "Term_t", "ψ" ] ]
            ]
          ]
        }
      ]
    },
    {
      "name": "tvarzero",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Judge_t",
            "Judge",
            [
              [
                "V",
                "Env_t",
                "Cons",
                [ [ "M", "Term_t", "φ" ], [ "M", "Env_t", "Γ" ] ]
              ],
              [ "M", "Term_t", "φ" ]
            ]
          ]
        }
      ]
    }
  ],
  "input": [
    "V",
    "Judge_t",
    "Judge",
    [
      [ "M", "Env_t", "Γ" ],
      [
        "V",
        "Term_t",
        "Arrow",
        [
          [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Var",
                [ [ "V", "Var_t", "V", [ [ "V", "String", "φ", [] ] ] ] ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Var",
                    [
                      [ "V", "Var_t", "V", [ [ "V", "String", "ψ", [] ] ] ]
                    ]
                  ],
                  [
                    "V",
                    "Term_t",
                    "Var",
                    [
                      [ "V", "Var_t", "V", [ [ "V", "String", "χ", [] ] ] ]
                    ]
                  ]
                ]
              ]
            ]
          ],
          [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Var",
                    [
                      [ "V", "Var_t", "V", [ [ "V", "String", "φ", [] ] ] ]
                    ]
                  ],
                  [
                    "V",
                    "Term_t",
                    "Var",
                    [
                      [ "V", "Var_t", "V", [ [ "V", "String", "ψ", [] ] ] ]
                    ]
                  ]
                ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Var",
                    [
                      [ "V", "Var_t", "V", [ [ "V", "String", "φ", [] ] ] ]
                    ]
                  ],
                  [
                    "V",
                    "Term_t",
                    "Var",
                    [
                      [ "V", "Var_t", "V", [ [ "V", "String", "χ", [] ] ] ]
                    ]
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
}