Metamath Proof Explorer
Table of Contents - 2.6.14. The Ackermann bijection
- ackbij2lem1
- ackbij1lem1
- ackbij1lem2
- ackbij1lem3
- ackbij1lem4
- ackbij1lem5
- ackbij1lem6
- ackbij1lem7
- ackbij1lem8
- ackbij1lem9
- ackbij1lem10
- ackbij1lem11
- ackbij1lem12
- ackbij1lem13
- ackbij1lem14
- ackbij1lem15
- ackbij1lem16
- ackbij1lem17
- ackbij1lem18
- ackbij1
- ackbij1b
- ackbij2lem2
- ackbij2lem3
- ackbij2lem4
- ackbij2
- r1om
- fictb