OAI/Computability/Logspace/BoundedTours.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

Bounded tours, paired path operations, and finite traversal programs.

From OpenAI, Exact Derandomization of Logarithmic Space: L = RL = BPL.

  1. def OAI.ExactDerandomization.Plaza.pledge line 19
  2. lemma OAI.ExactDerandomization.Plaza.pledge_eq line 20
  3. def OAI.ExactDerandomization.Plaza.sealG line 27
  4. structure OAI.ExactDerandomization.Plaza.Deck line 28
  5. abbrev OAI.ExactDerandomization.Plaza.Deck.dom line 34
  6. abbrev OAI.ExactDerandomization.Plaza.Deck.slots line 35
  7. structure OAI.ExactDerandomization.Plaza.Deck.Licence line 37
  8. def OAI.ExactDerandomization.Plaza.Deck.rim line 43
  9. def OAI.ExactDerandomization.Plaza.Deck.takes line 44
  10. lemma OAI.ExactDerandomization.Plaza.Deck.rimmem line 45
  11. lemma OAI.ExactDerandomization.Plaza.Deck.splitup line 47
  12. lemma OAI.ExactDerandomization.Plaza.Deck.uniq1 line 56
  13. lemma OAI.ExactDerandomization.Plaza.Deck.uniq2 line 62
  14. lemma OAI.ExactDerandomization.Plaza.Deck.Licence.scented line 74
  15. lemma OAI.ExactDerandomization.Plaza.Deck.Licence.trace0 line 77
  16. lemma OAI.ExactDerandomization.Plaza.Deck.Licence.traceL line 82
  17. lemma OAI.ExactDerandomization.Plaza.Deck.Licence.entry line 86
  18. lemma OAI.ExactDerandomization.Plaza.Deck.Licence.agree line 88
  19. lemma OAI.ExactDerandomization.Plaza.Deck.back0 line 95
  20. abbrev OAI.ExactDerandomization.Plaza.pan line 108
  21. def OAI.ExactDerandomization.Plaza.pr line 109
  22. abbrev OAI.ExactDerandomization.Plaza.tags line 110
  23. def OAI.ExactDerandomization.Plaza.opn line 111
  24. def OAI.ExactDerandomization.Plaza.clearp line 115
  25. def OAI.ExactDerandomization.Plaza.launch line 117
  26. def OAI.ExactDerandomization.Plaza.screen line 121
  27. def OAI.ExactDerandomization.Plaza.forwardp line 126
  28. abbrev OAI.ExactDerandomization.Plaza.rowFlag line 131
  29. def OAI.ExactDerandomization.Plaza.reversep line 134
  30. abbrev OAI.ExactDerandomization.Plaza.Deck.at0 line 142
  31. abbrev OAI.ExactDerandomization.Plaza.Deck.hq line 143
  32. abbrev OAI.ExactDerandomization.Plaza.Deck.angi line 144
  33. abbrev OAI.ExactDerandomization.Plaza.Deck.ctg line 145
  34. abbrev OAI.ExactDerandomization.Plaza.Deck.net line 146
  35. abbrev OAI.ExactDerandomization.Plaza.Deck.now line 147
  36. abbrev OAI.ExactDerandomization.Plaza.Deck.atpred line 148
  37. def OAI.ExactDerandomization.Plaza.Deck.berth line 149
  38. lemma OAI.ExactDerandomization.Plaza.Deck.bitAdm line 153
  39. lemma OAI.ExactDerandomization.Plaza.Deck.trackAll line 165
  40. lemma OAI.ExactDerandomization.Plaza.Deck.march line 191
  41. lemma OAI.ExactDerandomization.Plaza.Deck.era line 237
  42. lemma OAI.ExactDerandomization.Plaza.Deck.beam line 292
  43. abbrev OAI.ExactDerandomization.Plaza.PowerTop line 351
  44. structure OAI.ExactDerandomization.Plaza.WheelTop line 353
  45. abbrev OAI.ExactDerandomization.Plaza.WheelTop.Eqpt line 360
  46. abbrev OAI.ExactDerandomization.Plaza.WheelTop.minPt line 361
  47. def OAI.ExactDerandomization.Plaza.WheelTop.headQ line 362
  48. def OAI.ExactDerandomization.Plaza.WheelTop.point line 363
  49. lemma OAI.ExactDerandomization.Plaza.WheelTop.minK line 364
  50. lemma OAI.ExactDerandomization.Plaza.WheelTop.pointK line 368
  51. lemma OAI.ExactDerandomization.Plaza.WheelTop.headK line 373
  52. def OAI.ExactDerandomization.Plaza.WheelTop.busy line 374
  53. lemma OAI.ExactDerandomization.Plaza.WheelTop.busyK line 376
  54. def OAI.ExactDerandomization.Plaza.WheelTop.full line 380
  55. def OAI.ExactDerandomization.Plaza.WheelTop.undoTop line 382
  56. def OAI.ExactDerandomization.Plaza.WheelTop.ang line 383
  57. def OAI.ExactDerandomization.Plaza.WheelTop.update line 384
  58. lemma OAI.ExactDerandomization.Plaza.WheelTop.updateK line 388
  59. def OAI.ExactDerandomization.Plaza.WheelTop.chart line 393
  60. lemma OAI.ExactDerandomization.Plaza.WheelTop.chartK line 394
  61. def OAI.ExactDerandomization.Plaza.WheelTop.per line 395
  62. def OAI.ExactDerandomization.Plaza.WheelTop.hunt line 396
  63. def OAI.ExactDerandomization.Plaza.WheelTop.track line 397
  64. def OAI.ExactDerandomization.Plaza.tinc line 401
  65. lemma OAI.ExactDerandomization.Plaza.width line 402
  66. lemma OAI.ExactDerandomization.Plaza.segment line 409
  67. structure OAI.ExactDerandomization.Plaza.Isle line 411
  68. abbrev OAI.ExactDerandomization.Plaza.Isle.p line 422
  69. abbrev OAI.ExactDerandomization.Plaza.Isle.P line 423
  70. abbrev OAI.ExactDerandomization.Plaza.Isle.Hq line 424
  71. abbrev OAI.ExactDerandomization.Plaza.Isle.slot line 425
  72. structure OAI.ExactDerandomization.Plaza.Isle.Wrap line 426
  73. abbrev OAI.ExactDerandomization.Plaza.Isle.speed line 433
  74. abbrev OAI.ExactDerandomization.Plaza.Isle.pay1 line 434
  75. abbrev OAI.ExactDerandomization.Plaza.Isle.pay line 435
  76. abbrev OAI.ExactDerandomization.Plaza.Isle.way line 436
  77. abbrev OAI.ExactDerandomization.Plaza.Isle.line line 437
  78. abbrev OAI.ExactDerandomization.Plaza.Isle.term line 438
  79. abbrev OAI.ExactDerandomization.Plaza.Isle.ball line 451
  80. abbrev OAI.ExactDerandomization.Plaza.Isle.hall2 line 452
  81. abbrev OAI.ExactDerandomization.Plaza.Isle.cur line 454
  82. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.hc0 line 460
  83. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.dollar line 465
  84. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.person line 469
  85. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.shortterm line 473
  86. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.wider line 481
  87. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.circul line 488
  88. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.harvest line 496
  89. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.sound line 507
  90. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.off0 line 513
  91. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.plusstep line 519
  92. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.runout line 546
  93. lemma OAI.ExactDerandomization.Plaza.Isle.Wrap.support0 line 583
  94. theorem OAI.ExactDerandomization.Plaza.Isle.Wrap.cash line 590
  95. def OAI.ExactDerandomization.Plaza.rakeword line 613
  96. lemma OAI.ExactDerandomization.Plaza.width0 line 616
  97. def OAI.ExactDerandomization.Plaza.neigh line 618
  98. lemma OAI.ExactDerandomization.Plaza.neighK line 619
  99. abbrev OAI.ExactDerandomization.Plaza.pot line 623
  100. def OAI.ExactDerandomization.Plaza.cutter line 624
  101. lemma OAI.ExactDerandomization.Plaza.cutterK line 627
  102. lemma OAI.ExactDerandomization.Plaza.checked_max line 630
  103. lemma OAI.ExactDerandomization.Plaza.land line 647
  104. lemma OAI.ExactDerandomization.Plaza.high_mesh line 661
  105. lemma OAI.ExactDerandomization.Plaza.cutcorrect line 665
  106. lemma OAI.ExactDerandomization.Plaza.chaints line 679
  107. def OAI.ExactDerandomization.Plaza.padValue line 710
  108. lemma OAI.ExactDerandomization.Plaza.padK line 712
  109. def OAI.ExactDerandomization.Plaza.tagsA line 715
  110. lemma OAI.ExactDerandomization.Plaza.tag_est line 716
  111. lemma OAI.ExactDerandomization.Plaza.stringentQ line 735