OAI/Computability/Superstring/Arithmetic.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Superstring.BitCode.Poly.mapFn line 15
2. theorem OAI.Superstring.BitCode.Poly.filterFn line 20
3. theorem OAI.Superstring.BitCode.Poly.sub line 25
4. theorem OAI.Superstring.BitCode.Poly.le line 40
5. theorem OAI.Superstring.BitCode.Poly.lt line 45
6. theorem OAI.Superstring.BitCode.Poly.max line 52
7. theorem OAI.Superstring.BitCode.Poly.min line 59
8. theorem OAI.Superstring.BitCode.Poly.mul line 68
9. theorem OAI.Superstring.BitCode.Poly.drop line 87
10. theorem OAI.Superstring.BitCode.Poly.take line 102
11. theorem OAI.Superstring.BitCode.Poly.getD line 110
12. theorem OAI.Superstring.BitCode.Poly.eqFn line 124
13. theorem OAI.Superstring.BitCode.Poly.leFn line 128
14. theorem OAI.Superstring.BitCode.Poly.ltFn line 131
15. theorem OAI.Superstring.BitCode.Poly.anyB line 134
16. theorem OAI.Superstring.BitCode.Poly.allB line 146
17. theorem OAI.Superstring.BitCode.Poly.anyFn line 153
18. theorem OAI.Superstring.BitCode.Poly.allFn line 160
19. theorem OAI.Superstring.BitCode.Poly.mem line 167
20. theorem OAI.Superstring.BitCode.Poly.memFn line 178
21. theorem OAI.Superstring.BitCode.Poly.sum line 182
22. theorem OAI.Superstring.BitCode.Poly.maxFold line 193
23. def OAI.Superstring.BitCode.rangeStep line 204
24. theorem OAI.Superstring.BitCode.iterate_rangeStep line 206
25. theorem OAI.Superstring.BitCode.Poly.range line 218
26. def OAI.Superstring.BitCode.equal line 245
27. def OAI.Superstring.BitCode.less line 246
28. def OAI.Superstring.BitCode.lessEq line 247
29. theorem OAI.Superstring.BitCode.Poly.equal line 251
30. theorem OAI.Superstring.BitCode.Poly.less line 253
31. theorem OAI.Superstring.BitCode.Poly.lessEq line 254
32. theorem OAI.Superstring.BitCode.Poly.recode line 257

    Source documentation

    Output reinterpretation executes exactly the same bits, not a hidden function.

     theorem recode {α β γ : Type} [Coded α] [Coded β] [Coded γ]
        {f : α → β} {g : α → γ} (hf : Poly f) (he : ∀ a, bits (g a) = bits (f a)) : Poly g := by
    …

    Mentions: OAI.Superstring.BitCode.Coded, OAI.Superstring.BitCode.Poly, OAI.Superstring.BitCode.bits

33. theorem OAI.Superstring.BitCode.Poly.inl line 264
34. theorem OAI.Superstring.BitCode.Poly.inr line 267
35. theorem OAI.Superstring.BitCode.Poly.headDWith line 270
36. def OAI.Superstring.BitCode.cappedStep line 279
37. theorem OAI.Superstring.BitCode.iterate_cappedStep_size line 282
38. theorem OAI.Superstring.BitCode.iterate_cappedStep_eq line 292
39. theorem OAI.Superstring.BitCode.Poly.cappedStep line 305
40. theorem OAI.Superstring.BitCode.Poly.cappedIterate line 311

    Source documentation

    A genuine bounded-workspace loop. The clock and workspace cap are unary input data. Every attempted step is executed/charged before its size check.

     theorem cappedIterate {α : Type} [Coded α] {f : α → α} (hf : Poly f) :
         Poly (fun p : ℕ × (ℕ × α) => ((Superstring.BitCode.cappedStep f)^[p.1] p.2).2) := by
    …

    Mentions: OAI.Superstring.BitCode.Coded, OAI.Superstring.BitCode.Poly, OAI.Superstring.BitCode.cappedStep

41. def OAI.Superstring.BitCode.uniqueStep line 324
42. def OAI.Superstring.BitCode.unique line 326
43. theorem OAI.Superstring.BitCode.mem_foldl_uniqueStep line 328
44. theorem OAI.Superstring.BitCode.nodup_foldl_uniqueStep line 336
45. theorem OAI.Superstring.BitCode.mem_unique line 347
46. theorem OAI.Superstring.BitCode.nodup_unique line 349
47. theorem OAI.Superstring.BitCode.Poly.unique line 354
48. theorem OAI.Superstring.BitCode.Poly.product line 372
49. def OAI.Superstring.BitCode.residueStep line 394
50. theorem OAI.Superstring.BitCode.iterate_residueStep_bound line 397
51. theorem OAI.Superstring.BitCode.iterate_residueStep line 406
52. theorem OAI.Superstring.BitCode.Poly.mod line 425
53. def OAI.Superstring.BitCode.intView line 442
54. theorem OAI.Superstring.BitCode.Parses.precomp line 446
55. instance OAI.Superstring.BitCode.codedInt line 451
56. theorem OAI.Superstring.BitCode.Poly.intCases line 464
57. theorem OAI.Superstring.BitCode.Poly.intCasesWith line 469
58. theorem OAI.Superstring.BitCode.Poly.ofNat line 479
59. theorem OAI.Superstring.BitCode.Poly.negSucc line 481
60. theorem OAI.Superstring.BitCode.Poly.toNat line 483
61. theorem OAI.Superstring.BitCode.Poly.natAbs line 484
62. theorem OAI.Superstring.BitCode.Poly.subNatNat line 491
63. theorem OAI.Superstring.BitCode.Poly.negInt line 499
64. theorem OAI.Superstring.BitCode.Poly.addInt line 504
65. theorem OAI.Superstring.BitCode.Poly.subInt line 521
66. theorem OAI.Superstring.BitCode.Poly.modIntNat line 526
67. theorem OAI.Superstring.BitCode.Poly.natCastInt line 537
68. def OAI.Superstring.BitCode.member line 543

    Source documentation

    Freeze the equality implementation at the abstract element type. Nested lists may otherwise elaborate different, extensionally equal BEq instances.

    def member {α : Type} [DecidableEq α] (a : α) (xs : List α) : Bool := decide (a ∈ xs)

69. theorem OAI.Superstring.BitCode.member_eq line 544
70. theorem OAI.Superstring.BitCode.Poly.member line 547