OAI/Combinatorics/ParityLifts/FunctionalCompile.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ParityWL.Complexity.FWhile.lower line 7
2. lemma OAI.ParityWL.Complexity.FEval.lower line 49
3. def OAI.ParityWL.Complexity.FCode.decision line 207
4. lemma OAI.ParityWL.Complexity.FEval.decision line 212
5. lemma OAI.ParityWL.Complexity.FEval.mono line 250
6. def OAI.ParityWL.Complexity.BEval line 269

   Source documentation

   One common budget bounds both the number of functional instructions and every intermediate serialized value. The compiler uses a universal quadratic power, independent of the finite program's syntax.

   def BEval (p : FCode) (x : DataTree) (B : ℕ) (y : DataTree) : Prop :=
   …

   Mentions: OAI.ParityWL.Complexity.FCode, OAI.ParityWL.Complexity.DataTree

7. lemma OAI.ParityWL.Complexity.BEval.mono line 272
8. lemma OAI.ParityWL.Complexity.BEval.bounds line 277
9. lemma OAI.ParityWL.Complexity.BEval.id line 283
10. lemma OAI.ParityWL.Complexity.BEval.nil line 285
11. lemma OAI.ParityWL.Complexity.BEval.left line 287
12. lemma OAI.ParityWL.Complexity.BEval.right line 289
13. lemma OAI.ParityWL.Complexity.BEval.pair line 292
14. lemma OAI.ParityWL.Complexity.BEval.seq line 301
15. lemma OAI.ParityWL.Complexity.BEval.nil_branch line 307
16. lemma OAI.ParityWL.Complexity.BEval.node_branch line 312
17. lemma OAI.ParityWL.Complexity.BEval.nil_cond line 317
18. lemma OAI.ParityWL.Complexity.BEval.node_cond line 323
19. lemma OAI.ParityWL.Complexity.BEval.loop_stop line 330
20. lemma OAI.ParityWL.Complexity.BEval.loop_next line 333
21. lemma OAI.ParityWL.Complexity.BEval.decision line 340