OAI/Computability/WLIdentification/PolynomialArithmetic.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.WordExpressions.Poly.replicate line 11
  2. theorem OAI.WLIdentification.WordExpressions.Poly.mapBits line 17
  3. theorem OAI.WLIdentification.WordExpressions.Poly.append line 22
  4. theorem OAI.WLIdentification.WordExpressions.Poly.reverse line 53
  5. theorem OAI.WLIdentification.WordExpressions.Poly.take line 66
  6. theorem OAI.WLIdentification.WordExpressions.Poly.dropPrefix line 76
  7. theorem OAI.WLIdentification.WordExpressions.NatPoly.sum line 96
  8. theorem OAI.WLIdentification.WordExpressions.NatPoly.pair line 141
  9. theorem OAI.WLIdentification.WordExpressions.NatPoly.sqrt line 148
  10. theorem OAI.WLIdentification.WordExpressions.NatPoly.unpair_fst line 163
  11. theorem OAI.WLIdentification.WordExpressions.NatPoly.unpair_snd line 171
  12. theorem OAI.WLIdentification.WordExpressions.NatPoly.cap_mul line 184
  13. theorem OAI.WLIdentification.WordExpressions.NatPoly.cappedPow line 193
  14. theorem OAI.WLIdentification.WordExpressions.NatPoly.bitsSize line 216
  15. theorem OAI.WLIdentification.WordExpressions.NatPoly.div_cap line 250
  16. theorem OAI.WLIdentification.WordExpressions.NatPoly.testBit line 255
  17. theorem OAI.WLIdentification.WordExpressions.Poly.bits line 265
  18. theorem OAI.WLIdentification.WordExpressions.Poly.binary line 276
  19. def OAI.WLIdentification.WordExpressions.NatPoly.decodeCap line 286

    Source documentation

    Saturated, genuine left-to-right binary decoding. It stays unary-bounded by c.

    def decodeCap (w : Word) (c : ℕ) : ℕ := w.foldl (fun x b => Min.min (2*x+if b then 1 else 0) c) 0

    Mentions: OAI.WLIdentification.Word

  20. theorem OAI.WLIdentification.WordExpressions.NatPoly.decodeCap_aux line 288
  21. theorem OAI.WLIdentification.WordExpressions.NatPoly.decodeCap_correct line 306
  22. theorem OAI.WLIdentification.WordExpressions.NatPoly.decode line 309