OAI/Computability/MinUncut/PCP/PreprocessingRegularBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.offset_succ line 15
  2. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.blocksPrefix_length_le line 23
  3. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.header line 29
  4. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.ownerBits line 32
  5. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix line 37
  6. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix line 42
  7. def OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix line 48
  8. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.originalPrefix_length_le line 56
  9. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.ownerPrefix_length_le line 64
  10. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.dummyPrefix_length_le line 75
  11. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.regular_originalPrefix_le line 89
  12. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.regular_ownerPrefix_le line 96
  13. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.regular_dummyPrefix_le line 103
  14. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.visits_le_input line 110
  15. theorem OAI.MinUncutGames.Foundations.PCP.PreprocessingRegularBounds.sum_body_costs_le line 120