OAI/Computability/Logspace/AllocationPrograms.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Guarded allocation and finite instruction interfaces for recursive queries.

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

  1. abbrev OAI.ExactDerandomization.Mint.Node line 18
  2. abbrev OAI.ExactDerandomization.Mint.Bean line 19
  3. structure OAI.ExactDerandomization.Mint.Rune line 21
  4. structure OAI.ExactDerandomization.Mint.Valve line 28
  5. structure OAI.ExactDerandomization.Mint.Mill line 39
  6. def OAI.ExactDerandomization.Mint.Mill.O line 45
  7. def OAI.ExactDerandomization.Mint.Mill.E0 line 46
  8. def OAI.ExactDerandomization.Mint.Mill.shoot line 47
  9. lemma OAI.ExactDerandomization.Mint.Mill.shootK line 48
  10. def OAI.ExactDerandomization.Mint.Mill.total line 49
  11. lemma OAI.ExactDerandomization.Mint.Mill.totalK line 50
  12. def OAI.ExactDerandomization.Mint.Mill.loanP line 54
  13. instance OAI.ExactDerandomization.Mint.Mill.loanD line 61
  14. def OAI.ExactDerandomization.Mint.Mill.loan line 62
  15. lemma OAI.ExactDerandomization.Mint.Mill.conj line 64
  16. lemma OAI.ExactDerandomization.Mint.Mill.loanK line 68
  17. def OAI.ExactDerandomization.Mint.Mill.axis line 81
  18. lemma OAI.ExactDerandomization.Mint.Mill.axisK line 82
  19. def OAI.ExactDerandomization.Mint.Mill.road line 84
  20. lemma OAI.ExactDerandomization.Mint.Mill.roadK line 88
  21. def OAI.ExactDerandomization.Mint.Mill.limits line 92
  22. lemma OAI.ExactDerandomization.Mint.Mill.limitsK line 94
  23. def OAI.ExactDerandomization.Mint.Mill.good0 line 96
  24. lemma OAI.ExactDerandomization.Mint.Mill.good0K line 104
  25. def OAI.ExactDerandomization.Mint.Mill.permit line 113
  26. lemma OAI.ExactDerandomization.Mint.Mill.permitK line 114
  27. def OAI.ExactDerandomization.Mint.Mill.bud line 117
  28. structure OAI.ExactDerandomization.Mint.Mill.Fuel line 120

    Source documentation

    semantic call responses

    structure Fuel where
…
  29. abbrev OAI.ExactDerandomization.Mint.Mill.price line 127
  30. abbrev OAI.ExactDerandomization.Mint.Mill.slipk line 128
  31. def OAI.ExactDerandomization.Mint.Mill.clay line 129
  32. abbrev OAI.ExactDerandomization.Mint.Mill.entitled line 133
  33. def OAI.ExactDerandomization.Mint.Mill.motor line 135
  34. structure OAI.ExactDerandomization.Mint.Mill.Fires line 139
  35. lemma OAI.ExactDerandomization.Mint.Mill.plusbase line 154
  36. lemma OAI.ExactDerandomization.Mint.Mill.lumax line 161
  37. lemma OAI.ExactDerandomization.Mint.Mill.cheaply line 167
  38. abbrev OAI.ExactDerandomization.Mint.Mill.view line 191
  39. abbrev OAI.ExactDerandomization.Mint.Mill.compo line 192
  40. abbrev OAI.ExactDerandomization.Mint.Mill.label line 193
  41. abbrev OAI.ExactDerandomization.Mint.Mill.wherep line 194
  42. abbrev OAI.ExactDerandomization.Mint.Mill.faith line 196
  43. abbrev OAI.ExactDerandomization.Mint.Mill.afoot line 197
  44. abbrev OAI.ExactDerandomization.Mint.Mill.swept line 199
  45. abbrev OAI.ExactDerandomization.Mint.Mill.swift line 201
  46. lemma OAI.ExactDerandomization.Mint.Mill.purity line 204
  47. lemma OAI.ExactDerandomization.Mint.Mill.bright line 206
  48. lemma OAI.ExactDerandomization.Mint.Mill.abroad line 210
  49. lemma OAI.ExactDerandomization.Mint.Mill.stamp line 221
  50. lemma OAI.ExactDerandomization.Mint.Mill.stampm line 223
  51. lemma OAI.ExactDerandomization.Mint.Mill.approved line 227
  52. lemma OAI.ExactDerandomization.Mint.Mill.Fires.tilt line 239
  53. abbrev OAI.ExactDerandomization.Mint.Mill.prize line 308
  54. def OAI.ExactDerandomization.Mint.Mill.Reserve line 309
  55. def OAI.ExactDerandomization.Mint.Mill.fitting line 310
  56. abbrev OAI.ExactDerandomization.Mint.Mill.minted line 312
  57. lemma OAI.ExactDerandomization.Mint.Mill.mem_of line 313
  58. lemma OAI.ExactDerandomization.Mint.Mill.bid line 318
  59. lemma OAI.ExactDerandomization.Mint.Mill.meets0 line 325
  60. lemma OAI.ExactDerandomization.Mint.Mill.meets1 line 331
  61. lemma OAI.ExactDerandomization.Mint.Mill.meets2 line 338
  62. abbrev OAI.ExactDerandomization.Mint.Mill.mate line 348
  63. lemma OAI.ExactDerandomization.Mint.Mill.cinder0 line 349
  64. lemma OAI.ExactDerandomization.Mint.Mill.cinder1 line 353