OAI/Computability/WLIdentification/WordArithmetic.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLIdentification.WordExpressions.NatPoly line 8
  2. abbrev OAI.WLIdentification.WordExpressions.BoolPoly line 9
  3. theorem OAI.WLIdentification.WordExpressions.BoolPoly.const line 13
  4. theorem OAI.WLIdentification.WordExpressions.BoolPoly.not line 14
  5. theorem OAI.WLIdentification.WordExpressions.BoolPoly.and line 17
  6. theorem OAI.WLIdentification.WordExpressions.BoolPoly.or line 21
  7. theorem OAI.WLIdentification.WordExpressions.BoolPoly.rename line 25
  8. theorem OAI.WLIdentification.WordExpressions.NatPoly.length line 31
  9. theorem OAI.WLIdentification.WordExpressions.NatPoly.var line 33
  10. theorem OAI.WLIdentification.WordExpressions.NatPoly.const line 34
  11. theorem OAI.WLIdentification.WordExpressions.NatPoly.rename line 35
  12. theorem OAI.WLIdentification.WordExpressions.NatPoly.add line 38
  13. theorem OAI.WLIdentification.WordExpressions.NatPoly.succ line 41
  14. theorem OAI.WLIdentification.WordExpressions.NatPoly.sub line 42
  15. theorem OAI.WLIdentification.WordExpressions.NatPoly.le line 45
  16. theorem OAI.WLIdentification.WordExpressions.NatPoly.lt line 49
  17. theorem OAI.WLIdentification.WordExpressions.NatPoly.eqtest line 53
  18. theorem OAI.WLIdentification.WordExpressions.NatPoly.ite line 57
  19. theorem OAI.WLIdentification.WordExpressions.NatPoly.max line 63
  20. theorem OAI.WLIdentification.WordExpressions.NatPoly.min line 67
  21. theorem OAI.WLIdentification.WordExpressions.NatPoly.mulVars line 72
  22. theorem OAI.WLIdentification.WordExpressions.NatPoly.mul line 86
  23. theorem OAI.WLIdentification.WordExpressions.NatPoly.pow_const line 92
  24. theorem OAI.WLIdentification.WordExpressions.Poly.nth line 103

    Source documentation

    The i-th bit in left-to-right order, with a false default outside the word.

    theorem nth {w : (Fin n → Word) → Word} {i : (Fin n → Word) → ℕ}
    (hw : Poly w) (hi : NatPoly i) : BoolPoly (fun S => (w S)[i S]?.getD false) := by
…

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.Poly, OAI.WLIdentification.WordExpressions.NatPoly, OAI.WLIdentification.WordExpressions.BoolPoly

  25. theorem OAI.WLIdentification.WordExpressions.Poly.tabulate line 133

    Source documentation

    Polynomially bounded tabulation is implemented by captured-count iteration; there is no list-construction oracle in the underlying Machine.

    theorem tabulate {c : (Fin n → Word) → ℕ} {p : (Fin (n+1) → Word) → Bool}
    (hc : NatPoly c) (hp : BoolPoly p) :
    Poly (fun S => (List.range (c S)).map (fun i => p (Fin.snoc S (unary i)))) := by
…

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.NatPoly, OAI.WLIdentification.WordExpressions.BoolPoly, OAI.WLIdentification.WordExpressions.Poly, OAI.WLIdentification.WordExpressions.unary

  26. theorem OAI.WLIdentification.WordExpressions.Poly.length_bound line 171
  27. theorem OAI.WLIdentification.WordExpressions.NatPoly.bound line 181
  28. def OAI.WLIdentification.WordExpressions.NatPoly.stages line 187

    Source documentation

    Natural-valued iteration, represented by literal unary words.

    def stages (f : (Fin (n+2) → Word) → ℕ) (S : Fin n → Word) (a : ℕ) : ℕ → ℕ
  | 0 => a
  | k+1 => f (Fin.snoc (Fin.snoc S (unary k)) (unary (stages f S a k)))

    Mentions: OAI.WLIdentification.Word, OAI.WLIdentification.WordExpressions.unary

  29. theorem OAI.WLIdentification.WordExpressions.NatPoly.stages_word line 191
  30. theorem OAI.WLIdentification.WordExpressions.NatPoly.loop line 197
  31. theorem OAI.WLIdentification.WordExpressions.BoolPoly.boundedAll line 212
  32. theorem OAI.WLIdentification.WordExpressions.BoolPoly.boundedAny line 234
  33. theorem OAI.WLIdentification.WordExpressions.Poly.applyWord line 248
  34. theorem OAI.WLIdentification.WordExpressions.NatPoly.findGreatest line 261
  35. theorem OAI.WLIdentification.WordExpressions.NatPoly.div line 287
  36. theorem OAI.WLIdentification.WordExpressions.NatPoly.mod line 317
  37. theorem OAI.WLIdentification.WordExpressions.Poly.computes line 326