OAI/Computability/Logspace/ContourPrograms.lean

GitHub source file

176 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ExactDerandomization.Sub.Bow line 21

   Source documentation

   Common path-table scripts. The prefix of the digit stream attached to an endpoint will be assembled with repeated stationary queries from the initiation. use steps=0 for the plain cap kernel.

   structure Bow where
   …

2. abbrev OAI.ExactDerandomization.Sub.Jet line 36
3. abbrev OAI.ExactDerandomization.Sub.Jet.band line 38
4. abbrev OAI.ExactDerandomization.Sub.Jet.port line 39
5. abbrev OAI.ExactDerandomization.Sub.Jet.rune line 40
6. abbrev OAI.ExactDerandomization.Sub.Jet.invp line 41
7. abbrev OAI.ExactDerandomization.Sub.Jet.sizeJ line 42
8. def OAI.ExactDerandomization.Sub.Jet.jik line 43
9. def OAI.ExactDerandomization.Sub.Jet.turn line 44
10. def OAI.ExactDerandomization.Sub.Jet.cap line 46
11. lemma OAI.ExactDerandomization.Sub.Jet.capK line 47
12. lemma OAI.ExactDerandomization.Sub.Jet.jikK line 49
13. lemma OAI.ExactDerandomization.Sub.Jet.turnK line 52
14. def OAI.ExactDerandomization.Sub.Jet.tug line 55
15. lemma OAI.ExactDerandomization.Sub.Jet.tugK line 56
16. lemma OAI.ExactDerandomization.Sub.Jet.cap_tug line 58
17. lemma OAI.ExactDerandomization.Sub.Jet.aft_tug line 59
18. abbrev OAI.ExactDerandomization.Sub.Card line 61
19. def OAI.ExactDerandomization.Sub.cname line 63
20. abbrev OAI.ExactDerandomization.Sub.prime line 64
21. abbrev OAI.ExactDerandomization.Sub.tell line 65
22. abbrev OAI.ExactDerandomization.Sub.going line 66
23. abbrev OAI.ExactDerandomization.Sub.done line 67
24. lemma OAI.ExactDerandomization.Sub.cnameK line 68
25. lemma OAI.ExactDerandomization.Sub.decname line 71
26. def OAI.ExactDerandomization.Sub.Bow.readyJ line 76
27. lemma OAI.ExactDerandomization.Sub.Bow.readyK line 77
28. def OAI.ExactDerandomization.Sub.Bow.hint line 80
29. abbrev OAI.ExactDerandomization.Sub.Bow.Xtra line 82
30. def OAI.ExactDerandomization.Sub.Bow.along line 83
31. def OAI.ExactDerandomization.Sub.Bow.journey line 85
32. lemma OAI.ExactDerandomization.Sub.Bow.hintK line 88
33. lemma OAI.ExactDerandomization.Sub.Bow.journeyK line 90
34. abbrev OAI.ExactDerandomization.Sub.Bow.Cap line 95
35. abbrev OAI.ExactDerandomization.Sub.Bow.Lift line 96
36. abbrev OAI.ExactDerandomization.Sub.Bow.purec line 97
37. def OAI.ExactDerandomization.Sub.Bow.inprog line 98
38. lemma OAI.ExactDerandomization.Sub.Bow.pureK line 117
39. lemma OAI.ExactDerandomization.Sub.Bow.goingK line 119
40. lemma OAI.ExactDerandomization.Sub.Bow.progK line 124
41. abbrev OAI.ExactDerandomization.Sub.Bow.Cover line 176
42. def OAI.ExactDerandomization.Sub.Bow.air line 177
43. def OAI.ExactDerandomization.Sub.Bow.loom line 189
44. lemma OAI.ExactDerandomization.Sub.Bow.airK line 190
45. lemma OAI.ExactDerandomization.Sub.Bow.loomK line 210
46. def OAI.ExactDerandomization.Sub.Bow.peel line 213

    Source documentation

    token extraction (destination)

    def peel (v:Card):ℕ :=
    …

    Mentions: OAI.ExactDerandomization.Sub.Card

