OAI/Computability/VertexCover/Machines/ParseFormula.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VertexCover.Machine.FormulaParser.Acc line 44
  2. abbrev OAI.VertexCover.Machine.FormulaParser.accCode line 45
  3. abbrev OAI.VertexCover.Machine.FormulaParser.State line 46
  4. abbrev OAI.VertexCover.Machine.FormulaParser.stateCode line 47
  5. def OAI.VertexCover.Machine.FormulaParser.oneStep line 49
  6. def OAI.VertexCover.Machine.FormulaParser.step line 56
  7. def OAI.VertexCover.Machine.FormulaParser.oneStepPoly line 58
  8. def OAI.VertexCover.Machine.FormulaParser.stepPoly line 75
  9. def OAI.VertexCover.Machine.FormulaParser.budget line 80
  10. theorem OAI.VertexCover.Machine.FormulaParser.size_le_budget line 84
  11. theorem OAI.VertexCover.Machine.FormulaParser.budget_le_size line 93
  12. theorem OAI.VertexCover.Machine.FormulaParser.step_budget line 102
  13. theorem OAI.VertexCover.Machine.FormulaParser.run_budget line 129
  14. def OAI.VertexCover.Machine.FormulaParser.runPoly line 134
  15. def OAI.VertexCover.Machine.FormulaParser.observe line 144
  16. theorem OAI.VertexCover.Machine.FormulaParser.run_done line 146
  17. theorem OAI.VertexCover.Machine.FormulaParser.observe_run line 151
  18. def OAI.VertexCover.Machine.FormulaParser.observePoly line 181
  19. def OAI.VertexCover.Machine.FormulaParser.clausesPoly line 185
  20. def OAI.VertexCover.Machine.FormulaParser.decodePoly line 203
  21. def OAI.VertexCover.Machine.FormulaParser.inputFormulaPoly line 217