OAI/Computability/PerfectCompleteness/Machines/CircuitEmission.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextSource_ne_scratch line 13
  2. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextSource_ne_reversed line 20
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextOutput line 27
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextSteps line 31
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes line 34
  6. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes_other line 37
  7. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes_source line 42
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextTapes_scratch line 46
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextOutput_update line 50
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextSteps_update line 55
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.setupStep line 60
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextTrace line 64
  13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextInTime line 84
  14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.output_eq_flatMap line 94
  15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.literalEmit_word line 102
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.affineEmit_word line 111
  17. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextWords line 123
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.output_word line 129
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextTrace_word line 140
  20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextListOutput line 151
  21. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextListSteps line 154
  22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextListStart line 157
  23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.ContextListLinked line 162
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextListOutput_update line 167
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextListSteps_update line 172
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.chain line 177
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextListTrace line 181
  28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateContexts line 208
  29. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.outputContexts line 211
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateContexts_linked line 213
  31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.outputContexts_linked line 218
  32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.contextOutput_gate_word line 222
  33. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.encodeWords_flatMap line 242
  34. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateOutput_words line 248
  35. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps line 259
  36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps_eq line 263
  37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.slot_le_sum line 280
  38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.sum_map_le_length_mul line 285
  39. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps_le line 296
  40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.length_flatMap_le_length_mul line 308
  41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.outputBits_length_le line 320
  42. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.recordBits_length line 338
  43. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateSteps_le_inputSize line 343
  44. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.outputBits_length_le_inputSize line 349
  45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateTrace line 355
  46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.gateInTime line 370
  47. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.outputTrace line 384
  48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.CircuitEmission.outputInTime line 402