b,c:
. 
(b ~ 1) & (c ~ 1) & a = b
c
a:. reducible(a) 
Propa,b:. (a ~ b) Prop == {i:| i 
0 } Type b T == a = b TA:Type, x,y:A. (x y) PropA == A 
FalseA:Prop. (A) Propc:. a = bca,b:. (a | b) Prop| Who Cites reducible? | |
| 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 | |
| int_nzero | Def == {i:| i 0 } |
| Thm* Type | |
| nequal | Def a b T == a = b T |
| Thm* A:Type, x,y:A. (x y) Prop | |
| not | Def A == A False |
| Thm* A:Prop. (A) Prop | |
| divides | Def b | a == c:. a = bc |
| Thm* a,b:. (a | b) Prop |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |