OAI/Combinatorics/IndependentSets/Machines/MachineCloudPrefix.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.Tape line 14
  2. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.Label line 19
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.Alphabet line 25
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.State line 26
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.memory line 28
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame line 35
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_query line 38
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_count line 40
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_power line 42
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_level line 44
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_bound line 46
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_remaining line 48
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.frame_total line 50
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.update_frame_query line 53
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.update_frame_count line 61
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.update_frame_power line 69
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.update_frame_level line 77
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.update_frame_remaining line 85
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.update_frame_total line 89
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.paddingView line 94
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.paddingView_left line 98
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.paddingView_right line 100
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.placedTapes line 104
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.program line 111
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.appendTrace line 127
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.paddingTrace line 131
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.incrementStep line 149
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.bodyTime line 158
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.bodyTrace line 163
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.guardStep_succ line 205
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.guardStep_zero line 215
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.zeroTrace line 223
  33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.amount line 237
  34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.cycleTime line 240
  35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.sumFrom line 243
  36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.loopTime line 247
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.loopTrace line 251
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_list line 282
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_eq_offset line 301
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.initStep line 310
  41. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.totalTime line 317
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.prefixTrace line 320
  43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.cycleBudget line 348
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.bodyTime_le line 352
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.loopTime_le line 380
  46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.inputLength line 393
  47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.timePolynomial line 396
  48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.totalTime_le line 403
  49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.prefixInTime line 423
  50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.all_padding_sum line 438
  51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudPrefix.paddingOrder_eq_prefix line 442