OAI/Algebra/FormulaHitting/ProgramCost.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NCHitting.BitModel.bitSize_le_self line 9
  2. theorem OAI.NCHitting.BitModel.bitSize_mul_le line 13
  3. theorem OAI.NCHitting.BitModel.bitSize_pow_le line 18
  4. def OAI.NCHitting.BitModel.powerStepBound line 27
  5. theorem OAI.NCHitting.BitModel.width_le_of_le line 30
  6. theorem OAI.NCHitting.BitModel.powerRun_cost_le line 33
  7. theorem OAI.NCHitting.BitModel.sum_map_le_length_mul line 66
  8. theorem OAI.NCHitting.BitModel.outputBits_append line 79
  9. theorem OAI.NCHitting.BitModel.outputBits_flatMap line 83
  10. def OAI.NCHitting.BitModel.loopControlBound line 89
  11. theorem OAI.NCHitting.BitModel.loop_control_le line 91
  12. theorem OAI.NCHitting.BitModel.loop_cost_le line 99
  13. theorem OAI.NCHitting.BitModel.loop_outputBits_le line 123
  14. def OAI.NCHitting.BitModel.expressionBudget line 138
  15. def OAI.NCHitting.BitModel.Expr.nodes line 141
  16. def OAI.NCHitting.BitModel.Expr.Bounded line 147
  17. theorem OAI.NCHitting.BitModel.Expr.bounded_width line 168
  18. theorem OAI.NCHitting.BitModel.addCost_le_budget line 172
  19. theorem OAI.NCHitting.BitModel.mulCost_le_budget line 178
  20. theorem OAI.NCHitting.BitModel.compareCost_le_budget line 186
  21. theorem OAI.NCHitting.BitModel.Expr.cost_le_nodes_budget line 192
  22. theorem OAI.NCHitting.BitModel.width_mul_le line 266
  23. theorem OAI.NCHitting.BitModel.width_pow_le line 271
  24. def OAI.NCHitting.BitModel.registerReadBound line 276
  25. def OAI.NCHitting.BitModel.intermediateWidthBound line 278
  26. theorem OAI.NCHitting.BitModel.small_width line 280
  27. theorem OAI.NCHitting.BitModel.Expr.bounded_literal line 285
  28. theorem OAI.NCHitting.BitModel.Expr.bounded_read line 289
  29. theorem OAI.NCHitting.BitModel.emit_cost_le line 311
  30. theorem OAI.NCHitting.BitModel.emit_outputBits_le line 323
  31. theorem OAI.NCHitting.BitModel.branch_cost_le line 333
  32. theorem OAI.NCHitting.BitModel.branch_outputBits_le line 340