OAI/Computability/Scheduling/UniformRoutines.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.volume_pos line 12
  2. theorem OAI.ThreeMachine.StackCompiler.volume_le_cons line 16
  3. theorem OAI.ThreeMachine.StackCompiler.volume_list_member line 19
  4. theorem OAI.ThreeMachine.StackCompiler.volume_list_le line 27
  5. theorem OAI.ThreeMachine.StackCompiler.length_le_volume line 37
  6. theorem OAI.ThreeMachine.StackCompiler.Realizer.foldTime_bound line 45
  7. def OAI.ThreeMachine.StackCompiler.Realizer.onFst line 70
  8. def OAI.ThreeMachine.StackCompiler.Realizer.onSnd line 73
  9. def OAI.ThreeMachine.StackCompiler.Realizer.swap line 76
  10. theorem OAI.ThreeMachine.StackCompiler.Realizer.fold_cons_eq line 79
  11. def OAI.ThreeMachine.StackCompiler.Realizer.reverse line 85
  12. def OAI.ThreeMachine.StackCompiler.Realizer.mapBody line 89
  13. theorem OAI.ThreeMachine.StackCompiler.Realizer.map_fold_eq line 94
  14. def OAI.ThreeMachine.StackCompiler.Realizer.map line 101
  15. structure OAI.ThreeMachine.StackCompiler.Uniform line 110
  16. def OAI.ThreeMachine.StackCompiler.Uniform.specialize line 122
  17. def OAI.ThreeMachine.StackCompiler.Uniform.time line 125
  18. def OAI.ThreeMachine.StackCompiler.Uniform.id line 127
  19. def OAI.ThreeMachine.StackCompiler.Uniform.unit line 130
  20. def OAI.ThreeMachine.StackCompiler.Uniform.nil line 133
  21. def OAI.ThreeMachine.StackCompiler.Uniform.zero line 136
  22. def OAI.ThreeMachine.StackCompiler.Uniform.false line 139
  23. def OAI.ThreeMachine.StackCompiler.Uniform.comp line 142
  24. def OAI.ThreeMachine.StackCompiler.Uniform.pair line 148
  25. def OAI.ThreeMachine.StackCompiler.Uniform.fst line 155
  26. def OAI.ThreeMachine.StackCompiler.Uniform.snd line 158
  27. def OAI.ThreeMachine.StackCompiler.Uniform.congr line 161
  28. def OAI.ThreeMachine.StackCompiler.Uniform.reinterpret line 164
  29. def OAI.ThreeMachine.StackCompiler.Uniform.fold line 167
  30. def OAI.ThreeMachine.StackCompiler.Uniform.choose line 174
  31. def OAI.ThreeMachine.StackCompiler.Uniform.ite line 181
  32. def OAI.ThreeMachine.StackCompiler.Uniform.cons line 186
  33. def OAI.ThreeMachine.StackCompiler.Uniform.onFst line 188
  34. def OAI.ThreeMachine.StackCompiler.Uniform.onSnd line 191
  35. def OAI.ThreeMachine.StackCompiler.Uniform.reverse line 194
  36. def OAI.ThreeMachine.StackCompiler.Uniform.mapBody line 198
  37. def OAI.ThreeMachine.StackCompiler.Uniform.map line 202
  38. def OAI.ThreeMachine.StackCompiler.Realizer.uniform line 211
  39. def OAI.ThreeMachine.StackCompiler.Realizer.test line 221
  40. def OAI.ThreeMachine.StackCompiler.Realizer.not line 228
  41. def OAI.ThreeMachine.StackCompiler.Realizer.and line 232
  42. def OAI.ThreeMachine.StackCompiler.Realizer.or line 235
  43. def OAI.ThreeMachine.StackCompiler.Realizer.positive line 238
  44. def OAI.ThreeMachine.StackCompiler.Realizer.isZero line 241
  45. def OAI.ThreeMachine.StackCompiler.Realizer.pred line 244
  46. theorem OAI.ThreeMachine.StackCompiler.Realizer.encode_replicate_unit line 247
  47. def OAI.ThreeMachine.StackCompiler.Realizer.unroll line 252
  48. theorem OAI.ThreeMachine.StackCompiler.Realizer.fold_replicate line 256
  49. def OAI.ThreeMachine.StackCompiler.Realizer.iterate line 262
  50. theorem OAI.ThreeMachine.StackCompiler.Realizer.iterate_pred line 265
  51. theorem OAI.ThreeMachine.StackCompiler.Realizer.iterate_succ line 270
  52. def OAI.ThreeMachine.StackCompiler.Realizer.add line 275
  53. def OAI.ThreeMachine.StackCompiler.Realizer.sub line 278
  54. def OAI.ThreeMachine.StackCompiler.Realizer.le line 281
  55. def OAI.ThreeMachine.StackCompiler.Realizer.eqNat line 284
  56. def OAI.ThreeMachine.StackCompiler.Uniform.test line 296
  57. def OAI.ThreeMachine.StackCompiler.Uniform.isCons line 303
  58. def OAI.ThreeMachine.StackCompiler.Uniform.head? line 306
  59. def OAI.ThreeMachine.StackCompiler.Uniform.swap line 313
  60. def OAI.ThreeMachine.StackCompiler.Uniform.append line 315
  61. theorem OAI.ThreeMachine.StackCompiler.Uniform.fold_append_eq line 320
  62. theorem OAI.ThreeMachine.StackCompiler.Uniform.flatten_fold_eq line 327
  63. def OAI.ThreeMachine.StackCompiler.Uniform.flatten line 335
  64. def OAI.ThreeMachine.StackCompiler.Uniform.flatMap line 339
  65. def OAI.ThreeMachine.StackCompiler.Uniform.filterBody line 343
  66. theorem OAI.ThreeMachine.StackCompiler.Uniform.filter_fold_eq line 350
  67. def OAI.ThreeMachine.StackCompiler.Uniform.filter line 359
  68. def OAI.ThreeMachine.StackCompiler.Uniform.optionToList line 364
  69. def OAI.ThreeMachine.StackCompiler.Uniform.filterMap line 367
  70. def OAI.ThreeMachine.StackCompiler.Uniform.optionMap line 376
  71. def OAI.ThreeMachine.StackCompiler.Uniform.constant line 388
  72. def OAI.ThreeMachine.StackCompiler.Uniform.some line 395
  73. def OAI.ThreeMachine.StackCompiler.Uniform.none line 401
  74. def OAI.ThreeMachine.StackCompiler.Uniform.optionIsSome line 404
  75. def OAI.ThreeMachine.StackCompiler.Uniform.getD line 407
  76. def OAI.ThreeMachine.StackCompiler.Uniform.length line 411
  77. def OAI.ThreeMachine.StackCompiler.Uniform.iterate line 420
  78. def OAI.ThreeMachine.StackCompiler.Uniform.anyBody line 425
  79. theorem OAI.ThreeMachine.StackCompiler.Uniform.any_fold_eq line 432
  80. def OAI.ThreeMachine.StackCompiler.Uniform.any line 440
  81. def OAI.ThreeMachine.StackCompiler.Uniform.all line 445
  82. def OAI.ThreeMachine.StackCompiler.Uniform.find? line 450
  83. def OAI.ThreeMachine.StackCompiler.Uniform.firstResult line 458
  84. def OAI.ThreeMachine.StackCompiler.Uniform.tableOf line 462