OAI/Computability/PerfectCompleteness/Machines/ForestStage.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.Tape line 16
  2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.Ports line 21
  3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.Alphabet line 22
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.State line 23
  5. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.Label line 25
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.lowerPorts line 31
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.initialLocal line 36
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.finalLocal line 45
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.coreBase line 53
  10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.coreInitial line 57
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.coreFinal line 60
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.chain line 64
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.coreTrace line 68
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.stateEquiv line 97
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.framedStatement line 103
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.framedProgram line 108
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.framedCfg line 112
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.framed_step line 117
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.framed_coreTrace line 134
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.steps line 144
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forest_length_le_cost line 150
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forest_rootsBits_length_le line 159
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forest_rootRefresh_le line 172
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forest_cost_quadratic line 178
  25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.timePolynomial line 205
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forest_steps_le line 208
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.localLowerPorts line 225
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.lowerFill line 228
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.fill_lower_eq line 233
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.program line 242
  31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.extras line 257
  32. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.afterRecords line 262
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.localTrace line 270
  34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.statement line 386
  35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.traceAt line 390
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forestTraceAt line 404
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forestInPolynomialTime line 419
  38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.preparedSize line 439
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.preparedSize_initial line 445
  40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.forestInPreparedTime line 454
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.final_other line 479
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.final_counter line 485
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.final_lower_clean line 488
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.final_forest_roots line 493
  45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.machine line 501
  46. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ForestStage.machine_alphabet_finite line 512