OAI/Combinatorics/IndependentSets/Machines/MachineRegularFamily.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.CoreTape line 11
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.NativeTape line 12
  3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.Tape line 13
  4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.Alphabet line 14
  5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.SmallTable line 15
  6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.FamilyState line 16
  7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.State line 17
  8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.inputNative line 19
  9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.outputNative line 20
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.powerNative line 21
  11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.sizeNative line 22
  12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.levelNative line 23
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.powerTape line 25
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.sizeTape line 26
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.levelTape line 27
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.familyTape line 29
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.familyView line 32
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.familyView_left line 36
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.familyView_right line 43
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.stateEquiv line 64
  21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.seedState line 67
  22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.readyState line 70
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.sourceProgram line 72
  24. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.Label line 76
  25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.program line 82
  26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.frame line 89
  27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.rotor line 93
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.resultCore line 96
  29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.working line 99
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.working_power line 104
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.working_size line 107
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.working_level line 111
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.update_working_power line 115
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.update_working_size line 122
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.update_working_level line 132
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.working_empty line 142
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.initial_other line 146
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.final_other line 152
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.initial_placement line 173
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.final_placement line 194
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.source_initial_state line 242
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.source_final_state line 246
  43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.familyInTime line 251
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.appendTrace line 272
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.cleanupTrace line 276
  46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.cleanupInTime line 298
  47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.startInTime line 307
  48. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.timePolynomial line 317
  49. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.totalBudget_le line 321
  50. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.familyCleanInTime line 332
  51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.result_output line 348
  52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.result_preserves_core line 351
  53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.result_private_empty line 355
  54. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularFamily.placedInTime line 359