a,b:
. Dec(a | b)a:. a | aa:. 0 | a 
a = 0 (A 
B) Dec(B)a:, b:
. b | a (a rem b) = 0| Rank | Theorem | Name |
| 7 | a,b:. Dec(a | b) | [decidable__divides] |
| cites the following: | ||
| 0 | a:. a | a | [divides_reflexivity] |
| 0 | a:. 0 | a a = 0 | [zero_divs_only_zero] |
| 0 | (A B) Dec(B) | [iff_preserves_decidability] |
| 6 | a:, b:. b | a (a rem b) = 0 | [divides_iff_rem_zero] |