| | Who Cites Formula? |
|
| Formula | Def Formula == rec(formula.Var+formula+(formula formula)+(formulaformula)+(formulaformula)) |
| | | Thm* Formula  Type |
|
| formula_rank | Def  == (letrec formula_rank f = case f: x  0; p (formula_rank(p)+1);p q (formula_rank(p)+formula_rank(q)+1);p q (formula_rank(p)+formula_rank(q)+1);p  q (formula_rank(p)+formula_rank(q)+1); ) |
| | | Thm* Formula   |
|
| formula_case | Def case F:x varC(x);p1 notC(p1);p2p3 andC(p2;p3);p4p5 orC(p4;p5);p6p7 impC(p6;p7); == InjCase(F; x. varC(x); F. InjCase(F; p1. notC(p1); F. InjCase(F; x. x/p2,p3. andC(p2;p3); F. InjCase(F; x. x/p4,p5. orC(p4;p5), x/p6,p7. impC(p6;p7))))) |
|
| nat | Def == {i: | 0 i } |
| | | Thm* Type |
|
| Var | Def Var == Atom |
| | | Thm* Var Type |
|
| letrec_body | Def = b == b |
|
| letrec_arg | Def x b(x) (x) == b(x) |
|
| letrec | Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive) |
|
| le | Def AB ==  B < A |
| | | Thm*  i,j:. (ij) Prop |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
