OAI/Computability/Logspace/CatalyticComparison.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

Catalytic comparison of encoded identifiers and bounded traversal operations.

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

  1. abbrev OAI.ExactDerandomization.Glass.NatD.dig line 22
  2. def OAI.ExactDerandomization.Glass.NatD.record line 23
  3. lemma OAI.ExactDerandomization.Glass.NatD.next line 24
  4. lemma OAI.ExactDerandomization.Glass.NatD.under line 25
  5. lemma OAI.ExactDerandomization.Glass.NatD.letter line 34
  6. lemma OAI.ExactDerandomization.Glass.NatD.record_mod line 51
  7. lemma OAI.ExactDerandomization.Glass.NatD.equal line 59
  8. lemma OAI.ExactDerandomization.Glass.NatD.dial_eq line 67
  9. lemma OAI.ExactDerandomization.Glass.NatD.digK line 71
  10. structure OAI.ExactDerandomization.Glass.Rod line 82
  11. def OAI.ExactDerandomization.Glass.Rod.B line 87
  12. def OAI.ExactDerandomization.Glass.Rod.e line 88
  13. def OAI.ExactDerandomization.Glass.Rod.n line 89
  14. def OAI.ExactDerandomization.Glass.Rod.L line 90
  15. def OAI.ExactDerandomization.Glass.Rod.M line 91
  16. def OAI.ExactDerandomization.Glass.Rod.F line 92
  17. def OAI.ExactDerandomization.Glass.Rod.Q line 93
  18. lemma OAI.ExactDerandomization.Glass.Rod.b0 line 94
  19. lemma OAI.ExactDerandomization.Glass.Rod.e0 line 95
  20. lemma OAI.ExactDerandomization.Glass.Rod.e2 line 96
  21. lemma OAI.ExactDerandomization.Glass.Rod.n2 line 99
  22. lemma OAI.ExactDerandomization.Glass.Rod.n_hi line 101
  23. lemma OAI.ExactDerandomization.Glass.Rod.n_low line 102
  24. lemma OAI.ExactDerandomization.Glass.Rod.L_le line 103
  25. lemma OAI.ExactDerandomization.Glass.Rod.L_price line 105
  26. lemma OAI.ExactDerandomization.Glass.Rod.coded line 109
  27. lemma OAI.ExactDerandomization.Glass.Rod.M4 line 113
  28. lemma OAI.ExactDerandomization.Glass.Rod.costs line 116
  29. lemma OAI.ExactDerandomization.Glass.Rod.costs2 line 122
  30. def OAI.ExactDerandomization.Glass.shove line 136
  31. lemma OAI.ExactDerandomization.Glass.enoughS line 138
  32. instance OAI.ExactDerandomization.Glass.Rod.nzM line 143
  33. lemma OAI.ExactDerandomization.Glass.Rod.equals line 144
  34. lemma OAI.ExactDerandomization.Glass.Rod.cast_shove line 148
  35. lemma OAI.ExactDerandomization.Glass.Rod.cancel line 154
  36. def OAI.ExactDerandomization.Glass.Rod.mix line 158
  37. lemma OAI.ExactDerandomization.Glass.Rod.pigment line 160
  38. lemma OAI.ExactDerandomization.Glass.Rod.component line 163
  39. lemma OAI.ExactDerandomization.Glass.Rod.opposite line 168
  40. def OAI.ExactDerandomization.Glass.Rod.hinge line 175
  41. def OAI.ExactDerandomization.Glass.Rod.aloft line 176
  42. lemma OAI.ExactDerandomization.Glass.Rod.twist line 178
  43. abbrev OAI.ExactDerandomization.Glass.Rod.Pane line 185
  44. def OAI.ExactDerandomization.Glass.Rod.proper line 186
  45. def OAI.ExactDerandomization.Glass.Rod.first line 188
  46. def OAI.ExactDerandomization.Glass.Rod.second line 190
  47. def OAI.ExactDerandomization.Glass.Rod.pointR line 192
  48. def OAI.ExactDerandomization.Glass.Rod.pointZ line 193
  49. lemma OAI.ExactDerandomization.Glass.Rod.stay line 195
  50. lemma OAI.ExactDerandomization.Glass.Rod.negone line 200
  51. def OAI.ExactDerandomization.Glass.Rod.fair line 214
  52. def OAI.ExactDerandomization.Glass.Rod.dark line 215
  53. lemma OAI.ExactDerandomization.Glass.Rod.sepia line 216
  54. lemma OAI.ExactDerandomization.Glass.Rod.back line 218
  55. def OAI.ExactDerandomization.Glass.Rod.moat line 231
  56. def OAI.ExactDerandomization.Glass.Rod.hugs line 232
  57. lemma OAI.ExactDerandomization.Glass.Rod.bows line 234
  58. lemma OAI.ExactDerandomization.Glass.Rod.small line 243
  59. lemma OAI.ExactDerandomization.Glass.Rod.paw line 253
  60. lemma OAI.ExactDerandomization.Glass.Rod.pupils line 265
  61. lemma OAI.ExactDerandomization.Glass.Rod.test_eye line 286
  62. def OAI.ExactDerandomization.Glass.Rod.line line 311
  63. def OAI.ExactDerandomization.Glass.Rod.foil line 312
  64. lemma OAI.ExactDerandomization.Glass.Rod.foil_lt line 313
  65. def OAI.ExactDerandomization.Glass.Rod.frosting line 315
  66. lemma OAI.ExactDerandomization.Glass.Rod.freeze line 316
  67. lemma OAI.ExactDerandomization.Glass.Rod.hit line 317
  68. lemma OAI.ExactDerandomization.Glass.Rod.frost_eq line 319
  69. lemma OAI.ExactDerandomization.Glass.Rod.frost_c line 326
  70. def OAI.ExactDerandomization.Glass.Rod.glaze line 335
  71. def OAI.ExactDerandomization.Glass.Rod.ask line 337
  72. lemma OAI.ExactDerandomization.Glass.Rod.glaze2 line 338
  73. lemma OAI.ExactDerandomization.Glass.Rod.glass line 340
  74. lemma OAI.ExactDerandomization.Glass.Rod.learned line 348
  75. abbrev OAI.ExactDerandomization.Glass.Rod.toR line 369
  76. lemma OAI.ExactDerandomization.Glass.Rod.nFun line 370
  77. lemma OAI.ExactDerandomization.Glass.Rod.lFun line 371
  78. lemma OAI.ExactDerandomization.Glass.Rod.mFun line 373
  79. lemma OAI.ExactDerandomization.Glass.Rod.fFun line 374
  80. lemma OAI.ExactDerandomization.Glass.Rod.qFun line 377
  81. lemma OAI.ExactDerandomization.Glass.Rod.shoveK line 381
  82. lemma OAI.ExactDerandomization.Glass.Rod.drew line 386
  83. lemma OAI.ExactDerandomization.Glass.Rod.mixK line 408
  84. lemma OAI.ExactDerandomization.Glass.Rod.glazeK line 417
  85. lemma OAI.ExactDerandomization.Glass.Rod.askK line 428
  86. lemma OAI.ExactDerandomization.Glass.Rod.sumFun line 431
  87. lemma OAI.ExactDerandomization.Glass.Rod.shadeSumK line 444
  88. lemma OAI.ExactDerandomization.Glass.Rod.hingeK line 452
  89. lemma OAI.ExactDerandomization.Glass.Rod.aloK line 454
  90. lemma OAI.ExactDerandomization.Glass.Rod.firstK line 457
  91. lemma OAI.ExactDerandomization.Glass.Rod.upzK line 460
  92. lemma OAI.ExactDerandomization.Glass.Rod.svK line 464
  93. lemma OAI.ExactDerandomization.Glass.Rod.secondK line 467
  94. abbrev OAI.ExactDerandomization.Glass.Foot line 482
  95. inductive OAI.ExactDerandomization.Glass.Mode line 484
  96. def OAI.ExactDerandomization.Glass.pivot line 487
  97. def OAI.ExactDerandomization.Glass.pigment line 490
  98. structure OAI.ExactDerandomization.Glass.Eye line 496
  99. def OAI.ExactDerandomization.Glass.Eye.eye line 502
  100. def OAI.ExactDerandomization.Glass.Eye.peg line 503
  101. def OAI.ExactDerandomization.Glass.Eye.flip line 504
  102. lemma OAI.ExactDerandomization.Glass.Eye.flipK line 507
  103. def OAI.ExactDerandomization.Glass.Eye.glare line 511
  104. lemma OAI.ExactDerandomization.Glass.Eye.glareK line 512
  105. def OAI.ExactDerandomization.Glass.Eye.fairp line 514
  106. def OAI.ExactDerandomization.Glass.Eye.fairm line 517
  107. def OAI.ExactDerandomization.Glass.Eye.Glare line 520
  108. def OAI.ExactDerandomization.Glass.Eye.Toggle line 521
  109. def OAI.ExactDerandomization.Glass.Eye.after line 522
  110. def OAI.ExactDerandomization.Glass.Eye.block line 527
  111. def OAI.ExactDerandomization.Glass.Eye.nexts line 529
  112. structure OAI.ExactDerandomization.Glass.Eye.Mantle line 533
  113. abbrev OAI.ExactDerandomization.Glass.Eye.Mantle.param line 542
  114. abbrev OAI.ExactDerandomization.Glass.Eye.Mantle.knot line 543
  115. abbrev OAI.ExactDerandomization.Glass.Eye.Mantle.wants line 544
  116. structure OAI.ExactDerandomization.Glass.Eye.Twirl line 547
  117. abbrev OAI.ExactDerandomization.Glass.Eye.Twirl.rod line 555
  118. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.idol line 556
  119. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.tint line 557
  120. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.looked line 562
  121. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.furl line 564
  122. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.moot line 573
  123. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.retina line 586
  124. abbrev OAI.ExactDerandomization.Glass.Eye.Twirl.condH line 609
  125. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.rosette line 611
  126. lemma OAI.ExactDerandomization.Glass.Eye.Twirl.blocks line 629
  127. theorem OAI.ExactDerandomization.Glass.Eye.Twirl.done0 line 644
  128. structure OAI.ExactDerandomization.Glass.Vase line 668

    Source documentation

    A visit whose (single) optional subterminal path is delegated. The hop tokens forward/back are determined by the selector's code, which belongs to a short range. Its pure action compiled at leaves can incorporate post label maps.

    structure Vase where
