x
varC(x);
p1 notC(p1);p2
p3 andC(p2;p3);p4
p5 orC(p4;p5);p6
p7 impC(p6;p7);
B
A
| Def | | [formula_rank] | ||
| Def | | [nat] | int 1 | |
| Def | Formula | [Formula] | formula | |
| Def | case F:x varC(x);p1 notC(p1);p2p3 andC(p2;p3);p4p5 orC(p4;p5);p6p7 impC(p6;p7); | [formula_case] | formula | |
| Def | = b | [letrec_body] | lambda jlc | |
| Def | x b(x) | [letrec_arg] | lambda jlc | |
| Def | (letrec f b(f)) | [letrec] | lambda jlc | |
| Def | AB | [le] | core | |
| Def | Var | [Var] | var jlc | |
| Def | A | [not] | core |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |
 |  |  |