| | Who Cites Formula? |
|
| Formula | Def Formula == rec(formula.Var+formula+(formula formula)+(formulaformula)+(formulaformula)) |
| | | Thm* Formula  Type |
|
| Var | Def Var == Atom |
| | | Thm* Var Type |
|
| f_or | Def p   q == inr(inr(inr(inl( < p,q > )))) |
| | | Thm*  p,q:Formula. pq Formula |
|
| fand | Def p q == inr(inr(inl( < p,q > ))) |
| | | Thm* p,q:Formula. pq Formula |
|
| fimp | Def p  q == inr(inr(inr(inr( < p,q > )))) |
| | | Thm* p,q:Formula. pq Formula |
|
| fnot | Def  p == inr(inl(p)) |
| | | Thm* x:Formula. x Formula |
|
| formula_rank | Def  == (letrec formula_rank f = case f:x  0;p (formula_rank(p)+1);pq (formula_rank(p)+formula_rank(q)+1);pq (formula_rank(p)+formula_rank(q)+1);pq (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))))) |
|
| fvar | Def F == inl(F) |
| | | Thm* x:Var. x Formula |
|
| nat | Def == {i: | 0 i } |
| | | Thm* 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 |
