OAI/Combinatorics/ParityLifts/Polynomial.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.nat_poly_add line 7
  2. lemma OAI.ParityWL.Complexity.nat_poly_substitute line 16
  3. structure OAI.ParityWL.Complexity.PolyProgram line 24

    Source documentation

    Polynomial cost is witnessed by an actual finite tree program.

    structure PolyProgram (α β : Type) [TreeCodec α] [TreeCodec β] (f : α → β) where
…

    Mentions: OAI.ParityWL.Complexity.TreeCodec

  4. def OAI.ParityWL.Complexity.PolyProgram.of_linear line 30
  5. def OAI.ParityWL.Complexity.PolyProgram.id line 38
  6. def OAI.ParityWL.Complexity.PolyProgram.const line 41
  7. def OAI.ParityWL.Complexity.PolyProgram.fst line 45
  8. def OAI.ParityWL.Complexity.PolyProgram.snd line 49
  9. def OAI.ParityWL.Complexity.PolyProgram.comp line 53
  10. def OAI.ParityWL.Complexity.PolyProgram.pair line 77
  11. def OAI.ParityWL.Complexity.PolyProgram.congr line 88
  12. def OAI.ParityWL.Complexity.PolyProgram.ite line 95
  13. def OAI.ParityWL.Complexity.PolyProgram.equal line 114
  14. def OAI.ParityWL.Complexity.PolyProgram.expr line 125
  15. def OAI.ParityWL.Complexity.PolyProgram.cons line 133
  16. def OAI.ParityWL.Complexity.PolyProgram.tail line 137
  17. def OAI.ParityWL.Complexity.PolyProgram.head line 141
  18. def OAI.ParityWL.Complexity.PolyProgram.null line 146
  19. def OAI.ParityWL.Complexity.PolyProgram.not line 151
  20. def OAI.ParityWL.Complexity.PolyProgram.and line 155
  21. def OAI.ParityWL.Complexity.PolyProgram.or line 159
  22. lemma OAI.ParityWL.Complexity.treeEncode_list_length line 163
  23. lemma OAI.ParityWL.Complexity.treeEncode_of_mem line 169
  24. lemma OAI.ParityWL.Complexity.treeEncode_append_size line 179
  25. lemma OAI.ParityWL.Complexity.treeEncode_reverse_size line 185
  26. lemma OAI.ParityWL.Complexity.TreeProgram.foldWork_growing line 189
  27. lemma OAI.ParityWL.Complexity.list_sum_map_le line 229
  28. lemma OAI.ParityWL.Complexity.list_polynomial_sum line 239
  29. def OAI.ParityWL.Complexity.PolyProgram.foldlGrowing line 253
  30. lemma OAI.ParityWL.Complexity.list_fold_cons line 311
  31. def OAI.ParityWL.Complexity.PolyProgram.reverse line 317
  32. def OAI.ParityWL.Complexity.PolyProgram.append line 326