| | Who Cites Formula? |
|
| Formula | Def Formula == rec(formula.Var+formula+(formula formula)+(formulaformula)+(formulaformula)) |
| | | Thm* Formula  Type |
|
| Var | Def Var == Atom |
| | | Thm* Var Type |
|
| decidable | Def Dec(P) == P   P |
| | | Thm*  A:Prop. Dec(A) Prop |
|
| 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 |
|
| fvar | Def F == inl(F) |
| | | Thm* x:Var. x Formula |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
