OAI/Combinatorics/MatchingCount/Complexity/StackCompilerCost.lean
11 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MatchingFPRAS.StackCost.accessesline 11 - def
OAI.MatchingFPRAS.StackCost.StackBoundline 19 - lemma
OAI.MatchingFPRAS.StackCost.accesses_runline 21 - lemma
OAI.MatchingFPRAS.StackCost.go_timeline 24 - lemma
OAI.MatchingFPRAS.StackCost.return_timeline 39 - lemma
OAI.MatchingFPRAS.StackCost.action_boundline 55 - lemma
OAI.MatchingFPRAS.StackCost.stepAux_boundline 66 - theorem
OAI.MatchingFPRAS.StackCost.statement_timeline 83 - lemma
OAI.MatchingFPRAS.StackCost.advance_boundline 142 - lemma
OAI.MatchingFPRAS.StackCost.one_step_timeline 151 - theorem
OAI.MatchingFPRAS.StackCost.execution_timeline 169