{
  "terms": {
    "name": "judge_t",
    "types": [
      {
        "type_name": "var_t",
        "constrs": [
          {
            "constr_name": "V",
            "args": [ { "arg_name": "x1", "arg_type": [ "StringT" ] } ],
            "draw": [ [ "Arg", "x1" ] ]
          }
        ]
      },
      {
        "type_name": "term_t",
        "constrs": [
          {
            "constr_name": "Var",
            "args": [ { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] } ],
            "draw": [ [ "Arg", "x1" ] ]
          },
          {
            "constr_name": "Fun",
            "args": [
              { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] },
              { "arg_name": "e2", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [
              [ "Str", "(λ" ],
              [ "Arg", "x1" ],
              [ "Str", ". " ],
              [ "Arg", "e2" ],
              [ "Str", ")" ]
            ]
          },
          {
            "constr_name": "App",
            "args": [
              { "arg_name": "e1", "arg_type": [ "RecT", "term_t" ] },
              { "arg_name": "e2", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [
              [ "Str", "(" ],
              [ "Arg", "e1" ],
              [ "Str", " @ " ],
              [ "Arg", "e2" ],
              [ "Str", ")" ]
            ]
          },
          {
            "constr_name": "Shift",
            "args": [
              { "arg_name": "k", "arg_type": [ "RecT", "var_t" ] },
              { "arg_name": "e", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [
              [ "Str", "(S" ],
              [ "Arg", "k" ],
              [ "Str", ". " ],
              [ "Arg", "e" ],
              [ "Str", ")" ]
            ]
          },
          {
            "constr_name": "Reset",
            "args": [ { "arg_name": "e", "arg_type": [ "RecT", "term_t" ] } ],
            "draw": [ [ "Str", "<" ], [ "Arg", "e" ], [ "Str", ">" ] ]
          }
        ]
      },
      {
        "type_name": "tvar_t",
        "constrs": [
          {
            "constr_name": "Tv",
            "args": [ { "arg_name": "t1", "arg_type": [ "StringT" ] } ],
            "draw": [ [ "Arg", "t1" ] ]
          }
        ]
      },
      {
        "type_name": "type_t",
        "constrs": [
          { "constr_name": "Int", "args": [], "draw": [ [ "Str", "int" ] ] },
          {
            "constr_name": "Tvar",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "tvar_t" ] }
            ],
            "draw": [ [ "Arg", "t1" ] ]
          },
          {
            "constr_name": "Arrow",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t3", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t4", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Str", "(" ],
              [ "Arg", "t1" ],
              [ "Str", " → " ],
              [ "Arg", "t2" ],
              [ "Str", " @[" ],
              [ "Arg", "t3" ],
              [ "Str", ", " ],
              [ "Arg", "t4" ],
              [ "Str", "])" ]
            ]
          }
        ]
      },
      {
        "type_name": "env_t",
        "constrs": [
          { "constr_name": "Empty", "args": [], "draw": [ [ "Str", "[]" ] ] },
          {
            "constr_name": "Cons",
            "args": [
              { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "e3", "arg_type": [ "RecT", "env_t" ] }
            ],
            "draw": [
              [ "Arg", "x1" ],
              [ "Str", " :: " ],
              [ "Arg", "t2" ],
              [ "Str", ", " ],
              [ "Arg", "e3" ]
            ]
          }
        ]
      },
      {
        "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" ] },
              { "arg_name": "type", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "alpha", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "beta", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Arg", "env" ],
              [ "Str", " |- " ],
              [ "Arg", "term" ],
              [ "Str", " : " ],
              [ "Arg", "type" ],
              [ "Str", " @[" ],
              [ "Arg", "alpha" ],
              [ "Str", ", " ],
              [ "Arg", "beta" ],
              [ "Str", "]" ]
            ]
          },
          {
            "constr_name": "Equal",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [ [ "Arg", "t1" ], [ "Str", " = " ], [ "Arg", "t2" ] ]
          }
        ]
      }
    ]
  },
  "infers": [
    {
      "name": "Tzero",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "Judge",
            [
              [
                "V",
                "env_t",
                "Cons",
                [
                  [ "M", "var_t", "x" ],
                  [ "M", "type_t", "t" ],
                  [ "M", "env_t", "Γ" ]
                ]
              ],
              [ "V", "term_t", "Var", [ [ "M", "var_t", "x" ] ] ],
              [ "M", "type_t", "t" ],
              [ "M", "type_t", "α" ],
              [ "M", "type_t", "α" ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Tsucc",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "Judge",
            [
              [
                "V",
                "env_t",
                "Cons",
                [
                  [ "M", "var_t", "x" ],
                  [ "M", "type_t", "u" ],
                  [ "M", "env_t", "Γ" ]
                ]
              ],
              [ "V", "term_t", "Var", [ [ "M", "var_t", "y" ] ] ],
              [ "M", "type_t", "t" ],
              [ "M", "type_t", "α" ],
              [ "M", "type_t", "α" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "Judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "V", "term_t", "Var", [ [ "M", "var_t", "y" ] ] ],
                [ "M", "type_t", "t" ],
                [ "M", "type_t", "α" ],
                [ "M", "type_t", "α" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Tfun",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "Judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "Fun",
                [ [ "M", "var_t", "x" ], [ "M", "term_t", "e" ] ]
              ],
              [
                "V",
                "type_t",
                "Arrow",
                [
                  [ "M", "type_t", "t2" ],
                  [ "M", "type_t", "t1" ],
                  [ "M", "type_t", "α" ],
                  [ "M", "type_t", "β" ]
                ]
              ],
              [ "M", "type_t", "γ" ],
              [ "M", "type_t", "γ" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "Judge",
              [
                [
                  "V",
                  "env_t",
                  "Cons",
                  [
                    [ "M", "var_t", "x" ],
                    [ "M", "type_t", "t2" ],
                    [ "M", "env_t", "Γ" ]
                  ]
                ],
                [ "M", "term_t", "e" ],
                [ "M", "type_t", "t1" ],
                [ "M", "type_t", "α" ],
                [ "M", "type_t", "β" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Tapp",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "Judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "App",
                [ [ "M", "term_t", "e1" ], [ "M", "term_t", "e2" ] ]
              ],
              [ "M", "type_t", "t1" ],
              [ "M", "type_t", "α" ],
              [ "M", "type_t", "δ" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "Judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "e1" ],
                [
                  "V",
                  "type_t",
                  "Arrow",
                  [
                    [ "M", "type_t", "t2" ],
                    [ "M", "type_t", "t1" ],
                    [ "M", "type_t", "α" ],
                    [ "M", "type_t", "β" ]
                  ]
                ],
                [ "M", "type_t", "γ" ],
                [ "M", "type_t", "δ" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "Judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "e2" ],
                [ "M", "type_t", "t2" ],
                [ "M", "type_t", "β" ],
                [ "M", "type_t", "γ" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Tshift",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "Judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "Shift",
                [ [ "M", "var_t", "k" ], [ "M", "term_t", "e" ] ]
              ],
              [ "M", "type_t", "t" ],
              [ "M", "type_t", "α" ],
              [ "M", "type_t", "δ" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "Judge",
              [
                [
                  "V",
                  "env_t",
                  "Cons",
                  [
                    [ "M", "var_t", "k" ],
                    [
                      "V",
                      "type_t",
                      "Arrow",
                      [
                        [ "M", "type_t", "t" ],
                        [ "M", "type_t", "α" ],
                        [ "M", "type_t", "γ" ],
                        [ "M", "type_t", "γ" ]
                      ]
                    ],
                    [ "M", "env_t", "Γ" ]
                  ]
                ],
                [ "M", "term_t", "e" ],
                [ "M", "type_t", "β" ],
                [ "M", "type_t", "β" ],
                [ "M", "type_t", "δ" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Treset",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "Judge",
            [
              [ "M", "env_t", "Γ" ],
              [ "V", "term_t", "Reset", [ [ "M", "term_t", "e" ] ] ],
              [ "M", "type_t", "α" ],
              [ "M", "type_t", "β" ],
              [ "M", "type_t", "β" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "Judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "e" ],
                [ "M", "type_t", "t" ],
                [ "M", "type_t", "t" ],
                [ "M", "type_t", "α" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Tequal",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "Equal",
            [ [ "M", "type_t", "t" ], [ "M", "type_t", "t" ] ]
          ]
        }
      ]
    }
  ],
   "input" :   [ "M", "type_t", "t" ]
}