OAI/Computability/Logspace/ConfigurationEvaluation.lean

GitHub source file

157 declarations, 0 contain sorry, 0 declared as axioms

Uniform configuration, copy-arc, and reward evaluation.

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

  1. def OAI.ExactDerandomization.Spring.Aqua.tally line 29
  2. lemma OAI.ExactDerandomization.Spring.Aqua.tallyK line 31
  3. lemma OAI.ExactDerandomization.Spring.Aqua.wideT line 36
  4. lemma OAI.ExactDerandomization.Spring.Aqua.tank line 37
  5. lemma OAI.ExactDerandomization.Spring.Aqua.maxv line 50
  6. lemma OAI.ExactDerandomization.Spring.Aqua.room line 63
  7. def OAI.ExactDerandomization.Spring.Aqua.dbox line 67
  8. abbrev OAI.ExactDerandomization.Spring.Aqua.qua line 68
  9. def OAI.ExactDerandomization.Spring.Aqua.qq line 69
  10. def OAI.ExactDerandomization.Spring.Aqua.quo line 70
  11. def OAI.ExactDerandomization.Spring.Aqua.rawcoins line 73
  12. def OAI.ExactDerandomization.Spring.Aqua.sbase line 74
  13. def OAI.ExactDerandomization.Spring.Aqua.zet line 76
  14. lemma OAI.ExactDerandomization.Spring.Aqua.coinZ line 77
  15. lemma OAI.ExactDerandomization.Spring.Aqua.dboxK line 81
  16. lemma OAI.ExactDerandomization.Spring.Aqua.qqK line 83
  17. lemma OAI.ExactDerandomization.Spring.Aqua.largeK line 85
  18. lemma OAI.ExactDerandomization.Spring.Aqua.quoK line 87
  19. lemma OAI.ExactDerandomization.Spring.Aqua.rawK line 90
  20. lemma OAI.ExactDerandomization.Spring.Aqua.priceT line 95
  21. lemma OAI.ExactDerandomization.Spring.Aqua.priceV line 97
  22. lemma OAI.ExactDerandomization.Spring.Aqua.pc line 99
  23. lemma OAI.ExactDerandomization.Spring.Aqua.pureG line 101
  24. lemma OAI.ExactDerandomization.Spring.Aqua.raw line 107
  25. lemma OAI.ExactDerandomization.Spring.Aqua.seed line 110
  26. abbrev OAI.ExactDerandomization.Spring.WindY.tx line 115
  27. lemma OAI.ExactDerandomization.Spring.WindY.nowM line 116
  28. def OAI.ExactDerandomization.Spring.WindY.shower line 118
  29. lemma OAI.ExactDerandomization.Spring.WindY.showerK line 121
  30. lemma OAI.ExactDerandomization.Spring.WindY.rains line 123
  31. lemma OAI.ExactDerandomization.Spring.WindY.careful line 136
  32. def OAI.ExactDerandomization.Spring.Prism.swap line 145
  33. lemma OAI.ExactDerandomization.Spring.Prism.swapK line 146
  34. lemma OAI.ExactDerandomization.Spring.Prism.masked line 149
  35. def OAI.ExactDerandomization.Spring.Prism.leftE line 157
  36. def OAI.ExactDerandomization.Spring.Prism.rightE line 158
  37. def OAI.ExactDerandomization.Spring.Prism.crossE line 159
  38. abbrev OAI.ExactDerandomization.Spring.Garden.fence line 180
  39. abbrev OAI.ExactDerandomization.Spring.Garden.m line 181
  40. abbrev OAI.ExactDerandomization.Spring.Garden.origin line 182
  41. abbrev OAI.ExactDerandomization.Spring.Garden.stageQ line 183
  42. abbrev OAI.ExactDerandomization.Spring.Garden.params line 184
  43. abbrev OAI.ExactDerandomization.Spring.Garden.greenY line 185
  44. abbrev OAI.ExactDerandomization.Spring.Garden.matchZ line 186
  45. abbrev OAI.ExactDerandomization.Spring.Garden.countO line 187
  46. def OAI.ExactDerandomization.Spring.Garden.asker line 189
  47. def OAI.ExactDerandomization.Spring.Garden.foreground line 190
  48. def OAI.ExactDerandomization.Spring.Garden.atmos line 197
  49. def OAI.ExactDerandomization.Spring.Garden.retired line 200
  50. def OAI.ExactDerandomization.Spring.Garden.began line 202
  51. def OAI.ExactDerandomization.Spring.Garden.ace line 204
  52. abbrev OAI.ExactDerandomization.Spring.Garden.Lead line 206
  53. abbrev OAI.ExactDerandomization.Spring.Garden.Pan line 207
  54. def OAI.ExactDerandomization.Spring.Garden.clean line 208
  55. lemma OAI.ExactDerandomization.Spring.Garden.Plot.wall line 212
  56. lemma OAI.ExactDerandomization.Spring.Garden.Plot.matt line 215
  57. lemma OAI.ExactDerandomization.Spring.Garden.Plot.countEat line 219
  58. lemma OAI.ExactDerandomization.Spring.Garden.Plot.askG line 223
  59. lemma OAI.ExactDerandomization.Spring.Garden.Plot.fgG line 230
  60. lemma OAI.ExactDerandomization.Spring.Garden.Plot.fogK line 247
  61. lemma OAI.ExactDerandomization.Spring.Garden.Plot.reachK line 252
  62. lemma OAI.ExactDerandomization.Spring.Garden.Plot.yokeK line 255
  63. lemma OAI.ExactDerandomization.Spring.Garden.Plot.habG line 259
  64. lemma OAI.ExactDerandomization.Spring.Garden.Plot.atmosK line 274
  65. lemma OAI.ExactDerandomization.Spring.Garden.Plot.oldKn line 278
  66. lemma OAI.ExactDerandomization.Spring.Garden.Plot.retireK line 280
  67. lemma OAI.ExactDerandomization.Spring.Garden.Plot.beganK line 285
  68. lemma OAI.ExactDerandomization.Spring.Garden.Plot.cleanK line 291
  69. lemma OAI.ExactDerandomization.Spring.Garden.Plot.basin line 293
  70. abbrev OAI.ExactDerandomization.Spring.Blade.Embellish line 316
  71. def OAI.ExactDerandomization.Spring.Blade.bald line 317
  72. abbrev OAI.ExactDerandomization.Spring.Blade.HullT.determine line 322
  73. def OAI.ExactDerandomization.Spring.Blade.HullT.tides line 323
  74. lemma OAI.ExactDerandomization.Spring.Blade.HullT.tideK line 325
  75. abbrev OAI.ExactDerandomization.Spring.Blade.Crest.portN line 334
  76. abbrev OAI.ExactDerandomization.Spring.Blade.Crest.postN line 335
  77. def OAI.ExactDerandomization.Spring.Blade.Crest.pastC line 336
  78. def OAI.ExactDerandomization.Spring.Blade.Crest.bronze line 337
  79. def OAI.ExactDerandomization.Spring.Blade.Crest.newelf line 339
  80. abbrev OAI.ExactDerandomization.Spring.Blade.Crest.launch line 342
  81. abbrev OAI.ExactDerandomization.Spring.Blade.Crest.op line 343
  82. def OAI.ExactDerandomization.Spring.Blade.Crest.ordinary line 344
  83. def OAI.ExactDerandomization.Spring.Blade.Crest.company line 346
  84. def OAI.ExactDerandomization.Spring.Blade.Crest.twins line 352
  85. lemma OAI.ExactDerandomization.Spring.Blade.Crest.pastK line 359
  86. lemma OAI.ExactDerandomization.Spring.Blade.Crest.bronzeK line 361
  87. lemma OAI.ExactDerandomization.Spring.Blade.Crest.opK line 364
  88. lemma OAI.ExactDerandomization.Spring.Blade.Crest.portK line 366
  89. lemma OAI.ExactDerandomization.Spring.Blade.Crest.neoK line 368
  90. lemma OAI.ExactDerandomization.Spring.Blade.Crest.orbitK line 371
  91. lemma OAI.ExactDerandomization.Spring.Blade.Crest.ordinaryK line 373
  92. lemma OAI.ExactDerandomization.Spring.Blade.Crest.companyK line 377
  93. lemma OAI.ExactDerandomization.Spring.Blade.Crest.twinK line 386
  94. def OAI.ExactDerandomization.Spring.Blade.RowD.foreC line 404
  95. def OAI.ExactDerandomization.Spring.Blade.RowD.school line 407
  96. def OAI.ExactDerandomization.Spring.Blade.RowD.hinge line 408
  97. def OAI.ExactDerandomization.Spring.Blade.RowD.coral line 411
  98. abbrev OAI.ExactDerandomization.Spring.Blade.RowD.n line 414
  99. def OAI.ExactDerandomization.Spring.Blade.RowD.dock line 415
  100. abbrev OAI.ExactDerandomization.Spring.Blade.RowD.skies line 416
  101. def OAI.ExactDerandomization.Spring.Blade.RowD.startF line 418
  102. def OAI.ExactDerandomization.Spring.Blade.RowD.scaleB line 421
  103. def OAI.ExactDerandomization.Spring.Blade.RowD.pickA line 424
  104. lemma OAI.ExactDerandomization.Spring.Blade.RowD.chartK line 447
  105. lemma OAI.ExactDerandomization.Spring.Blade.RowD.skiesK line 449
  106. lemma OAI.ExactDerandomization.Spring.Blade.RowD.startK line 453
  107. lemma OAI.ExactDerandomization.Spring.Blade.RowD.scaleBK line 456
  108. lemma OAI.ExactDerandomization.Spring.Blade.RowD.cal line 459
  109. lemma OAI.ExactDerandomization.Spring.Blade.RowD.skol line 462
  110. lemma OAI.ExactDerandomization.Spring.Blade.RowD.canK line 468
  111. lemma OAI.ExactDerandomization.Spring.Blade.RowD.coalK line 478
  112. lemma OAI.ExactDerandomization.Spring.Blade.RowD.pollen line 482
  113. abbrev OAI.ExactDerandomization.Spring.Lily.defaultH line 529
  114. def OAI.ExactDerandomization.Spring.Lily.recruit line 530
  115. def OAI.ExactDerandomization.Spring.Lily.arms line 538
  116. def OAI.ExactDerandomization.Spring.Lily.wraps line 540
  117. def OAI.ExactDerandomization.Spring.Lily.pose0 line 541
  118. lemma OAI.ExactDerandomization.Spring.Lily.armsK line 543
  119. def OAI.ExactDerandomization.Spring.Lily.poseX line 554
  120. lemma OAI.ExactDerandomization.Spring.Lily.goalF line 560
  121. def OAI.ExactDerandomization.Spring.Lily.bay line 562
  122. lemma OAI.ExactDerandomization.Spring.Lily.bayK line 565
  123. abbrev OAI.ExactDerandomization.Spring.Lily.liftq line 567
  124. def OAI.ExactDerandomization.Spring.Lily.foreP line 568
  125. lemma OAI.ExactDerandomization.Spring.Lily.foreP_choice line 573
  126. abbrev OAI.ExactDerandomization.Spring.Lily.prog line 578
  127. structure OAI.ExactDerandomization.Spring.Lily.Service.Fits line 586
  128. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.stow line 595
  129. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.traced0 line 600
  130. abbrev OAI.ExactDerandomization.Spring.Lily.Service.Fits.prS line 604
  131. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.cupF line 605
  132. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.cupG line 609
  133. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.engrave line 613
  134. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.supplies line 625
  135. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.portraits line 635
  136. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.beams_band line 640
  137. lemma OAI.ExactDerandomization.Spring.Lily.Service.Fits.beams line 647
  138. lemma OAI.ExactDerandomization.Spring.Fen.Kpos line 682
  139. abbrev OAI.ExactDerandomization.Spring.Fen.owner line 688
  140. lemma OAI.ExactDerandomization.Spring.Fen.heir line 689
  141. lemma OAI.ExactDerandomization.Spring.Fen.therein line 690
  142. abbrev OAI.ExactDerandomization.Spring.Fen.year line 691
  143. abbrev OAI.ExactDerandomization.Spring.Fen.ashes line 692
  144. abbrev OAI.ExactDerandomization.Spring.Fen.gridR line 694
  145. lemma OAI.ExactDerandomization.Spring.Fen.force line 696
  146. lemma OAI.ExactDerandomization.Spring.Fen.fuel line 723
  147. lemma OAI.ExactDerandomization.Spring.Fen.quietox line 724
  148. lemma OAI.ExactDerandomization.Spring.Fen.GardenV.oldcap line 729
  149. lemma OAI.ExactDerandomization.Spring.Fen.GardenV.forestLen line 751
  150. lemma OAI.ExactDerandomization.Spring.Fen.GardenV.windowN line 765
  151. abbrev OAI.ExactDerandomization.Spring.Fen.R line 799
  152. abbrev OAI.ExactDerandomization.Spring.Fen.area line 800
  153. def OAI.ExactDerandomization.Spring.Fen.chenille line 801
  154. def OAI.ExactDerandomization.Spring.Fen.fanD line 802
  155. lemma OAI.ExactDerandomization.Spring.Fen.sauna line 804
  156. lemma OAI.ExactDerandomization.Spring.Fen.skyfell line 811
  157. lemma OAI.ExactDerandomization.Spring.Fen.meadow line 835