OAI/Combinatorics/IndependentSets/Machines/PoweringMachineTapes.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.Tape line 8
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.table line 10
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.start line 11
  4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.query line 12
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.scan line 13
  6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.reverse line 14
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.scratch line 15
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.leftEndpoint line 16
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.rightEndpoint line 17
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.leftCopy line 18
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.rightCopy line 19
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.rowOutput line 20
  13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.endpoint line 22
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.endpoint_false line 25
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.endpoint_true line 26
  16. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole line 28
  17. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement line 32
  18. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement line 35
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_zero line 40
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_one line 42
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_two line 44
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_three line 46
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_four line 48
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_five line 50
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_first line 52
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_succ line 54
  27. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement line 57
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_zero line 61
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_one line 62
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_two line 63
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_three line 64
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_four line 65
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_five line 66
  34. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement line 68
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_zero line 72
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_one line 73
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_two line 74
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_three line 75
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_four line 76
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_five line 77
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_injective line 79
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_start line 82
  43. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_rowOutput line 86
  44. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement_injective line 90
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordShared_ne_trajectory line 111
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_injective line 124
  47. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_injective line 141
  48. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_injective line 145
  49. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_ne_rowOutput line 149
  50. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineTapes.shared_ne_wordPlacement_succ line 165