OAI/Computability/Logspace/CompressionPrograms.lean

GitHub source file

171 declarations, 0 contain sorry, 0 declared as axioms

Programs implementing sparse endpoint pools and row compression.

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

  1. structure OAI.ExactDerandomization.Reed.Poolx line 24
  2. abbrev OAI.ExactDerandomization.Reed.Poolx.P line 34
  3. abbrev OAI.ExactDerandomization.Reed.Poolx.valid line 35
  4. abbrev OAI.ExactDerandomization.Reed.Poolx.joins line 36
  5. abbrev OAI.ExactDerandomization.Reed.Poolx.pals line 37
  6. abbrev OAI.ExactDerandomization.Reed.Poolx.mayor line 38
  7. abbrev OAI.ExactDerandomization.Reed.Poolx.b line 39
  8. abbrev OAI.ExactDerandomization.Reed.Poolx.S line 40
  9. def OAI.ExactDerandomization.Reed.Poolx.grainp line 41
  10. def OAI.ExactDerandomization.Reed.Poolx.meal line 42
  11. structure OAI.ExactDerandomization.Reed.Poolx.Nice line 44
  12. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.serves line 52
  13. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.deserted line 54
  14. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.unique line 74
  15. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.citizens line 79
  16. def OAI.ExactDerandomization.Reed.Poolx.Nice.listP line 83
  17. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.sampled line 85
  18. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.staged line 111
  19. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.higherEnd line 126
  20. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.middleEnd line 129
  21. abbrev OAI.ExactDerandomization.Reed.Poolx.Nice.U line 133
  22. abbrev OAI.ExactDerandomization.Reed.Poolx.Nice.Z line 134
  23. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.whole line 135
  24. lemma OAI.ExactDerandomization.Reed.Poolx.Nice.coverHome line 147
  25. abbrev OAI.ExactDerandomization.Reed.Stool line 171
  26. def OAI.ExactDerandomization.Reed.film line 172
  27. abbrev OAI.ExactDerandomization.Reed.V line 173
  28. lemma OAI.ExactDerandomization.Reed.VK line 174
  29. def OAI.ExactDerandomization.Reed.rootsD line 176
  30. def OAI.ExactDerandomization.Reed.leftQ line 178
  31. def OAI.ExactDerandomization.Reed.stairs line 179
  32. lemma OAI.ExactDerandomization.Reed.stairK line 182
  33. def OAI.ExactDerandomization.Reed.centra line 187
  34. lemma OAI.ExactDerandomization.Reed.centerK line 188
  35. def OAI.ExactDerandomization.Reed.campk line 189
  36. lemma OAI.ExactDerandomization.Reed.spread line 190
  37. lemma OAI.ExactDerandomization.Reed.spanFilm line 197
  38. def OAI.ExactDerandomization.Reed.sideq line 201
  39. structure OAI.ExactDerandomization.Reed.Board line 202
  40. def OAI.ExactDerandomization.Reed.Board.bridgeQ line 219
  41. lemma OAI.ExactDerandomization.Reed.Board.backBE line 220
  42. lemma OAI.ExactDerandomization.Reed.Board.numbers line 224
  43. lemma OAI.ExactDerandomization.Reed.Board.centeral line 226
  44. abbrev OAI.ExactDerandomization.Reed.Board.R line 229
  45. def OAI.ExactDerandomization.Reed.Board.gcat line 230
  46. abbrev OAI.ExactDerandomization.Reed.Board.address line 232
  47. structure OAI.ExactDerandomization.Reed.Board.Holds line 234

    Source documentation

    Supply over all seats and a common work horizon. Carry lip & reservoir budget abstract.

    structure Holds (s:Seats)(c T:ℕ)(v:Poolx):Prop where
