OAI/Combinatorics/KMedianRecovery/Encoding/PushWord.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.pushWord line 9
2. lemma OAI.MetricKMedianRecovery.BitMachine.pushWord_step line 13
3. abbrev OAI.MetricKMedianRecovery.BitMachine.FiniteFold.program line 25
4. def OAI.MetricKMedianRecovery.BitMachine.FiniteFold.cfg line 40
5. def OAI.MetricKMedianRecovery.BitMachine.FiniteFold.finish line 42
6. def OAI.MetricKMedianRecovery.BitMachine.FiniteFold.done line 44
7. lemma OAI.MetricKMedianRecovery.BitMachine.FiniteFold.nil_step line 47
8. lemma OAI.MetricKMedianRecovery.BitMachine.FiniteFold.cons_step line 51
9. lemma OAI.MetricKMedianRecovery.BitMachine.FiniteFold.finish_step line 56
10. def OAI.MetricKMedianRecovery.BitMachine.FiniteFold.outputs line 61
11. lemma OAI.MetricKMedianRecovery.BitMachine.FiniteFold.initial line 70
12. lemma OAI.MetricKMedianRecovery.BitMachine.FiniteFold.final line 73
13. def OAI.MetricKMedianRecovery.BitMachine.FiniteFold.computes line 77
14. lemma OAI.MetricKMedianRecovery.BitMachine.fold_orElse line 86
15. def OAI.MetricKMedianRecovery.BitMachine.head_computes line 94
16. lemma OAI.MetricKMedianRecovery.BitMachine.fold_empty line 98
17. def OAI.MetricKMedianRecovery.BitMachine.isEmpty_computes line 104