OAI/Combinatorics/KMedianRecovery/Recovery/Normalize.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.value_append line 12
2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.value_append_true_pos line 17
3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.bits_value_append_true line 23
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.bits_value_reverse line 31
5. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.normalize line 40
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.normalize_eq_bits line 43
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.normalize_add line 46
8. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trimProgram line 50
9. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trimCfg line 65
10. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trimDone line 66
11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_initial line 68
12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_final line 71
13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_nil line 74
14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_false line 77
15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_true line 81
16. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_outputs line 86
17. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.trim_computes line 96
18. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.add_computes line 103
19. def OAI.MetricKMedianRecovery.BitMachine.BinaryArithmetic.addition line 108