OAI/Combinatorics/KMedian/Binary/BooleanLoop.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.Loop.Key line 14
  2. abbrev OAI.MetricKMedian.Binary.Loop.Label line 15
  3. abbrev OAI.MetricKMedian.Binary.Loop.State line 16
  4. abbrev OAI.MetricKMedian.Binary.Loop.auxiliary line 17
  5. abbrev OAI.MetricKMedian.Binary.Loop.check line 18
  6. abbrev OAI.MetricKMedian.Binary.Loop.phase line 19
  7. def OAI.MetricKMedian.Binary.Loop.body line 21
  8. def OAI.MetricKMedian.Binary.Loop.source line 39
  9. def OAI.MetricKMedian.Binary.Loop.target line 41
  10. theorem OAI.MetricKMedian.Binary.Loop.source_ne_target line 43
  11. def OAI.MetricKMedian.Binary.Loop.following line 46
  12. def OAI.MetricKMedian.Binary.Loop.clean line 48
  13. def OAI.MetricKMedian.Binary.Loop.transfer line 50
  14. def OAI.MetricKMedian.Binary.Loop.checkCode line 57
  15. def OAI.MetricKMedian.Binary.Loop.code line 63
  16. abbrev OAI.MetricKMedian.Binary.Loop.machine line 68
  17. theorem OAI.MetricKMedian.Binary.Loop.code_body line 78
  18. theorem OAI.MetricKMedian.Binary.Loop.initial_body line 81
  19. def OAI.MetricKMedian.Binary.Loop.transferCfg line 87
  20. theorem OAI.MetricKMedian.Binary.Loop.transfer_cons line 90
  21. theorem OAI.MetricKMedian.Binary.Loop.transfer_run line 101
  22. theorem OAI.MetricKMedian.Binary.Loop.transfer_empty line 110
  23. theorem OAI.MetricKMedian.Binary.Loop.transfer_change line 119
  24. theorem OAI.MetricKMedian.Binary.Loop.transfer_end line 127
  25. theorem OAI.MetricKMedian.Binary.Loop.transfer_full line 135
  26. def OAI.MetricKMedian.Binary.Loop.checkCfg line 145
  27. theorem OAI.MetricKMedian.Binary.Loop.body_final line 148
  28. theorem OAI.MetricKMedian.Binary.Loop.check_step line 153
  29. theorem OAI.MetricKMedian.Binary.Loop.check_false line 168
  30. theorem OAI.MetricKMedian.Binary.Loop.check_true line 173
  31. theorem OAI.MetricKMedian.Binary.Loop.stop line 181
  32. theorem OAI.MetricKMedian.Binary.Loop.next line 188
  33. def OAI.MetricKMedian.Binary.encodeLoop line 200
  34. inductive OAI.MetricKMedian.Binary.BoundedRun line 204
  35. def OAI.MetricKMedian.Binary.PolyProgram.passTime line 214
  36. theorem OAI.MetricKMedian.Binary.PolyProgram.run_loop line 217
  37. def OAI.MetricKMedian.Binary.PolyProgram.loop line 249