OAI/Computability/Scheduling/TransitionCosts.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThreeMachine.StackCompiler.Uniform.StatesInput line 9
  2. def OAI.ThreeMachine.StackCompiler.Uniform.statesC line 11
  3. def OAI.ThreeMachine.StackCompiler.Uniform.statesF line 14
  4. def OAI.ThreeMachine.StackCompiler.Uniform.statesZ line 15
  5. def OAI.ThreeMachine.StackCompiler.Uniform.statesW line 16
  6. def OAI.ThreeMachine.StackCompiler.Uniform.statesPairs line 17
  7. def OAI.ThreeMachine.StackCompiler.Uniform.statesS line 18
  8. def OAI.ThreeMachine.StackCompiler.Uniform.statesP line 19
  9. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_states line 23
  10. theorem OAI.ThreeMachine.StackCompiler.Costs.statesC line 28
  11. theorem OAI.ThreeMachine.StackCompiler.Costs.statesP line 31
  12. theorem OAI.ThreeMachine.StackCompiler.Costs.statesPairs line 41
  13. theorem OAI.ThreeMachine.StackCompiler.Costs.statesS line 48
  14. theorem OAI.ThreeMachine.StackCompiler.Costs.states line 56
  15. abbrev OAI.ThreeMachine.StackCompiler.Uniform.BlockAppendCellInput line 68
  16. def OAI.ThreeMachine.StackCompiler.Uniform.appendCellS line 70
  17. def OAI.ThreeMachine.StackCompiler.Uniform.appendCellT line 71
  18. def OAI.ThreeMachine.StackCompiler.Uniform.appendCellTest line 72
  19. def OAI.ThreeMachine.StackCompiler.Uniform.appendCellLeft line 74
  20. def OAI.ThreeMachine.StackCompiler.Uniform.appendCellRight line 76
  21. def OAI.ThreeMachine.StackCompiler.Uniform.appendCell line 79
  22. abbrev OAI.ThreeMachine.StackCompiler.Uniform.BlockAppendInput line 82
  23. def OAI.ThreeMachine.StackCompiler.Uniform.appendLength line 84
  24. def OAI.ThreeMachine.StackCompiler.Uniform.blockAppendNamed line 87
  25. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_blockAppend line 90
  26. theorem OAI.ThreeMachine.StackCompiler.Costs.appendCellLeft line 95
  27. theorem OAI.ThreeMachine.StackCompiler.Costs.appendCellRight line 100
  28. theorem OAI.ThreeMachine.StackCompiler.Costs.appendCell line 105
  29. def OAI.ThreeMachine.StackCompiler.Uniform.appendVector line 117
  30. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_blockAppendNamed line 118
  31. theorem OAI.ThreeMachine.StackCompiler.Costs.appendLength line 126
  32. theorem OAI.ThreeMachine.StackCompiler.Costs.appendVector line 132
  33. theorem OAI.ThreeMachine.StackCompiler.Costs.blockAppend line 140
  34. abbrev OAI.ThreeMachine.StackCompiler.Uniform.AdvanceInput line 152
  35. def OAI.ThreeMachine.StackCompiler.Uniform.advanceU line 154
  36. def OAI.ThreeMachine.StackCompiler.Uniform.advanceV line 155
  37. def OAI.ThreeMachine.StackCompiler.Uniform.advanceS line 156
  38. def OAI.ThreeMachine.StackCompiler.Uniform.advanceT line 157
  39. def OAI.ThreeMachine.StackCompiler.Uniform.advanceB line 158
  40. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_stateAdvance line 162
  41. theorem OAI.ThreeMachine.StackCompiler.Poly.volumeAppendTriple line 169
  42. theorem OAI.ThreeMachine.StackCompiler.Costs.advanceB line 186
  43. theorem OAI.ThreeMachine.StackCompiler.Costs.stateAdvance line 193
  44. theorem OAI.ThreeMachine.StackCompiler.volume_option_mem_le line 208
  45. theorem OAI.ThreeMachine.StackCompiler.volume_find_le line 211
  46. theorem OAI.ThreeMachine.StackCompiler.volume_lookup_le line 215
  47. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_mapSndOption_le line 224
  48. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_lookup_le line 245
  49. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_lookup_setEq_le line 271
  50. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_lookup_stateEq_le line 278
  51. abbrev OAI.ThreeMachine.StackCompiler.Uniform.TryInput line 290
  52. def OAI.ThreeMachine.StackCompiler.Uniform.tryU line 292
  53. def OAI.ThreeMachine.StackCompiler.Uniform.tryT line 293
  54. def OAI.ThreeMachine.StackCompiler.Uniform.tryA line 294
  55. def OAI.ThreeMachine.StackCompiler.Uniform.tryV line 295
  56. def OAI.ThreeMachine.StackCompiler.Uniform.tryW line 296
  57. def OAI.ThreeMachine.StackCompiler.Uniform.tryL line 297
  58. def OAI.ThreeMachine.StackCompiler.Uniform.tryP line 298
  59. def OAI.ThreeMachine.StackCompiler.Uniform.tryDiff line 299
  60. def OAI.ThreeMachine.StackCompiler.Uniform.tryO line 300
  61. def OAI.ThreeMachine.StackCompiler.Uniform.tryWork line 301
  62. theorem OAI.ThreeMachine.StackCompiler.Uniform.time_tryAdvance line 302
  63. theorem OAI.ThreeMachine.StackCompiler.Costs.advanceLast line 309