OAI/Algebra/FormulaHitting/BitRefinement.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NCHitting.BitRefinement.width_pos line 10
  2. theorem OAI.NCHitting.BitRefinement.width_mono line 12
  3. theorem OAI.NCHitting.BitRefinement.width_add_le line 15
  4. theorem OAI.NCHitting.BitRefinement.addCost_ge_widths line 27
  5. theorem OAI.NCHitting.BitRefinement.mulCost_ge_widths line 31
  6. theorem OAI.NCHitting.BitRefinement.powerRun_count_le line 37
  7. theorem OAI.NCHitting.BitRefinement.powerRun_width_le line 42
  8. theorem OAI.NCHitting.BitRefinement.listBits_mem_le line 52
  9. theorem OAI.NCHitting.BitRefinement.expr_width_le line 64
  10. inductive OAI.NCHitting.BitRefinement.Step line 109
  11. def OAI.NCHitting.BitRefinement.Step.tariff line 124
  12. def OAI.NCHitting.BitRefinement.Step.steps line 136
  13. theorem OAI.NCHitting.BitRefinement.self_le_square line 144
  14. theorem OAI.NCHitting.BitRefinement.Step.steps_le line 149
  15. abbrev OAI.NCHitting.BitRefinement.Trace line 158
  16. def OAI.NCHitting.BitRefinement.Trace.steps line 159
  17. def OAI.NCHitting.BitRefinement.powerTrace line 161
  18. def OAI.NCHitting.BitRefinement.exprTrace line 166
  19. def OAI.NCHitting.BitRefinement.programTrace line 183
  20. inductive OAI.NCHitting.BitRefinement.PowerExecution line 197
  21. inductive OAI.NCHitting.BitRefinement.ExprExecution line 205
  22. inductive OAI.NCHitting.BitRefinement.ProgramExecution line 229
  23. def OAI.NCHitting.BitRefinement.Exec line 255
  24. theorem OAI.NCHitting.BitRefinement.powerTrace_correct line 258
  25. theorem OAI.NCHitting.BitRefinement.exprTrace_correct line 266
  26. theorem OAI.NCHitting.BitRefinement.programTrace_correct line 288
  27. structure OAI.NCHitting.BitRefinement.Bounded line 314
  28. theorem OAI.NCHitting.BitRefinement.Bounded.mono line 318
  29. theorem OAI.NCHitting.BitRefinement.Bounded.append line 322
  30. theorem OAI.NCHitting.BitRefinement.bounded_flatMap line 334
  31. theorem OAI.NCHitting.BitRefinement.bounded_pair line 342
  32. theorem OAI.NCHitting.BitRefinement.bounded_single line 351
  33. theorem OAI.NCHitting.BitRefinement.expr_cost_pos line 359
  34. theorem OAI.NCHitting.BitRefinement.program_cost_pos line 362
  35. theorem OAI.NCHitting.BitRefinement.powerTrace_bounded line 365
  36. theorem OAI.NCHitting.BitRefinement.binary_bounded line 400
  37. theorem OAI.NCHitting.BitRefinement.exprTrace_bounded line 409
  38. theorem OAI.NCHitting.BitRefinement.sum_map_mem_le line 442
  39. def OAI.NCHitting.BitRefinement.iterationCost line 454
  40. theorem OAI.NCHitting.BitRefinement.loop_cost line 457
  41. theorem OAI.NCHitting.BitRefinement.programTrace_bounded line 463
  42. def OAI.NCHitting.BitRefinement.executionSteps line 591
  43. theorem OAI.NCHitting.BitRefinement.executionSteps_exec line 594
  44. theorem OAI.NCHitting.BitRefinement.executionSteps_le line 598
  45. theorem OAI.NCHitting.BitRefinement.execute_refines line 625