OAI/Computability/Logspace/TransitionEvaluation.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

Programs evaluating transitions and the next level of the probability hierarchy.

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

  1. def OAI.ExactDerandomization.Tiber.Sky.whichSide line 25
  2. lemma OAI.ExactDerandomization.Tiber.Sky.whoK line 26
  3. def OAI.ExactDerandomization.Tiber.Sky.pre line 27
  4. abbrev OAI.ExactDerandomization.Tiber.Sky.pK line 29
  5. def OAI.ExactDerandomization.Tiber.Sky.seek line 31
  6. abbrev OAI.ExactDerandomization.Tiber.Sky.tag line 33
  7. def OAI.ExactDerandomization.Tiber.Sky.rocket line 35
  8. def OAI.ExactDerandomization.Tiber.Sky.globe line 38
  9. def OAI.ExactDerandomization.Tiber.Sky.queryEq line 39
  10. def OAI.ExactDerandomization.Tiber.Sky.rimN line 46
  11. def OAI.ExactDerandomization.Tiber.Sky.spilt line 47
  12. def OAI.ExactDerandomization.Tiber.Sky.stadium line 51
  13. abbrev OAI.ExactDerandomization.Tiber.Sky.wafer line 62
  14. def OAI.ExactDerandomization.Tiber.Sky.bodyP line 63
  15. abbrev OAI.ExactDerandomization.Tiber.Sky.progP line 66
  16. abbrev OAI.ExactDerandomization.Tiber.Sky.coverC line 67
  17. abbrev OAI.ExactDerandomization.Tiber.Sky.baseC line 69
  18. def OAI.ExactDerandomization.Tiber.Sky.festival line 70
  19. def OAI.ExactDerandomization.Tiber.Sky.budget0 line 71
  20. lemma OAI.ExactDerandomization.Tiber.Sky.Estate.pile line 75
  21. lemma OAI.ExactDerandomization.Tiber.Sky.Estate.sta line 80
  22. lemma OAI.ExactDerandomization.Tiber.Sky.booster line 121
  23. lemma OAI.ExactDerandomization.Tiber.Sky.swamp line 122
  24. lemma OAI.ExactDerandomization.Tiber.Sky.funded line 127
  25. structure OAI.ExactDerandomization.Tiber.SliceD.Fire line 135
  26. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.inc line 142
  27. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.bud line 143
  28. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.frame line 144
  29. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.cost line 145
  30. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.a line 146
  31. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.pond line 147
  32. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.d line 148
  33. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.μ line 149
  34. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.h0 line 150
  35. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.H line 151
  36. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.pan line 152
  37. structure OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0 line 153
  38. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.againC line 165
  39. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.primal line 166
  40. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.aimD line 167
  41. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.jump line 169
  42. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.price line 175
  43. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.height0 line 179
  44. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.stored line 182
  45. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.urn line 186
  46. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.quoted line 196
  47. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Lamp0.moderate line 207
  48. structure OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq line 232
  49. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.fits line 240
  50. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.trunk line 241
  51. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.stepC line 247
  52. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.glows line 257
  53. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.equalityP line 290
  54. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.bolt line 348
  55. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.amp line 362
  56. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.qpres line 369
  57. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.qcall line 374
  58. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.qstamp line 381
  59. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.leadX line 391
  60. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.leafC line 395
  61. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.sizes0 line 410
  62. theorem OAI.ExactDerandomization.Tiber.SliceD.Fire.Bindq.offeredR line 419
  63. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Basket line 463
  64. def OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.trackQ line 465
  65. def OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.readP line 466
  66. def OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.cookP line 467
  67. structure OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives line 468
  68. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.beforeK line 476
  69. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.earn0 line 482
  70. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.lawful0 line 496
  71. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.salary line 513
  72. abbrev OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.coinC line 517
  73. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.amount line 518
  74. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.boot line 522
  75. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.corded line 530
  76. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.bare0 line 540
  77. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.baseP_band line 541
  78. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.baseP line 550
  79. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.taxed line 557
  80. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.costed line 569
  81. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.harvest0 line 575
  82. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.vault line 585
  83. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.pegged line 599
  84. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.plates line 627
  85. lemma OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.Receives.tucked line 633
  86. theorem OAI.ExactDerandomization.Tiber.SliceD.Fire.Bakin.beam0 line 645