OAI/Combinatorics/IndependentSets/Expansion/PoweringPlanBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.fieldBudget line 12
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.field_steps_le line 15
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.plan_steps_le line 40
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.boundedRowPlan_length line 57
  5. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.rowBudget line 63
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.rowPlan_steps_le line 67
  7. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.planInTime line 80
  8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringPlanBudget.rowPlanInTime line 99
  9. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.blockSize line 133
  10. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseOffset line 135
  11. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.reverseValue line 138
  12. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.tailVertex line 142
  13. def OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords line 146
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.table_tail line 150
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.table_reverseValue line 162
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.headerWords_eq line 172
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PoweringRowHeaderSemantics.header_relation_bits line 182