OAI/Computability/PerfectCompleteness/Machines/TransitionTemplate.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.instantiate line 28
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.nodeCount line 41
  4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.instantiate_size_le line 48
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.disjoin line 64
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.mux line 68
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_disjoin line 72
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_mux line 78
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.finiteTable line 82
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.finiteTable₂ line 86
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_table line 91
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_table₂ line 98
  13. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Data line 105
  14. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Result line 109
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Data.Matches line 112
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Result.Matches line 118
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.initial line 123
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.initial_matches line 128
  19. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.read line 134
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_read line 138
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.push line 149
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.peek line 155
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.pop line 160
  24. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.load line 165
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.mux line 170
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.push_matches line 177
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.peek_matches line 195
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.pop_matches line 209
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.load_matches line 221
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.mux_matches line 230
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.compile line 244
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.compile_matches line 257
  33. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.OutputKind line 281
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.bitKind line 284
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.bitCursor line 289
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.select line 293
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.transition line 298
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.transition_instantiate line 301
  39. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global line 311
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.instantiate line 318
  41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.nodeCount line 326
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.instantiate_size_le line 333
  43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.disjoin line 344
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_global_disjoin line 351
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.self line 357
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.self_instantiate line 364
  47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.sticky line 374
  48. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.sticky_instantiate line 380
  49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.kindIndexEquiv line 389
  50. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.templateBank line 398
  51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.templateBank_select line 404
  52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.rootLookup line 409
  53. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.configWire line 411
  54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.labelAddress_lt_width line 417
  55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.stateAddress_lt_width line 425
  56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.cellAddress_lt_width line 433
  57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.rootLookup_present line 442
  58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.configWire_present line 451
  59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.tokens line 456
  60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Term.tokens_eq line 475
  61. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.tokens line 494
  62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.tokens_eq line 504
  63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.sticky_tokens_eq line 517
  64. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.Global.tokens_length_le line 526
  65. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.sticky_tokens_length_le line 532
  66. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.outputOrder line 539
  67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.forestTokens line 543
  68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.forestTokens_eq line 548
  69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.outputOrder_length line 560
  70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TransitionTemplate.forestTokens_length_le line 564