OAI/Combinatorics/IndependentSets/PCP/FinalCNFPattern.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.Label line 14
  2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.labelEquiv line 16
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 18
  4. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.labelIndex line 23
  5. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.labelBits line 25
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 27
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 30
  8. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.leftHalf line 33
  9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.rightHalf line 36
  10. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.relationAddress line 39
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 42
  12. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 47
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 50
  14. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.tableGraph line 53
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 57
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 60
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 63
  18. abbrev OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.tableVerifier line 68
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 71
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 76
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 81
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 86
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 93