OAI/Combinatorics/KMedianRecovery/Recovery/Stack2.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedianRecovery.BitMachine.SameIO.Stack line 11
2. def OAI.MetricKMedianRecovery.BitMachine.SameIO.baseStack line 13
3. def OAI.MetricKMedianRecovery.BitMachine.SameIO.firstStack line 14
4. def OAI.MetricKMedianRecovery.BitMachine.SameIO.secondStack line 17
5. abbrev OAI.MetricKMedianRecovery.BitMachine.SameIO.program line 21
6. def OAI.MetricKMedianRecovery.BitMachine.SameIO.baseCfg line 37
7. def OAI.MetricKMedianRecovery.BitMachine.SameIO.firstCfg line 39
8. def OAI.MetricKMedianRecovery.BitMachine.SameIO.secondCfg line 41
9. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.base_step line 44
10. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.first_step line 58
11. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.second_step line 74
12. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.base_initial line 90
13. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.first_handoff line 98
14. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.second_handoff line 108
15. lemma OAI.MetricKMedianRecovery.BitMachine.SameIO.second_final line 118
16. def OAI.MetricKMedianRecovery.BitMachine.SameIO.outputs line 126
17. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.sameIO line 154