OAI/Combinatorics/MatchingCount/Tapes/Online.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- inductive
OAI.MatchingFPRAS.OnlineStack.Executesline 11 - lemma
OAI.MatchingFPRAS.OnlineStack.Executes.bindline 25 - def
OAI.MatchingFPRAS.OnlineStack.Executes.factorline 36 - lemma
OAI.MatchingFPRAS.OnlineStack.Executes.factor_monoline 39 - lemma
OAI.MatchingFPRAS.OnlineStack.Executes.factor_shiftline 43 - theorem
OAI.MatchingFPRAS.OnlineStack.Executes.compileline 48