47. def OAI.ExactDerandomization.Sub.Bow.peel0 line 216
48. lemma OAI.ExactDerandomization.Sub.Bow.peelK line 219
49. def OAI.ExactDerandomization.Sub.Bow.stripe0 line 226
50. lemma OAI.ExactDerandomization.Sub.Bow.stripeK line 231
51. def OAI.ExactDerandomization.Sub.Bow.reader line 242
52. lemma OAI.ExactDerandomization.Sub.Bow.readerK line 243
53. def OAI.ExactDerandomization.Sub.Bow.Rune0 line 245
54. structure OAI.ExactDerandomization.Sub.Quill line 261

    Source documentation

    Settings for local correctness at a contour invocation.

    structure Quill where
    …

55. def OAI.ExactDerandomization.Sub.Quill.p line 272
56. abbrev OAI.ExactDerandomization.Sub.Quill.x0 line 273
57. abbrev OAI.ExactDerandomization.Sub.Quill.q line 274
58. abbrev OAI.ExactDerandomization.Sub.Quill.B line 275
59. abbrev OAI.ExactDerandomization.Sub.Quill.H line 276
60. abbrev OAI.ExactDerandomization.Sub.Quill.child line 277
61. abbrev OAI.ExactDerandomization.Sub.Quill.ceiling line 278
62. structure OAI.ExactDerandomization.Sub.Quill.Tidy line 280
63. def OAI.ExactDerandomization.Sub.Quill.Cush line 290
64. lemma OAI.ExactDerandomization.Sub.Quill.leftP line 291
65. lemma OAI.ExactDerandomization.Sub.Quill.rightP line 292
66. lemma OAI.ExactDerandomization.Sub.Quill.cname_l line 294
67. lemma OAI.ExactDerandomization.Sub.Quill.inProgG line 309
68. lemma OAI.ExactDerandomization.Sub.Quill.capDone line 322
69. lemma OAI.ExactDerandomization.Sub.Quill.capPrime line 330
70. lemma OAI.ExactDerandomization.Sub.Quill.capTell line 335
71. lemma OAI.ExactDerandomization.Sub.Quill.prepaid line 345
72. lemma OAI.ExactDerandomization.Sub.Quill.team0 line 359
73. lemma OAI.ExactDerandomization.Sub.Quill.team line 366
74. lemma OAI.ExactDerandomization.Sub.Quill.structure_pay line 370
75. lemma OAI.ExactDerandomization.Sub.Quill.score_pay line 385
76. abbrev OAI.ExactDerandomization.Sub.Quill.Cr line 411
77. abbrev OAI.ExactDerandomization.Sub.Quill.Track line 412
78. abbrev OAI.ExactDerandomization.Sub.Quill.Aq line 414
79. lemma OAI.ExactDerandomization.Sub.Quill.Ax line 415
80. lemma OAI.ExactDerandomization.Sub.Quill.deco line 416
81. lemma OAI.ExactDerandomization.Sub.Quill.tripk line 419
82. lemma OAI.ExactDerandomization.Sub.Quill.stable line 421
83. abbrev OAI.ExactDerandomization.Sub.Quill.garnish line 424
84. def OAI.ExactDerandomization.Sub.Quill.chainR line 425
85. lemma OAI.ExactDerandomization.Sub.Quill.chain_next line 426
86. abbrev OAI.ExactDerandomization.Sub.Quill.scent line 427
87. def OAI.ExactDerandomization.Sub.Quill.Stringent line 429
88. structure OAI.ExactDerandomization.Sub.Quill.Gown line 431
89. lemma OAI.ExactDerandomization.Sub.Quill.chain_size line 440
90. lemma OAI.ExactDerandomization.Sub.Quill.pointing line 453
91. lemma OAI.ExactDerandomization.Sub.Quill.prepared line 458
92. lemma OAI.ExactDerandomization.Sub.Quill.shut line 486
93. lemma OAI.ExactDerandomization.Sub.Quill.different line 490
94. abbrev OAI.ExactDerandomization.Sub.Quill.fill line 507
95. abbrev OAI.ExactDerandomization.Sub.Quill.hear line 508
96. abbrev OAI.ExactDerandomization.Sub.Quill.tagH line 509
97. abbrev OAI.ExactDerandomization.Sub.Quill.callB line 510
98. abbrev OAI.ExactDerandomization.Sub.Quill.callP line 511
99. abbrev OAI.ExactDerandomization.Sub.Quill.lower line 512
100. abbrev OAI.ExactDerandomization.Sub.Quill.portD line 513
101. abbrev OAI.ExactDerandomization.Sub.Quill.dives line 514
102. def OAI.ExactDerandomization.Sub.Quill.kidJ line 515
103. lemma OAI.ExactDerandomization.Sub.Quill.turnkid line 516
104. def OAI.ExactDerandomization.Sub.Quill.calm line 518
105. def OAI.ExactDerandomization.Sub.Quill.Orders line 520
106. def OAI.ExactDerandomization.Sub.Quill.little line 523
107. structure OAI.ExactDerandomization.Sub.Quill.Rating line 526
108. structure OAI.ExactDerandomization.Sub.Quill.Bolts line 534
109. structure OAI.ExactDerandomization.Sub.Quill.Chess line 542

     Source documentation

     canonical path selection supplies a coherent and costed path, not just a validity bit.

     structure Chess (a p h e c z y w:ℕ) : Prop where
     …

     Mentions: OAI.ExactDerandomization.Sub.Quill.p

