OAI/Combinatorics/IndependentSets/Machines/FinalCNFOutput.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader line 14
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.formulaHeader_eq line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.headerPlan_eq_formulaHeader line 23
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.outputStream_eq_clauseBits line 29
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.header_append_outputStream line 48
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.emitted_output_eq line 54
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.reversed_accumulator_output line 63
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.accumulator_length_bound line 68
  9. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial line 78
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowTimePolynomial_eval line 82
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.rowTime_expanded line 87
  12. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial line 91
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval line 96
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTimePolynomial_eval_expanded line 103
  15. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.phaseTime_le line 109
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.table_phaseTime_le line 117
  17. def OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial line 125
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.finalTimePolynomial_eval line 129
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.FinalCNFMachine.Program.finalTime_le line 135