OAI/Computability/Logspace/HierarchyEvaluation.lean

GitHub source file

283 declarations, 0 contain sorry, 0 declared as axioms

Correctness and space bounds of recursive hierarchy evaluation.

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

  1. structure OAI.ExactDerandomization.Chron.Moon line 24
  2. abbrev OAI.ExactDerandomization.Chron.Moon.cageX line 31
  3. abbrev OAI.ExactDerandomization.Chron.Moon.a line 32
  4. abbrev OAI.ExactDerandomization.Chron.Moon.d line 33
  5. abbrev OAI.ExactDerandomization.Chron.Moon.c line 34
  6. abbrev OAI.ExactDerandomization.Chron.Moon.sE line 35
  7. abbrev OAI.ExactDerandomization.Chron.Moon.s line 36
  8. structure OAI.ExactDerandomization.Chron.Moon.Lo line 37
  9. lemma OAI.ExactDerandomization.Chron.Moon.baseD line 45
  10. lemma OAI.ExactDerandomization.Chron.Moon.Lo.ed line 49
  11. lemma OAI.ExactDerandomization.Chron.Moon.Lo.wpaid line 50
  12. lemma OAI.ExactDerandomization.Chron.Moon.Lo.test line 51
  13. def OAI.ExactDerandomization.Chron.Moon.stash line 53
  14. lemma OAI.ExactDerandomization.Chron.Moon.heap line 57
  15. lemma OAI.ExactDerandomization.Chron.Moon.cam line 64
  16. lemma OAI.ExactDerandomization.Chron.Moon.loomF line 67
  17. structure OAI.ExactDerandomization.Chron.Coinage line 74
  18. abbrev OAI.ExactDerandomization.Chron.Coinage.i line 78
  19. abbrev OAI.ExactDerandomization.Chron.Coinage.p line 79
  20. abbrev OAI.ExactDerandomization.Chron.Coinage.fired line 80
  21. def OAI.ExactDerandomization.Chron.Coinage.pigment line 81
  22. def OAI.ExactDerandomization.Chron.Coinage.dies line 82
  23. structure OAI.ExactDerandomization.Chron.Moon.Spend line 86
  24. lemma OAI.ExactDerandomization.Chron.Moon.Spend.briefly line 97
  25. lemma OAI.ExactDerandomization.Chron.Moon.cold line 104
  26. lemma OAI.ExactDerandomization.Chron.Moon.dun line 131
  27. abbrev OAI.ExactDerandomization.Chron.Moon.tideC line 164
  28. abbrev OAI.ExactDerandomization.Chron.Moon.ny line 165
  29. abbrev OAI.ExactDerandomization.Chron.Moon.zone line 166
  30. lemma OAI.ExactDerandomization.Chron.Moon.formQ line 167
  31. abbrev OAI.ExactDerandomization.Chron.Moon.played line 170
  32. lemma OAI.ExactDerandomization.Chron.Moon.parked line 172
  33. def OAI.ExactDerandomization.Chron.Moon.walking line 176
  34. lemma OAI.ExactDerandomization.Chron.Moon.sunny line 179
  35. lemma OAI.ExactDerandomization.Chron.Moon.zeda line 182
  36. lemma OAI.ExactDerandomization.Chron.Moon.zedo line 183
  37. lemma OAI.ExactDerandomization.Chron.Moon.Lo.zenith line 188
  38. lemma OAI.ExactDerandomization.Chron.Moon.Lo.city line 193
  39. lemma OAI.ExactDerandomization.Chron.Moon.Lo.ending line 202
  40. lemma OAI.ExactDerandomization.Chron.Moon.Lo.equinox line 210
  41. lemma OAI.ExactDerandomization.Chron.Moon.Lo.terra line 224
  42. lemma OAI.ExactDerandomization.Chron.Moon.Lo.join line 232
  43. lemma OAI.ExactDerandomization.Chron.Moon.armleg line 239
  44. structure OAI.ExactDerandomization.Chron.Moon.Weather line 263
  45. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.φ line 269
  46. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.raysQ line 270
  47. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.scroll line 271
  48. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.spark0 line 272
  49. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.job0 line 273
  50. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.d0 line 274
  51. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.hullC line 275
  52. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.lane0 line 276
  53. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.windP line 277
  54. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.α line 278
  55. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.β line 279
  56. def OAI.ExactDerandomization.Chron.Moon.Weather.arcQ line 280
  57. def OAI.ExactDerandomization.Chron.Moon.Weather.forced line 283
  58. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.vol line 284
  59. lemma OAI.ExactDerandomization.Chron.Moon.Weather.helm0 line 286
  60. lemma OAI.ExactDerandomization.Chron.Moon.Weather.spokenE line 287
  61. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.house line 308
  62. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.step0 line 310
  63. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.cost0 line 312
  64. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.cards line 315
  65. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.early0 line 324
  66. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.sigmas line 326
  67. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.sphere line 331
  68. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.stanza line 351
  69. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.humid line 359
  70. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.braid line 373
  71. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.itemized line 377
  72. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.calm line 381
  73. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.shareq line 385
  74. lemma OAI.ExactDerandomization.Chron.Moon.Weather.forced.sharesC line 389
  75. lemma OAI.ExactDerandomization.Chron.Moon.FogX.plain line 406
  76. lemma OAI.ExactDerandomization.Chron.Moon.FogX.alleG line 407
  77. structure OAI.ExactDerandomization.Chron.Moon.Weather.Ship line 435
  78. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Ship.cage line 440
  79. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Ship.src line 441
  80. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Ship.aimP line 442
  81. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Ship.scholar line 443
  82. structure OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed line 444
  83. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed.mom line 451
  84. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed.here1 line 454
  85. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed.here0 line 455
  86. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed.pricey line 456
  87. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed.tempo line 458
  88. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Ship.Armed.stop line 463
  89. structure OAI.ExactDerandomization.Chron.Moon.Weather.Pale line 471

    Source documentation

    One fixed incoming port/s station op, varying endpoint ray index j of second. First score and MAX-prefix values supplied whenever first starts. Not depending on j.

    structure Pale (e:Chron.Moon u)where
