OAI/Combinatorics/KMedianRecovery/Recovery/DigitBit.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.digitBit line 11
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.digitRem line 12
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.process line 15
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.evalMSB line 19
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.evalMSB_eq line 23
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.digit_balance line 32
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.process_spec line 54
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.next_pack_nil line 65
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.next_pack_cons line 70
10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.iterate_pack line 79
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.rank_pack line 88
12. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.normalize_computes line 92
13. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.zeroTest_computes line 95
14. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.setupWords line 99
15. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.withDivision line 102
16. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.rawDivide line 104
17. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divide line 107
18. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.setupWords_computes line 110
19. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.withDivision_computes line 114
20. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.rawDivide_computes line 119
21. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divide_computes line 126
22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.divide_pair line 133
23. def OAI.MetricKMedianRecovery.BitMachine.BinaryDivision.division line 153