OAI/Combinatorics/KMedianRecovery/Recovery/Stack.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.embedStacks_empty line 9
2. lemma OAI.MetricKMedianRecovery.BitMachine.embedStacks_pure line 16
3. lemma OAI.MetricKMedianRecovery.BitMachine.initList_bool line 22
4. lemma OAI.MetricKMedianRecovery.BitMachine.haltList_bool line 30
5. abbrev OAI.MetricKMedianRecovery.BitMachine.Composition.Stack line 41
6. def OAI.MetricKMedianRecovery.BitMachine.Composition.leftStack line 43
7. def OAI.MetricKMedianRecovery.BitMachine.Composition.rightStack line 45
8. lemma OAI.MetricKMedianRecovery.BitMachine.Composition.rightStack_input line 58
9. abbrev OAI.MetricKMedianRecovery.BitMachine.Composition.program line 61
10. def OAI.MetricKMedianRecovery.BitMachine.Composition.leftCfg line 75
11. def OAI.MetricKMedianRecovery.BitMachine.Composition.rightCfg line 78
12. lemma OAI.MetricKMedianRecovery.BitMachine.Composition.left_step line 81
13. lemma OAI.MetricKMedianRecovery.BitMachine.Composition.right_step line 96
14. lemma OAI.MetricKMedianRecovery.BitMachine.Composition.left_initial line 111
15. lemma OAI.MetricKMedianRecovery.BitMachine.Composition.handoff line 119
16. lemma OAI.MetricKMedianRecovery.BitMachine.Composition.right_final line 129
17. def OAI.MetricKMedianRecovery.BitMachine.Composition.outputs line 136