OAI/Combinatorics/IndependentSets/Machines/MachineCloudSelect.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.BaseTape line 12
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.BaseAlphabet line 13
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.BaseState line 14
  4. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.BaseLabel line 16
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.skipLabel line 22
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.baseProgram line 27
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.baseProgram_skip line 47
  8. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.Phase line 52
  9. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.(instance at line 55) line 55
  10. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.Control line 59
  11. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.(instance at line 62) line 62
  12. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.Tape line 66
  13. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.Alphabet line 67
  14. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.Label line 68
  15. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.State line 69
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.go line 71
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.dispatcher line 74
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.extra line 87
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.program line 91
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.memory line 94
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.memory_inl line 99
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.memory_position line 101
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.update_memory_hit line 104
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.update_memory_rank line 110
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.update_memory_position line 116
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.cfg line 123
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.liftTrace line 128
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.compareTrace line 141
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.dispatch_miss line 164
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_succ line 171
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_zero line 180
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.advanceStep line 188
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.finishStep line 197
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.initializeStep line 203
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.skipTrace line 210
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.rowSkipTrace line 234
  37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.prefixTime line 278
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.prefixTrace line 282
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.cleanupTrace line 310
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.selectedTrace line 344
  41. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.queryWord line 361
  42. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.prepareSteps line 363
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.prepareTrace line 367
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.prefixSelectedTrace line 426
  45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.totalSteps line 448
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.fullTrace line 453
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.prefixTime_le line 477
  48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.totalSteps_le line 489
  49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.remainder line 507
  50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.tableRows_getElem line 511
  51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.tableWord_split line 521
  52. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps line 534
  53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.cloudSelectTrace line 540
  54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps_le line 564
  55. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.timePolynomial line 574
  56. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.cloudSelectInTime line 577
  57. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.machine line 593
  58. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCloudSelect.machineInTime line 604