OAI/Computability/MatchingCount/RecursiveEval.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinaryMatching.RecursiveEval.Branch line 9
2. inductive OAI.BinaryMatching.RecursiveEval.Command line 13
3. abbrev OAI.BinaryMatching.RecursiveEval.State line 17
4. def OAI.BinaryMatching.RecursiveEval.value line 22
5. def OAI.BinaryMatching.RecursiveEval.cost line 28
6. def OAI.BinaryMatching.RecursiveEval.calls line 34
7. def OAI.BinaryMatching.RecursiveEval.step line 40
8. lemma OAI.BinaryMatching.RecursiveEval.cost_le_calls line 51
9. lemma OAI.BinaryMatching.RecursiveEval.runs line 60
10. lemma OAI.BinaryMatching.RecursiveEval.runs_extra line 77