OAI/Probability/MatroidProphet/Reverse/Trace.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MatroidProphet.ReverseTransition line 11
2. def OAI.MatroidProphet.reverseTrace line 16
3. lemma OAI.MatroidProphet.reverseCost_le_of_trace line 24
4. def OAI.MatroidProphet.traceHazards line 38
5. lemma OAI.MatroidProphet.mem_traceHazards line 44
6. def OAI.MatroidProphet.reverseFinal line 51
7. lemma OAI.MatroidProphet.reverseStepTree_path line 58
8. lemma OAI.MatroidProphet.reverseFinal_path line 74
9. lemma OAI.MatroidProphet.reverseFinal_from_univ line 94
10. def OAI.MatroidProphet.exitCost line 106
11. lemma OAI.MatroidProphet.reverseCost_exit_telescope line 109
12. lemma OAI.MatroidProphet.reverse_exit_total_one line 125