x:
. Dec(prime(x))x:
. prime(x) 
2
x & 
(
i:{2..x
}. i | x)y:. prime(-y) prime(y)| Rank | Theorem | Name |
| 11 | x:. Dec(prime(x)) | [decidable__prime] |
| cites the following: | ||
| 10 | x:. prime(x) 2x & (i:{2..x}. i | x) | [prime_nat] |
| 3 | y:. prime(-y) prime(y) | [prime_neg] |