| Rank | Theorem | Name |
| 10 | Thm*  x: . prime(x)   2 x &  ( i:{2..x }. i | x) | [prime_nat] |
| cites the following: |
| 9 | Thm* p: . prime(p)  p = 0 & (p ~ 1) & (a:. a | p (a ~ 1)  (a ~ p)) | [prime_elim] |
| 9 | Thm* a:. atomic(a) prime(a) | [atomic_imp_prime] |
| 7 | Thm* a:. atomic(a) (a ~ 1) & (b:. b | a (b ~ 1) (b ~ a)) | [atomic_char] |
| 2 | Thm* a,b:. |a| | |b| a | b | [divides_of_absvals] |
| 0 | Thm* i:. |i| = i | [absval_pos] |
| 2 | Thm* EquivRel x,y:. x ~ y | [assoced_equiv_rel] |
| 3 | Thm* a:. |a| ~ a | [absval_assoced] |
| 6 | Thm* a,b:. (a ~ b) a = b | [assoced_nelim] |
| 1 | Thm* a:, b: . a | b ab | [divisors_bound] |
| 0 | Thm* a:. 0 | a a = 0 | [zero_divs_only_zero] |
| 1 | Thm* Dec(A) ((A & B) A B) | [not_over_and] |