OAI/Combinatorics/RamseyFive/Trees/ReachedFailure.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.TreeCodec.flagTest line 17
2. def OAI.SharpRamseyFive.TreeCodec.flagAt line 20
3. lemma OAI.SharpRamseyFive.TreeCodec.flagAt_mono line 25
4. lemma OAI.SharpRamseyFive.TreeCodec.flagAt_or line 42
5. lemma OAI.SharpRamseyFive.TreeCodec.flagAt_context line 60
6. lemma OAI.SharpRamseyFive.TreeCodec.flagAt_abort line 77
7. lemma OAI.SharpRamseyFive.TreeCodec.flagAt_bound line 92
8. theorem OAI.SharpRamseyFive.TreeCodec.reached_abort_bound line 106