OAI/Computability/MatchingCount/RecursiveBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryMatching.RecursiveEval.CommandGood line 11
2. def OAI.BinaryMatching.RecursiveEval.StateGood line 15
3. lemma OAI.BinaryMatching.RecursiveEval.step_good line 18
4. lemma OAI.BinaryMatching.RecursiveEval.step_length line 70
5. lemma OAI.BinaryMatching.RecursiveEval.iterate_length line 86
6. lemma OAI.BinaryMatching.RecursiveEval.iterate_good line 96
7. lemma OAI.BinaryMatching.RecursiveEval.code_call line 107
8. lemma OAI.BinaryMatching.RecursiveEval.code_join line 112
9. lemma OAI.BinaryMatching.RecursiveEval.state_code_bound line 118