OAI/Computability/Scheduling/PolynomialLists.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ThreeMachine.StackCompiler.volume_block line 10
  2. theorem OAI.ThreeMachine.StackCompiler.block_length_le_volume line 15
  3. theorem OAI.ThreeMachine.StackCompiler.block_time_volume_le line 18
  4. theorem OAI.ThreeMachine.StackCompiler.Poly.blockLength line 23
  5. theorem OAI.ThreeMachine.StackCompiler.Poly.blockTime line 27
  6. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeBlock line 31
  7. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeFst line 38
  8. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeSnd line 41
  9. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeOption line 45
  10. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeOptionSome line 51
  11. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeOptionNone line 55
  12. theorem OAI.ThreeMachine.StackCompiler.Poly.flatMapTime line 68
  13. theorem OAI.ThreeMachine.StackCompiler.Poly.optionMapTime line 94
  14. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthOption line 118
  15. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeIte line 122
  16. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeOptionMap line 129
  17. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeLookup line 147
  18. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeOptionToList line 160
  19. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthCons line 170
  20. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthTail line 175
  21. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthTake line 180
  22. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthDrop line 185
  23. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthReverse line 190
  24. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthAppend line 194
  25. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthRange line 199
  26. theorem OAI.ThreeMachine.StackCompiler.Poly.lengthReplicate line 202