OAI/Combinatorics/IndependentSets/Machines/Machine2.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.naturalWordsEncoding line 11
  2. def OAI.IndependentSetsGames.Foundations.Complexity.formulaEncoding line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.gameEncoding line 21
  4. def OAI.IndependentSetsGames.Foundations.Complexity.prefixBitMachine line 26
  5. def OAI.IndependentSetsGames.Foundations.Complexity.prefixBitPolyTime line 37
  6. def OAI.IndependentSetsGames.Foundations.Complexity.enlargePolynomialBound line 56
  7. def OAI.IndependentSetsGames.Foundations.Complexity.composeMachinePhases line 69
  8. structure OAI.IndependentSetsGames.Foundations.Complexity.PolynomialGapReduction line 81
  9. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.inputLength line 94
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.cloudSize_le_input line 96
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.cloudTotal_le_input line 100
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.level_le_input line 106
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.regularVertices_le_input line 110
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.offset_le_sum line 115
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.prefix_le_input line 126
  16. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.tablePolynomial line 134
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.tableBits_le_of_counts line 139
  18. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.regularPolynomial line 149
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.regularBits_le line 152
  20. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.rotorPolynomial line 166
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingMachineBounds.cloudRotorBits_le line 170