OAI/Computability/MinUncut/Estimates/CodeComputability.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncut.CodeEffective.NCode line 8
  2. def OAI.MinUncut.CodeEffective.embed line 10
  3. def OAI.MinUncut.CodeEffective.retract line 19
  4. lemma OAI.MinUncut.CodeEffective.retract_embed line 28
  5. def OAI.MinUncut.CodeEffective.normalize line 31
  6. lemma OAI.MinUncut.CodeEffective.primrec_normalize line 32
  7. instance OAI.MinUncut.CodeEffective.(instance at line 51) line 51
  8. lemma OAI.MinUncut.CodeEffective.primrec_embed line 63
  9. lemma OAI.MinUncut.CodeEffective.primrec_retract line 67
  10. lemma OAI.MinUncut.CodeEffective.primrec_cons line 71
  11. lemma OAI.MinUncut.CodeEffective.primrec_comp line 77
  12. lemma OAI.MinUncut.CodeEffective.primrec_case line 82
  13. lemma OAI.MinUncut.CodeEffective.primrec_fix line 87
  14. lemma OAI.MinUncut.CodeEffective.computable_cons line 91
  15. lemma OAI.MinUncut.CodeEffective.computable_comp line 92
  16. lemma OAI.MinUncut.CodeEffective.computable_case line 93
  17. lemma OAI.MinUncut.CodeEffective.computable_fix line 94
  18. def OAI.MinUncut.Costed.bitsize line 100
  19. inductive OAI.MinUncut.Costed.CodeRun line 102
  20. theorem OAI.MinUncut.Costed.CodeRun.sound line 120
  21. theorem OAI.MinUncut.Costed.CodeRun.complete line 145
  22. lemma OAI.MinUncut.Costed.trPosNum_length_le line 220
  23. lemma OAI.MinUncut.Costed.trNum_length_le line 231
  24. lemma OAI.MinUncut.Costed.trNat_length_le line 236
  25. def OAI.MinUncut.Costed.magnitude line 240
  26. lemma OAI.MinUncut.Costed.magnitude_nil line 242
  27. lemma OAI.MinUncut.Costed.magnitude_cons line 243
  28. lemma OAI.MinUncut.Costed.magnitude_head line 244
  29. lemma OAI.MinUncut.Costed.magnitude_tail line 246
  30. lemma OAI.MinUncut.Costed.magnitude_drop line 248
  31. lemma OAI.MinUncut.Costed.bitsize_le_magnitude line 254
  32. lemma OAI.MinUncut.Costed.magnitude_length line 262
  33. def OAI.MinUncut.Costed.Runs line 267
  34. lemma OAI.MinUncut.Costed.Runs.mono line 270
  35. lemma OAI.MinUncut.Costed.Runs.sound line 273
  36. lemma OAI.MinUncut.Costed.run_zero line 275
  37. lemma OAI.MinUncut.Costed.run_succ line 276
  38. lemma OAI.MinUncut.Costed.run_tail line 278
  39. lemma OAI.MinUncut.Costed.run_comp line 280
  40. lemma OAI.MinUncut.Costed.run_cons line 285
  41. lemma OAI.MinUncut.Costed.run_id line 294
  42. lemma OAI.MinUncut.Costed.run_nil line 298
  43. lemma OAI.MinUncut.Costed.run_head line 305
  44. lemma OAI.MinUncut.Costed.run_const_zero line 309
  45. lemma OAI.MinUncut.Costed.run_caseZero line 316
  46. lemma OAI.MinUncut.Costed.run_caseSucc line 320
  47. lemma OAI.MinUncut.Costed.run_pred line 325
  48. def OAI.MinUncut.Costed.dropCode line 339
  49. lemma OAI.MinUncut.Costed.run_drop line 343
  50. def OAI.MinUncut.Costed.atCode line 355
  51. lemma OAI.MinUncut.Costed.run_at line 356
  52. def OAI.MinUncut.Costed.constCode line 363
  53. lemma OAI.MinUncut.Costed.run_const line 367
  54. lemma OAI.MinUncut.Costed.run_fix_bounded line 377
  55. def OAI.MinUncut.Costed.dynamicDropBody line 406
  56. def OAI.MinUncut.Costed.dynamicDrop line 408
  57. lemma OAI.MinUncut.Costed.run_dynamicDropBody_zero line 410
  58. lemma OAI.MinUncut.Costed.run_dynamicDropBody_succ line 414
  59. lemma OAI.MinUncut.Costed.run_dynamicDrop line 425
  60. def OAI.MinUncut.Costed.dynamicAt line 445
  61. lemma OAI.MinUncut.Costed.run_dynamicAt line 446
  62. def OAI.MinUncut.Costed.precBody line 457
  63. lemma OAI.MinUncut.Costed.run_precBody line 461
  64. lemma OAI.MinUncut.Costed.run_precLoop line 477
  65. lemma OAI.MinUncut.Costed.run_prec line 501
  66. lemma OAI.MinUncut.Costed.evalNat_mono line 538
  67. structure OAI.MinUncut.Costed.PolyProgram line 544
  68. def OAI.MinUncut.Costed.PolyProgram.id line 553
  69. def OAI.MinUncut.Costed.PolyProgram.tail line 559
  70. def OAI.MinUncut.Costed.PolyProgram.head line 565
  71. def OAI.MinUncut.Costed.PolyProgram.nil line 571
  72. def OAI.MinUncut.Costed.PolyProgram.zero line 577
  73. def OAI.MinUncut.Costed.PolyProgram.succ line 583
  74. def OAI.MinUncut.Costed.PolyProgram.pred line 589
  75. def OAI.MinUncut.Costed.PolyProgram.const line 595
  76. def OAI.MinUncut.Costed.PolyProgram.drop line 601
  77. def OAI.MinUncut.Costed.PolyProgram.projection line 607
  78. def OAI.MinUncut.Costed.PolyProgram.comp line 613
  79. def OAI.MinUncut.Costed.PolyProgram.cons line 626
  80. def OAI.MinUncut.Costed.PolyProgram.ofEq line 641
  81. def OAI.MinUncut.Costed.PolyProgram.branch line 651
  82. def OAI.MinUncut.Costed.PolyProgram.collect line 682
  83. def OAI.MinUncut.Costed.PolyProgram.replace line 688