OAI/Computability/PerfectCompleteness/Reduction/FixedRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PerfectCompleteness.FixedRows.Plan line 17
  2. theorem OAI.PerfectCompleteness.FixedRows.exists_plan line 41
  3. def OAI.PerfectCompleteness.FixedRows.rows line 71
  4. def OAI.PerfectCompleteness.FixedRows.repeats line 72
  5. def OAI.PerfectCompleteness.FixedRows.cutoff line 74
  6. theorem OAI.PerfectCompleteness.FixedRows.cutoff_pos line 78
  7. instance OAI.PerfectCompleteness.FixedRows.cutoff_neZero line 82
  8. def OAI.PerfectCompleteness.FixedRows.sourceLength line 85
  9. theorem OAI.PerfectCompleteness.FixedRows.sourceLength_pos line 89
  10. theorem OAI.PerfectCompleteness.FixedRows.source_oddList_value_le_half line 93
  11. theorem OAI.PerfectCompleteness.FixedRows.lower_row_requirement line 103