OAI/Combinatorics/SharpRamsey/Selection/FreshAccrual.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FreshExecution.labels line 13
2. lemma OAI.SharpLogRamsey.FreshExecution.labels_nil line 15
3. lemma OAI.SharpLogRamsey.FreshExecution.labels_node line 17
4. def OAI.SharpLogRamsey.FreshExecution.Separated line 24
5. lemma OAI.SharpLogRamsey.FreshExecution.separated_of_nodup line 29
6. lemma OAI.SharpLogRamsey.FreshExecution.arrive_absent line 43
7. def OAI.SharpLogRamsey.FreshExecution.accrued line 62
8. lemma OAI.SharpLogRamsey.FreshExecution.produced_root line 72
9. lemma OAI.SharpLogRamsey.FreshExecution.produced_left line 78
10. lemma OAI.SharpLogRamsey.FreshExecution.produced_right line 93
11. lemma OAI.SharpLogRamsey.FreshExecution.produced_deleted line 108
12. theorem OAI.SharpLogRamsey.FreshExecution.accrued_eq_sum line 115
13. theorem OAI.SharpLogRamsey.FreshExecution.accrued_expectation line 147