OAI/Combinatorics/IndependentSets/Machines/FinalCNFRowPlan.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue line 12
  2. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.auxiliaryFlag line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.tailFlag line 20
  4. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headFlag line 24
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.pattern_lt line 28
  6. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.referenceOffset line 32
  7. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan line 36
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_length line 45
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_bits line 48
  10. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.patternLiteral line 76
  11. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan line 81
  12. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan line 85
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_length line 88
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_length line 99
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap line 107
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_bits line 113
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue_eq_resolve line 144
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_bits line 170