…

    Mentions: OAI.ExactDerandomization.Chron.Moon

  90. def OAI.ExactDerandomization.Chron.Moon.Weather.Pale.surf line 487
  91. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.warm line 488
  92. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.astro line 489
  93. def OAI.ExactDerandomization.Chron.Moon.Weather.Pale.prodQ line 490
  94. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.crop line 491
  95. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.front line 492
  96. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.ash line 493
  97. def OAI.ExactDerandomization.Chron.Moon.Weather.Pale.rest line 495
  98. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.medal line 496
  99. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.harvest0 line 497
  100. def OAI.ExactDerandomization.Chron.Moon.Weather.Pale.grade0 line 499
  101. structure OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span line 502
  102. structure OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Kin line 513
  103. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.forming line 528
  104. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.launch line 548

    Source documentation

    Successful captures and their time-independent guard conditions.

    lemma launch  :
    v.front=true ↔ v.x ∈ e.v.S0∧e.played v.k.b v.x v.k.scroll true=true:=h0.helm.1.city _ _ rfl _
  105. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.leading line 550
  106. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.harvest line 555
  107. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.mayor line 579
  108. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.boltQ line 609
  109. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.meterB line 610
  110. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.screenP line 613
  111. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.peel line 614
  112. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pale.goodY line 615
  113. def OAI.ExactDerandomization.Chron.Moon.Weather.Pale.till line 617
  114. def OAI.ExactDerandomization.Chron.Moon.Weather.Pale.seekR line 618
  115. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.fee line 624
  116. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.upG line 632
  117. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.downG line 636
  118. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.fizzle line 639
  119. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.haze line 651
  120. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.dueP line 653
  121. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.architect line 687
  122. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Kin.worn line 732
  123. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Kin.draft line 750
  124. structure OAI.ExactDerandomization.Chron.Moon.Weather.Crude line 816

    Source documentation

    recursive premises needed for one order data/pulses.

    structure Crude : Prop where
