OAI/Computability/Scheduling/CostBounds.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.volume_unit line 11
  2. theorem OAI.ThreeMachine.StackCompiler.volume_bool_false line 12
  3. theorem OAI.ThreeMachine.StackCompiler.volume_bool_true line 13
  4. theorem OAI.ThreeMachine.StackCompiler.volume_none line 14
  5. theorem OAI.ThreeMachine.StackCompiler.volume_some line 15
  6. theorem OAI.ThreeMachine.StackCompiler.volume_bool line 18
  7. theorem OAI.ThreeMachine.StackCompiler.volume_list line 20
  8. theorem OAI.ThreeMachine.StackCompiler.volume_mem_le line 26
  9. theorem OAI.ThreeMachine.StackCompiler.volume_sublist line 36
  10. theorem OAI.ThreeMachine.StackCompiler.volume_filter_le line 43
  11. theorem OAI.ThreeMachine.StackCompiler.volume_option_le line 46
  12. theorem OAI.ThreeMachine.StackCompiler.volume_optionToList line 52
  13. theorem OAI.ThreeMachine.StackCompiler.volume_finset_le line 55
  14. theorem OAI.ThreeMachine.StackCompiler.volume_function_le line 64
  15. theorem OAI.ThreeMachine.StackCompiler.Realizer.foldTime_le line 74
  16. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_fold_le line 99
  17. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_not_le line 117
  18. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_and_le line 119
  19. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_or_le line 122
  20. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_succ_le line 125
  21. theorem OAI.ThreeMachine.StackCompiler.Realizer.time_test_le line 133
  22. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_uniform line 150
  23. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_test_le line 153
  24. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_head?_le line 157
  25. def OAI.ThreeMachine.StackCompiler.Majorized line 176
  26. theorem OAI.ThreeMachine.StackCompiler.Majorized.refl line 181
  27. theorem OAI.ThreeMachine.StackCompiler.Majorized.of_le line 182
  28. theorem OAI.ThreeMachine.StackCompiler.Majorized.trans line 183
  29. theorem OAI.ThreeMachine.StackCompiler.Majorized.mono line 186
  30. theorem OAI.ThreeMachine.StackCompiler.Majorized.precomp line 188
  31. theorem OAI.ThreeMachine.StackCompiler.Majorized.add line 190
  32. theorem OAI.ThreeMachine.StackCompiler.Majorized.mul line 194
  33. theorem OAI.ThreeMachine.StackCompiler.Majorized.const line 199
  34. theorem OAI.ThreeMachine.StackCompiler.Majorized.zero line 201
  35. theorem OAI.ThreeMachine.StackCompiler.Majorized.const_mul line 202
  36. theorem OAI.ThreeMachine.StackCompiler.Majorized.mul_const line 205
  37. theorem OAI.ThreeMachine.StackCompiler.Majorized.pow line 208
  38. theorem OAI.ThreeMachine.StackCompiler.Majorized.pow_mono line 213
  39. theorem OAI.ThreeMachine.StackCompiler.Majorized.sum line 217
  40. theorem OAI.ThreeMachine.StackCompiler.volume_flatten line 231
  41. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_tail line 244
  42. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_none line 245
  43. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_some_le line 247
  44. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_ite_le line 251
  45. theorem OAI.ThreeMachine.StackCompiler.Uniform.foldTime_cons line 259
  46. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_consFold line 271
  47. theorem OAI.ThreeMachine.StackCompiler.Uniform.foldTime_flatten line 278
  48. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_flatten line 295
  49. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_filterBody line 312
  50. theorem OAI.ThreeMachine.StackCompiler.Uniform.foldTime_filterBody line 325
  51. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_filter line 346
  52. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_optionMap line 359
  53. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_getD_le line 377
  54. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_anyBody line 396
  55. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_any line 406
  56. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_all line 425
  57. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_find? line 441
  58. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_flatMap line 451
  59. theorem OAI.ThreeMachine.StackCompiler.Uniform.volume_map_options line 463
  60. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_filterMap line 471
  61. theorem OAI.ThreeMachine.StackCompiler.volume_replicate_unit line 499
  62. theorem OAI.ThreeMachine.StackCompiler.Uniform.foldTime_iterate_le line 509
  63. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_iterate_le line 531
  64. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_firstResult line 544