Metamath Proof Explorer

Table of Contents - 21.50.21. Complexity theory

1. Auxiliary theorems
   1. suppdm
   2. eluz2cnn0n1
   3. divge1b
   4. divgt1b
   5. ltsubaddb
   6. ltsubsubb
   7. ltsubadd2b
   8. divsub1dir
   9. expnegico01
   10. elfzolborelfzop1
   11. pw2m1lepw2m1
   12. zgtp1leeq
   13. flsubz
2. Even and odd integers
   1. nn0onn0ex
   2. nn0enn0ex
   3. nnennex
   4. nneop
   5. nneom
   6. nn0eo
   7. nnpw2even
   8. zefldiv2
   9. zofldiv2
   10. nn0ofldiv2
   11. flnn0div2ge
   12. flnn0ohalf
3. The natural logarithm on complex numbers (extension)
   1. logcxp0
   2. regt1loggt0
4. Division of functions
   1. cfdiv
   2. df-fdiv
   3. fdivval
   4. fdivmpt
   5. fdivmptf
   6. refdivmptf
   7. fdivpm
   8. refdivpm
   9. fdivmptfv
   10. refdivmptfv
5. Upper bounds
   1. cbigo
   2. df-bigo
   3. bigoval
   4. elbigofrcl
   5. elbigo
   6. elbigo2
   7. elbigo2r
   8. elbigof
   9. elbigodm
   10. elbigoimp
   11. elbigolo1
6. Logarithm to an arbitrary base (extension)
   1. rege1logbrege0
   2. rege1logbzge0
   3. fllogbd
   4. relogbmulbexp
   5. relogbdivb
   6. logbge0b
   7. logblt1b
7. The binary logarithm
   1. fldivexpfllog2
   2. nnlog2ge0lt1
   3. logbpw2m1
   4. fllog2
8. Binary length
   1. cblen
   2. df-blen
   3. blenval
   4. blen0
   5. blenn0
   6. blenre
   7. blennn
   8. blennnelnn
   9. blennn0elnn
   10. blenpw2
   11. blenpw2m1
   12. nnpw2blen
   13. nnpw2blenfzo
   14. nnpw2blenfzo2
   15. nnpw2pmod
   16. blen1
   17. blen2
   18. nnpw2p
   19. nnpw2pb
   20. blen1b
   21. blennnt2
   22. nnolog2flm1
   23. blennn0em1
   24. blennngt2o2
   25. blengt1fldiv2p1
   26. blennn0e2
9. Digits
   1. cdig
   2. df-dig
   3. digfval
   4. digval
   5. digvalnn0
   6. nn0digval
   7. dignn0fr
   8. dignn0ldlem
   9. dignnld
   10. dig2nn0ld
   11. dig2nn1st
   12. dig0
   13. digexp
   14. dig1
   15. 0dig1
   16. 0dig2pr01
   17. dig2nn0
   18. 0dig2nn0e
   19. 0dig2nn0o
   20. dig2bits
10. Nonnegative integer as sum of its shifted digits
    1. dignn0flhalflem1
    2. dignn0flhalflem2
    3. dignn0ehalf
    4. dignn0flhalf
    5. nn0sumshdiglemA
    6. nn0sumshdiglemB
    7. nn0sumshdiglem1
    8. nn0sumshdiglem2
    9. nn0sumshdig
11. Algorithms for the multiplication of nonnegative integers
    1. nn0mulfsum
    2. nn0mullong
12. N-ary functions
    1. cnaryf
    2. df-naryf
    3. naryfval
    4. naryfvalixp
    5. naryfvalel
    6. naryrcl
    7. naryfvalelfv
    8. naryfvalelwrdf
    9. 0aryfvalel
    10. 0aryfvalelfv
    11. 1aryfvalel
    12. fv1arycl
    13. 1arympt1
    14. 1arympt1fv
    15. 1arymaptfv
    16. 1arymaptf
    17. 1arymaptf1
    18. 1arymaptfo
    19. 1arymaptf1o
    20. 1aryenef
    21. 1aryenefmnd
    22. 2aryfvalel
    23. fv2arycl
    24. 2arympt
    25. 2arymptfv
    26. 2arymaptfv
    27. 2arymaptf
    28. 2arymaptf1
    29. 2arymaptfo
    30. 2arymaptf1o
    31. 2aryenef
13. Primitive recursive functions
14. The Ackermann function
    1. citco
    2. cack
    3. df-itco
    4. df-ack
    5. itcoval
    6. itcoval0
    7. itcoval1
    8. itcoval2
    9. itcoval3
    10. itcoval0mpt
    11. itcovalsuc
    12. itcovalsucov
    13. itcovalendof
    14. itcovalpclem1
    15. itcovalpclem2
    16. itcovalpc
    17. itcovalt2lem2lem1
    18. itcovalt2lem2lem2
    19. itcovalt2lem1
    20. itcovalt2lem2
    21. itcovalt2
    22. ackvalsuc1mpt
    23. ackvalsuc1
    24. ackval0
    25. ackval1
    26. ackval2
    27. ackval3
    28. ackendofnn0
    29. ackfnnn0
    30. ackval0val
    31. ackvalsuc0val
    32. ackvalsucsucval
    33. ackval0012
    34. ackval1012
    35. ackval2012
    36. ackval3012
    37. ackval40
    38. ackval41a
    39. ackval41
    40. ackval42
    41. ackval42a
    42. ackval50