OAI/Combinatorics/KMedianRecovery/Recovery/Step.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.step line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.step_computes line 13
3. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.next line 23
4. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.data_next line 24
5. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.counter_next line 28
6. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.output_next line 33
7. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.length_next line 40
8. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.rank_next line 46
9. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.iterate_bounds line 58
10. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.stop line 82
11. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.loop_computes line 88
12. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.next_nil line 103
13. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.next_cons line 106
14. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.loop_spec line 110
15. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.run line 119
16. def OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.run_computes line 122
17. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.run_pair line 131
18. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.clamp_iterate_eq line 134
19. lemma OAI.MetricKMedianRecovery.BitMachine.BoundedIteration.run_eq line 142