a:
. atomic(a) 
(a ~ 1) & (b:. b | a 
(b ~ 1) 
(b ~ a))(A B) A & B Stable{P}a,b:. a
b = 0 a = 0 & b = 0b:. b | 0a,b:. (a ~ b) a = b a = -ba,b:, n:
. ((na) ~ (nb)) (a ~ b)a,b:. ab = 0 a = 0 b = 0| Rank | Theorem | Name |
| 7 | a:. atomic(a) (a ~ 1) & (b:. b | a (b ~ 1) (b ~ a)) | [atomic_char] |
| cites the following: | ||
| 0 | (A B) A & B | [not_over_or] |
| 0 | Stable{P} | [stable__from_decidable] |
| 0 | a,b:. ab = 0 a = 0 & b = 0 | [zero_ann_b] |
| 0 | b:. b | 0 | [any_divs_zero] |
| 5 | a,b:. (a ~ b) a = b a = -b | [assoced_elim] |
| 6 | a,b:, n:. ((na) ~ (nb)) (a ~ b) | [mul_cancel_in_assoced] |
| 4 | a,b:. ab = 0 a = 0 b = 0 | [int_entire] |