OAI/Combinatorics/SharpRamsey/Execution/FreshExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.FreshExecution.arrive line 15
2. theorem OAI.SharpLogRamsey.FreshExecution.arrive_congr line 27
3. def OAI.SharpLogRamsey.FreshExecution.outsideState line 44
4. theorem OAI.SharpLogRamsey.FreshExecution.arrive_outside line 50
5. def OAI.SharpLogRamsey.FreshExecution.produced line 59
6. theorem OAI.SharpLogRamsey.FreshExecution.produced_bound line 69
7. def OAI.SharpLogRamsey.FreshExecution.fixedRead line 97
8. def OAI.SharpLogRamsey.FreshExecution.fixedChoose line 100
9. theorem OAI.SharpLogRamsey.FreshExecution.fixed_decoder_correct line 105