OAI/Probability/MatroidProphet/RevealComposition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatroidProphet.RevealTree.bind line 10
2. lemma OAI.MatroidProphet.RevealTree.run_bind line 15
3. lemma OAI.MatroidProphet.RevealTree.queried_bind line 24
4. lemma OAI.MatroidProphet.RevealTree.fresh_bind line 34
5. lemma OAI.MatroidProphet.RevealTree.run_congr line 54
6. lemma OAI.MatroidProphet.RevealTree.queried_congr line 72
7. def OAI.MatroidProphet.RevealTree.transaction line 90
8. lemma OAI.MatroidProphet.RevealTree.transaction_fresh line 95
9. lemma OAI.MatroidProphet.RevealTree.transaction_run line 115