{
  "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": "num_t",
        "constrs": [
          {
            "constr_name": "n",
            "args": [ { "arg_name": "n1", "arg_type": [ "IntT" ] } ],
            "draw": [ [ "Arg", "n1" ] ]
          }
        ]
      },
      {
        "type_name": "bol_t",
        "constrs": [
          {
            "constr_name": "true",
            "args": [],
            "draw": [ [ "Str", "true" ] ]
          },
          {
            "constr_name": "false",
            "args": [],
            "draw": [ [ "Str", "false" ] ]
          }
        ]
      },
      {
        "type_name": "value_t",
        "constrs": [
          {
            "constr_name": "var",
            "args": [ { "arg_name": "x1", "arg_type": [ "RecT", "var_t" ] } ],
            "draw": [ [ "Arg", "x1" ] ]
          },
          {
            "constr_name": "int",
            "args": [ { "arg_name": "n", "arg_type": [ "RecT", "num_t" ] } ],
            "draw": [ [ "Arg", "n" ] ]
          },
          {
            "constr_name": "bol",
            "args": [ { "arg_name": "b", "arg_type": [ "RecT", "bol_t" ] } ],
            "draw": [ [ "Arg", "b" ] ]
          },
          {
            "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" ]
            ]
          }
        ]
      },
      {
        "type_name": "term_t",
        "constrs": [
          {
            "constr_name": "val",
            "args": [
              { "arg_name": "v1", "arg_type": [ "RecT", "value_t" ] }
            ],
            "draw": [ [ "Arg", "v1" ] ]
          },
          {
            "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": "plus",
            "args": [
              { "arg_name": "e1", "arg_type": [ "RecT", "term_t" ] },
              { "arg_name": "e2", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [ [ "Arg", "e1" ], [ "Str", " + " ], [ "Arg", "e2" ] ]
          },
          {
            "constr_name": "control",
            "args": [
              { "arg_name": "k", "arg_type": [ "RecT", "var_t" ] },
              { "arg_name": "e", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [
              [ "Str", "(F " ],
              [ "Arg", "k" ],
              [ "Str", " . " ],
              [ "Arg", "e" ],
              [ "Str", ") " ]
            ]
          },
          {
            "constr_name": "prompt",
            "args": [ { "arg_name": "e", "arg_type": [ "RecT", "term_t" ] } ],
            "draw": [ [ "Str", "< " ], [ "Arg", "e" ], [ "Str", " > " ] ]
          },
          {
            "constr_name": "iszero",
            "args": [
              { "arg_name": "term", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [ [ "Str", "Iszero " ], [ "Arg", "term" ] ]
          },
          {
            "constr_name": "B2S",
            "args": [
              { "arg_name": "term", "arg_type": [ "RecT", "term_t" ] }
            ],
            "draw": [ [ "Str", "B2S " ], [ "Arg", "term" ] ]
          }
        ]
      },
      {
        "type_name": "type_t",
        "constrs": [
          { "constr_name": "int", "args": [], "draw": [ [ "Str", "int" ] ] },
          {
            "constr_name": "arrow",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "μα", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "α", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "μβ", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "β", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Str", "( " ],
              [ "Arg", "t1" ],
              [ "Str", " → " ],
              [ "Arg", "t2" ],
              [ "Str", " <" ],
              [ "Arg", "μα" ],
              [ "Str", "> " ],
              [ "Arg", "α" ],
              [ "Str", " < " ],
              [ "Arg", "μβ" ],
              [ "Str", "> " ],
              [ "Arg", "β" ],
              [ "Str", " ) " ]
            ]
          },
          { "constr_name": "bol", "args": [], "draw": [ [ "Str", "bol" ] ] },
          { "constr_name": "str", "args": [], "draw": [ [ "Str", "str" ] ] }
        ]
      },
      {
        "type_name": "trailtype",
        "constrs": [
          { "constr_name": ".", "args": [], "draw": [ [ "Str", "・" ] ] },
          {
            "constr_name": "arrow",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "μ", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Str", "( " ],
              [ "Arg", "t1" ],
              [ "Str", " → " ],
              [ "Str", "< " ],
              [ "Arg", "μ" ],
              [ "Str", " >" ],
              [ "Arg", "t2" ],
              [ "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": [
              [ "Str", "( " ],
              [ "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": "t", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "μα", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "α", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "μβ", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "β", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Arg", "env" ],
              [ "Str", " |- " ],
              [ "Arg", "term" ],
              [ "Str", " : " ],
              [ "Arg", "t" ],
              [ "Str", " < " ],
              [ "Arg", "μα" ],
              [ "Str", " > " ],
              [ "Arg", "α" ],
              [ "Str", " < " ],
              [ "Arg", "μβ" ],
              [ "Str", " > " ],
              [ "Arg", "β" ]
            ]
          },
          {
            "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" ] ]
          },
          {
            "constr_name": "id-cont-type",
            "args": [
              { "arg_name": "t1", "arg_type": [ "RecT", "type_t" ] },
              { "arg_name": "μ", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "t2", "arg_type": [ "RecT", "type_t" ] }
            ],
            "draw": [
              [ "Str", "id-cont-type( " ],
              [ "Arg", "t1" ],
              [ "Str", " , " ],
              [ "Arg", "μ" ],
              [ "Str", " ,  " ],
              [ "Arg", "t2" ],
              [ "Str", " ) " ]
            ]
          },
          {
            "constr_name": "compatible",
            "args": [
              { "arg_name": "μ1", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "μ2", "arg_type": [ "RecT", "trailtype" ] },
              { "arg_name": "μ3", "arg_type": [ "RecT", "trailtype" ] }
            ],
            "draw": [
              [ "Str", "compatible ( " ],
              [ "Arg", "μ1" ],
              [ "Str", " , " ],
              [ "Arg", "μ2" ],
              [ "Str", " , " ],
              [ "Arg", "μ3" ],
              [ "Str", " ) " ]
            ]
          }
        ]
      }
    ]
  },
  "infers": [
    {
      "name": "INT",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "val",
                [ [ "V", "value_t", "int", [ [ "M", "num_t", "n" ] ] ] ]
              ],
              [ "V", "type_t", "int", [] ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ]
            ]
          ]
        }
      ]
    },
    {
      "name": "BOOL",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "val",
                [ [ "V", "value_t", "bol", [ [ "M", "bol_t", "b" ] ] ] ]
              ],
              [ "V", "type_t", "bol", [] ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ]
            ]
          ]
        }
      ]
    },
    {
      "name": "ABS",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "val",
                [
                  [
                    "V",
                    "value_t",
                    "fun",
                    [ [ "M", "var_t", "x" ], [ "M", "term_t", "e" ] ]
                  ]
                ]
              ],
              [
                "V",
                "type_t",
                "arrow",
                [
                  [ "M", "type_t", "τ1" ],
                  [ "M", "type_t", "τ2" ],
                  [ "M", "trailtype", "μα" ],
                  [ "M", "type_t", "α" ],
                  [ "M", "trailtype", "μβ" ],
                  [ "M", "type_t", "μβ" ]
                ]
              ],
              [ "M", "trailtype", "μγ" ],
              [ "M", "type_t", "γ" ],
              [ "M", "trailtype", "μγ" ],
              [ "M", "type_t", "γ" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [
                  "V",
                  "env_t",
                  "cons",
                  [
                    [ "M", "var_t", "x" ],
                    [ "M", "type_t", "τ1" ],
                    [ "M", "env_t", "Γ" ]
                  ]
                ],
                [ "M", "term_t", "e" ],
                [ "M", "type_t", "τ2" ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ],
                [ "M", "trailtype", "μβ" ],
                [ "M", "type_t", "β" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "APP",
      "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", "τ2" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μδ" ],
              [ "M", "type_t", "δ" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "e1" ],
                [
                  "V",
                  "type_t",
                  "arrow",
                  [
                    [ "M", "type_t", "τ1" ],
                    [ "M", "type_t", "τ2" ],
                    [ "M", "trailtype", "μα" ],
                    [ "M", "type_t", "α" ],
                    [ "M", "trailtype", "μβ" ],
                    [ "M", "type_t", "β" ]
                  ]
                ],
                [ "M", "trailtype", "μγ" ],
                [ "M", "type_t", "γ" ],
                [ "M", "trailtype", "μδ" ],
                [ "M", "type_t", "δ" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "e2" ],
                [ "M", "type_t", "τ1" ],
                [ "M", "trailtype", "μβ" ],
                [ "M", "type_t", "β" ],
                [ "M", "trailtype", "μγ" ],
                [ "M", "type_t", "γ" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "CONTROL",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "control",
                [ [ "M", "var_t", "k" ], [ "M", "term_t", "e" ] ]
              ],
              [ "M", "type_t", "τ" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μβ" ],
              [ "M", "type_t", "β" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [
                  "V",
                  "env_t",
                  "cons",
                  [
                    [ "M", "var_t", "k" ],
                    [
                      "V",
                      "type_t",
                      "arrow",
                      [
                        [ "M", "type_t", "τ" ],
                        [ "M", "type_t", "τ1" ],
                        [ "M", "trailtype", "μ1" ],
                        [ "M", "type_t", "τ1'" ],
                        [ "M", "trailtype", "μ2" ],
                        [ "M", "type_t", "α" ]
                      ]
                    ],
                    [ "M", "env_t", "Γ" ]
                  ]
                ],
                [ "M", "term_t", "e" ],
                [ "M", "type_t", "γ" ],
                [ "M", "trailtype", "μ3" ],
                [ "M", "type_t", "γ'" ],
                [ "V", "trailtype", ".", [] ],
                [ "M", "type_t", "β" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "id-cont-type",
              [
                [ "M", "type_t", "γ" ],
                [ "M", "trailtype", "μ3" ],
                [ "M", "type_t", "γ'" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "compatible",
              [
                [
                  "V",
                  "trailtype",
                  "arrow",
                  [
                    [ "M", "type_t", "τ1" ],
                    [ "M", "trailtype", "μ1" ],
                    [ "M", "type_t", "τ1'" ]
                  ]
                ],
                [ "M", "trailtype", "μ2" ],
                [ "M", "trailtype", "μ0" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "compatible",
              [
                [ "M", "trailtype", "μβ" ],
                [ "M", "trailtype", "μ0" ],
                [ "M", "trailtype", "μα" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "PROMPT",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [ "V", "term_t", "prompt", [ [ "M", "term_t", "e" ] ] ],
              [ "M", "type_t", "τ" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "e" ],
                [ "M", "type_t", "β" ],
                [ "M", "trailtype", "μi" ],
                [ "M", "type_t", "β'" ],
                [ "V", "trailtype", ".", [] ],
                [ "M", "type_t", "τ" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "id-cont-type",
              [
                [ "M", "type_t", "β" ],
                [ "M", "trailtype", "μi" ],
                [ "M", "type_t", "β'" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "EQUAL",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "equal",
            [ [ "M", "type_t", "t" ], [ "M", "type_t", "t" ] ]
          ]
        }
      ]
    },
    {
      "name": "TVARZERO",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [
                "V",
                "env_t",
                "cons",
                [
                  [ "M", "var_t", "x" ],
                  [ "M", "type_t", "tp1" ],
                  [ "M", "env_t", "Γ" ]
                ]
              ],
              [
                "V",
                "term_t",
                "val",
                [ [ "V", "value_t", "var", [ [ "M", "var_t", "x" ] ] ] ]
              ],
              [ "M", "type_t", "tp2" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "equal",
              [ [ "M", "type_t", "tp1" ], [ "M", "type_t", "tp2" ] ]
            ]
          ]
        }
      ]
    },
    {
      "name": "TVARSUC",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [
                "V",
                "env_t",
                "cons",
                [
                  [ "M", "var_t", "y" ],
                  [ "M", "type_t", "tp1" ],
                  [ "M", "env_t", "Γ" ]
                ]
              ],
              [
                "V",
                "term_t",
                "val",
                [ [ "V", "value_t", "var", [ [ "M", "var_t", "x" ] ] ] ]
              ],
              [ "M", "type_t", "tp2" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [
                  "V",
                  "term_t",
                  "val",
                  [ [ "V", "value_t", "var", [ [ "M", "var_t", "x" ] ] ] ]
                ],
                [ "M", "type_t", "tp2" ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "idconttype1",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "id-cont-type",
            [
              [ "M", "type_t", "τ" ],
              [ "V", "trailtype", ".", [] ],
              [ "M", "type_t", "τ" ]
            ]
          ]
        }
      ]
    },
    {
      "name": "idconttype2",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "id-cont-type",
            [
              [ "M", "type_t", "τ" ],
              [
                "V",
                "trailtype",
                "arrow",
                [
                  [ "M", "type_t", "τ" ],
                  [ "V", "trailtype", ".", [] ],
                  [ "M", "type_t", "τ'" ]
                ]
              ],
              [ "M", "type_t", "τ'" ]
            ]
          ]
        }
      ]
    },
    {
      "name": "compatible1",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "compatible",
            [
              [ "V", "trailtype", ".", [] ],
              [ "M", "trailtype", "μ" ],
              [ "M", "trailtype", "μ" ]
            ]
          ]
        }
      ]
    },
    {
      "name": "compatible2",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "judge_t",
            "compatible",
            [
              [
                "V",
                "trailtype",
                "arrow",
                [
                  [ "M", "type_t", "τ1" ],
                  [ "M", "trailtype", "μ" ],
                  [ "M", "type_t", "τ2" ]
                ]
              ],
              [ "V", "trailtype", ".", [] ],
              [
                "V",
                "trailtype",
                "arrow",
                [
                  [ "M", "type_t", "τ1" ],
                  [ "M", "trailtype", "μ" ],
                  [ "M", "type_t", "τ2" ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "compatible3",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "compatible",
            [
              [
                "V",
                "trailtype",
                "arrow",
                [
                  [ "M", "type_t", "τ1" ],
                  [ "M", "trailtype", "μ1" ],
                  [ "M", "type_t", "τ1'" ]
                ]
              ],
              [
                "V",
                "trailtype",
                "arrow",
                [
                  [ "M", "type_t", "τ2" ],
                  [ "M", "trailtype", "μ2" ],
                  [ "M", "type_t", "τ2'" ]
                ]
              ],
              [
                "V",
                "trailtype",
                "arrow",
                [
                  [ "M", "type_t", "τ1" ],
                  [ "M", "trailtype", "μ3" ],
                  [ "M", "type_t", "τ1'" ]
                ]
              ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "compatible",
              [
                [
                  "V",
                  "trailtype",
                  "arrow",
                  [
                    [ "M", "type_t", "τ2" ],
                    [ "M", "trailtype", "μ2" ],
                    [ "M", "type_t", "τ2'" ]
                  ]
                ],
                [ "M", "trailtype", "μ3" ],
                [ "M", "trailtype", "μ1" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "Plus",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [
                "V",
                "term_t",
                "plus",
                [ [ "M", "term_t", "n1" ], [ "M", "term_t", "n2" ] ]
              ],
              [ "V", "type_t", "int", [] ],
              [ "M", "trailtype", "μγ" ],
              [ "M", "type_t", "γ" ],
              [ "M", "trailtype", "μβ" ],
              [ "M", "type_t", "β" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "n1" ],
                [ "V", "type_t", "int", [] ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ],
                [ "M", "trailtype", "μβ" ],
                [ "M", "type_t", "β" ]
              ]
            ],
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "n2" ],
                [ "V", "type_t", "int", [] ],
                [ "M", "trailtype", "μγ" ],
                [ "M", "type_t", "γ" ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "IsZero",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [ "V", "term_t", "iszero", [ [ "M", "term_t", "n" ] ] ],
              [ "V", "type_t", "bol", [] ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μβ" ],
              [ "M", "type_t", "β" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "n" ],
                [ "V", "type_t", "int", [] ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ],
                [ "M", "trailtype", "μβ" ],
                [ "M", "type_t", "β" ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "B2S",
      "rule": [
        "I",
        {
          "conclusion": [
            "V",
            "judge_t",
            "judge",
            [
              [ "M", "env_t", "Γ" ],
              [ "V", "term_t", "B2S", [ [ "M", "term_t", "b" ] ] ],
              [ "V", "type_t", "str", [] ],
              [ "M", "trailtype", "μα" ],
              [ "M", "type_t", "α" ],
              [ "M", "trailtype", "μβ" ],
              [ "M", "type_t", "β" ]
            ]
          ],
          "premises": [
            [
              "V",
              "judge_t",
              "judge",
              [
                [ "M", "env_t", "Γ" ],
                [ "M", "term_t", "b" ],
                [ "V", "type_t", "bol", [] ],
                [ "M", "trailtype", "μα" ],
                [ "M", "type_t", "α" ],
                [ "M", "trailtype", "μβ" ],
                [ "M", "type_t", "β" ]
              ]
            ]
          ]
        }
      ]
    }
  ],
  "input": [
    "V",
    "judge_t",
    "judge",
    [
      [ "M", "env_t", "Γ" ],
      [
        "V",
        "term_t",
        "prompt",
        [
          [
            "V",
            "term_t",
            "plus",
            [
              [
                "V",
                "term_t",
                "control",
                [
                  [ "V", "var_t", "v", [ [ "V", "String", "k1", [] ] ] ],
                  [
                    "V",
                    "term_t",
                    "iszero",
                    [
                      [
                        "V",
                        "term_t",
                        "app",
                        [
                          [
                            "V",
                            "term_t",
                            "val",
                            [
                              [
                                "V",
                                "value_t",
                                "var",
                                [
                                  [
                                    "V",
                                    "var_t",
                                    "v",
                                    [ [ "V", "String", "k1", [] ] ]
                                  ]
                                ]
                              ]
                            ]
                          ],
                          [
                            "V",
                            "term_t",
                            "val",
                            [
                              [
                                "V",
                                "value_t",
                                "int",
                                [
                                  [
                                    "V",
                                    "num_t",
                                    "n",
                                    [ [ "V", "Int", "5", [] ] ]
                                  ]
                                ]
                              ]
                            ]
                          ]
                        ]
                      ]
                    ]
                  ]
                ]
              ],
              [
                "V",
                "term_t",
                "control",
                [
                  [ "V", "var_t", "v", [ [ "V", "String", "k2", [] ] ] ],
                  [
                    "V",
                    "term_t",
                    "B2S",
                    [
                      [
                        "V",
                        "term_t",
                        "app",
                        [
                          [
                            "V",
                            "term_t",
                            "val",
                            [
                              [
                                "V",
                                "value_t",
                                "var",
                                [
                                  [
                                    "V",
                                    "var_t",
                                    "v",
                                    [ [ "V", "String", "k2", [] ] ]
                                  ]
                                ]
                              ]
                            ]
                          ],
                          [
                            "V",
                            "term_t",
                            "val",
                            [
                              [
                                "V",
                                "value_t",
                                "int",
                                [
                                  [
                                    "V",
                                    "num_t",
                                    "n",
                                    [ [ "V", "Int", "5", [] ] ]
                                  ]
                                ]
                              ]
                            ]
                          ]
                        ]
                      ]
                    ]
                  ]
                ]
              ]
            ]
          ]
        ]
      ],
      [ "M", "type_t", "τ" ],
      [ "M", "trailtype", "μα" ],
      [ "M", "type_t", "α" ],
      [ "M", "trailtype", "μβ" ],
      [ "M", "type_t", "β" ]
    ]
  ]
}