OAI/Combinatorics/SharpRamsey/Execution/ExecutedDeletion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FreshExecution.plannedPath line 13
2. lemma OAI.SharpLogRamsey.FreshExecution.plannedPath_subset line 18
3. lemma OAI.SharpLogRamsey.FreshExecution.plannedPath_card line 28
4. def OAI.SharpLogRamsey.FreshExecution.trialFailure line 39
5. def OAI.SharpLogRamsey.FreshExecution.pivotSuccess line 42
6. theorem OAI.SharpLogRamsey.FreshExecution.deletion_eq_path line 47
7. theorem OAI.SharpLogRamsey.FreshExecution.expected_deletion line 122
8. theorem OAI.SharpLogRamsey.FreshExecution.expected_deletion_quadratic line 137