OAI/Combinatorics/ParityLifts/FunctionalCode.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ParityWL.Complexity.FCode line 10

   Source documentation

   A finite first-order functional language on binary trees. There are no function-valued atoms: only projections, pairing, composition, branching and an ordinary data-dependent loop.

   inductive FCode where
   …

2. inductive OAI.ParityWL.Complexity.FWhile line 19
3. inductive OAI.ParityWL.Complexity.FEval line 25
4. lemma OAI.ParityWL.Complexity.FEval.bounds line 46
5. lemma OAI.ParityWL.Complexity.FEval.loop_iff line 62
6. def OAI.ParityWL.Complexity.FCode.depth line 76
7. lemma OAI.ParityWL.Complexity.FCode.depth_pos line 83
8. def OAI.ParityWL.Complexity.FCode.lower line 86
9. def OAI.ParityWL.Complexity.FCode.factor line 113
10. lemma OAI.ParityWL.Complexity.FCode.factor_pos line 120
11. def OAI.ParityWL.Complexity.CleanAbove line 122
12. lemma OAI.ParityWL.Complexity.CleanAbove.update_self line 125
13. lemma OAI.ParityWL.Complexity.CleanAbove.update_later line 131
14. lemma OAI.ParityWL.Complexity.CleanAbove.erase_next line 138