Metamath Proof Explorer


Table of Contents - 2.6.14. The Ackermann bijection

  1. ackbij2lem1
  2. ackbij1lem1
  3. ackbij1lem2
  4. ackbij1lem3
  5. ackbij1lem4
  6. ackbij1lem5
  7. ackbij1lem6
  8. ackbij1lem7
  9. ackbij1lem8
  10. ackbij1lem9
  11. ackbij1lem10
  12. ackbij1lem11
  13. ackbij1lem12
  14. ackbij1lem13
  15. ackbij1lem14
  16. ackbij1lem15
  17. ackbij1lem16
  18. ackbij1lem17
  19. ackbij1lem18
  20. ackbij1
  21. ackbij1b
  22. ackbij2lem2
  23. ackbij2lem3
  24. ackbij2lem4
  25. ackbij2
  26. r1om
  27. fictb