Metamath Proof Explorer

Table of Contents - 15.4. Induction and recursion

1. Induction and recursion on one variable
   1. cnorec
   2. df-norec
   3. lrrecval
   4. lrrecval2
   5. lrrecpo
   6. lrrecse
   7. lrrecfr
   8. lrrecpred
   9. noinds
   10. norecfn
   11. norecov
2. Induction and recursion on two variables
   1. cnorec2
   2. df-norec2
   3. noxpordpo
   4. noxpordfr
   5. noxpordse
   6. noxpordpred
   7. no2indslem
   8. no2inds
   9. norec2fn
   10. norec2ov
   11. no3inds