Metamath Proof Explorer

Table of Contents - 21.36.2. Natural addition of Cantor normal forms

1. oawordex2
2. nnawordexg
3. succlg
4. dflim5
5. oacl2g
6. onmcl
7. omabs2
8. omcl2
9. omcl3g
10. ordsssucb
11. tfsconcatlem
12. tfsconcatun
13. tfsconcatfn
14. tfsconcatfv1
15. tfsconcatfv2
16. tfsconcatfv
17. tfsconcatrn
18. tfsconcatfo
19. tfsconcatb0
20. tfsconcat0i
21. tfsconcat0b
22. tfsconcat00
23. tfsconcatrev
24. tfsconcatrnss12
25. tfsconcatrnss
26. tfsconcatrnsson
27. tfsnfin
28. rp-tfslim
29. ofoafg
30. ofoaf
31. ofoafo
32. ofoacl
33. ofoaid1
34. ofoaid2
35. ofoaass
36. ofoacom
37. naddcnff
38. naddcnffn
39. naddcnffo
40. naddcnfcl
41. naddcnfcom
42. naddcnfid1
43. naddcnfid2
44. naddcnfass
45. onsucunifi
46. sucunisn
47. onsucunipr
48. onsucunitp
49. oaun3lem1
50. oaun3lem2
51. oaun3lem3
52. oaun3lem4
53. rp-abid
54. oadif1lem
55. oadif1
56. oaun2
57. oaun3
58. naddov4
59. nadd2rabtr
60. nadd2rabord
61. nadd2rabex
62. nadd2rabon
63. nadd1rabtr
64. nadd1rabord
65. nadd1rabex
66. nadd1rabon
67. nadd1suc
68. naddsuc2
69. naddass1
70. naddgeoa
71. naddonnn
72. naddwordnexlem0
73. naddwordnexlem1
74. naddwordnexlem2
75. naddwordnexlem3
76. oawordex3
77. naddwordnexlem4
78. ordsssucim
79. insucid
80. om2
81. oaltom
82. oe2
83. omltoe