OAI/Computability/PerfectCompleteness/Machines/PositionLemmas.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Position line 12
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Position.eval line 19
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.usesCurrent line 35
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.initialValue line 41
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.transform line 44
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.transform_initialValue line 50
  7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.Alphabet line 66
  8. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.State line 67
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.decrement line 69
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.stepAux_decrement line 77
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.suffixStatement line 87
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.stepAux_suffixStatement line 96
  13. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.Label line 114
  14. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.(instance at line 121) line 121
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.statement line 125
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.seedSteps line 137
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.steps line 140
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.seedTrace line 142
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.finishTrace line 169
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.positionTrace line 184
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.timePolynomial line 202
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.steps_le_time line 204
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.positionInPolynomialTime line 210
  24. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.machine line 230
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PositionMachine.machineInPolynomialTime line 241
  26. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.Token line 259
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.Token.tag line 267
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.Token.words line 275
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.Token.bits line 283
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.Token.takeGate line 285
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.tokenWords line 295
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.tokenBits line 296
  33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.compileTokens line 298
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PostfixModel.inputBits line 306
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens line 319
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_eq_flatMap_range line 323
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_eq_ofFn line 329
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_succ_first line 337
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_congr line 341
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_length_le line 349
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_length_eq line 360
  42. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.closeOr line 369
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.nonemptyTokens line 371
  44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.clashPairTokens line 374
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.clashRowTokens line 377
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.clashTokens line 380
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.validityTokens line 383
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.presenceTokens line 386
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens line 390
  50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.threshold_zero_iff line 393
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens_length line 396
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens_succ line 403
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens_presence line 416
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.presenceTokens_length line 424