OAI/Computability/VertexCover/Encoding/FinalCNFPattern.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.Label line 35
  2. abbrev OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.labelEquiv line 37
  3. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 39
  4. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.labelIndex line 44
  5. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.labelBits line 46
  6. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 48
  7. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 51
  8. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.leftHalf line 54
  9. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.rightHalf line 57
  10. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.relationAddress line 60
  11. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 63
  12. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 68
  13. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 71
  14. def OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.tableGraph line 74
  15. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 78
  16. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 81
  17. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 84
  18. abbrev OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.tableVerifier line 89
  19. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 92
  20. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 97
  21. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 102
  22. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 107
  23. theorem OAI.UniqueGames.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 114