x:
. 
prime(x) 
x<2 
(
i,j:{2..x
}. x = i
j)
(A A) ((A & B) A B)x:. prime(x) 2
x & (i:{2..x}. i | x)k:
, i:{2..k}, j:
. ij = k 2 j < k & i<k| Rank | Theorem | Name |
| 11 | x:. prime(x) x<2 (i,j:{2..x}. x = ij) | [nonprime_nat] |
| cites the following: | ||
| 2 | (A A) | [dneg_elim_a] |
| 1 | ((A & B) A B) | [not_over_and] |
| 10 | x:. prime(x) 2x & (i:{2..x}. i | x) | [prime_nat] |
| 4 | k:, i:{2..k}, j:. ij = k 2 j < k & i<k | [factors_smaller2] |