Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
{ "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", "χ", [] ] ] ] ] ] ] ] ] ] ] ] ] ] }