…
  125. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Crude.taken line 826
  126. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Crude.caul line 833
  127. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.regionQ line 854
  128. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.simple line 856
  129. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.Span.listP line 868
  130. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.boostOne line 877
  131. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pale.windId line 887
  132. def OAI.ExactDerandomization.Chron.Moon.Weather.prize line 892

    Source comment

    Bucket equations sum over endpoint for each first port, then firsts.
    def prize(v:Weather e)(x y:ℕ):Pt:=
…

    Mentions: OAI.ExactDerandomization.Chron.Moon.Weather

  133. lemma OAI.ExactDerandomization.Chron.Moon.Weather.worth line 894
  134. structure OAI.ExactDerandomization.Chron.Moon.Weather.Carnival line 900
  135. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.creditD line 905
  136. lemma OAI.ExactDerandomization.Chron.Moon.Weather.only0 line 907
  137. lemma OAI.ExactDerandomization.Chron.Moon.Weather.solace line 908
  138. lemma OAI.ExactDerandomization.Chron.Moon.Weather.festival line 928
  139. structure OAI.ExactDerandomization.Chron.Moon.Weather.Single.Aim line 961
  140. def OAI.ExactDerandomization.Chron.Moon.Weather.Single.nave line 971
  141. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Single.Aim.bears line 978
  142. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Single.Aim.partake line 1001
  143. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Single.Aim.festival1 line 1014
  144. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Single.companion line 1021
  145. structure OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX line 1086
  146. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.cash line 1094
  147. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.circle line 1101
  148. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.safe line 1103
  149. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.joint line 1111
  150. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.chop line 1121
  151. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.door line 1129
  152. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.spiral line 1132
  153. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.potC line 1140
  154. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.wing line 1147
  155. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.beams line 1159
  156. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.actor line 1162
  157. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.lastC line 1197
  158. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Pairing.ahead line 1259
  159. def OAI.ExactDerandomization.Chron.Moon.Weather.Pairing.servants line 1260
  160. structure OAI.ExactDerandomization.Chron.Moon.Weather.Pairing.Union4 line 1264
  161. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pairing.Union4.forms line 1280
  162. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pairing.Union4.royalty line 1325
  163. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pairing.Union4.bills line 1373
  164. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Pore.MillX.mix4 line 1400
  165. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Royal.M line 1473
  166. def OAI.ExactDerandomization.Chron.Moon.Weather.Royal.stain line 1474
  167. abbrev OAI.ExactDerandomization.Chron.Moon.Weather.Royal.wreath line 1476
  168. def OAI.ExactDerandomization.Chron.Moon.Weather.Royal.lace line 1477
  169. def OAI.ExactDerandomization.Chron.Moon.Weather.Royal.pick line 1479
  170. def OAI.ExactDerandomization.Chron.Moon.Weather.Royal.ratchet line 1480
  171. structure OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona line 1484
  172. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.tokenM line 1501
  173. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.cardK line 1506
  174. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.alive line 1507
  175. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.cornea line 1516
  176. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.labour line 1530
  177. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.royale line 1608
  178. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.Corona.spiral line 1627
  179. lemma OAI.ExactDerandomization.Chron.Moon.Weather.Royal.roadCrew line 1653
  180. lemma OAI.ExactDerandomization.Chron.Moon.Weather.rally line 1735
  181. abbrev OAI.ExactDerandomization.Chron.Moon.rear0 line 1773
  182. abbrev OAI.ExactDerandomization.Chron.Moon.firstG line 1774
  183. structure OAI.ExactDerandomization.Chron.Moon.Recent.Ink line 1779
  184. abbrev OAI.ExactDerandomization.Chron.Moon.Recent.Ink.u0 line 1783
  185. abbrev OAI.ExactDerandomization.Chron.Moon.Recent.Ink.frame0 line 1784
  186. abbrev OAI.ExactDerandomization.Chron.Moon.Recent.Ink.pos line 1785
  187. def OAI.ExactDerandomization.Chron.Moon.Recent.Ink.pulse line 1786
  188. abbrev OAI.ExactDerandomization.Chron.Moon.Recent.Ink.word line 1787
  189. abbrev OAI.ExactDerandomization.Chron.Moon.Recent.Ink.s line 1788
  190. structure OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints line 1789
  191. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.turn0 line 1798
  192. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.board line 1804
  193. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.teeth line 1809
  194. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.history line 1814
  195. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.legacy line 1822
  196. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.harvested line 1874
  197. def OAI.ExactDerandomization.Chron.Moon.Local.ready line 1920
  198. abbrev OAI.ExactDerandomization.Chron.Moon.Local.seed line 1921
  199. def OAI.ExactDerandomization.Chron.Moon.Local.interim line 1923
  200. abbrev OAI.ExactDerandomization.Chron.Moon.Local.ucanon line 1926
  201. lemma OAI.ExactDerandomization.Chron.Moon.Local.knows line 1927
  202. lemma OAI.ExactDerandomization.Chron.Moon.Local.seekRead line 1940
  203. lemma OAI.ExactDerandomization.Chron.Moon.Local.flair line 1946
  204. abbrev OAI.ExactDerandomization.Chron.Moon.Local.trueW line 1950
  205. def OAI.ExactDerandomization.Chron.Moon.Local.sell line 1951
  206. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.home0 line 1959
  207. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.truthX line 1960
  208. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.extentA line 1974
  209. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.cash line 1983
  210. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.minted line 1998
  211. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.illustrious line 2018
  212. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.kindness line 2041
  213. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.crystal line 2059
  214. def OAI.ExactDerandomization.Chron.Moon.basepart line 2126
  215. lemma OAI.ExactDerandomization.Chron.Moon.basef line 2128
  216. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.remits line 2154
  217. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.taunted line 2166
  218. lemma OAI.ExactDerandomization.Chron.Moon.Local.Ready.total line 2179
  219. lemma OAI.ExactDerandomization.Chron.Moon.rains0 line 2221
  220. def OAI.ExactDerandomization.Chron.Moon.Recent.Ink.diffq line 2271
  221. def OAI.ExactDerandomization.Chron.Moon.Recent.Ink.turns line 2272
  222. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.existent line 2278
  223. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.teach line 2280
  224. lemma OAI.ExactDerandomization.Chron.Moon.Recent.Ink.Prints.total line 2351
  225. structure OAI.ExactDerandomization.Chron.Moon.Fields line 2402
  226. def OAI.ExactDerandomization.Chron.Moon.Fields.rain line 2407
  227. def OAI.ExactDerandomization.Chron.Moon.Fields.meet line 2408
  228. def OAI.ExactDerandomization.Chron.Moon.Fields.empty line 2409
  229. lemma OAI.ExactDerandomization.Chron.Moon.Fields.flooded line 2410
  230. def OAI.ExactDerandomization.Chron.Moon.Fields.fine line 2418
  231. structure OAI.ExactDerandomization.Chron.Moon.Fields.Good line 2419
  232. lemma OAI.ExactDerandomization.Chron.Moon.Fields.Good.fused line 2424
  233. lemma OAI.ExactDerandomization.Chron.Moon.Fields.Good.apart line 2432
  234. lemma OAI.ExactDerandomization.Chron.Moon.Fields.Good.fairM line 2434
  235. def OAI.ExactDerandomization.Chron.Moon.Fields.meadow line 2443
  236. lemma OAI.ExactDerandomization.Chron.Moon.Fields.meadowed line 2445
  237. lemma OAI.ExactDerandomization.Chron.Moon.Fields.parkS line 2449
  238. lemma OAI.ExactDerandomization.Chron.Moon.Fields.floraC line 2454
  239. lemma OAI.ExactDerandomization.Chron.Moon.Fields.flushed line 2459
  240. abbrev OAI.ExactDerandomization.Chron.Moon.signE line 2465
  241. structure OAI.ExactDerandomization.Chron.Moon.Spirit line 2466
  242. lemma OAI.ExactDerandomization.Chron.Moon.Spirit.lamp line 2474
  243. lemma OAI.ExactDerandomization.Chron.Moon.reties line 2498
  244. structure OAI.ExactDerandomization.Chron.Moon.Rise line 2499
  245. lemma OAI.ExactDerandomization.Chron.Moon.appears line 2503
  246. structure OAI.ExactDerandomization.Chron.Moon.Frolic line 2530
  247. lemma OAI.ExactDerandomization.Chron.Moon.smeared line 2535
  248. lemma OAI.ExactDerandomization.Chron.Moon.frolic line 2541
  249. abbrev OAI.ExactDerandomization.Chron.Bevel.proofL line 2584
  250. def OAI.ExactDerandomization.Chron.Bevel.Thurs line 2585
  251. def OAI.ExactDerandomization.Chron.Bevel.supplyC line 2587
  252. abbrev OAI.ExactDerandomization.Chron.Bevel.June line 2590
  253. def OAI.ExactDerandomization.Chron.Bevel.sky line 2591
  254. abbrev OAI.ExactDerandomization.Chron.Bevel.headK line 2593
  255. abbrev OAI.ExactDerandomization.Chron.Bevel.rentG line 2594
  256. def OAI.ExactDerandomization.Chron.Bevel.median line 2596
  257. lemma OAI.ExactDerandomization.Chron.Bevel.estate line 2598
  258. abbrev OAI.ExactDerandomization.Chron.Moon.homeE line 2613
  259. abbrev OAI.ExactDerandomization.Chron.Moon.serve line 2614
  260. structure OAI.ExactDerandomization.Chron.Moon.Back line 2615
  261. structure OAI.ExactDerandomization.Chron.Moon.Spire line 2621
  262. abbrev OAI.ExactDerandomization.Chron.Moon.Spire.C line 2628
  263. abbrev OAI.ExactDerandomization.Chron.Moon.Spire.k0 line 2629
  264. abbrev OAI.ExactDerandomization.Chron.Moon.Spire.tB line 2630
  265. lemma OAI.ExactDerandomization.Chron.Moon.Spire.stableA line 2631
  266. lemma OAI.ExactDerandomization.Chron.Moon.Spire.pin line 2636
  267. lemma OAI.ExactDerandomization.Chron.Moon.Spire.tips line 2640
  268. lemma OAI.ExactDerandomization.Chron.Moon.Spire.echoU line 2643
  269. lemma OAI.ExactDerandomization.Chron.Moon.Spire.blank line 2650
  270. lemma OAI.ExactDerandomization.Chron.Moon.Spire.ante line 2660
  271. lemma OAI.ExactDerandomization.Chron.Moon.Spire.projectB line 2691
  272. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.genc line 2753
  273. def OAI.ExactDerandomization.Chron.Moon.Moonlit.limit line 2754
  274. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.koa line 2755
  275. def OAI.ExactDerandomization.Chron.Moon.Moonlit.spread line 2757
  276. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.kinship line 2759
  277. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.begins line 2767
  278. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.summer line 2770
  279. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.emits line 2778
  280. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.terminal line 2785
  281. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.cloud line 2791
  282. lemma OAI.ExactDerandomization.Chron.Moon.Moonlit.enrolled line 2810
  283. lemma OAI.ExactDerandomization.Chron.Moon.nursery line 2852

    Source documentation

    instruction-bound local derivation.

    lemma nursery (h:Weather.Crude e)(hs:e.Spire)
     (ho:∀ x∈u.D.P,∀ j,e.i=j+1→∃ t:e.v.Hinge e.p j x,e.v.HFine e.p j x t):
   ∀ x∈u.D.P,∃ t:e.v.Yolk e.p e.i x,e.v.YFine e.p e.i x t∧∀ j,t.raw.tag j ≤ Era.budget u.r:=by
…

    Mentions: OAI.ExactDerandomization.Chron.Moon.Weather.Crude