OAI/Computability/PerfectCompleteness/Machines/CircuitEncodingLemmas.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateRecord line 11
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateRecords line 18
  3. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.records line 22
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.recordsWords line 24
  5. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.recordsBits line 25
  6. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitWords line 27
  7. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitBits line 30
  8. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateRecords_length line 32
  9. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.records_length line 38
  10. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.recordsWords_cons line 41
  11. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.recordsBits_cons line 44
  12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.recordsWords_length line 48
  13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitWords_length line 57
  14. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateFromFields line 62
  15. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodeGateWords line 70
  16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodeGateWords_gateRecord line 75
  17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.decodeGateWords_gateRecords line 84
  18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitWords_injective line 91
  19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitBits_injective line 115
  20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateRecord_fields_le line 119
  21. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateRecords_fields_le line 128
  22. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitWords_bounded line 144
  23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuitBits_length_le line 156
  24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.circuit_header_le_length line 162
  25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateClauses_words line 178
  26. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.unitClause_words line 186
  27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.gateRecords_outputWords line 189
  28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.gateBlocks_words line 207
  29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.formulaWords_eq_records line 219
  30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.Circuit.formulaBits_eq_records line 233