OAI/Computability/PerfectCompleteness/Machines/InitializationTemplateLemmas.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.exprTokens_disjoin line 15
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.forestTokens_ofFn line 23
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.muxTokens line 27
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.exprTokens_mux line 30
  5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.nonemptyTokens_eq line 35
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.clashPairTokens_eq line 40
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.clashRowTokens_eq line 47
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.clashTokens_eq line 57
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.validityTokens_eq line 66
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.presenceTokens_eq line 71
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.payloadSymbolTokens line 80
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.payloadSymbolTokens_eq line 84
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.inputCellTokens line 89
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.inputCellTokens_eq line 98
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initialCellTokens line 117
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initialCellTokens_eq line 126
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initTokens line 136
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initTokens_eq line 142
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initTokens_length_le line 150
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.validityTokens_length_le line 158
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody line 171
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_index line 176
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_label line 184
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_state line 191
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_cell line 198
  26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens line 207
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.tokenBound line 211
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_eq line 215
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_length line 230
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initialization_inputBits line 234
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_length_le line 240
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_compile line 250
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initialization_tokenWords_bounded line 259
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.InitializationTemplate.initialization_tokenBits_length_le line 265
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.headMask line 297
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.accepting_label line 304
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.accepting_state line 307
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.accepting_cell line 311
  39. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.targetBit line 323
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.mismatchTokens line 326
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.tokens line 329
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.mismatchTokens_eq line 336
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.tokens_eq line 345
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.compile_tokens line 352
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptanceTemplate.tokens_length_le line 361
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.negateIf line 384
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.stateTemplate line 387
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.cellTemplate line 391
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.plan line 399
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.mismatchForest line 413
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.label_tokens line 418
  52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.state_tokens line 429
  53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.cell_tokens line 439
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.outputTokens_eq line 456
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.mismatchForest_circuit line 482
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.AcceptancePlan.fullTokens_eq line 490