OAI/Computability/MinUncut/Estimates/FiberPrefix.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MinUncut.Costed.FiberPrefix.scalar_code line 9
  2. lemma OAI.MinUncut.Costed.FiberPrefix.scalarâ‚‚_code line 17
  3. def OAI.MinUncut.Costed.FiberPrefix.args line 26
  4. lemma OAI.MinUncut.Costed.FiberPrefix.run_args line 27
  5. def OAI.MinUncut.Costed.FiberPrefix.step line 34
  6. lemma OAI.MinUncut.Costed.FiberPrefix.run_step line 36
  7. def OAI.MinUncut.Costed.FiberPrefix.state line 48
  8. lemma OAI.MinUncut.Costed.FiberPrefix.state_zero line 50
  9. lemma OAI.MinUncut.Costed.FiberPrefix.state_step line 51
  10. lemma OAI.MinUncut.Costed.FiberPrefix.magnitude_append line 56
  11. lemma OAI.MinUncut.Costed.FiberPrefix.magnitude_reverse line 60
  12. lemma OAI.MinUncut.Costed.FiberPrefix.magnitude_take line 64
  13. lemma OAI.MinUncut.Costed.FiberPrefix.state_size line 70
  14. def OAI.MinUncut.Costed.FiberPrefix.init line 76
  15. lemma OAI.MinUncut.Costed.FiberPrefix.run_init line 78
  16. def OAI.MinUncut.Costed.FiberPrefix.code line 88
  17. def OAI.MinUncut.Costed.FiberPrefix.transition line 90
  18. lemma OAI.MinUncut.Costed.FiberPrefix.iterate_state line 92
  19. lemma OAI.MinUncut.Costed.FiberPrefix.run_code line 99
  20. lemma OAI.MinUncut.Costed.FiberPrefix.exists_code line 159
  21. lemma OAI.MinUncut.Costed.Arena.listCells_ptr' line 176
  22. lemma OAI.MinUncut.Costed.Arena.listCells_get line 182
  23. lemma OAI.MinUncut.Costed.Arena.listCells_drop line 205
  24. def OAI.MinUncut.Costed.Arena.dataCells line 210
  25. lemma OAI.MinUncut.Costed.Arena.dataCells_length line 213
  26. lemma OAI.MinUncut.Costed.Arena.dataCells_eq_take line 214
  27. lemma OAI.MinUncut.Costed.Arena.listCells_split line 223
  28. def OAI.MinUncut.Costed.quadruple line 234
  29. lemma OAI.MinUncut.Costed.quadruple_length line 235
  30. def OAI.MinUncut.Costed.quadrupleWords line 238
  31. def OAI.MinUncut.Costed.quadrupleProgram line 240
  32. lemma OAI.MinUncut.Costed.quadruple_spec line 242
  33. def OAI.MinUncut.Costed.Arena.Init.input line 255
  34. def OAI.MinUncut.Costed.Arena.Init.countExpr line 258
  35. def OAI.MinUncut.Costed.Arena.Init.sizeExpr line 259
  36. def OAI.MinUncut.Costed.Arena.Init.restExpr line 260
  37. def OAI.MinUncut.Costed.Arena.Init.lengthExpr line 261
  38. lemma OAI.MinUncut.Costed.Arena.Init.input_drop line 263
  39. lemma OAI.MinUncut.Costed.Arena.Init.input_count line 267
  40. lemma OAI.MinUncut.Costed.Arena.Init.input_size line 269
  41. lemma OAI.MinUncut.Costed.Arena.Init.input_rest line 275
  42. lemma OAI.MinUncut.Costed.Arena.Init.input_length line 281
  43. lemma OAI.MinUncut.Costed.Arena.Init.input_lengthExpr line 284
  44. def OAI.MinUncut.Costed.Arena.Init.canvas line 288
  45. def OAI.MinUncut.Costed.Arena.Init.canvasWords line 290
  46. def OAI.MinUncut.Costed.Arena.Init.canvasProgram line 292
  47. lemma OAI.MinUncut.Costed.Arena.Init.canvasProgram_spec line 295
  48. lemma OAI.MinUncut.Costed.Arena.Init.canvas_length line 298
  49. lemma OAI.MinUncut.Costed.Arena.Init.canvas_drop line 301
  50. lemma OAI.MinUncut.Costed.Arena.Init.canvas_at line 309
  51. def OAI.MinUncut.Costed.Arena.Init.cExpr line 319
  52. def OAI.MinUncut.Costed.Arena.Init.mExpr line 320
  53. def OAI.MinUncut.Costed.Arena.Init.lExpr line 321
  54. def OAI.MinUncut.Costed.Arena.Init.iExpr line 322
  55. def OAI.MinUncut.Costed.Arena.Init.bExpr line 323
  56. def OAI.MinUncut.Costed.Arena.Init.rawCell line 324
  57. def OAI.MinUncut.Costed.Arena.Init.rawData line 326
  58. def OAI.MinUncut.Costed.Arena.Init.pointerExpr line 328
  59. def OAI.MinUncut.Costed.Arena.Init.isData line 329
  60. def OAI.MinUncut.Costed.Arena.Init.dataPointer line 330
  61. def OAI.MinUncut.Costed.Arena.Init.rowExpressions line 332
  62. def OAI.MinUncut.Costed.Arena.Init.baseLength line 336
  63. lemma OAI.MinUncut.Costed.Arena.Init.cExpr_eval line 338
  64. lemma OAI.MinUncut.Costed.Arena.Init.mExpr_eval line 340
  65. lemma OAI.MinUncut.Costed.Arena.Init.lExpr_eval line 342
  66. lemma OAI.MinUncut.Costed.Arena.Init.iExpr_eval line 344
  67. lemma OAI.MinUncut.Costed.Arena.Init.bExpr_eval line 346
  68. lemma OAI.MinUncut.Costed.Arena.Init.at_append line 349
  69. lemma OAI.MinUncut.Costed.Arena.Init.rawCell_eval line 354
  70. lemma OAI.MinUncut.Costed.Arena.Init.rawData_eval line 366
  71. lemma OAI.MinUncut.Costed.Arena.Init.pointerExpr_eval line 383
  72. lemma OAI.MinUncut.Costed.Arena.Init.row_data line 388
  73. lemma OAI.MinUncut.Costed.Arena.Init.row_code line 402
  74. def OAI.MinUncut.Costed.Arena.Init.newHeap line 424
  75. def OAI.MinUncut.Costed.Arena.Init.countRows line 428
  76. lemma OAI.MinUncut.Costed.Arena.Init.countRows_eval line 429
  77. lemma OAI.MinUncut.Costed.Arena.Init.map_drop_head line 432
  78. lemma OAI.MinUncut.Costed.Arena.Init.emitted_data line 441
  79. lemma OAI.MinUncut.Costed.Arena.Init.emitted_code line 451
  80. lemma OAI.MinUncut.Costed.Arena.Init.emitted_spec line 465
  81. lemma OAI.MinUncut.Costed.Arena.Init.newHeap_length line 472
  82. def OAI.MinUncut.Costed.Arena.Init.oldWords line 479
  83. def OAI.MinUncut.Costed.Arena.Init.base line 481
  84. lemma OAI.MinUncut.Costed.Arena.Init.oldWords_length line 483
  85. lemma OAI.MinUncut.Costed.Arena.Init.base_length line 488
  86. lemma OAI.MinUncut.Costed.Arena.Init.base_words line 492
  87. lemma OAI.MinUncut.Costed.Arena.Init.heap_match line 495
  88. def OAI.MinUncut.Costed.Arena.Init.canvasBase line 501
  89. def OAI.MinUncut.Costed.Arena.Init.canvasPc line 502
  90. def OAI.MinUncut.Costed.Arena.Init.canvasTotal line 503
  91. def OAI.MinUncut.Costed.Arena.Init.canvasEnv line 504
  92. def OAI.MinUncut.Costed.Arena.Init.header line 505
  93. lemma OAI.MinUncut.Costed.Arena.Init.canvasBase_eval line 506
  94. lemma OAI.MinUncut.Costed.Arena.Init.canvasPc_eval line 508
  95. lemma OAI.MinUncut.Costed.Arena.Init.canvasTotal_eval line 510
  96. lemma OAI.MinUncut.Costed.Arena.Init.canvasEnv_eval line 512
  97. lemma OAI.MinUncut.Costed.Arena.Init.header_match line 520
  98. def OAI.MinUncut.Costed.Arena.Init.initialized line 530
  99. def OAI.MinUncut.Costed.Arena.Init.initializer line 534
  100. lemma OAI.MinUncut.Costed.Arena.Init.initializer_spec line 536
  101. def OAI.MinUncut.Costed.UnaryWords.symbol line 550
  102. def OAI.MinUncut.Costed.UnaryWords.step line 552
  103. def OAI.MinUncut.Costed.UnaryWords.finish line 557
  104. def OAI.MinUncut.Costed.UnaryWords.body line 559
  105. def OAI.MinUncut.Costed.UnaryWords.symbolProgram line 561
  106. def OAI.MinUncut.Costed.UnaryWords.stepProgram line 563
  107. def OAI.MinUncut.Costed.UnaryWords.finishProgram line 573
  108. def OAI.MinUncut.Costed.UnaryWords.bodyProgram line 575
  109. lemma OAI.MinUncut.Costed.UnaryWords.step_safe line 579
  110. def OAI.MinUncut.Costed.UnaryWords.state line 590
  111. lemma OAI.MinUncut.Costed.UnaryWords.symbol_state line 592
  112. lemma OAI.MinUncut.Costed.UnaryWords.step_state line 598
  113. def OAI.MinUncut.Costed.UnaryWords.count line 605
  114. def OAI.MinUncut.Costed.UnaryWords.decodeAux line 609
  115. def OAI.MinUncut.Costed.UnaryWords.lastCounter line 613
  116. lemma OAI.MinUncut.Costed.UnaryWords.count_le line 617
  117. lemma OAI.MinUncut.Costed.UnaryWords.count_drop_head line 622
  118. lemma OAI.MinUncut.Costed.UnaryWords.iterate_state line 631
  119. lemma OAI.MinUncut.Costed.UnaryWords.count_drop_ne line 654
  120. lemma OAI.MinUncut.Costed.UnaryWords.iterate_shape line 666
  121. lemma OAI.MinUncut.Costed.UnaryWords.symbol_iterate line 677
  122. def OAI.MinUncut.Costed.UnaryWords.parsed line 682
  123. def OAI.MinUncut.Costed.UnaryWords.parseSize line 684
  124. lemma OAI.MinUncut.Costed.UnaryWords.iterate_size line 685
  125. lemma OAI.MinUncut.Costed.UnaryWords.finish_iterate line 702
  126. def OAI.MinUncut.Costed.UnaryWords.parserBound line 707
  127. lemma OAI.MinUncut.Costed.UnaryWords.run_parser line 710
  128. def OAI.MinUncut.Costed.UnaryWords.initializer line 734
  129. def OAI.MinUncut.Costed.UnaryWords.parserProgram line 737