OAI/Computability/MinUncut/Games/FinalCNFPattern.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.Label line 12
  2. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.labelEquiv line 14
  3. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 16
  4. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.labelIndex line 21
  5. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.labelBits line 23
  6. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 25
  7. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 28
  8. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.leftHalf line 31
  9. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.rightHalf line 34
  10. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.relationAddress line 37
  11. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 40
  12. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 45
  13. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 48
  14. def OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.tableGraph line 51
  15. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 55
  16. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 58
  17. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 61
  18. abbrev OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.tableVerifier line 66
  19. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 69
  20. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 74
  21. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 79
  22. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 84
  23. theorem OAI.MinUncutGames.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 91