OAI/Combinatorics/KMedianRecovery/Recovery/StepThen.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.unit_update line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.step_then line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.time_mono line 23
  4. def OAI.MetricKMedianRecovery.BitMachine.one_step line 27
  5. def OAI.MetricKMedianRecovery.BitMachine.discardPrefix line 31
  6. lemma OAI.MetricKMedianRecovery.BitMachine.discardPrefix_pair line 37
  7. abbrev OAI.MetricKMedianRecovery.BitMachine.tailProgram line 43
  8. def OAI.MetricKMedianRecovery.BitMachine.tailCfg line 56
  9. def OAI.MetricKMedianRecovery.BitMachine.tailEnd line 57
  10. lemma OAI.MetricKMedianRecovery.BitMachine.tail_initial line 59
  11. lemma OAI.MetricKMedianRecovery.BitMachine.tail_final line 64
  12. lemma OAI.MetricKMedianRecovery.BitMachine.tail_step_nil line 69
  13. lemma OAI.MetricKMedianRecovery.BitMachine.tail_step_false line 73
  14. lemma OAI.MetricKMedianRecovery.BitMachine.tail_step_true line 78
  15. def OAI.MetricKMedianRecovery.BitMachine.tail_outputs line 83
  16. def OAI.MetricKMedianRecovery.BitMachine.discardPrefix_computes line 99
  17. def OAI.MetricKMedianRecovery.BitMachine.twoStacks line 106
  18. lemma OAI.MetricKMedianRecovery.BitMachine.twoStacks_false line 108
  19. lemma OAI.MetricKMedianRecovery.BitMachine.twoStacks_true line 109
  20. lemma OAI.MetricKMedianRecovery.BitMachine.twoStacks_update_false line 111
  21. lemma OAI.MetricKMedianRecovery.BitMachine.twoStacks_update_true line 116
  22. lemma OAI.MetricKMedianRecovery.BitMachine.twoStacks_pure_false line 121
  23. lemma OAI.MetricKMedianRecovery.BitMachine.twoStacks_pure_true line 126
  24. abbrev OAI.MetricKMedianRecovery.BitMachine.reverseProgram line 131
  25. def OAI.MetricKMedianRecovery.BitMachine.reverseCfg line 144
  26. def OAI.MetricKMedianRecovery.BitMachine.reverseEnd line 146
  27. lemma OAI.MetricKMedianRecovery.BitMachine.reverse_initial line 149
  28. lemma OAI.MetricKMedianRecovery.BitMachine.reverse_final line 154
  29. lemma OAI.MetricKMedianRecovery.BitMachine.reverse_step_nil line 159
  30. lemma OAI.MetricKMedianRecovery.BitMachine.reverse_step_cons line 164
  31. def OAI.MetricKMedianRecovery.BitMachine.reverse_outputs line 170
  32. def OAI.MetricKMedianRecovery.BitMachine.reverse_computes line 179