OAI/Computability/MinUncut/Estimates/BlocksEffectivity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncut.Preprocess.Syntax.prefCode line 12
2. lemma OAI.MinUncut.Preprocess.Syntax.p_prefCode line 14
3. def OAI.MinUncut.Preprocess.Syntax.stepCode line 20
4. lemma OAI.MinUncut.Preprocess.Syntax.p_stepCode line 23
5. lemma OAI.MinUncut.Preprocess.Syntax.prefCode_eq line 27
6. lemma OAI.MinUncut.Preprocess.Syntax.stepCode_eq line 32
7. lemma OAI.MinUncut.Preprocess.Syntax.p_iterCode line 35
8. def OAI.MinUncut.Preprocess.Syntax.forwardCode line 39
9. lemma OAI.MinUncut.Preprocess.Syntax.p_forwardCode line 43
10. lemma OAI.MinUncut.Preprocess.Syntax.forwardCode_eq line 48