…

    Mentions: OAI.ExactDerandomization.Reed.Poolx

  48. def OAI.ExactDerandomization.Reed.Board.pollStack line 252
  49. def OAI.ExactDerandomization.Reed.Board.detective line 253
  50. def OAI.ExactDerandomization.Reed.Board.offer line 254
  51. abbrev OAI.ExactDerandomization.Reed.Board.postC line 256
  52. def OAI.ExactDerandomization.Reed.Board.solar line 257
  53. lemma OAI.ExactDerandomization.Reed.Board.nowEQ line 258
  54. lemma OAI.ExactDerandomization.Reed.Board.Holds.hpos line 266
  55. lemma OAI.ExactDerandomization.Reed.Board.Holds.act line 267
  56. lemma OAI.ExactDerandomization.Reed.Board.Holds.lenpoll line 268
  57. lemma OAI.ExactDerandomization.Reed.Board.Holds.book line 271
  58. def OAI.ExactDerandomization.Reed.Lu.son line 326
  59. abbrev OAI.ExactDerandomization.Reed.Lu.psum line 327
  60. abbrev OAI.ExactDerandomization.Reed.Lu.diff line 328
  61. abbrev OAI.ExactDerandomization.Reed.Lu.times line 329
  62. abbrev OAI.ExactDerandomization.Reed.Lu.sup line 330
  63. abbrev OAI.ExactDerandomization.Reed.Lu.inf line 331
  64. abbrev OAI.ExactDerandomization.Reed.Lu.zeroE line 332
  65. def OAI.ExactDerandomization.Reed.Lu.kohn line 333
  66. abbrev OAI.ExactDerandomization.Reed.Lu.absE line 334
  67. abbrev OAI.ExactDerandomization.Reed.Lu.clippy line 335
  68. abbrev OAI.ExactDerandomization.Reed.Lu.reset line 336
  69. structure OAI.ExactDerandomization.Reed.Lu.Standard line 338
  70. lemma OAI.ExactDerandomization.Reed.Lu.Standard.shins line 344
  71. lemma OAI.ExactDerandomization.Reed.Lu.Standard.rove line 348
  72. lemma OAI.ExactDerandomization.Reed.Lu.Standard.sil line 349
  73. lemma OAI.ExactDerandomization.Reed.Lu.Standard.up0 line 352
  74. lemma OAI.ExactDerandomization.Reed.Lu.Standard.lo0 line 354
  75. lemma OAI.ExactDerandomization.Reed.Lu.Standard.additions line 356
  76. lemma OAI.ExactDerandomization.Reed.Lu.Standard.dubs line 358
  77. lemma OAI.ExactDerandomization.Reed.Lu.Standard.mult0 line 360
  78. lemma OAI.ExactDerandomization.Reed.Lu.Standard.neg0 line 362
  79. lemma OAI.ExactDerandomization.Reed.Lu.Standard.absti line 364
  80. lemma OAI.ExactDerandomization.Reed.Lu.Standard.clips line 367
  81. lemma OAI.ExactDerandomization.Reed.Lu.Standard.ring0 line 369
  82. def OAI.ExactDerandomization.Reed.Board.music line 382
  83. def OAI.ExactDerandomization.Reed.Board.warmth line 385
  84. def OAI.ExactDerandomization.Reed.Board.pit0 line 386
  85. def OAI.ExactDerandomization.Reed.Board.pit line 387
  86. abbrev OAI.ExactDerandomization.Reed.Board.goalCost line 388
  87. abbrev OAI.ExactDerandomization.Reed.Board.Holds.Cext line 392
  88. lemma OAI.ExactDerandomization.Reed.Board.Holds.stifle line 393
  89. lemma OAI.ExactDerandomization.Reed.Board.Holds.currency line 395
  90. lemma OAI.ExactDerandomization.Reed.Board.Holds.chorus line 396
  91. lemma OAI.ExactDerandomization.Reed.Board.Holds.slices line 415
  92. def OAI.ExactDerandomization.Reed.Board.rowB line 449
  93. def OAI.ExactDerandomization.Reed.Board.bites line 450
  94. abbrev OAI.ExactDerandomization.Reed.Board.rawP line 453
  95. abbrev OAI.ExactDerandomization.Reed.Board.sight line 454
  96. abbrev OAI.ExactDerandomization.Reed.Board.starsR line 455
  97. abbrev OAI.ExactDerandomization.Reed.Board.riseR line 458
  98. abbrev OAI.ExactDerandomization.Reed.Board.zenith line 459
  99. abbrev OAI.ExactDerandomization.Reed.Board.border line 461
  100. abbrev OAI.ExactDerandomization.Reed.Board.shore line 462
  101. abbrev OAI.ExactDerandomization.Reed.Board.surf line 463
  102. def OAI.ExactDerandomization.Reed.Board.topE line 464
  103. abbrev OAI.ExactDerandomization.Reed.Board.guardE line 466
  104. abbrev OAI.ExactDerandomization.Reed.Board.borderE line 467
  105. abbrev OAI.ExactDerandomization.Reed.Board.harsh line 468
  106. lemma OAI.ExactDerandomization.Reed.Board.Holds.rowUp line 474
  107. lemma OAI.ExactDerandomization.Reed.Board.Holds.scoopG line 479
  108. lemma OAI.ExactDerandomization.Reed.Board.Holds.bowlC line 494
  109. lemma OAI.ExactDerandomization.Reed.Board.Holds.sky line 503
  110. lemma OAI.ExactDerandomization.Reed.Board.Holds.weep line 507
  111. lemma OAI.ExactDerandomization.Reed.Board.Holds.starship line 518
  112. lemma OAI.ExactDerandomization.Reed.Board.Holds.aurora line 540
  113. lemma OAI.ExactDerandomization.Reed.Board.Holds.skyline line 547
  114. lemma OAI.ExactDerandomization.Reed.Board.Holds.trench line 556
  115. lemma OAI.ExactDerandomization.Reed.Board.Holds.blankx line 562
  116. lemma OAI.ExactDerandomization.Reed.Board.Holds.boardU line 566
  117. lemma OAI.ExactDerandomization.Reed.Board.Holds.heights line 575
  118. abbrev OAI.ExactDerandomization.Reed.Board.Holds.paid line 584
  119. lemma OAI.ExactDerandomization.Reed.Board.Holds.foam line 585
  120. def OAI.ExactDerandomization.Reed.Test.heated line 619
  121. abbrev OAI.ExactDerandomization.Reed.Test.draw line 622
  122. def OAI.ExactDerandomization.Reed.Test.arm line 623
  123. abbrev OAI.ExactDerandomization.Reed.Test.extra line 625
  124. lemma OAI.ExactDerandomization.Reed.Test.f_marg line 626
  125. def OAI.ExactDerandomization.Reed.Test.seatC line 634
  126. lemma OAI.ExactDerandomization.Reed.Test.felt line 636
  127. abbrev OAI.ExactDerandomization.Reed.Board.heatp line 667
  128. abbrev OAI.ExactDerandomization.Reed.Board.touchp line 668
  129. def OAI.ExactDerandomization.Reed.Board.melt line 669
  130. abbrev OAI.ExactDerandomization.Reed.Board.keep0 line 670
  131. def OAI.ExactDerandomization.Reed.Board.jack line 672
  132. def OAI.ExactDerandomization.Reed.Board.shift line 673
  133. def OAI.ExactDerandomization.Reed.Board.bankC line 675
  134. abbrev OAI.ExactDerandomization.Reed.Board.burn line 677
  135. abbrev OAI.ExactDerandomization.Reed.Board.payC line 678
  136. structure OAI.ExactDerandomization.Reed.Board.Broom line 680
  137. def OAI.ExactDerandomization.Reed.Board.Broom.reach line 685
  138. def OAI.ExactDerandomization.Reed.Board.Broom.answer line 686
  139. structure OAI.ExactDerandomization.Reed.Board.Broom.Fell line 687
  140. lemma OAI.ExactDerandomization.Reed.Board.Holds.pay_arc line 700
  141. lemma OAI.ExactDerandomization.Reed.Board.Holds.brooms line 704
  142. def OAI.ExactDerandomization.Reed.Board.rearm line 792

    Source documentation

    Routes the packed choice back to the walk head (outer i replaced by the packed rep index).

    def rearm (x:Word)(a:History):ℕ:= stairs true x (a.1,(dec a.2:History).1)

    Mentions: OAI.ExactDerandomization.Word, OAI.ExactDerandomization.Reed.stairs

  143. lemma OAI.ExactDerandomization.Reed.Board.rearmK line 793
  144. abbrev OAI.ExactDerandomization.Reed.Board.scoreMood line 794
  145. abbrev OAI.ExactDerandomization.Reed.Board.plaza line 795
  146. abbrev OAI.ExactDerandomization.Reed.Board.primary line 796
  147. def OAI.ExactDerandomization.Reed.Board.rateMood line 797
  148. abbrev OAI.ExactDerandomization.Reed.Board.hills line 799
  149. abbrev OAI.ExactDerandomization.Reed.Board.prompt line 800
  150. abbrev OAI.ExactDerandomization.Reed.Board.vibes line 801
  151. abbrev OAI.ExactDerandomization.Reed.Board.tuneC line 802
  152. abbrev OAI.ExactDerandomization.Reed.Board.totalC line 803
  153. lemma OAI.ExactDerandomization.Reed.Board.pays_sides line 805
  154. lemma OAI.ExactDerandomization.Reed.Board.tune_sides line 809
  155. def OAI.ExactDerandomization.Reed.Board.Broom.product line 815
  156. abbrev OAI.ExactDerandomization.Reed.Board.Broom.who line 816
  157. abbrev OAI.ExactDerandomization.Reed.Board.Broom.spot line 817
  158. def OAI.ExactDerandomization.Reed.Board.Broom.valueq line 818
  159. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.there line 824
  160. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.capacity line 830
  161. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.locale line 834
  162. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.allot line 850
  163. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.locates line 855
  164. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.sole line 865
  165. lemma OAI.ExactDerandomization.Reed.Board.Broom.Fell.framed line 870
  166. lemma OAI.ExactDerandomization.Reed.Board.Holds.tune1 line 892
  167. lemma OAI.ExactDerandomization.Reed.Board.Holds.tune0 line 893
  168. lemma OAI.ExactDerandomization.Reed.Board.Holds.baseHear line 899
  169. lemma OAI.ExactDerandomization.Reed.Board.Holds.turmoil line 907
  170. structure OAI.ExactDerandomization.Reed.Board.Page line 932

    Source documentation

    Package for a single executable prefix update, all higher-precision probes.

    structure Page (s:Seats)(c T:ℕ)(v:Poolx)(b:Broom p s c v):Prop where
…

    Mentions: OAI.ExactDerandomization.Reed.Poolx, OAI.ExactDerandomization.Reed.Board.Broom

  171. theorem OAI.ExactDerandomization.Reed.Board.mounted line 939