…
  129. def OAI.ExactDerandomization.Glass.Vase.start line 677
  130. def OAI.ExactDerandomization.Glass.Vase.fork line 679
  131. def OAI.ExactDerandomization.Glass.Vase.ahead line 680
  132. abbrev OAI.ExactDerandomization.Glass.Vase.Belt line 682
  133. def OAI.ExactDerandomization.Glass.Vase.budfeed line 683
  134. lemma OAI.ExactDerandomization.Glass.Vase.budK line 684
  135. def OAI.ExactDerandomization.Glass.Vase.seed line 685
  136. lemma OAI.ExactDerandomization.Glass.Vase.seedK line 687
  137. def OAI.ExactDerandomization.Glass.Vase.lance line 688
  138. def OAI.ExactDerandomization.Glass.Vase.headQ line 689
  139. def OAI.ExactDerandomization.Glass.Vase.lastQ line 690
  140. lemma OAI.ExactDerandomization.Glass.Vase.headK line 691
  141. lemma OAI.ExactDerandomization.Glass.Vase.lastK line 693
  142. def OAI.ExactDerandomization.Glass.Vase.dawn line 694
  143. def OAI.ExactDerandomization.Glass.Vase.cold0 line 695
  144. def OAI.ExactDerandomization.Glass.Vase.play line 696
  145. structure OAI.ExactDerandomization.Glass.Vase.Den line 698
  146. abbrev OAI.ExactDerandomization.Glass.Vase.Den.charge line 706
  147. def OAI.ExactDerandomization.Glass.Vase.Den.good line 707
  148. def OAI.ExactDerandomization.Glass.Vase.Den.pull line 708
  149. abbrev OAI.ExactDerandomization.Glass.Vase.Den.rootD line 709
  150. abbrev OAI.ExactDerandomization.Glass.Vase.Den.meets line 710
  151. def OAI.ExactDerandomization.Glass.Vase.Den.bit line 711
  152. abbrev OAI.ExactDerandomization.Glass.Vase.Den.atCall line 712
  153. lemma OAI.ExactDerandomization.Glass.Vase.Den.affordable line 713
  154. lemma OAI.ExactDerandomization.Glass.Vase.Den.fit line 719
  155. lemma OAI.ExactDerandomization.Glass.Vase.Den.sizeQ line 726
  156. lemma OAI.ExactDerandomization.Glass.Vase.Den.bsize line 727
  157. lemma OAI.ExactDerandomization.Glass.Vase.Den.bit0 line 731
  158. lemma OAI.ExactDerandomization.Glass.Vase.perform line 734
  159. lemma OAI.ExactDerandomization.Glass.Vase.arrives line 742
  160. lemma OAI.ExactDerandomization.Glass.Vase.failed line 771