OAI/Combinatorics/KMedian/Binary/BooleanComposition.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Binary.Compose.Key line 15
  2. abbrev OAI.MetricKMedian.Binary.Compose.Label line 16
  3. abbrev OAI.MetricKMedian.Binary.Compose.State line 17
  4. abbrev OAI.MetricKMedian.Binary.Compose.phaseLabel line 19
  5. abbrev OAI.MetricKMedian.Binary.Compose.auxiliary line 20
  6. def OAI.MetricKMedian.Binary.Compose.left line 22
  7. def OAI.MetricKMedian.Binary.Compose.right line 41
  8. def OAI.MetricKMedian.Binary.Compose.source line 60
  9. def OAI.MetricKMedian.Binary.Compose.target line 62
  10. theorem OAI.MetricKMedian.Binary.Compose.source_ne_target line 64
  11. def OAI.MetricKMedian.Binary.Compose.following line 67
  12. def OAI.MetricKMedian.Binary.Compose.clean line 70
  13. def OAI.MetricKMedian.Binary.Compose.transfer line 72
  14. def OAI.MetricKMedian.Binary.Compose.code line 79
  15. abbrev OAI.MetricKMedian.Binary.Compose.machine line 84
  16. theorem OAI.MetricKMedian.Binary.Compose.code_left line 94
  17. theorem OAI.MetricKMedian.Binary.Compose.code_right line 97
  18. theorem OAI.MetricKMedian.Binary.Compose.initial_left line 100
  19. theorem OAI.MetricKMedian.Binary.Compose.final_right line 106
  20. def OAI.MetricKMedian.Binary.twoStacks line 116
  21. theorem OAI.MetricKMedian.Binary.twoStacks_source line 119
  22. theorem OAI.MetricKMedian.Binary.twoStacks_target line 122
  23. theorem OAI.MetricKMedian.Binary.twoStacks_move line 125
  24. theorem OAI.MetricKMedian.Binary.twoStacks_pop_empty line 135
  25. def OAI.MetricKMedian.Binary.Compose.transferCfg line 143
  26. theorem OAI.MetricKMedian.Binary.Compose.transfer_cons line 147
  27. theorem OAI.MetricKMedian.Binary.Compose.transfer_run line 159
  28. theorem OAI.MetricKMedian.Binary.Compose.transfer_empty line 168
  29. theorem OAI.MetricKMedian.Binary.Compose.left_final_transfer line 178
  30. theorem OAI.MetricKMedian.Binary.Compose.transfer_change line 187
  31. theorem OAI.MetricKMedian.Binary.Compose.transfer_end line 197
  32. theorem OAI.MetricKMedian.Binary.Compose.transfer_full line 208
  33. theorem OAI.MetricKMedian.Binary.Compose.run line 220