Metamath Proof Explorer

Table of Contents - 2.4.14. Well-founded recursion

1. cwrecs
2. df-wrecs
3. wrecseq123
4. nfwrecs
5. wrecseq1
6. wrecseq2
7. wrecseq3
8. wfr3g
9. wfrlem1
10. wfrlem2
11. wfrlem3
12. wfrlem3a
13. wfrlem4
14. wfrlem5
15. wfrrel
16. wfrdmss
17. wfrlem8
18. wfrdmcl
19. wfrlem10
20. wfrfun
21. wfrlem12
22. wfrlem13
23. wfrlem14
24. wfrlem15
25. wfrlem16
26. wfrlem17
27. wfr2a
28. wfr1
29. wfr2
30. wfr3