OAI/Combinatorics/KMedian/Programs/GreedyPackingProgram.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Completion.Rational.PackingProgram.Input line 15
  2. abbrev OAI.MetricKMedian.Completion.Rational.PackingProgram.Raw line 21
  3. def OAI.MetricKMedian.Completion.Rational.PackingProgram.Input.raw line 22
  4. def OAI.MetricKMedian.Completion.Rational.PackingProgram.Input.encode line 23
  5. abbrev OAI.MetricKMedian.Completion.Rational.PackingProgram.Cut line 24
  6. def OAI.MetricKMedian.Completion.Rational.PackingProgram.advance line 25
  7. structure OAI.MetricKMedian.Completion.Rational.PackingProgram.State line 30
  8. def OAI.MetricKMedian.Completion.Rational.PackingProgram.State.raw line 33
  9. def OAI.MetricKMedian.Completion.Rational.PackingProgram.State.encode line 34
  10. def OAI.MetricKMedian.Completion.Rational.PackingProgram.State.step line 35
  11. def OAI.MetricKMedian.Completion.Rational.PackingProgram.Input.state line 36
  12. def OAI.MetricKMedian.Completion.Rational.PackingProgram.Input.start line 37
  13. def OAI.MetricKMedian.Completion.Rational.PackingProgram.stepRaw line 39
  14. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.stepRaw_poly line 46
  15. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.any_view line 54
  16. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.stepRaw_state line 61
  17. def OAI.MetricKMedian.Completion.Rational.PackingProgram.stepProgram line 86
  18. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.state_iterate line 88
  19. def OAI.MetricKMedian.Completion.Rational.PackingProgram.startProgram line 96
  20. def OAI.MetricKMedian.Completion.Rational.PackingProgram.countProgram line 107
  21. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.input_bound line 110
  22. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.mask_length line 117
  23. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.state_size line 120
  24. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.packing_empty line 131
  25. theorem OAI.MetricKMedian.Completion.Rational.PackingProgram.advance_result line 133
  26. def OAI.MetricKMedian.Completion.Rational.PackingProgram.program line 147