OAI/Combinatorics/SharpRamsey/Execution/ExecutedLoss.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FreshExecution.compatible line 13
2. lemma OAI.SharpLogRamsey.FreshExecution.compatible_append line 16
3. lemma OAI.SharpLogRamsey.FreshExecution.retained_all line 20
4. def OAI.SharpLogRamsey.FreshExecution.fullOutput line 24
5. lemma OAI.SharpLogRamsey.FreshExecution.fullOutput_nil line 32
6. lemma OAI.SharpLogRamsey.FreshExecution.fullOutput_fail line 39
7. lemma OAI.SharpLogRamsey.FreshExecution.fullOutput_success line 48
8. def OAI.SharpLogRamsey.FreshExecution.nodeCharge line 60
9. def OAI.SharpLogRamsey.FreshExecution.charges line 72
10. lemma OAI.SharpLogRamsey.FreshExecution.accrued_congr line 81
11. theorem OAI.SharpLogRamsey.FreshExecution.output_loss_eq_accrued line 101
12. theorem OAI.SharpLogRamsey.FreshExecution.expected_output_loss line 146