110. inductive OAI.ExactDerandomization.Sub.Quill.Herd line 555

     Source documentation

     Valid terminal program coherence/cost trace

     inductive Herd : ℕ→ℕ→ℕ→ℕ→ℕ→ℕ→Prop
     
        | solo {a p h e c z w} (h0:u.Chess a p h e c z z w) (hd:u.dives a p h=false):
                              Herd a p c h e w
        | pair {a p h e c z y w f g} (hr:u.Chess a p h e c z y w) (hv:u.dives a p h=true)
                 (hd:u.bulk (u.lower a p h)+u.grit a ≤ u.bulk a)
                 (hy:u.grit (u.lower a p h) ≤ 2*u.grit a)
                 (he:Herd (u.lower a p h) (u.portD a p h) z f g y):
                               Herd a p c h e w

     Mentions: OAI.ExactDerandomization.Sub.Quill.p

111. lemma OAI.ExactDerandomization.Sub.Quill.Herd.on line 565
112. inductive OAI.ExactDerandomization.Sub.Quill.Lane line 568
113. abbrev OAI.ExactDerandomization.Sub.Quill.wagon line 573
114. lemma OAI.ExactDerandomization.Sub.Quill.wagon_eq line 574
115. def OAI.ExactDerandomization.Sub.Quill.cart line 575
116. structure OAI.ExactDerandomization.Sub.Quill.Course line 577
117. lemma OAI.ExactDerandomization.Sub.Quill.coal line 583
118. lemma OAI.ExactDerandomization.Sub.Quill.rag line 592
119. lemma OAI.ExactDerandomization.Sub.Quill.aloft line 596
120. lemma OAI.ExactDerandomization.Sub.Quill.goto line 601
121. lemma OAI.ExactDerandomization.Sub.Quill.price1 line 615
122. lemma OAI.ExactDerandomization.Sub.Quill.timeok line 620
123. lemma OAI.ExactDerandomization.Sub.Quill.ae line 626
124. lemma OAI.ExactDerandomization.Sub.Quill.resultv line 630
125. lemma OAI.ExactDerandomization.Sub.Quill.taking line 665
126. abbrev OAI.ExactDerandomization.Sub.Quill.future1 line 670
127. lemma OAI.ExactDerandomization.Sub.Quill.future_eq line 671
128. lemma OAI.ExactDerandomization.Sub.Quill.ore0 line 673
129. lemma OAI.ExactDerandomization.Sub.Quill.ore1 line 677
130. lemma OAI.ExactDerandomization.Sub.Quill.ore4 line 681
131. lemma OAI.ExactDerandomization.Sub.Quill.pairTok2 line 686
132. lemma OAI.ExactDerandomization.Sub.Quill.pairTok5 line 690
133. lemma OAI.ExactDerandomization.Sub.Quill.first0 line 695
134. lemma OAI.ExactDerandomization.Sub.Quill.helm line 706
135. lemma OAI.ExactDerandomization.Sub.Quill.swift0 line 720
136. lemma OAI.ExactDerandomization.Sub.Quill.prowl line 727
137. lemma OAI.ExactDerandomization.Sub.Quill.shiver line 740
138. abbrev OAI.ExactDerandomization.Sub.Quill.nextJ line 763
139. lemma OAI.ExactDerandomization.Sub.Quill.ore2 line 764
140. lemma OAI.ExactDerandomization.Sub.Quill.blink0 line 772
141. lemma OAI.ExactDerandomization.Sub.Quill.downfit line 776
142. lemma OAI.ExactDerandomization.Sub.Quill.pop5 line 784
143. lemma OAI.ExactDerandomization.Sub.Quill.popped_only line 801
144. lemma OAI.ExactDerandomization.Sub.Quill.reverse_fit line 804
145. lemma OAI.ExactDerandomization.Sub.Quill.flagdown line 807
146. lemma OAI.ExactDerandomization.Sub.Quill.ladder line 813
147. lemma OAI.ExactDerandomization.Sub.Quill.dawn line 838
148. lemma OAI.ExactDerandomization.Sub.Quill.cool line 842
149. lemma OAI.ExactDerandomization.Sub.Quill.onion line 855
150. def OAI.ExactDerandomization.Sub.helmet line 879
151. lemma OAI.ExactDerandomization.Sub.helmetK line 880
152. def OAI.ExactDerandomization.Sub.snag line 881
153. abbrev OAI.ExactDerandomization.Sub.gem0 line 883
154. lemma OAI.ExactDerandomization.Sub.priority line 884
155. abbrev OAI.ExactDerandomization.Sub.Quill.forge line 890
156. def OAI.ExactDerandomization.Sub.Quill.hall line 891
157. lemma OAI.ExactDerandomization.Sub.Quill.marked line 892
158. lemma OAI.ExactDerandomization.Sub.Quill.capped line 900
159. lemma OAI.ExactDerandomization.Sub.Quill.casing line 906
160. abbrev OAI.ExactDerandomization.Sub.Quill.upG line 921
161. lemma OAI.ExactDerandomization.Sub.Quill.up_act line 922
162. lemma OAI.ExactDerandomization.Sub.Quill.blocked line 924
163. lemma OAI.ExactDerandomization.Sub.Quill.domain_ok line 929
164. lemma OAI.ExactDerandomization.Sub.Quill.root_ok line 931
165. def OAI.ExactDerandomization.Sub.Quill.Budded line 936
166. lemma OAI.ExactDerandomization.Sub.Quill.together line 937
167. lemma OAI.ExactDerandomization.Sub.Quill.unite line 951
168. lemma OAI.ExactDerandomization.Sub.Quill.to_entry line 955
169. def OAI.ExactDerandomization.Sub.Quill.ent line 984
170. structure OAI.ExactDerandomization.Sub.Quill.Suite line 987
171. lemma OAI.ExactDerandomization.Sub.Quill.arrival line 991
172. structure OAI.ExactDerandomization.Sub.Quill.Wheel line 1008
173. lemma OAI.ExactDerandomization.Sub.Quill.beat line 1016
174. lemma OAI.ExactDerandomization.Sub.Quill.drum line 1028
175. def OAI.ExactDerandomization.Sub.Quill.gloved line 1038

     Source documentation

     The contour order is an invariant of the effective graph.

     def gloved (w:ℕ→ℕ) : Quill:={u with s:={u.s with hand:=w}}

     Mentions: OAI.ExactDerandomization.Sub.Quill

176. lemma OAI.ExactDerandomization.Sub.Quill.past line 1040