OAI/Computability/MinUncut/Estimates/PolynomialRecursor.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Costed.PolyProgram.scalarRec line 11
  2. def OAI.MinUncut.Costed.PolyProgram.prec line 15
  3. inductive OAI.MinUncut.Costed.Expr line 70
  4. def OAI.MinUncut.Costed.Expr.eval line 81
  5. def OAI.MinUncut.Costed.Expr.program line 92
  6. def OAI.MinUncut.Costed.Expr.or line 107
  7. def OAI.MinUncut.Costed.Expr.edge line 108
  8. lemma OAI.MinUncut.Costed.Expr.eval_or line 111
  9. lemma OAI.MinUncut.Costed.Expr.eval_cond line 113
  10. lemma OAI.MinUncut.Costed.Expr.eval_add line 115
  11. lemma OAI.MinUncut.Costed.Expr.eval_mul line 117
  12. lemma OAI.MinUncut.Costed.Expr.eval_reg line 119
  13. lemma OAI.MinUncut.Costed.Expr.eval_const line 120
  14. lemma OAI.MinUncut.Costed.Expr.eval_or_le_one line 122
  15. lemma OAI.MinUncut.Costed.Expr.eval_edge_le_one line 124
  16. lemma OAI.MinUncut.Costed.Expr.eval_edge line 130
  17. abbrev OAI.MinUncut.Costed.Arena.Node line 141
  18. abbrev OAI.MinUncut.Costed.Arena.Heap line 142
  19. def OAI.MinUncut.Costed.Arena.words line 144
  20. def OAI.MinUncut.Costed.Arena.read line 146
  21. lemma OAI.MinUncut.Costed.Arena.words_nil line 149
  22. lemma OAI.MinUncut.Costed.Arena.words_cons line 150
  23. lemma OAI.MinUncut.Costed.Arena.length_words line 154
  24. lemma OAI.MinUncut.Costed.Arena.words_drop line 159
  25. lemma OAI.MinUncut.Costed.Arena.words_at line 170
  26. lemma OAI.MinUncut.Costed.Arena.read_words line 179
  27. lemma OAI.MinUncut.Costed.Arena.read_null line 183
  28. lemma OAI.MinUncut.Costed.Arena.read_new line 185
  29. lemma OAI.MinUncut.Costed.Arena.read_old line 188
  30. def OAI.MinUncut.Costed.Arena.readExpr line 196
  31. lemma OAI.MinUncut.Costed.Arena.readExpr_eval line 201
  32. lemma OAI.MinUncut.Costed.Arena.magnitude_words_le line 214
  33. def OAI.MinUncut.Costed.Arena.node line 227
  34. lemma OAI.MinUncut.Costed.Arena.node_zero line 229
  35. lemma OAI.MinUncut.Costed.Arena.node_one line 230
  36. lemma OAI.MinUncut.Costed.Arena.node_two line 231
  37. lemma OAI.MinUncut.Costed.Arena.node_three line 232
  38. inductive OAI.MinUncut.Costed.Arena.ListRep line 234
  39. lemma OAI.MinUncut.Costed.Arena.ListRep.bound line 239
  40. lemma OAI.MinUncut.Costed.Arena.ListRep.head line 244
  41. lemma OAI.MinUncut.Costed.Arena.ListRep.tail line 249
  42. lemma OAI.MinUncut.Costed.Arena.ListRep.extend line 254
  43. lemma OAI.MinUncut.Costed.Arena.ListRep.push line 261
  44. inductive OAI.MinUncut.Costed.Arena.CodeAt line 267
  45. lemma OAI.MinUncut.Costed.Arena.CodeAt.bound line 280
  46. lemma OAI.MinUncut.Costed.Arena.CodeAt.extend line 282
  47. lemma OAI.MinUncut.Costed.Arena.ListRep.prepend line 303
  48. lemma OAI.MinUncut.Costed.Arena.CodeAt.prepend line 308
  49. def OAI.MinUncut.Costed.Arena.codeCells line 313
  50. lemma OAI.MinUncut.Costed.Arena.codeCells_spec line 333
  51. structure OAI.MinUncut.Costed.Arena.State line 393
  52. def OAI.MinUncut.Costed.Arena.State.encode line 400
  53. def OAI.MinUncut.Costed.Arena.State.tick line 403
  54. inductive OAI.MinUncut.Costed.Arena.Action line 430
  55. def OAI.MinUncut.Costed.Arena.Action.eval line 434
  56. def OAI.MinUncut.Costed.Arena.expressionList line 438
  57. def OAI.MinUncut.Costed.Arena.Action.program line 444
  58. abbrev OAI.MinUncut.Costed.Arena.r line 451
  59. abbrev OAI.MinUncut.Costed.Arena.c line 452
  60. abbrev OAI.MinUncut.Costed.Arena.g line 453
  61. abbrev OAI.MinUncut.Costed.Arena.n line 454
  62. abbrev OAI.MinUncut.Costed.Arena.fresh line 455
  63. def OAI.MinUncut.Costed.Arena.put line 457
  64. def OAI.MinUncut.Costed.Arena.alloc line 458
  65. def OAI.MinUncut.Costed.Arena.halt line 461
  66. def OAI.MinUncut.Costed.Arena.evalZero line 463
  67. def OAI.MinUncut.Costed.Arena.evalSucc line 464
  68. def OAI.MinUncut.Costed.Arena.evalTail line 465
  69. def OAI.MinUncut.Costed.Arena.evalCons line 466
  70. def OAI.MinUncut.Costed.Arena.evalComp line 467
  71. def OAI.MinUncut.Costed.Arena.evalCase line 468
  72. def OAI.MinUncut.Costed.Arena.evalFix line 471
  73. def OAI.MinUncut.Costed.Arena.switch line 473
  74. def OAI.MinUncut.Costed.Arena.evalAction line 477
  75. def OAI.MinUncut.Costed.Arena.retCons1 line 480
  76. def OAI.MinUncut.Costed.Arena.retCons2 line 482
  77. def OAI.MinUncut.Costed.Arena.retComp line 484
  78. def OAI.MinUncut.Costed.Arena.retFix line 485
  79. def OAI.MinUncut.Costed.Arena.returnAction line 488
  80. def OAI.MinUncut.Costed.Arena.tickAction line 491
  81. def OAI.MinUncut.Costed.Arena.rawTick line 494
  82. def OAI.MinUncut.Costed.Arena.tickProgram line 495
  83. lemma OAI.MinUncut.Costed.Arena.expr_reg_encode line 497
  84. lemma OAI.MinUncut.Costed.Arena.expr_read_encode line 501
  85. lemma OAI.MinUncut.Costed.Arena.put_encode line 505
  86. lemma OAI.MinUncut.Costed.Arena.alloc_encode line 511
  87. lemma OAI.MinUncut.Costed.Arena.encode_head line 519
  88. lemma OAI.MinUncut.Costed.Arena.encode_tail_head line 520
  89. lemma OAI.MinUncut.Costed.Arena.encode_reg0 line 521
  90. lemma OAI.MinUncut.Costed.Arena.encode_reg1 line 522
  91. lemma OAI.MinUncut.Costed.Arena.encode_reg2 line 523
  92. lemma OAI.MinUncut.Costed.Arena.encode_reg3 line 524
  93. lemma OAI.MinUncut.Costed.Arena.encode_reg4 line 525
  94. lemma OAI.MinUncut.Costed.Arena.rawTick_encode line 527
  95. def OAI.MinUncut.Costed.Arena.maximum line 558
  96. lemma OAI.MinUncut.Costed.Arena.maximum_nil line 559
  97. lemma OAI.MinUncut.Costed.Arena.maximum_cons line 560
  98. lemma OAI.MinUncut.Costed.Arena.maximum_append line 562
  99. lemma OAI.MinUncut.Costed.Arena.maximum_drop line 567
  100. lemma OAI.MinUncut.Costed.Arena.head_le_maximum line 575
  101. lemma OAI.MinUncut.Costed.Arena.maximum_le_magnitude line 580
  102. lemma OAI.MinUncut.Costed.Arena.length_le_magnitude line 585
  103. lemma OAI.MinUncut.Costed.Arena.magnitude_le_length_maximum line 590
  104. lemma OAI.MinUncut.Costed.Arena.reg_le_maximum line 600
  105. lemma OAI.MinUncut.Costed.Arena.get_le_maximum line 603
  106. def OAI.MinUncut.Costed.Arena.Small line 611
  107. lemma OAI.MinUncut.Costed.Arena.small_reg line 612
  108. lemma OAI.MinUncut.Costed.Arena.small_get line 613
  109. lemma OAI.MinUncut.Costed.Arena.small_const line 614
  110. lemma OAI.MinUncut.Costed.Arena.small_fresh line 615
  111. lemma OAI.MinUncut.Costed.Arena.small_succ_get line 619
  112. lemma OAI.MinUncut.Costed.Arena.small_pred_get line 623
  113. def OAI.MinUncut.Costed.Arena.Action.Safe line 628
  114. lemma OAI.MinUncut.Costed.Arena.maximum_map_small line 631
  115. lemma OAI.MinUncut.Costed.Arena.Action.Safe.put line 639
  116. lemma OAI.MinUncut.Costed.Arena.Action.Safe.test line 648
  117. lemma OAI.MinUncut.Costed.Arena.safe_put line 654
  118. lemma OAI.MinUncut.Costed.Arena.safe_alloc line 666
  119. lemma OAI.MinUncut.Costed.Arena.safe_halt line 684
  120. lemma OAI.MinUncut.Costed.Arena.safe_switch line 687
  121. lemma OAI.MinUncut.Costed.Arena.safe_evalAction line 694
  122. lemma OAI.MinUncut.Costed.Arena.safe_returnAction line 705
  123. lemma OAI.MinUncut.Costed.Arena.rawTick_safe line 716
  124. lemma OAI.MinUncut.Costed.Arena.rawTick_iter_bounds line 721
  125. lemma OAI.MinUncut.Costed.Arena.rawTick_iter_magnitude line 730
  126. def OAI.MinUncut.Costed.Arena.boundedInterpreter line 743