OAI/Computability/PerfectCompleteness/Machines/ExactTargetOdometer.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ExactTargetOdometer.setCoordinate line 21
  2. theorem OAI.PerfectCompleteness.ExactTargetOdometer.setCoordinate_self line 25
  3. theorem OAI.PerfectCompleteness.ExactTargetOdometer.setCoordinate_eq_update line 30
  4. theorem OAI.PerfectCompleteness.ExactTargetOdometer.setCoordinate_zero line 40
  5. def OAI.PerfectCompleteness.ExactTargetOdometer.fillCoordinates line 50
  6. theorem OAI.PerfectCompleteness.ExactTargetOdometer.fillCoordinates_zero line 54
  7. theorem OAI.PerfectCompleteness.ExactTargetOdometer.fillCoordinates_all line 59
  8. theorem OAI.PerfectCompleteness.ExactTargetOdometer.fillCoordinates_snoc line 64
  9. def OAI.PerfectCompleteness.ExactTargetOdometer.visits line 77
  10. theorem OAI.PerfectCompleteness.ExactTargetOdometer.visits_eq_tupleOrder line 82
  11. theorem OAI.PerfectCompleteness.ExactTargetOdometer.visits_all line 98
  12. def OAI.PerfectCompleteness.ExactTargetOdometer.foldVisits line 106
  13. theorem OAI.PerfectCompleteness.ExactTargetOdometer.foldVisits_zero line 110
  14. def OAI.PerfectCompleteness.ExactTargetOdometer.blockPrefix line 114
  15. theorem OAI.PerfectCompleteness.ExactTargetOdometer.blockPrefix_zero line 119
  16. theorem OAI.PerfectCompleteness.ExactTargetOdometer.blockPrefix_succ line 123
  17. theorem OAI.PerfectCompleteness.ExactTargetOdometer.blockPrefix_all line 133
  18. theorem OAI.PerfectCompleteness.ExactTargetOdometer.visits_sourceOrder line 143
  19. theorem OAI.PerfectCompleteness.ExactTargetOdometer.visits_completedOrder line 153
  20. def OAI.PerfectCompleteness.ExactTargetOdometer.baseTapes line 167
  21. theorem OAI.PerfectCompleteness.ExactTargetOdometer.baseTapes_input line 176
  22. theorem OAI.PerfectCompleteness.ExactTargetOdometer.baseTapes_edgeWork line 190
  23. theorem OAI.PerfectCompleteness.ExactTargetOdometer.baseTapes_emptyWork line 195
  24. def OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes line 208
  25. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_table line 216
  26. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_current line 222
  27. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_remaining line 228
  28. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_output line 235
  29. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_count line 241
  30. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_extra line 247
  31. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_input line 253
  32. theorem OAI.PerfectCompleteness.ExactTargetOdometer.nativeTapes_emptyWork line 261
  33. theorem OAI.PerfectCompleteness.ExactTargetOdometer.digitTapes_nativeTapes line 268
  34. inductive OAI.PerfectCompleteness.ExactTargetOdometer.Label line 326
  35. abbrev OAI.PerfectCompleteness.ExactTargetOdometer.Control line 346
  36. abbrev OAI.PerfectCompleteness.ExactTargetOdometer.Ambient line 347
  37. abbrev OAI.PerfectCompleteness.ExactTargetOdometer.NativeLabel line 348
  38. def OAI.PerfectCompleteness.ExactTargetOdometer.checkAt line 357
  39. def OAI.PerfectCompleteness.ExactTargetOdometer.resetAt line 360
  40. def OAI.PerfectCompleteness.ExactTargetOdometer.currentAt line 363
  41. def OAI.PerfectCompleteness.ExactTargetOdometer.remainingAt line 366
  42. def OAI.PerfectCompleteness.ExactTargetOdometer.body line 369
  43. def OAI.PerfectCompleteness.ExactTargetOdometer.program line 371
  44. def OAI.PerfectCompleteness.ExactTargetOdometer.tupleStep line 384
  45. theorem OAI.PerfectCompleteness.ExactTargetOdometer.tupleStep_count line 395
  46. theorem OAI.PerfectCompleteness.ExactTargetOdometer.tupleStep_eq line 401
  47. def OAI.PerfectCompleteness.ExactTargetOdometer.configuration line 420
  48. def OAI.PerfectCompleteness.ExactTargetOdometer.leafBudget line 428
  49. def OAI.PerfectCompleteness.ExactTargetOdometer.leafInTime line 436
  50. def OAI.PerfectCompleteness.ExactTargetOdometer.maxLeafBudget line 452
  51. def OAI.PerfectCompleteness.ExactTargetOdometer.CostsAtMost line 460
  52. theorem OAI.PerfectCompleteness.ExactTargetOdometer.costsAtMost_of_max line 468
  53. theorem OAI.PerfectCompleteness.ExactTargetOdometer.digitTapes_at line 480
  54. theorem OAI.PerfectCompleteness.ExactTargetOdometer.existsTree line 501
  55. def OAI.PerfectCompleteness.ExactTargetOdometer.result line 651
  56. theorem OAI.PerfectCompleteness.ExactTargetOdometer.result_count line 656
  57. def OAI.PerfectCompleteness.ExactTargetOdometer.enumerateInTime line 672
  58. def OAI.PerfectCompleteness.ExactTargetOdometer.enumerateInTimeOfBound line 695
  59. theorem OAI.PerfectCompleteness.ExactTargetOdometer.foldl_chunks_eq_prefix line 718
  60. theorem OAI.PerfectCompleteness.ExactTargetOdometer.tupleStep_dataOfPrefix line 754
  61. theorem OAI.PerfectCompleteness.ExactTargetOdometer.fold_tupleSteps_dataOfPrefix line 771
  62. theorem OAI.PerfectCompleteness.ExactTargetOdometer.result_dataOfPrefix line 793
  63. def OAI.PerfectCompleteness.ExactTargetOdometer.targetInTime line 816
  64. theorem OAI.PerfectCompleteness.ExactTargetOdometer.visits_split_at line 836
  65. theorem OAI.PerfectCompleteness.ExactTargetOdometer.costsAtMost_of_chronological line 882
  66. theorem OAI.PerfectCompleteness.ExactTargetOdometer.costsAtMost_full line 938
  67. def OAI.PerfectCompleteness.ExactTargetOdometer.timeBound line 956
  68. def OAI.PerfectCompleteness.ExactTargetOdometer.targetInTimePolynomial line 960