Metamath Proof Explorer

Table of Contents - 21.38.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. naddass1
69. naddgeoa
70. naddonnn
71. naddwordnexlem0
72. naddwordnexlem1
73. naddwordnexlem2
74. naddwordnexlem3
75. oawordex3
76. naddwordnexlem4
77. ordsssucim
78. insucid
79. om2
80. oaltom
81. oe2
82. omltoe