x:{x:
| (x rem 2) = 0 }. x!
i,j:. i
j a:, n:
. a
n 
(a rem n) = ((a-n) rem n)| Rank | Theorem | Name |
| 4 | x:{x:| (x rem 2) = 0 }. x! | [sfa_doc_factorial2_wf] |
| cites the following: | ||
| 2 | i,j:. ij | [multiply_nat_wf] |
| 3 | a:, n:. an (a rem n) = ((a-n) rem n) | [rem_rec_case] |