OAI/Computability/PerfectCompleteness/Machines/PayloadCellsMachine.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Alphabet line 16
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.chain line 18
  3. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.SymbolSpec line 22
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.payloadTokens line 29
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.symbolTokens line 32
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.inputMap line 40
  7. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.Label line 42
  8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.statement line 50
  9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.addressSteps line 71
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.addressTrace line 73
  11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.steps line 108
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.trace line 111
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.steps_le line 172
  14. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.Label line 180
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.firstLabels line 189
  16. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.secondLabels line 190
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.statement line 192
  18. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.steps line 208
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.trace line 213
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.steps_le line 273
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tableAt line 287
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokensFrom line 290
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokens line 293
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokensFrom_succ line 295
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokens_eq_ofFn line 305
  26. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.Label line 313
  27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.symbolLabels line 318
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.statement line 321
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.stepsFrom line 328
  30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.steps line 332
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.traceFrom line 334
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.trace line 370
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.stepsFrom_le line 380
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.steps_le line 390
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.inTime line 393
  36. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.machine line 411
  37. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.machineInTime line 423