<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
{
  "terms": {
    "name": "Term_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", ")" ]
            ]
          }
        ]
      }
    ]
  },
  "infers": [
    {
      "name": "S",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [ "M", "Term_t", "tm1" ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm2" ], [ "M", "Term_t", "tm3" ] ]
                  ]
                ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
                  ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm3" ] ]
                  ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "K",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [ "M", "Term_t", "tm1" ],
              [
                "V",
                "Term_t",
                "Arrow",
                [ [ "M", "Term_t", "tm2" ], [ "M", "Term_t", "tm1" ] ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "I",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [ [ "M", "Term_t", "tm" ], [ "M", "Term_t", "tm" ] ]
          ]
        }
      ]
    },
    {
      "name": "B",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Arrow",
                [ [ "M", "Term_t", "tm2" ], [ "M", "Term_t", "tm3" ] ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
                  ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm3" ] ]
                  ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "C",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [ "M", "Term_t", "tm1" ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm2" ], [ "M", "Term_t", "tm3" ] ]
                  ]
                ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [ "M", "Term_t", "tm2" ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm3" ] ]
                  ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "W",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [ "M", "Term_t", "tm1" ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
                  ]
                ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "B'",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [
                "V",
                "Term_t",
                "Arrow",
                [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
              ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm2" ], [ "M", "Term_t", "tm3" ] ]
                  ],
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm3" ] ]
                  ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "C*",
      "rule": [
        "A",
        {
          "axiom": [
            "V",
            "Term_t",
            "Arrow",
            [
              [ "M", "Term_t", "tm1" ],
              [
                "V",
                "Term_t",
                "Arrow",
                [
                  [
                    "V",
                    "Term_t",
                    "Arrow",
                    [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
                  ],
                  [ "M", "Term_t", "tm2" ]
                ]
              ]
            ]
          ]
        }
      ]
    },
    {
      "name": "MP",
      "rule": [
        "I",
        {
          "conclusion": [ "M", "Term_t", "tm2" ],
          "premises": [
            [
              "V",
              "Term_t",
              "Arrow",
              [ [ "M", "Term_t", "tm1" ], [ "M", "Term_t", "tm2" ] ]
            ],
            [ "M", "Term_t", "tm1" ]
          ]
        }
      ]
    }
  ],
   "input" :  [ "M", "Term_t", "tm1" ]
}