OAI/Computability/PerfectCompleteness/Machines/OrClosure.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.Alphabet line 17
  2. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.Ports line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.frame line 27
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.frame_remaining line 32
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.frame_reversed line 37
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.frame_count line 42
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.frame_other line 47
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.frame_self line 53
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.update_remaining line 57
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.update_reversed line 67
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.update_count line 77
  12. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.seed line 83
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.loop line 89
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.seedPushBound line 101
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.loopPushBound line 105
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.seedStep line 109
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.loopStep_zero line 117
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.loopStep_succ line 126
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.tokenBits_append line 136
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.tokenBits_or line 140
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.tokenBits_false line 142
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.tokenBits_closeOr line 144
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.tokenBits_replicate_succ line 149
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.replicate_push line 156
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.loopTrace line 164
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.closureTrace line 191
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.closureInTime line 212
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.increment_count line 231
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.machine line 241
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.OrClosure.machineTrace line 253