OAI/Combinatorics/ParityLifts/Arithmetic.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.fold_pred line 7
  2. lemma OAI.ParityWL.Complexity.fold_succ line 12
  3. def OAI.ParityWL.Complexity.PolyProgram.natAdd line 15
  4. def OAI.ParityWL.Complexity.PolyProgram.natSub line 23
  5. def OAI.ParityWL.Complexity.PolyProgram.natLe line 31
  6. def OAI.ParityWL.Complexity.PolyProgram.natMin line 34
  7. def OAI.ParityWL.Complexity.PolyProgram.drop line 38
  8. def OAI.ParityWL.Complexity.PolyProgram.take line 42
  9. def OAI.ParityWL.Complexity.PolyProgram.getD line 46
  10. def OAI.ParityWL.Complexity.PolyProgram.evalFin line 50
  11. def OAI.ParityWL.Complexity.PolyProgram.finite line 58
  12. def OAI.ParityWL.Complexity.rangeStep line 65
  13. lemma OAI.ParityWL.Complexity.fold_rangeStep line 67
  14. lemma OAI.ParityWL.Complexity.treeEncode_range'_size line 80
  15. def OAI.ParityWL.Complexity.PolyProgram.range line 91
  16. def OAI.ParityWL.Complexity.succBits line 116
  17. lemma OAI.ParityWL.Complexity.succBits_nil line 119
  18. lemma OAI.ParityWL.Complexity.succBits_false line 120
  19. lemma OAI.ParityWL.Complexity.succBits_true line 121
  20. lemma OAI.ParityWL.Complexity.succBits_bits line 124
  21. lemma OAI.ParityWL.Complexity.succBits_size line 137
  22. def OAI.ParityWL.Complexity.PolyProgram.succBits line 144
  23. lemma OAI.ParityWL.Complexity.fold_succBits line 152
  24. def OAI.ParityWL.Complexity.PolyProgram.natBits line 158
  25. def OAI.ParityWL.Complexity.PolyProgram.encodeNat line 168