| Some definitions of interest. |
|
atomic | Def atomic(a) == a = 0 & (a ~ 1) & reducible(a) |
| | Thm* a:. atomic(a) Prop |
|
reducible | Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc |
| | Thm* a:. reducible(a) Prop |
|
assoced | Def a ~ b == a | b & b | a |
| | Thm* a,b:. (a ~ b) Prop |
|
divides | Def b | a == c:. a = bc |
| | Thm* a,b:. (a | b) Prop |
|
iff | Def P Q == (P Q) & (P Q) |
| | Thm* A,B:Prop. (A B) Prop |
|
not | Def A == A False |
| | Thm* A:Prop. (A) Prop |