OAI/Combinatorics/MatroidCounting/CommonBases.lean

GitHub source file

3078 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CommonBasesFPRAS.IndependenceOracle line 9

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:7 (same declaration text).

2. def OAI.CommonBasesFPRAS.ExactOracles line 11

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:9 (same declaration text).

3. def OAI.CommonBasesFPRAS.commonBaseCount line 16

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:14 (same declaration text).

4. inductive OAI.CommonBasesFPRAS.Instruction line 20

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:18 (same declaration text).

5. def OAI.CommonBasesFPRAS.Program line 27

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:25 (same declaration text).

6. def OAI.CommonBasesFPRAS.binaryValue line 29

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:27 (same declaration text).

7. structure OAI.CommonBasesFPRAS.MachineConfig line 33

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:31 (same declaration text).

8. def OAI.CommonBasesFPRAS.inputLength line 40

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:38 (same declaration text).

9. def OAI.CommonBasesFPRAS.initialConfig line 44

   Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:42 (same declaration text).

10. def OAI.CommonBasesFPRAS.machineStep line 55

    Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:53 (same declaration text).

11. def OAI.CommonBasesFPRAS.execution line 96

    Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:94 (same declaration text).

12. def OAI.CommonBasesFPRAS.finiteBits line 101

    Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:99 (same declaration text).

13. def OAI.CommonBasesFPRAS.relativeAccuracy line 104

    Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:102 (same declaration text).

14. def OAI.CommonBasesFPRAS.resourceBound line 107

    Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:105 (same declaration text).

15. def OAI.CommonBasesFPRAS.MainTheorem line 110

    Also declared: ComparatorChallenges/CommonBasesFPRAS.lean:108 (same declaration text).

16. def OAI.CommonBasesFPRAS.OnePositive line 133
17. theorem OAI.CommonBasesFPRAS.onePositive_of_nonpositive_kernel line 136
18. theorem OAI.CommonBasesFPRAS.spectral_kernel_nonpositive line 161
19. theorem OAI.CommonBasesFPRAS.matrix_bilin_symm line 200
20. def OAI.CommonBasesFPRAS.weightedSumLinear line 213
21. lemma OAI.CommonBasesFPRAS.dirichlet_identity line 219
22. lemma OAI.CommonBasesFPRAS.eigen_dirichlet line 241
23. lemma OAI.CommonBasesFPRAS.positive_eigen_contraction line 269
24. lemma OAI.CommonBasesFPRAS.positive_eigen_equality line 279
25. lemma OAI.CommonBasesFPRAS.euclidean_inner_matrix line 308
26. lemma OAI.CommonBasesFPRAS.euclidean_normsq line 320
27. theorem OAI.CommonBasesFPRAS.matrix_signature_of_squared line 324
28. def OAI.CommonBasesFPRAS.diagonalScale line 351
29. lemma OAI.CommonBasesFPRAS.diagonalScale_bilin line 354
30. lemma OAI.CommonBasesFPRAS.diagonalScale_mulVec line 365
31. lemma OAI.CommonBasesFPRAS.onePositive_unscale line 372
32. theorem OAI.CommonBasesFPRAS.signature_of_local_bound line 383
33. lemma OAI.CommonBasesFPRAS.onePositive_quadratic_bound line 417
34. def OAI.CommonBasesFPRAS.cubicContraction line 433
35. lemma OAI.CommonBasesFPRAS.cubicContraction_symm line 437
36. lemma OAI.CommonBasesFPRAS.cubicContraction_bilin line 443
37. lemma OAI.CommonBasesFPRAS.cubicContraction_row line 468
38. theorem OAI.CommonBasesFPRAS.cubic_local_estimate line 480
39. theorem OAI.CommonBasesFPRAS.cubic_signature line 498
40. def OAI.CommonBasesFPRAS.rankWeight line 534
41. def OAI.CommonBasesFPRAS.rawHessian line 537
42. lemma OAI.CommonBasesFPRAS.eRk_insert_of_mem_closure' line 541
43. lemma OAI.CommonBasesFPRAS.pair_rank_of_loop line 545
44. lemma OAI.CommonBasesFPRAS.pair_rank_parallel line 549
45. lemma OAI.CommonBasesFPRAS.pair_rank_nonparallel line 556
46. def OAI.CommonBasesFPRAS.rawPositive line 563
47. def OAI.CommonBasesFPRAS.parallelIndicator line 566
48. lemma OAI.CommonBasesFPRAS.parallel_gram line 570
49. lemma OAI.CommonBasesFPRAS.rawHessian_decomposition line 581
50. lemma OAI.CommonBasesFPRAS.sum_rankone line 614
51. lemma OAI.CommonBasesFPRAS.sum_diagonal line 623
52. lemma OAI.CommonBasesFPRAS.sum_gram line 631
53. lemma OAI.CommonBasesFPRAS.rawHessian_eval line 642
54. theorem OAI.CommonBasesFPRAS.raw_matroid_signature line 663
55. lemma OAI.CommonBasesFPRAS.contract_eRk_add line 692
56. def OAI.CommonBasesFPRAS.faceHessian line 709
57. def OAI.CommonBasesFPRAS.faceMatroid line 713
58. lemma OAI.CommonBasesFPRAS.faceMatroid_ground line 717
59. lemma OAI.CommonBasesFPRAS.faceMatroid_rank line 722
60. lemma OAI.CommonBasesFPRAS.faceHessian_rankWeight line 735
61. lemma OAI.CommonBasesFPRAS.onePositive_pos_smul line 746
62. theorem OAI.CommonBasesFPRAS.rankWeight_face_signature line 755
63. def OAI.CommonBasesFPRAS.coeffDeriv line 768
64. def OAI.CommonBasesFPRAS.coeffDerivs line 771
65. lemma OAI.CommonBasesFPRAS.card_outside line 776
66. lemma OAI.CommonBasesFPRAS.ncard_insert_eq line 782
67. lemma OAI.CommonBasesFPRAS.exists_outside_of_ncard_lt line 786
68. def OAI.CommonBasesFPRAS.FullPositive line 792
69. lemma OAI.CommonBasesFPRAS.FullPositive.nonneg line 797
70. lemma OAI.CommonBasesFPRAS.FullPositive.deriv line 803
71. lemma OAI.CommonBasesFPRAS.onePositive_comap line 826
72. def OAI.CommonBasesFPRAS.padMatrix line 832
73. lemma OAI.CommonBasesFPRAS.padMatrix_bilin line 836
74. lemma OAI.CommonBasesFPRAS.onePositive_padMatrix line 862
75. lemma OAI.CommonBasesFPRAS.matrix_reindex_bilin line 869
76. lemma OAI.CommonBasesFPRAS.onePositive_reindex line 880
77. def OAI.CommonBasesFPRAS.faceEraseEquiv line 887
78. def OAI.CommonBasesFPRAS.faceCubic line 897
79. lemma OAI.CommonBasesFPRAS.faceCubic_symm line 902
80. lemma OAI.CommonBasesFPRAS.faceCubic_transpose line 911
81. lemma OAI.CommonBasesFPRAS.faceCubic_pad line 921
82. lemma OAI.CommonBasesFPRAS.faceCubic_onePositive line 945
83. lemma OAI.CommonBasesFPRAS.ncard_union_pair line 956
84. lemma OAI.CommonBasesFPRAS.ncard_insert_union_pair line 963
85. lemma OAI.CommonBasesFPRAS.faceCubic_contraction line 971
86. lemma OAI.CommonBasesFPRAS.faceCubic_nonneg line 1004
87. lemma OAI.CommonBasesFPRAS.FullPositive.faceCubic_pos line 1011
88. lemma OAI.CommonBasesFPRAS.FullPositive.faceCubic_zero line 1020
89. theorem OAI.CommonBasesFPRAS.derivative_face_signature line 1031
90. lemma OAI.CommonBasesFPRAS.rankWeight_fullPositive line 1083
91. theorem OAI.CommonBasesFPRAS.rankWeight_positive_directions line 1091
92. lemma OAI.CommonBasesFPRAS.matrix_bilin_tendsto line 1104
93. lemma OAI.CommonBasesFPRAS.onePositive_of_tendsto line 1116
94. lemma OAI.CommonBasesFPRAS.faceHessian_symm line 1135
95. lemma OAI.CommonBasesFPRAS.continuous_coeffDerivs_perturb line 1144
96. theorem OAI.CommonBasesFPRAS.rankWeight_nonnegative_directions line 1157
97. lemma OAI.CommonBasesFPRAS.onePositive_matrix_substitution line 1186
98. def OAI.CommonBasesFPRAS.slotDirection line 1193
99. lemma OAI.CommonBasesFPRAS.slotDirection_nonneg line 1196
100. lemma OAI.CommonBasesFPRAS.coeffDeriv_slot line 1200
101. lemma OAI.CommonBasesFPRAS.coeffDeriv_pair line 1212
102. theorem OAI.CommonBasesFPRAS.matroid_slot_signature line 1218
103. lemma OAI.CommonBasesFPRAS.onePositive_smul line 1231
104. lemma OAI.CommonBasesFPRAS.onePositive_submatrix line 1241
105. theorem OAI.CommonBasesFPRAS.quadratic_split_bound line 1256
106. def OAI.CommonBasesFPRAS.splitMatrix line 1277
107. def OAI.CommonBasesFPRAS.oldVector line 1286
108. def OAI.CommonBasesFPRAS.splitPositive line 1290
109. def OAI.CommonBasesFPRAS.splitDifference line 1294
110. theorem OAI.CommonBasesFPRAS.splitMatrix_symm line 1299
111. theorem OAI.CommonBasesFPRAS.split_bound line 1311
112. def OAI.CommonBasesFPRAS.futureChild line 1347
113. def OAI.CommonBasesFPRAS.extendVector line 1353
114. theorem OAI.CommonBasesFPRAS.future_conservation line 1357
115. theorem OAI.CommonBasesFPRAS.child_balance line 1367
116. theorem OAI.CommonBasesFPRAS.demand_conservation line 1380
117. theorem OAI.CommonBasesFPRAS.potential_increment line 1388
118. theorem OAI.CommonBasesFPRAS.leaf_clique_bound line 1400
119. def OAI.CommonBasesFPRAS.pairDirection line 1429
120. def OAI.CommonBasesFPRAS.slotTotal line 1431
121. lemma OAI.CommonBasesFPRAS.slotTotal_nil line 1434
122. lemma OAI.CommonBasesFPRAS.slotTotal_cons line 1436
123. def OAI.CommonBasesFPRAS.SlotsFresh line 1442
124. lemma OAI.CommonBasesFPRAS.SlotsFresh.mono line 1448
125. lemma OAI.CommonBasesFPRAS.slotTotal_pos line 1457
126. def OAI.CommonBasesFPRAS.appendPoint line 1475
127. lemma OAI.CommonBasesFPRAS.range_appendPoint line 1480
128. lemma OAI.CommonBasesFPRAS.appendPoint_injective line 1493
129. lemma OAI.CommonBasesFPRAS.slotsFresh_child line 1503
130. lemma OAI.CommonBasesFPRAS.appendPoint_fresh line 1514
131. def OAI.CommonBasesFPRAS.pairMatrix line 1526
132. lemma OAI.CommonBasesFPRAS.pairMatrix_symm line 1531
133. def OAI.CommonBasesFPRAS.HasSlotSignature line 1539
134. lemma OAI.CommonBasesFPRAS.rankWeight_hasSlotSignature line 1543
135. lemma OAI.CommonBasesFPRAS.pairMatrix_signature line 1551
136. lemma OAI.CommonBasesFPRAS.star_le_half_clique line 1573
137. def OAI.CommonBasesFPRAS.cliqueEnergy line 1589
138. lemma OAI.CommonBasesFPRAS.cliqueEnergy_nonneg line 1593
139. lemma OAI.CommonBasesFPRAS.clique_linear_bound line 1604
140. def OAI.CommonBasesFPRAS.splitEmbedding line 1623
141. lemma OAI.CommonBasesFPRAS.splitEmbedding_injective line 1629
142. lemma OAI.CommonBasesFPRAS.pairMatrix_split line 1656
143. lemma OAI.CommonBasesFPRAS.slot_split_signature line 1674
144. lemma OAI.CommonBasesFPRAS.pairMatrix_append line 1694
145. lemma OAI.CommonBasesFPRAS.slotTotal_parent line 1702
146. lemma OAI.CommonBasesFPRAS.pairMatrix_parent line 1717
147. lemma OAI.CommonBasesFPRAS.slot_future_conservation line 1741
148. def OAI.CommonBasesFPRAS.transportDemand line 1756
149. def OAI.CommonBasesFPRAS.transportPotential line 1760
150. def OAI.CommonBasesFPRAS.slotPunctures line 1764
151. def OAI.CommonBasesFPRAS.transportCorrection line 1768
152. def OAI.CommonBasesFPRAS.transportEnergy line 1773
153. lemma OAI.CommonBasesFPRAS.transportEnergy_nil line 1783
154. lemma OAI.CommonBasesFPRAS.transportEnergy_cons line 1790
155. lemma OAI.CommonBasesFPRAS.transportDemand_split line 1797
156. lemma OAI.CommonBasesFPRAS.transportCorrection_split line 1810
157. lemma OAI.CommonBasesFPRAS.transportPotential_split line 1826
158. theorem OAI.CommonBasesFPRAS.transport_linear_bound line 1842
159. lemma OAI.CommonBasesFPRAS.transportDemand_smul line 1926
160. lemma OAI.CommonBasesFPRAS.transportPotential_smul line 1932
161. lemma OAI.CommonBasesFPRAS.transportCorrection_smul line 1942
162. lemma OAI.CommonBasesFPRAS.squared_le_of_linear_scalings line 1953
163. theorem OAI.CommonBasesFPRAS.transport_squared_bound line 1960
164. lemma OAI.CommonBasesFPRAS.slotTotal_nonneg line 1979
165. def OAI.CommonBasesFPRAS.rootEmbedding line 1991
166. lemma OAI.CommonBasesFPRAS.rootEmbedding_injective line 1994
167. def OAI.CommonBasesFPRAS.rootDemand line 1999
168. def OAI.CommonBasesFPRAS.rootCoefficient line 2002
169. lemma OAI.CommonBasesFPRAS.rootPotential line 2009
170. lemma OAI.CommonBasesFPRAS.rootCorrection line 2020
171. lemma OAI.CommonBasesFPRAS.rootCoefficient_pos line 2035
172. theorem OAI.CommonBasesFPRAS.transport_root_bound line 2061
173. def OAI.CommonBasesFPRAS.ExchangeAdjacent line 2104
174. def OAI.CommonBasesFPRAS.slotVertices line 2108
175. def OAI.CommonBasesFPRAS.transportEdges line 2116
176. def OAI.CommonBasesFPRAS.missingMultiplier line 2125
177. lemma OAI.CommonBasesFPRAS.transportEdges_fixed line 2131
178. lemma OAI.CommonBasesFPRAS.transportEdges_not_holes line 2148
179. lemma OAI.CommonBasesFPRAS.transportEdges_disjoint line 2178
180. lemma OAI.CommonBasesFPRAS.missingMultiplier_child_left line 2196
181. lemma OAI.CommonBasesFPRAS.missingMultiplier_child_right line 2205
182. lemma OAI.CommonBasesFPRAS.missingMultiplier_leaf line 2214
183. lemma OAI.CommonBasesFPRAS.insert_embedding_injective line 2221
184. def OAI.CommonBasesFPRAS.slotEdgeEnergy line 2229
185. lemma OAI.CommonBasesFPRAS.offdiag_sum line 2235
186. lemma OAI.CommonBasesFPRAS.transportEnergy_leaf_eq_sum line 2248
187. lemma OAI.CommonBasesFPRAS.transportEnergy_eq_sum line 2264
188. lemma OAI.CommonBasesFPRAS.transportEdges_states line 2308
189. lemma OAI.CommonBasesFPRAS.transportEdges_adjacent line 2330
190. def OAI.CommonBasesFPRAS.slotGraphEdges line 2357
191. def OAI.CommonBasesFPRAS.slotGraphEnergy line 2362
192. lemma OAI.CommonBasesFPRAS.missingMultiplier_nonneg line 2367
193. lemma OAI.CommonBasesFPRAS.transportEnergy_le_graphEnergy line 2377
194. theorem OAI.CommonBasesFPRAS.transport_graph_bound line 2395
195. lemma OAI.CommonBasesFPRAS.coeffDeriv_eq_sum_outside line 2418
196. lemma OAI.CommonBasesFPRAS.faceHessian_bilin_derivatives line 2434
197. lemma OAI.CommonBasesFPRAS.onePositive_pair_bound line 2469
198. lemma OAI.CommonBasesFPRAS.onePositive_triple_bound line 2476
199. lemma OAI.CommonBasesFPRAS.coeffDeriv_comm line 2492
200. lemma OAI.CommonBasesFPRAS.coeffDeriv_pair_twice line 2497
201. lemma OAI.CommonBasesFPRAS.faceHessian_nonnegative_vectors line 2506
202. theorem OAI.CommonBasesFPRAS.coefficient_pair line 2521
203. lemma OAI.CommonBasesFPRAS.SlotsFresh.tail line 2554
204. lemma OAI.CommonBasesFPRAS.SlotsFresh.swap line 2559
205. lemma OAI.CommonBasesFPRAS.coeffDeriv_pair_repeated line 2571
206. theorem OAI.CommonBasesFPRAS.coefficient_triple line 2583
207. theorem OAI.CommonBasesFPRAS.scores_have_sink line 2631
208. lemma OAI.CommonBasesFPRAS.coeffDeriv_scale line 2673
209. lemma OAI.CommonBasesFPRAS.coeffDerivs_scale line 2680
210. lemma OAI.CommonBasesFPRAS.HasSlotSignature.scale line 2691
211. def OAI.CommonBasesFPRAS.matroidWeight line 2704
212. lemma OAI.CommonBasesFPRAS.matroidWeight_eq_scaled line 2708
213. lemma OAI.CommonBasesFPRAS.matroidWeight_pos line 2721
214. lemma OAI.CommonBasesFPRAS.matroidWeight_signature line 2724
215. lemma OAI.CommonBasesFPRAS.dual_rank_equal_complement line 2733
216. lemma OAI.CommonBasesFPRAS.dual_eRank_half line 2743
217. lemma OAI.CommonBasesFPRAS.matroidWeight_dual_complement line 2752
218. theorem OAI.CommonBasesFPRAS.paired_matroid_weight_signatures line 2758
219. lemma OAI.CommonBasesFPRAS.SlotsFresh.perm line 2771
220. lemma OAI.CommonBasesFPRAS.slotTotal_perm line 2781
221. def OAI.CommonBasesFPRAS.slotDefect line 2793
222. lemma OAI.CommonBasesFPRAS.slots_perm_two line 2798
223. lemma OAI.CommonBasesFPRAS.slotDefect_perm line 2804
224. lemma OAI.CommonBasesFPRAS.slotDefect_pos line 2810
225. lemma OAI.CommonBasesFPRAS.slotDefect_pair_bound line 2820
226. lemma OAI.CommonBasesFPRAS.slots_perm_three line 2833
227. lemma OAI.CommonBasesFPRAS.slotDefect_triple_bound line 2841
228. lemma OAI.CommonBasesFPRAS.coefficient_scores_sink line 2855
229. theorem OAI.CommonBasesFPRAS.slot_scores_have_sink_forward line 2891
230. theorem OAI.CommonBasesFPRAS.slot_scores_have_sink line 2924
231. def OAI.CommonBasesFPRAS.slotVariance line 2965
232. lemma OAI.CommonBasesFPRAS.slotVariance_nil line 2969
233. lemma OAI.CommonBasesFPRAS.slotVariance_perm line 2976
234. lemma OAI.CommonBasesFPRAS.variance_split_algebra line 2982
235. lemma OAI.CommonBasesFPRAS.slotVariance_split line 2989
236. lemma OAI.CommonBasesFPRAS.slotVariance_nonneg line 3002
237. lemma OAI.CommonBasesFPRAS.slotPunctures_length line 3017
238. lemma OAI.CommonBasesFPRAS.list_sum_map_le_const line 3022
239. theorem OAI.CommonBasesFPRAS.transport_node_variance line 3032
240. def OAI.CommonBasesFPRAS.PairSingle line 3097
241. def OAI.CommonBasesFPRAS.PairFull line 3099
242. def OAI.CommonBasesFPRAS.PairEmpty line 3100
243. lemma OAI.CommonBasesFPRAS.PairSingle.not_full line 3103
244. lemma OAI.CommonBasesFPRAS.PairSingle.not_empty line 3107
245. lemma OAI.CommonBasesFPRAS.PairFull.not_empty line 3111
246. def OAI.CommonBasesFPRAS.PlainState line 3115
247. def OAI.CommonBasesFPRAS.DefectState line 3116
248. lemma OAI.CommonBasesFPRAS.DefectState.not_plain line 3120
249. lemma OAI.CommonBasesFPRAS.DefectState.unique line 3125
250. lemma OAI.CommonBasesFPRAS.SlotsFresh.elements_fresh line 3140
251. lemma OAI.CommonBasesFPRAS.SlotsFresh.pair_ne_of_mem line 3150
252. lemma OAI.CommonBasesFPRAS.SlotsFresh.nodup line 3156
253. lemma OAI.CommonBasesFPRAS.slotVertices_fixed line 3163
254. lemma OAI.CommonBasesFPRAS.slotVertices_classify line 3179
255. def OAI.CommonBasesFPRAS.Respects line 3267
256. def OAI.CommonBasesFPRAS.EdgeRespects line 3269
257. def OAI.CommonBasesFPRAS.restrictedEnergy line 3272
258. lemma OAI.CommonBasesFPRAS.Respects.parent line 3277
259. lemma OAI.CommonBasesFPRAS.Respects.child_disjoint line 3282
260. lemma OAI.CommonBasesFPRAS.restrictedEnergy_nonneg line 3289
261. lemma OAI.CommonBasesFPRAS.restrictedEnergy_children line 3299
262. theorem OAI.CommonBasesFPRAS.adaptive_variance_bound line 3320
263. lemma OAI.CommonBasesFPRAS.slotVertices_excluded line 3357
264. def OAI.CommonBasesFPRAS.FixedOutside line 3380
265. lemma OAI.CommonBasesFPRAS.FixedOutside.single line 3384
266. def OAI.CommonBasesFPRAS.chainMultiplier line 3391
267. lemma OAI.CommonBasesFPRAS.chainMultiplier_plain line 3395
268. lemma OAI.CommonBasesFPRAS.chainMultiplier_defect line 3402
269. lemma OAI.CommonBasesFPRAS.chainMultiplier_pos line 3412
270. def OAI.CommonBasesFPRAS.ChainState line 3417
271. def OAI.CommonBasesFPRAS.chainEdges line 3420
272. def OAI.CommonBasesFPRAS.chainConductance line 3424
273. lemma OAI.CommonBasesFPRAS.list_sum_single line 3428
274. lemma OAI.CommonBasesFPRAS.missingMultiplier_old line 3435
275. lemma OAI.CommonBasesFPRAS.missingMultiplier_new line 3449
276. lemma OAI.CommonBasesFPRAS.SlotsFresh.pair_contains_unique line 3461
277. def OAI.CommonBasesFPRAS.pairMultiplier line 3474
278. lemma OAI.CommonBasesFPRAS.pairMultiplier_pos line 3478
279. lemma OAI.CommonBasesFPRAS.pairMultiplier_on line 3483
280. lemma OAI.CommonBasesFPRAS.pairMultiplier_fresh line 3491
281. lemma OAI.CommonBasesFPRAS.variance_vertex_identification line 3500
282. lemma OAI.CommonBasesFPRAS.variance_energy_identification line 3550
283. lemma OAI.CommonBasesFPRAS.slotPunctures_perm line 3592
284. lemma OAI.CommonBasesFPRAS.slotDefect_puncture line 3603
285. def OAI.CommonBasesFPRAS.VarianceNode line 3612
286. lemma OAI.CommonBasesFPRAS.VarianceNode.perm line 3615
287. lemma OAI.CommonBasesFPRAS.VarianceNode.children line 3621
288. lemma OAI.CommonBasesFPRAS.variance_node_bound line 3660
289. theorem OAI.CommonBasesFPRAS.transversal_variance_bound line 3738
290. def OAI.CommonBasesFPRAS.pairSupport line 3759
291. lemma OAI.CommonBasesFPRAS.pairSupport_nil line 3763
292. lemma OAI.CommonBasesFPRAS.pairSupport_cons line 3765
293. def OAI.CommonBasesFPRAS.choiceVertices line 3771
294. lemma OAI.CommonBasesFPRAS.choiceVertices_fixed line 3777
295. lemma OAI.CommonBasesFPRAS.choiceVertices_excluded line 3790
296. lemma OAI.CommonBasesFPRAS.choiceVertices_disjoint line 3805
297. lemma OAI.CommonBasesFPRAS.slotTotal_eq_choice_sum line 3819
298. lemma OAI.CommonBasesFPRAS.choiceVertices_card line 3830
299. lemma OAI.CommonBasesFPRAS.mem_choiceVertices_iff line 3840
300. lemma OAI.CommonBasesFPRAS.choiceVertices_plain line 3927
301. lemma OAI.CommonBasesFPRAS.slotTotal_eq_plain_sum line 3934
302. lemma OAI.CommonBasesFPRAS.slotVariance_eq_plain_variance line 3939
303. lemma OAI.CommonBasesFPRAS.pairSupport_perm line 3956
304. lemma OAI.CommonBasesFPRAS.SlotsFresh.support_disjoint line 3960
305. lemma OAI.CommonBasesFPRAS.PlainState.perm line 3969
306. lemma OAI.CommonBasesFPRAS.DefectState.perm line 3973
307. lemma OAI.CommonBasesFPRAS.choiceVertices_defect line 3978
308. lemma OAI.CommonBasesFPRAS.slotDefect_eq_defect_sum line 4029
309. lemma OAI.CommonBasesFPRAS.choiceVertices_alternatives line 4042
310. def OAI.CommonBasesFPRAS.SamePair line 4054
311. lemma OAI.CommonBasesFPRAS.SamePair.full line 4057
312. lemma OAI.CommonBasesFPRAS.SamePair.empty line 4061
313. lemma OAI.CommonBasesFPRAS.SamePair.single line 4065
314. lemma OAI.CommonBasesFPRAS.SamePair.set line 4069
315. lemma OAI.CommonBasesFPRAS.SamePair.insert line 4073
316. lemma OAI.CommonBasesFPRAS.SamePair.fresh line 4077
317. lemma OAI.CommonBasesFPRAS.slot_energy_le_chain line 4085
318. lemma OAI.CommonBasesFPRAS.defect_vertex_identification line 4114
319. lemma OAI.CommonBasesFPRAS.SamePair.fresh_two line 4198
320. lemma OAI.CommonBasesFPRAS.slotDefect_rest line 4204
321. lemma OAI.CommonBasesFPRAS.defect_puncture_le line 4210
322. theorem OAI.CommonBasesFPRAS.defect_conditional_transport line 4239
323. def OAI.CommonBasesFPRAS.orientPair line 4361
324. lemma OAI.CommonBasesFPRAS.orientPair_same line 4363
325. lemma OAI.CommonBasesFPRAS.slotTotal_four line 4366
326. lemma OAI.CommonBasesFPRAS.weighted_square_mean line 4385
327. theorem OAI.CommonBasesFPRAS.defect_mean_bound line 4396
328. def OAI.CommonBasesFPRAS.chainStates line 4465
329. def OAI.CommonBasesFPRAS.defectTypes line 4467
330. def OAI.CommonBasesFPRAS.chainWeight line 4469
331. def OAI.CommonBasesFPRAS.chainTotal line 4472
332. def OAI.CommonBasesFPRAS.plainMean line 4475
333. def OAI.CommonBasesFPRAS.defectMean line 4477
334. def OAI.CommonBasesFPRAS.observableProjection line 4479
335. lemma OAI.CommonBasesFPRAS.observableProjection_plain line 4482
336. lemma OAI.CommonBasesFPRAS.observableProjection_defect line 4488
337. lemma OAI.CommonBasesFPRAS.mem_defectTypes line 4497
338. lemma OAI.CommonBasesFPRAS.chain_sum_decomposition line 4501
339. lemma OAI.CommonBasesFPRAS.chainTotal_eq line 4530
340. lemma OAI.CommonBasesFPRAS.chainTotal_ge_plain line 4542
341. lemma OAI.CommonBasesFPRAS.chainTotal_pos line 4553
342. lemma OAI.CommonBasesFPRAS.defectTypes_card_le line 4560
343. lemma OAI.CommonBasesFPRAS.chainTotal_le line 4566
344. lemma OAI.CommonBasesFPRAS.finite_center_sum line 4589
345. lemma OAI.CommonBasesFPRAS.finite_center_at_mean line 4596
346. lemma OAI.CommonBasesFPRAS.finite_center_min line 4604
347. lemma OAI.CommonBasesFPRAS.plain_center_eq_variance line 4614
348. lemma OAI.CommonBasesFPRAS.projection_center_decomposition line 4624
349. def OAI.CommonBasesFPRAS.chainMean line 4647
350. def OAI.CommonBasesFPRAS.chainVariance line 4650
351. def OAI.CommonBasesFPRAS.chainDirichlet line 4653
352. lemma OAI.CommonBasesFPRAS.projection_center_bound line 4658
353. theorem OAI.CommonBasesFPRAS.observable_poincare line 4689
354. lemma OAI.CommonBasesFPRAS.pairSupport_ncard line 4736
355. lemma OAI.CommonBasesFPRAS.slots_ground_card line 4751
356. lemma OAI.CommonBasesFPRAS.choiceVertices_ncard line 4756
357. lemma OAI.CommonBasesFPRAS.PlainState.ncard line 4776
358. lemma OAI.CommonBasesFPRAS.DefectState.ncard line 4781
359. lemma OAI.CommonBasesFPRAS.ChainState.ncard line 4801
360. lemma OAI.CommonBasesFPRAS.ExchangeAdjacent.symm line 4808
361. lemma OAI.CommonBasesFPRAS.ExchangeAdjacent.ne line 4812
362. lemma OAI.CommonBasesFPRAS.ExchangeAdjacent.move line 4819
363. lemma OAI.CommonBasesFPRAS.exchange_neighbors_card line 4833
364. abbrev OAI.CommonBasesFPRAS.ChainIndex line 4845
365. lemma OAI.CommonBasesFPRAS.chain_neighbors_card line 4847
366. structure OAI.CommonBasesFPRAS.FiniteChain line 4873
367. def OAI.CommonBasesFPRAS.FiniteChain.inner line 4886
368. def OAI.CommonBasesFPRAS.FiniteChain.apply line 4887
369. def OAI.CommonBasesFPRAS.FiniteChain.energy line 4888
370. def OAI.CommonBasesFPRAS.FiniteChain.iterate line 4889
371. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_symm line 4891
372. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_add_right line 4896
373. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_sub_right line 4898
374. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_add_left line 4900
375. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_sum_right line 4902
376. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_sum_left line 4906
377. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_nonneg line 4912
378. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_add line 4916
379. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_sum line 4919
380. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_const line 4924
381. lemma OAI.CommonBasesFPRAS.FiniteChain.stationary line 4928
382. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_selfAdjoint line 4931
383. lemma OAI.CommonBasesFPRAS.FiniteChain.energy_eq line 4945
384. lemma OAI.CommonBasesFPRAS.FiniteChain.energy_nonneg line 4974
385. lemma OAI.CommonBasesFPRAS.FiniteChain.energy_le_inner line 4983
386. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_positive line 5033
387. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_zero line 5038
388. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_succ line 5039
389. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_add line 5041
390. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_selfAdjoint line 5043
391. lemma OAI.CommonBasesFPRAS.FiniteChain.covariance_nonneg line 5051
392. def OAI.CommonBasesFPRAS.FiniteChain.partialResolvent line 5064
393. lemma OAI.CommonBasesFPRAS.FiniteChain.partialResolvent_zero line 5066
394. lemma OAI.CommonBasesFPRAS.FiniteChain.partialResolvent_succ line 5069
395. lemma OAI.CommonBasesFPRAS.FiniteChain.partialResolvent_residual line 5074
396. lemma OAI.CommonBasesFPRAS.FiniteChain.partialResolvent_inner line 5086
397. lemma OAI.CommonBasesFPRAS.FiniteChain.partialResolvent_energy_le line 5090
398. theorem OAI.CommonBasesFPRAS.FiniteChain.covariance_sum_bound line 5102
399. def OAI.CommonBasesFPRAS.FiniteChain.pathExpectation line 5112
400. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_nonneg line 5116
401. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_add line 5124
402. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_mul line 5129
403. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_const line 5134
404. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_congr line 5138
405. def OAI.CommonBasesFPRAS.FiniteChain.pathSum line 5144
406. def OAI.CommonBasesFPRAS.FiniteChain.squareMoment line 5145
407. lemma OAI.CommonBasesFPRAS.FiniteChain.pathSum_cons line 5149
408. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_sum line 5150
409. lemma OAI.CommonBasesFPRAS.FiniteChain.squareMoment_zero line 5166
410. lemma OAI.CommonBasesFPRAS.FiniteChain.squareMoment_succ line 5167
411. lemma OAI.CommonBasesFPRAS.FiniteChain.squareMoment_nonneg line 5195
412. lemma OAI.CommonBasesFPRAS.FiniteChain.stationary_apply line 5201
413. lemma OAI.CommonBasesFPRAS.FiniteChain.stationary_squareMoment_succ line 5209
414. theorem OAI.CommonBasesFPRAS.FiniteChain.stationary_squareMoment_bound line 5234
415. theorem OAI.CommonBasesFPRAS.FiniteChain.warm_squareMoment_bound line 5251
416. def OAI.CommonBasesFPRAS.FiniteChain.ofMoves line 5271
417. lemma OAI.CommonBasesFPRAS.FiniteChain.ofMoves_energy line 5290
418. lemma OAI.CommonBasesFPRAS.chainWeight_pos line 5312
419. lemma OAI.CommonBasesFPRAS.chain_sum_subtype line 5317
420. def OAI.CommonBasesFPRAS.metropolisMove line 5321
421. lemma OAI.CommonBasesFPRAS.metropolisMove_nonneg line 5327
422. lemma OAI.CommonBasesFPRAS.metropolisMove_row line 5338
423. lemma OAI.CommonBasesFPRAS.metropolisMove_balanced line 5365
424. def OAI.CommonBasesFPRAS.metropolisChain line 5378
425. lemma OAI.CommonBasesFPRAS.chainEdges_sum line 5388
426. lemma OAI.CommonBasesFPRAS.restrictedEnergy_chain_eq line 5410
427. theorem OAI.CommonBasesFPRAS.metropolisChain_energy line 5421
428. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_cauchy line 5446
429. def OAI.CommonBasesFPRAS.FiniteChain.mean line 5461
430. def OAI.CommonBasesFPRAS.FiniteChain.variance line 5462
431. lemma OAI.CommonBasesFPRAS.FiniteChain.centered_mean line 5464
432. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_center_right line 5468
433. def OAI.CommonBasesFPRAS.ClassObservable line 5483
434. lemma OAI.CommonBasesFPRAS.projection_classObservable line 5486
435. lemma OAI.CommonBasesFPRAS.ClassObservable.sub_const line 5492
436. lemma OAI.CommonBasesFPRAS.defect_pairing_projection line 5498
437. lemma OAI.CommonBasesFPRAS.chain_pairing_projection line 5539
438. def OAI.CommonBasesFPRAS.extendChainFun line 5556
439. lemma OAI.CommonBasesFPRAS.extendChainFun_apply line 5559
440. lemma OAI.CommonBasesFPRAS.metropolisChain_inner line 5568
441. lemma OAI.CommonBasesFPRAS.metropolisChain_mean line 5577
442. lemma OAI.CommonBasesFPRAS.metropolisChain_variance line 5586
443. theorem OAI.CommonBasesFPRAS.metropolisChain_dual line 5598
444. theorem OAI.CommonBasesFPRAS.metropolisChain_timeAverage line 5646
445. structure OAI.CommonBasesFPRAS.KilledKernel line 5673
446. def OAI.CommonBasesFPRAS.KilledKernel.apply line 5685
447. def OAI.CommonBasesFPRAS.KilledKernel.iterate line 5686
448. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_zero line 5687
449. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_succ line 5688
450. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_succ' line 5690
451. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_add line 5692
452. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_sub line 5695
453. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_sum line 5698
454. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_mul line 5703
455. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_nonneg line 5709
456. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_nonneg line 5711
457. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_abs_bound line 5718
458. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_abs_bound line 5727
459. lemma OAI.CommonBasesFPRAS.KilledKernel.summable_iterate line 5736
460. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_tendsto_zero line 5743
461. def OAI.CommonBasesFPRAS.KilledKernel.green line 5752
462. lemma OAI.CommonBasesFPRAS.KilledKernel.green_nonneg line 5753
463. lemma OAI.CommonBasesFPRAS.KilledKernel.green_firstStep line 5756
464. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_sub line 5764
465. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_sum line 5769
466. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_mul line 5774
467. lemma OAI.CommonBasesFPRAS.KilledKernel.green_sum line 5780
468. lemma OAI.CommonBasesFPRAS.KilledKernel.green_mul line 5785
469. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_residual_sum line 5790
470. lemma OAI.CommonBasesFPRAS.KilledKernel.green_residual line 5799
471. abbrev OAI.CommonBasesFPRAS.FiniteChain.Inside line 5813
472. abbrev OAI.CommonBasesFPRAS.FiniteChain.Outside line 5814
473. def OAI.CommonBasesFPRAS.FiniteChain.mergeFun line 5816
474. lemma OAI.CommonBasesFPRAS.FiniteChain.mergeFun_inside line 5819
475. lemma OAI.CommonBasesFPRAS.FiniteChain.mergeFun_outside line 5822
476. def OAI.CommonBasesFPRAS.FiniteChain.hitKernel line 5827
477. lemma OAI.CommonBasesFPRAS.FiniteChain.hitKernel_nonneg line 5829
478. lemma OAI.CommonBasesFPRAS.FiniteChain.exitRow line 5833
479. lemma OAI.CommonBasesFPRAS.FiniteChain.hitKernel_row line 5842
480. lemma OAI.CommonBasesFPRAS.FiniteChain.hitKernel_firstStep line 5852
481. def OAI.CommonBasesFPRAS.FiniteChain.traceMatrix line 5858
482. def OAI.CommonBasesFPRAS.FiniteChain.traceApply line 5860
483. lemma OAI.CommonBasesFPRAS.FiniteChain.traceMatrix_nonneg line 5863
484. lemma OAI.CommonBasesFPRAS.FiniteChain.traceMatrix_lazy line 5866
485. lemma OAI.CommonBasesFPRAS.FiniteChain.traceMatrix_stochastic line 5870
486. def OAI.CommonBasesFPRAS.FiniteChain.offExtension line 5876
487. def OAI.CommonBasesFPRAS.FiniteChain.harmonicExtension line 5878
488. lemma OAI.CommonBasesFPRAS.FiniteChain.harmonicExtension_inside line 5879
489. lemma OAI.CommonBasesFPRAS.FiniteChain.harmonicExtension_outside line 5881
490. lemma OAI.CommonBasesFPRAS.FiniteChain.offExtension_firstStep line 5885
491. lemma OAI.CommonBasesFPRAS.FiniteChain.harmonicExtension_harmonic line 5903
492. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_harmonicExtension_inside line 5910
493. lemma OAI.CommonBasesFPRAS.FiniteChain.harmonic_inner_residual line 5926
494. lemma OAI.CommonBasesFPRAS.FiniteChain.residual_symmetric line 5941
495. lemma OAI.CommonBasesFPRAS.FiniteChain.traceMatrix_reversible line 5947
496. def OAI.CommonBasesFPRAS.FiniteChain.insideMass line 5957
497. lemma OAI.CommonBasesFPRAS.FiniteChain.insideMass_pos line 5958
498. def OAI.CommonBasesFPRAS.FiniteChain.traceChain line 5963
499. lemma OAI.CommonBasesFPRAS.FiniteChain.traceChain_energy line 5975
500. lemma OAI.CommonBasesFPRAS.FiniteChain.mean_apply line 5986
501. lemma OAI.CommonBasesFPRAS.FiniteChain.mean_residual line 5991
502. def OAI.CommonBasesFPRAS.FiniteChain.duration line 5997
503. def OAI.CommonBasesFPRAS.FiniteChain.returnCost line 5998
504. lemma OAI.CommonBasesFPRAS.FiniteChain.duration_nonneg line 6000
505. lemma OAI.CommonBasesFPRAS.FiniteChain.returnCost_nonneg line 6002
506. lemma OAI.CommonBasesFPRAS.FiniteChain.expected_returnCost line 6007
507. lemma OAI.CommonBasesFPRAS.FiniteChain.traceChain_returnCost line 6034
508. lemma OAI.CommonBasesFPRAS.FiniteChain.warm_returnCost line 6040
509. def OAI.CommonBasesFPRAS.FiniteChain.exitProbability line 6053
510. lemma OAI.CommonBasesFPRAS.FiniteChain.exitProbability_nonneg line 6054
511. lemma OAI.CommonBasesFPRAS.FiniteChain.exitProbability_pos line 6057
512. lemma OAI.CommonBasesFPRAS.FiniteChain.exitProbability_le_one line 6060
513. def OAI.CommonBasesFPRAS.FiniteChain.killedChain line 6066
514. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_cauchy line 6091
515. lemma OAI.CommonBasesFPRAS.FiniteChain.inner_sub_left line 6109
516. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_sub line 6112
517. lemma OAI.CommonBasesFPRAS.FiniteChain.mean_const line 6115
518. lemma OAI.CommonBasesFPRAS.FiniteChain.mean_sub line 6117
519. lemma OAI.CommonBasesFPRAS.FiniteChain.variance_eq_inner line 6119
520. lemma OAI.CommonBasesFPRAS.FiniteChain.apply_contraction line 6122
521. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_mean line 6140
522. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_contraction line 6144
523. def OAI.CommonBasesFPRAS.FiniteChain.pointDensity line 6158
524. def OAI.CommonBasesFPRAS.FiniteChain.centeredPoint line 6159
525. lemma OAI.CommonBasesFPRAS.FiniteChain.pointDensity_mean line 6160
526. lemma OAI.CommonBasesFPRAS.FiniteChain.centeredPoint_mean line 6162
527. lemma OAI.CommonBasesFPRAS.FiniteChain.pointDensity_inner line 6165
528. lemma OAI.CommonBasesFPRAS.FiniteChain.centeredPoint_norm line 6167
529. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_const line 6176
530. lemma OAI.CommonBasesFPRAS.FiniteChain.iterate_sub line 6180
531. lemma OAI.CommonBasesFPRAS.FiniteChain.point_mixing_squared line 6186
532. lemma OAI.CommonBasesFPRAS.FiniteChain.variance_formula line 6211
533. lemma OAI.CommonBasesFPRAS.FiniteChain.poincare_rayleigh line 6223
534. lemma OAI.CommonBasesFPRAS.FiniteChain.point_mixing line 6233
535. lemma OAI.CommonBasesFPRAS.FiniteChain.point_mixing_exp line 6248
536. lemma OAI.CommonBasesFPRAS.SlotsFresh.cross_ne line 6269
537. lemma OAI.CommonBasesFPRAS.DefectState.plain_neighbor line 6276
538. abbrev OAI.CommonBasesFPRAS.PlainIndex line 6313
539. lemma OAI.CommonBasesFPRAS.plainIndex_sum line 6317
540. lemma OAI.CommonBasesFPRAS.plainIndex_nonempty line 6329
541. lemma OAI.CommonBasesFPRAS.metropolis_plain_exit line 6337
542. abbrev OAI.CommonBasesFPRAS.plainPredicate line 6362
543. def OAI.CommonBasesFPRAS.metropolisKilled line 6363
544. def OAI.CommonBasesFPRAS.metropolisTrace line 6367
545. lemma OAI.CommonBasesFPRAS.metropolis_insideMass line 6372
546. lemma OAI.CommonBasesFPRAS.metropolisTrace_pi line 6381
547. lemma OAI.CommonBasesFPRAS.metropolisTrace_variance line 6389
548. theorem OAI.CommonBasesFPRAS.metropolisTrace_poincare line 6404
549. lemma OAI.CommonBasesFPRAS.KilledKernel.apply_mono line 6449
550. lemma OAI.CommonBasesFPRAS.KilledKernel.iterate_mono line 6451
551. lemma OAI.CommonBasesFPRAS.KilledKernel.survival_antitone line 6456
552. lemma OAI.CommonBasesFPRAS.KilledKernel.duration_tail line 6463
553. def OAI.CommonBasesFPRAS.KilledKernel.partialGreen line 6471
554. lemma OAI.CommonBasesFPRAS.KilledKernel.partialGreen_nonneg line 6473
555. lemma OAI.CommonBasesFPRAS.KilledKernel.partialGreen_le line 6475
556. lemma OAI.CommonBasesFPRAS.KilledKernel.partialGreen_sum line 6478
557. def OAI.CommonBasesFPRAS.FiniteChain.cappedTrace line 6490
558. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_nonneg line 6493
559. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_le line 6497
560. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_mass line 6504
561. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_loss line 6520
562. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_substochastic line 6532
563. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_warm_loss line 6537
564. structure OAI.CommonBasesFPRAS.FiniteKernel line 6548
565. def OAI.CommonBasesFPRAS.FiniteKernel.identity line 6555
566. def OAI.CommonBasesFPRAS.FiniteKernel.comp line 6559
567. def OAI.CommonBasesFPRAS.FiniteKernel.push line 6569
568. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_nonneg line 6570
569. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_mono line 6572
570. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_comp line 6574
571. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_identity line 6579
572. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_mass line 6581
573. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_mass_le line 6584
574. def OAI.CommonBasesFPRAS.FiniteKernel.power line 6588
575. lemma OAI.CommonBasesFPRAS.FiniteKernel.power_push_succ line 6591
576. lemma OAI.CommonBasesFPRAS.FiniteKernel.push_domination line 6593
577. lemma OAI.CommonBasesFPRAS.FiniteKernel.power_domination line 6596
578. lemma OAI.CommonBasesFPRAS.FiniteKernel.one_step_defect line 6606
579. def OAI.CommonBasesFPRAS.FiniteChain.kernel line 6623
580. lemma OAI.CommonBasesFPRAS.FiniteChain.kernel_stationary line 6627
581. lemma OAI.CommonBasesFPRAS.FiniteChain.push_warm line 6629
582. lemma OAI.CommonBasesFPRAS.FiniteChain.power_warm line 6634
583. lemma OAI.CommonBasesFPRAS.FiniteChain.kernel_power_stochastic line 6639
584. lemma OAI.CommonBasesFPRAS.FiniteChain.power_push_mass line 6647
585. lemma OAI.CommonBasesFPRAS.FiniteChain.capped_power_mass line 6651
586. def OAI.CommonBasesFPRAS.FiniteChain.cappedTraceKernel line 6676
587. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_power_mass line 6680
588. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_mono line 6696
589. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_finsum line 6704
590. lemma OAI.CommonBasesFPRAS.FiniteChain.pathExpectation_congr_length line 6709
591. lemma OAI.CommonBasesFPRAS.FiniteChain.pathSum_center line 6721
592. def OAI.CommonBasesFPRAS.FiniteChain.pathProbability line 6727
593. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_nonneg line 6729
594. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_mono line 6732
595. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_union line 6742
596. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_average_error line 6769
597. lemma OAI.CommonBasesFPRAS.FiniteChain.variance_le_one line 6805
598. lemma OAI.CommonBasesFPRAS.FiniteChain.relative_union_bound line 6816
599. theorem OAI.CommonBasesFPRAS.metropolisChain_bounded_MSE line 6845
600. lemma OAI.CommonBasesFPRAS.phase_error_arithmetic line 6871
601. def OAI.CommonBasesFPRAS.plainObservable line 6898
602. def OAI.CommonBasesFPRAS.defectIndicator line 6900
603. lemma OAI.CommonBasesFPRAS.plainObservable_class line 6902
604. lemma OAI.CommonBasesFPRAS.defectIndicator_class line 6906
605. lemma OAI.CommonBasesFPRAS.plainObservable_mean line 6918
606. lemma OAI.CommonBasesFPRAS.defectIndicator_mean line 6941
607. lemma OAI.CommonBasesFPRAS.plain_mass_lower line 6972
608. lemma OAI.CommonBasesFPRAS.defect_mass_lower line 6982
609. lemma OAI.CommonBasesFPRAS.chainMean_mono line 7001
610. lemma OAI.CommonBasesFPRAS.plainObservable_mass_lower line 7010
611. abbrev OAI.CommonBasesFPRAS.PhaseObservables line 7032
612. lemma OAI.CommonBasesFPRAS.phaseObservables_card line 7033
613. def OAI.CommonBasesFPRAS.phaseObservable line 7042
614. lemma OAI.CommonBasesFPRAS.phaseObservable_class line 7047
615. lemma OAI.CommonBasesFPRAS.phaseObservable_bounded line 7054
616. lemma OAI.CommonBasesFPRAS.phaseObservable_mean_lower line 7064
617. theorem OAI.CommonBasesFPRAS.metropolis_phase_failure line 7078
618. lemma OAI.CommonBasesFPRAS.sum_eRank line 7118
619. def OAI.CommonBasesFPRAS.pairedMatroid line 7133
620. def OAI.CommonBasesFPRAS.transversal line 7135
621. lemma OAI.CommonBasesFPRAS.preimage_inl_transversal line 7137
622. lemma OAI.CommonBasesFPRAS.preimage_inr_transversal line 7141
623. lemma OAI.CommonBasesFPRAS.transversal_injective line 7146
624. lemma OAI.CommonBasesFPRAS.paired_ground line 7151
625. lemma OAI.CommonBasesFPRAS.transversal_isBase_iff line 7156
626. lemma OAI.CommonBasesFPRAS.paired_eRank line 7163
627. lemma OAI.CommonBasesFPRAS.transversal_encard line 7169
628. lemma OAI.CommonBasesFPRAS.transversal_ncard line 7179
629. def OAI.CommonBasesFPRAS.annealRho line 7187
630. def OAI.CommonBasesFPRAS.annealLength line 7188
631. def OAI.CommonBasesFPRAS.annealTolerance line 7189
632. lemma OAI.CommonBasesFPRAS.annealRho_bounds line 7191
633. lemma OAI.CommonBasesFPRAS.annealRho_pow_lower line 7200
634. lemma OAI.CommonBasesFPRAS.annealStep_bounds line 7208
635. def OAI.CommonBasesFPRAS.deficiencyPartition line 7218
636. lemma OAI.CommonBasesFPRAS.deficiencyPartition_pos line 7219
637. lemma OAI.CommonBasesFPRAS.coefficient_step line 7221
638. lemma OAI.CommonBasesFPRAS.normalized_drift line 7234
639. lemma OAI.CommonBasesFPRAS.estimated_ratio_bounds line 7252
640. lemma OAI.CommonBasesFPRAS.ratio_coarse_bounds line 7271
641. lemma OAI.CommonBasesFPRAS.learned_multiplier_good line 7277
642. lemma OAI.CommonBasesFPRAS.product_ratios line 7294
643. lemma OAI.CommonBasesFPRAS.relative_product_lower line 7302
644. lemma OAI.CommonBasesFPRAS.product_accuracy line 7319
645. lemma OAI.CommonBasesFPRAS.final_estimate_accuracy line 7354
646. def OAI.CommonBasesFPRAS.zeroDeficiencyCount line 7366
647. lemma OAI.CommonBasesFPRAS.partition_contamination line 7367
648. def OAI.CommonBasesFPRAS.FiniteExperiment.expect line 7394
649. def OAI.CommonBasesFPRAS.FiniteExperiment.mass line 7397
650. lemma OAI.CommonBasesFPRAS.FiniteExperiment.expect_nonneg line 7399
651. lemma OAI.CommonBasesFPRAS.FiniteExperiment.expect_mono line 7405
652. lemma OAI.CommonBasesFPRAS.FiniteExperiment.expect_kernel_mono line 7411
653. lemma OAI.CommonBasesFPRAS.FiniteExperiment.mass_nonneg line 7420
654. lemma OAI.CommonBasesFPRAS.FiniteExperiment.mass_le_one line 7422
655. theorem OAI.CommonBasesFPRAS.FiniteExperiment.adaptive_success line 7432
656. def OAI.CommonBasesFPRAS.FiniteExperiment.restrict line 7454
657. lemma OAI.CommonBasesFPRAS.FiniteExperiment.restrict_nonneg line 7457
658. lemma OAI.CommonBasesFPRAS.FiniteExperiment.restrict_le line 7461
659. lemma OAI.CommonBasesFPRAS.FiniteExperiment.restrict_support line 7465
660. lemma OAI.CommonBasesFPRAS.FiniteExperiment.mass_le_good_probability line 7469
661. theorem OAI.CommonBasesFPRAS.FiniteExperiment.good_probability line 7484
662. def OAI.CommonBasesFPRAS.slotPair line 7498
663. def OAI.CommonBasesFPRAS.pairedSlots line 7499
664. lemma OAI.CommonBasesFPRAS.slotPairList_fresh line 7502
665. lemma OAI.CommonBasesFPRAS.pairedSlots_fresh line 7514
666. lemma OAI.CommonBasesFPRAS.pairedSlots_length line 7516
667. lemma OAI.CommonBasesFPRAS.pairedSlots_ne_nil line 7517
668. lemma OAI.CommonBasesFPRAS.pairedSlots_cover line 7521
669. lemma OAI.CommonBasesFPRAS.pairedSlots_plain line 7527
670. lemma OAI.CommonBasesFPRAS.transversal_plain line 7540
671. lemma OAI.CommonBasesFPRAS.plain_eq_transversal line 7550
672. def OAI.CommonBasesFPRAS.plainEquivSubsets line 7564
673. lemma OAI.CommonBasesFPRAS.pairedPlain_card line 7570
674. def OAI.CommonBasesFPRAS.subsetDeficiency line 7574
675. lemma OAI.CommonBasesFPRAS.subsetDeficiency_zero line 7576
676. def OAI.CommonBasesFPRAS.commonSetFinsetEquiv line 7599
677. lemma OAI.CommonBasesFPRAS.zeroDeficiency_eq_commonBaseCount line 7606
678. lemma OAI.CommonBasesFPRAS.plainPartition_eq_subsets line 7618
679. theorem OAI.CommonBasesFPRAS.paired_partition_contamination line 7630
680. lemma OAI.CommonBasesFPRAS.annealRho_pow_upper line 7640
681. lemma OAI.CommonBasesFPRAS.anneal_final_bounds line 7658
682. lemma OAI.CommonBasesFPRAS.anneal_final_contamination line 7667
683. lemma OAI.CommonBasesFPRAS.partition_le_card line 7673
684. lemma OAI.CommonBasesFPRAS.anneal_minimum_mass line 7679
685. lemma OAI.CommonBasesFPRAS.FiniteChain.kernel_power_action line 7708
686. lemma OAI.CommonBasesFPRAS.FiniteChain.kernel_power_density line 7720
687. lemma OAI.CommonBasesFPRAS.FiniteChain.kernel_point_mixing line 7724
688. lemma OAI.CommonBasesFPRAS.FiniteChain.kernel_power_warm_any line 7730
689. lemma OAI.CommonBasesFPRAS.Annealing.restart_exponential line 7748
690. lemma OAI.CommonBasesFPRAS.slotTotal_mono line 7777
691. lemma OAI.CommonBasesFPRAS.slotTotal_scale line 7789
692. def OAI.CommonBasesFPRAS.annealWeight line 7791
693. lemma OAI.CommonBasesFPRAS.annealWeight_pos line 7793
694. lemma OAI.CommonBasesFPRAS.annealWeight_step line 7797
695. lemma OAI.CommonBasesFPRAS.annealWeight_drift line 7801
696. lemma OAI.CommonBasesFPRAS.anneal_slot_drift line 7810
697. lemma OAI.CommonBasesFPRAS.anneal_ideal_drift line 7817
698. structure OAI.CommonBasesFPRAS.GoodMultipliers line 7837
699. lemma OAI.CommonBasesFPRAS.anneal_ratio_mean line 7843
700. lemma OAI.CommonBasesFPRAS.plain_probability_mean line 7853
701. lemma OAI.CommonBasesFPRAS.weight_mean_identity line 7859
702. lemma OAI.CommonBasesFPRAS.plainIndex_card line 7868
703. lemma OAI.CommonBasesFPRAS.anneal_plainPartition line 7875
704. lemma OAI.CommonBasesFPRAS.actual_trace_minimum line 7882
705. lemma OAI.CommonBasesFPRAS.slotTotal_one line 7891
706. lemma OAI.CommonBasesFPRAS.initial_ideal line 7901
707. lemma OAI.CommonBasesFPRAS.initial_good line 7914
708. def OAI.CommonBasesFPRAS.empirical line 7926
709. def OAI.CommonBasesFPRAS.learnedMultipliers line 7928
710. def OAI.CommonBasesFPRAS.empiricalRatio line 7933
711. def OAI.CommonBasesFPRAS.AccuratePhase line 7936
712. lemma OAI.CommonBasesFPRAS.relative_error_bounds line 7941
713. lemma OAI.CommonBasesFPRAS.accurate_plain line 7945
714. lemma OAI.CommonBasesFPRAS.accurate_defect line 7950
715. theorem OAI.CommonBasesFPRAS.successful_phase_learns line 7957
716. theorem OAI.CommonBasesFPRAS.successful_phase_ratio line 8004
717. lemma OAI.CommonBasesFPRAS.FiniteChain.capped_power_submass line 8036
718. lemma OAI.CommonBasesFPRAS.FiniteChain.cappedTrace_power_submass line 8058
719. def OAI.CommonBasesFPRAS.actualTrace line 8077
720. lemma OAI.CommonBasesFPRAS.actual_trace_poincare line 8081
721. lemma OAI.CommonBasesFPRAS.actual_trace_mixing_warm line 8092
722. lemma OAI.CommonBasesFPRAS.actual_mu_drift line 8108
723. def OAI.CommonBasesFPRAS.actualCappedTrace line 8127
724. lemma OAI.CommonBasesFPRAS.actualCappedTrace_le line 8133
725. lemma OAI.CommonBasesFPRAS.actual_capped_mixing line 8136
726. lemma OAI.CommonBasesFPRAS.actual_capped_loss line 8145
727. def OAI.CommonBasesFPRAS.uniformPlain line 8170
728. lemma OAI.CommonBasesFPRAS.uniformPlain_mass line 8172
729. lemma OAI.CommonBasesFPRAS.uniformPlain_pi line 8174
730. def OAI.CommonBasesFPRAS.restartLaw line 8180
731. lemma OAI.CommonBasesFPRAS.restartLaw_nonneg line 8184
732. lemma OAI.CommonBasesFPRAS.restartLaw_mass_le line 8189
733. lemma OAI.CommonBasesFPRAS.restartLaw_warm line 8194
734. lemma OAI.CommonBasesFPRAS.restartLaw_missing_mass line 8211
735. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_congr_length line 8237
736. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_compl line 8247
737. lemma OAI.CommonBasesFPRAS.FiniteChain.pathProbability_le_mass line 8261
738. lemma OAI.CommonBasesFPRAS.empirical_trajectory line 8271
739. theorem OAI.CommonBasesFPRAS.accurate_phase_probability line 8275
740. lemma OAI.CommonBasesFPRAS.product_ratios_telescope line 8309
741. lemma OAI.CommonBasesFPRAS.accurate_phases_product line 8314
742. theorem OAI.CommonBasesFPRAS.actual_estimator_accuracy line 8350
743. def OAI.CommonBasesFPRAS.FiniteChain.Sample line 8380
744. instance OAI.CommonBasesFPRAS.FiniteChain.sampleFintype line 8383
745. def OAI.CommonBasesFPRAS.FiniteChain.Sample.toList line 8389
746. lemma OAI.CommonBasesFPRAS.FiniteChain.Sample.toList_length line 8393
747. def OAI.CommonBasesFPRAS.FiniteChain.sampleMass line 8398
748. lemma OAI.CommonBasesFPRAS.FiniteChain.sampleMass_nonneg line 8401
749. lemma OAI.CommonBasesFPRAS.FiniteChain.sampleMass_expect line 8406
750. lemma OAI.CommonBasesFPRAS.FiniteChain.sampleMass_total line 8419
751. lemma OAI.CommonBasesFPRAS.FiniteChain.sampleMass_event line 8423
752. def OAI.CommonBasesFPRAS.plainLift line 8434
753. lemma OAI.CommonBasesFPRAS.plainLift_nonneg line 8437
754. lemma OAI.CommonBasesFPRAS.plainLift_mass line 8440
755. lemma OAI.CommonBasesFPRAS.plainLift_warm line 8449
756. theorem OAI.CommonBasesFPRAS.FiniteExperiment.adaptive_success_bounded line 8474
757. theorem OAI.CommonBasesFPRAS.FiniteExperiment.good_probability_bounded line 8497
758. def OAI.CommonBasesFPRAS.historyWeights line 8512
759. lemma OAI.CommonBasesFPRAS.historyWeights_nil line 8516
760. lemma OAI.CommonBasesFPRAS.historyWeights_snoc line 8518
761. inductive OAI.CommonBasesFPRAS.SuccessfulHistory line 8522
762. lemma OAI.CommonBasesFPRAS.successfulHistory_take line 8527
763. lemma OAI.CommonBasesFPRAS.successfulHistory_good line 8539
764. lemma OAI.CommonBasesFPRAS.successfulHistory_snoc_iff line 8549
765. def OAI.CommonBasesFPRAS.restartCap line 8578
766. lemma OAI.CommonBasesFPRAS.restartCap_pos line 8580
767. lemma OAI.CommonBasesFPRAS.restartCap_loss line 8582
768. abbrev OAI.CommonBasesFPRAS.PhaseSample line 8596
769. def OAI.CommonBasesFPRAS.observedSets line 8597
770. def OAI.CommonBasesFPRAS.storedWeights line 8598
771. def OAI.CommonBasesFPRAS.HistoryPositive line 8600
772. lemma OAI.CommonBasesFPRAS.storedWeights_current line 8602
773. lemma OAI.CommonBasesFPRAS.historyPositive_all line 8604
774. lemma OAI.CommonBasesFPRAS.successfulHistory_positive line 8611
775. lemma OAI.CommonBasesFPRAS.successfulHistory_stored_good line 8618
776. def OAI.CommonBasesFPRAS.phaseStart line 8626
777. def OAI.CommonBasesFPRAS.phaseChain line 8628
778. def OAI.CommonBasesFPRAS.phaseKernel line 8632
779. lemma OAI.CommonBasesFPRAS.phaseStart_nonneg line 8635
780. lemma OAI.CommonBasesFPRAS.phaseKernel_nonneg line 8638
781. lemma OAI.CommonBasesFPRAS.phaseKernel_mass_le line 8643
782. lemma OAI.CommonBasesFPRAS.phaseStart_warm line 8657
783. lemma OAI.CommonBasesFPRAS.phaseStart_mass_lower line 8672
784. lemma OAI.CommonBasesFPRAS.phaseKernel_good_mass line 8684
785. theorem OAI.CommonBasesFPRAS.actual_history_success line 8727
786. def OAI.CommonBasesFPRAS.historySample line 8746
787. lemma OAI.CommonBasesFPRAS.historySample_getElem line 8748
788. lemma OAI.CommonBasesFPRAS.successfulHistory_accurate line 8750
789. def OAI.CommonBasesFPRAS.historyEstimate line 8763
790. lemma OAI.CommonBasesFPRAS.historyEstimate_accuracy line 8767
791. lemma OAI.CommonBasesFPRAS.empirical_nonneg line 8786
792. lemma OAI.CommonBasesFPRAS.empiricalRatio_nonneg line 8791
793. lemma OAI.CommonBasesFPRAS.historyEstimate_nonneg line 8798
794. def OAI.CommonBasesFPRAS.Witnessed line 8811
795. lemma OAI.CommonBasesFPRAS.witnessed_iff_common_base line 8812
796. lemma OAI.CommonBasesFPRAS.witnessed_count_pos line 8817
797. lemma OAI.CommonBasesFPRAS.warm_witness_bad_mass line 8825
798. def OAI.CommonBasesFPRAS.witnessKernel line 8855
799. lemma OAI.CommonBasesFPRAS.witnessKernel_nonneg line 8859
800. lemma OAI.CommonBasesFPRAS.witnessKernel_mass_le line 8865
801. lemma OAI.CommonBasesFPRAS.witnessKernel_good_mass line 8872
802. lemma OAI.CommonBasesFPRAS.FiniteExperiment.expect_mul_left line 8917
803. lemma OAI.CommonBasesFPRAS.FiniteExperiment.expect_mono_length line 8927
804. def OAI.CommonBasesFPRAS.guardedEstimate line 8947
805. lemma OAI.CommonBasesFPRAS.guardedEstimate_nonneg line 8950
806. lemma OAI.CommonBasesFPRAS.guardedEstimate_zero line 8956
807. def OAI.CommonBasesFPRAS.actualRealSuccess line 8964
808. theorem OAI.CommonBasesFPRAS.real_annealing_success line 8970
809. abbrev OAI.CommonBasesFPRAS.BitWord line 9024
810. def OAI.CommonBasesFPRAS.wordEquiv line 9026
811. def OAI.CommonBasesFPRAS.uniformAverage line 9039
812. lemma OAI.CommonBasesFPRAS.uniformAverage_equiv line 9041
813. lemma OAI.CommonBasesFPRAS.uniformAverage_const line 9044
814. lemma OAI.CommonBasesFPRAS.uniformAverage_add line 9048
815. lemma OAI.CommonBasesFPRAS.uniformAverage_mul_left line 9051
816. lemma OAI.CommonBasesFPRAS.uniformAverage_prod line 9054
817. lemma OAI.CommonBasesFPRAS.uniformAverage_fin_succ line 9059
818. def OAI.CommonBasesFPRAS.boundedUniform line 9065
819. def OAI.CommonBasesFPRAS.rejectionRate line 9070
820. lemma OAI.CommonBasesFPRAS.acceptedCard line 9071
821. lemma OAI.CommonBasesFPRAS.rejectedCard line 9079
822. lemma OAI.CommonBasesFPRAS.sum_ite_count line 9082
823. lemma OAI.CommonBasesFPRAS.one_trial_none line 9088
824. lemma OAI.CommonBasesFPRAS.one_trial_some line 9102
825. lemma OAI.CommonBasesFPRAS.boundedUniform_failure line 9127
826. lemma OAI.CommonBasesFPRAS.rejectionRate_bounds line 9144
827. lemma OAI.CommonBasesFPRAS.boundedUniform_failure_bound line 9153
828. lemma OAI.CommonBasesFPRAS.clog_trial_size line 9158
829. lemma OAI.CommonBasesFPRAS.boundedUniform_probability line 9168
830. lemma OAI.CommonBasesFPRAS.uniformAverage_sum line 9198
831. lemma OAI.CommonBasesFPRAS.boundedUniform_law line 9203
832. lemma OAI.CommonBasesFPRAS.uniformAverage_nonneg line 9221
833. lemma OAI.CommonBasesFPRAS.uniformAverage_mono line 9224
834. lemma OAI.CommonBasesFPRAS.uniformAverage_sub_const line 9227
835. def OAI.CommonBasesFPRAS.bitPrefix line 9235
836. lemma OAI.CommonBasesFPRAS.uniformAverage_bitPrefix line 9237
837. lemma OAI.CommonBasesFPRAS.uniformAverage_prefixTrials line 9247
838. inductive OAI.CommonBasesFPRAS.DrawTree line 9275
839. def OAI.CommonBasesFPRAS.DrawTree.expectation line 9283
840. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_nonneg line 9286
841. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_le_one line 9291
842. def OAI.CommonBasesFPRAS.DrawTree.Fits line 9299
843. def OAI.CommonBasesFPRAS.DrawTree.run line 9304
844. def OAI.CommonBasesFPRAS.DrawTree.optionValue line 9315
845. lemma OAI.CommonBasesFPRAS.DrawTree.run_draw_average line 9318
846. theorem OAI.CommonBasesFPRAS.DrawTree.run_lower line 9346
847. def OAI.CommonBasesFPRAS.DrawTree.bind line 9386
848. def OAI.CommonBasesFPRAS.DrawTree.map line 9389
849. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_bind line 9390
850. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_map line 9395
851. lemma OAI.CommonBasesFPRAS.DrawTree.fits_mono_steps line 9398
852. lemma OAI.CommonBasesFPRAS.DrawTree.fits_bind line 9409
853. def OAI.CommonBasesFPRAS.DrawTree.rationalCoin line 9423
854. lemma OAI.CommonBasesFPRAS.DrawTree.rationalCoin_expectation line 9425
855. lemma OAI.CommonBasesFPRAS.DrawTree.rationalCoin_fits line 9438
856. def OAI.CommonBasesFPRAS.DrawTree.bernoulli line 9440
857. lemma OAI.CommonBasesFPRAS.DrawTree.bernoulli_expectation line 9441
858. lemma OAI.CommonBasesFPRAS.DrawTree.bernoulli_fits line 9456
859. abbrev OAI.CommonBasesFPRAS.ExchangeChoice line 9467
860. def OAI.CommonBasesFPRAS.exchangedSet line 9468
861. lemma OAI.CommonBasesFPRAS.exchangedSet_adjacent line 9470
862. lemma OAI.CommonBasesFPRAS.exchangedSet_left_difference line 9487
863. lemma OAI.CommonBasesFPRAS.exchangedSet_right_difference line 9501
864. lemma OAI.CommonBasesFPRAS.exchangedSet_injective line 9510
865. lemma OAI.CommonBasesFPRAS.exchangedSet_exists_iff line 9521
866. lemma OAI.CommonBasesFPRAS.sum_exchangedSet_indicator line 9528
867. lemma OAI.CommonBasesFPRAS.exchangeChoice_card line 9539
868. def OAI.CommonBasesFPRAS.metropolisAcceptance line 9551
869. def OAI.CommonBasesFPRAS.exchangeOffer line 9554
870. lemma OAI.CommonBasesFPRAS.exchangeOffer_expansion line 9562
871. lemma OAI.CommonBasesFPRAS.metropolisAcceptance_min line 9581
872. lemma OAI.CommonBasesFPRAS.lazy_exchange_expectation line 9590
873. def OAI.CommonBasesFPRAS.rationalMultiplier line 9639
874. def OAI.CommonBasesFPRAS.rationalWeight line 9642
875. lemma OAI.CommonBasesFPRAS.rationalMultiplier_cast line 9646
876. lemma OAI.CommonBasesFPRAS.rationalWeight_cast line 9651
877. def OAI.CommonBasesFPRAS.rationalEmpirical line 9655
878. lemma OAI.CommonBasesFPRAS.rationalEmpirical_cast line 9658
879. def OAI.CommonBasesFPRAS.rationalPlain line 9661
880. lemma OAI.CommonBasesFPRAS.rationalPlain_cast line 9664
881. def OAI.CommonBasesFPRAS.rationalDefect line 9667
882. lemma OAI.CommonBasesFPRAS.rationalDefect_cast line 9670
883. def OAI.CommonBasesFPRAS.rationalLearn line 9673
884. lemma OAI.CommonBasesFPRAS.rationalLearn_cast line 9678
885. def OAI.CommonBasesFPRAS.rationalHistory line 9683
886. lemma OAI.CommonBasesFPRAS.rationalHistory_cast line 9686
887. def OAI.CommonBasesFPRAS.rationalRho line 9698
888. lemma OAI.CommonBasesFPRAS.rationalRho_cast line 9699
889. def OAI.CommonBasesFPRAS.rationalAnneal line 9700
890. lemma OAI.CommonBasesFPRAS.rationalAnneal_cast line 9703
891. def OAI.CommonBasesFPRAS.rationalRatio line 9705
892. lemma OAI.CommonBasesFPRAS.rationalRatio_cast line 9707
893. def OAI.CommonBasesFPRAS.DrawTree.uniformChoice line 9714
894. lemma OAI.CommonBasesFPRAS.DrawTree.uniformChoice_expectation line 9717
895. lemma OAI.CommonBasesFPRAS.DrawTree.uniformChoice_fits line 9722
896. def OAI.CommonBasesFPRAS.rationalAcceptance line 9734
897. lemma OAI.CommonBasesFPRAS.rationalAcceptance_cast line 9736
898. lemma OAI.CommonBasesFPRAS.rationalAcceptance_bounds line 9740
899. def OAI.CommonBasesFPRAS.rationalExchange line 9749
900. lemma OAI.CommonBasesFPRAS.rationalExchange_expectation line 9755
901. def OAI.CommonBasesFPRAS.rationalMetropolis line 9766
902. lemma OAI.CommonBasesFPRAS.rationalMetropolis_expectation line 9773
903. def OAI.CommonBasesFPRAS.DrawTree.optionBind line 9793
904. def OAI.CommonBasesFPRAS.DrawTree.pureSome line 9795
905. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_zero line 9796
906. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_add line 9800
907. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_mul_left line 9805
908. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_sum line 9810
909. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_mono line 9815
910. lemma OAI.CommonBasesFPRAS.DrawTree.expectation_optionBind line 9820
911. lemma OAI.CommonBasesFPRAS.DrawTree.optionBind_fits line 9825
912. def OAI.CommonBasesFPRAS.DrawTree.Matches line 9833
913. lemma OAI.CommonBasesFPRAS.DrawTree.matches_comp line 9835
914. def OAI.CommonBasesFPRAS.DrawTree.iterate line 9845
915. lemma OAI.CommonBasesFPRAS.DrawTree.iterate_matches line 9848
916. lemma OAI.CommonBasesFPRAS.DrawTree.iterate_fits line 9858
917. def OAI.CommonBasesFPRAS.hittingTree line 9872
918. lemma OAI.CommonBasesFPRAS.hittingTree_fits line 9876
919. lemma OAI.CommonBasesFPRAS.partialGreen_succ_apply line 9890
920. lemma OAI.CommonBasesFPRAS.hittingTree_outside line 9898
921. lemma OAI.CommonBasesFPRAS.hittingTree_inside line 9919
922. lemma OAI.CommonBasesFPRAS.DrawTree.map_fits line 9954
923. def OAI.CommonBasesFPRAS.DrawTree.sample line 9958
924. lemma OAI.CommonBasesFPRAS.DrawTree.sampleMass_delta line 9961
925. lemma OAI.CommonBasesFPRAS.DrawTree.sample_expectation line 9972
926. lemma OAI.CommonBasesFPRAS.DrawTree.sample_start_expectation line 9994
927. lemma OAI.CommonBasesFPRAS.DrawTree.sample_fits line 10011
928. def OAI.CommonBasesFPRAS.DrawTree.history line 10022
929. lemma OAI.CommonBasesFPRAS.DrawTree.history_expectation line 10025
930. lemma OAI.CommonBasesFPRAS.DrawTree.history_fits line 10035
931. def OAI.CommonBasesFPRAS.rationalStored line 10048
932. lemma OAI.CommonBasesFPRAS.rationalStored_cast line 10050
933. lemma OAI.CommonBasesFPRAS.rationalStored_pos line 10053
934. def OAI.CommonBasesFPRAS.actualStepTree line 10058
935. lemma OAI.CommonBasesFPRAS.actualStepTree_expectation line 10061
936. def OAI.CommonBasesFPRAS.actualTraceTree line 10071
937. lemma OAI.CommonBasesFPRAS.actualTraceTree_matches line 10074
938. def OAI.CommonBasesFPRAS.actualRestartTree line 10086
939. lemma OAI.CommonBasesFPRAS.actualRestartTree_expectation line 10092
940. def OAI.CommonBasesFPRAS.actualStartTree line 10110
941. lemma OAI.CommonBasesFPRAS.actualStartTree_expectation line 10112
942. def OAI.CommonBasesFPRAS.actualPhaseTree line 10131
943. lemma OAI.CommonBasesFPRAS.actualPhaseTree_matches line 10136
944. def OAI.CommonBasesFPRAS.rationalEstimate line 10149
945. lemma OAI.CommonBasesFPRAS.rationalEstimate_cast line 10153
946. def OAI.CommonBasesFPRAS.rationalGuard line 10157
947. lemma OAI.CommonBasesFPRAS.rationalGuard_cast line 10159
948. lemma OAI.CommonBasesFPRAS.rationalGuard_nonneg line 10164
949. lemma OAI.CommonBasesFPRAS.rationalGuard_zero line 10169
950. def OAI.CommonBasesFPRAS.rationalWitnessTree line 10175
951. lemma OAI.CommonBasesFPRAS.rationalWitnessTree_expectation line 10177
952. def OAI.CommonBasesFPRAS.rationalAlgorithmTree line 10184
953. lemma OAI.CommonBasesFPRAS.rationalAlgorithmTree_expectation line 10187
954. lemma OAI.CommonBasesFPRAS.rationalAlgorithmTree_success_eq line 10199
955. theorem OAI.CommonBasesFPRAS.rational_algorithm_success line 10215
956. def OAI.CommonBasesFPRAS.RatBound line 10229
957. lemma OAI.CommonBasesFPRAS.RatBound.nonneg line 10233
958. lemma OAI.CommonBasesFPRAS.RatBound.one_le line 10235
959. lemma OAI.CommonBasesFPRAS.RatBound.mono line 10237
960. lemma OAI.CommonBasesFPRAS.RatBound.nat line 10240
961. lemma OAI.CommonBasesFPRAS.RatBound.zero line 10242
962. lemma OAI.CommonBasesFPRAS.RatBound.one line 10243
963. lemma OAI.CommonBasesFPRAS.RatBound.mul line 10244
964. lemma OAI.CommonBasesFPRAS.RatBound.inv line 10248
965. lemma OAI.CommonBasesFPRAS.RatBound.div line 10253
966. lemma OAI.CommonBasesFPRAS.RatBound.pow line 10255
967. lemma OAI.CommonBasesFPRAS.RatBound.min_one line 10259
968. lemma OAI.CommonBasesFPRAS.RatBound.den_le line 10263
969. lemma OAI.CommonBasesFPRAS.RatBound.num_le line 10269
970. lemma OAI.CommonBasesFPRAS.RatBound.nat_div line 10281
971. lemma OAI.CommonBasesFPRAS.indicator_list_sum line 10285
972. lemma OAI.CommonBasesFPRAS.rationalTypeRatio line 10292
973. lemma OAI.CommonBasesFPRAS.rationalLearn_bound line 10303
974. lemma OAI.CommonBasesFPRAS.rationalHistory_bound line 10314
975. lemma OAI.CommonBasesFPRAS.rationalMultiplier_bound line 10326
976. lemma OAI.CommonBasesFPRAS.rationalRho_bound line 10333
977. lemma OAI.CommonBasesFPRAS.rationalAnneal_bound line 10341
978. lemma OAI.CommonBasesFPRAS.observedSets_length line 10355
979. lemma OAI.CommonBasesFPRAS.rationalStored_bound line 10358
980. lemma OAI.CommonBasesFPRAS.rationalWeight_bound line 10367
981. lemma OAI.CommonBasesFPRAS.rationalAcceptance_bound line 10377
982. def OAI.CommonBasesFPRAS.drawWordBound line 10389
983. lemma OAI.CommonBasesFPRAS.acceptance_word_bound line 10390
984. lemma OAI.CommonBasesFPRAS.drawWordBound_ge_one line 10402
985. lemma OAI.CommonBasesFPRAS.drawWordBound_ge_n line 10403
986. lemma OAI.CommonBasesFPRAS.drawWordBound_exchange line 10404
987. lemma OAI.CommonBasesFPRAS.actualStepTree_fits line 10414
988. lemma OAI.CommonBasesFPRAS.actualTraceTree_fits line 10442
989. lemma OAI.CommonBasesFPRAS.actualRestartTree_fits line 10446
990. def OAI.CommonBasesFPRAS.phaseDrawBound line 10466
991. lemma OAI.CommonBasesFPRAS.actualPhaseTree_fits line 10468
992. lemma OAI.CommonBasesFPRAS.DrawTree.bind_assoc line 10487
993. lemma OAI.CommonBasesFPRAS.DrawTree.optionBind_assoc line 10492
994. lemma OAI.CommonBasesFPRAS.DrawTree.leaf_fits line 10496
995. lemma OAI.CommonBasesFPRAS.rationalWitnessTree_fits line 10505
996. lemma OAI.CommonBasesFPRAS.rational_history_finish_fits line 10517
997. def OAI.CommonBasesFPRAS.algorithmDrawBound line 10534
998. lemma OAI.CommonBasesFPRAS.rationalAlgorithmTree_fits line 10536
999. def OAI.CommonBasesFPRAS.DrawTree.All line 10542
1000. lemma OAI.CommonBasesFPRAS.DrawTree.all_bind line 10545
1001. lemma OAI.CommonBasesFPRAS.DrawTree.all_map line 10550
1002. lemma OAI.CommonBasesFPRAS.DrawTree.run_all line 10552
1003. lemma OAI.CommonBasesFPRAS.rationalAlgorithmTree_all line 10573
1004. lemma OAI.CommonBasesFPRAS.uniformAverage_one_sub line 10595
1005. lemma OAI.CommonBasesFPRAS.rejectionBudget line 10600
1006. abbrev OAI.CommonBasesFPRAS.FairBank line 10606
1007. def OAI.CommonBasesFPRAS.fairOutput line 10608
1008. lemma OAI.CommonBasesFPRAS.fairOutput_nonneg line 10611
1009. lemma OAI.CommonBasesFPRAS.fairOutput_zero line 10623
1010. theorem OAI.CommonBasesFPRAS.fair_single_success line 10637
1011. def OAI.CommonBasesFPRAS.rationalMedian line 10681
1012. def OAI.CommonBasesFPRAS.outsideInterval line 10683
1013. lemma OAI.CommonBasesFPRAS.median_bad_count line 10684
1014. lemma OAI.CommonBasesFPRAS.uniformAverage_mul_const line 10725
1015. lemma OAI.CommonBasesFPRAS.countP_ofFn_cons line 10731
1016. lemma OAI.CommonBasesFPRAS.independent_bad_moment line 10738
1017. lemma OAI.CommonBasesFPRAS.countP_map line 10754
1018. theorem OAI.CommonBasesFPRAS.median_failure_bound line 10760
1019. def OAI.CommonBasesFPRAS.repetitionCount line 10798
1020. lemma OAI.CommonBasesFPRAS.repetitionCount_pos line 10799
1021. lemma OAI.CommonBasesFPRAS.rational_binary_accuracy line 10800
1022. lemma OAI.CommonBasesFPRAS.confidence_decay line 10810
1023. theorem OAI.CommonBasesFPRAS.median_confidence line 10818
1024. lemma OAI.CommonBasesFPRAS.rationalMedian_all line 10847
1025. def OAI.CommonBasesFPRAS.accuracyExponent line 10857
1026. lemma OAI.CommonBasesFPRAS.accuracyExponent_spec line 10858
1027. def OAI.CommonBasesFPRAS.sampleCount line 10866
1028. lemma OAI.CommonBasesFPRAS.sampleCount_pos line 10867
1029. lemma OAI.CommonBasesFPRAS.sampleCount_spec line 10868
1030. def OAI.CommonBasesFPRAS.amplifiedOutput line 10884
1031. lemma OAI.CommonBasesFPRAS.amplifiedOutput_nonneg line 10887
1032. lemma OAI.CommonBasesFPRAS.amplifiedOutput_zero line 10893
1033. theorem OAI.CommonBasesFPRAS.amplified_success line 10901
1034. abbrev OAI.CommonBasesFPRAS.FPRASBank line 10937
1035. def OAI.CommonBasesFPRAS.boundedFPRASOutput line 10939
1036. theorem OAI.CommonBasesFPRAS.bounded_fair_experiment line 10943
1037. def OAI.CommonBasesFPRAS.greedyOracle line 10961
1038. lemma OAI.CommonBasesFPRAS.greedyOracle_correct line 10965
1039. def OAI.CommonBasesFPRAS.greedyQueryCount line 10993
1040. lemma OAI.CommonBasesFPRAS.greedyQueryCount_eq line 10997
1041. lemma OAI.CommonBasesFPRAS.greedyOracle_rank line 11000
1042. def OAI.CommonBasesFPRAS.queryFinset line 11010
1043. def OAI.CommonBasesFPRAS.rankOracle line 11012
1044. lemma OAI.CommonBasesFPRAS.queryFinset_exact line 11014
1045. lemma OAI.CommonBasesFPRAS.rankOracle_correct line 11021
1046. lemma OAI.CommonBasesFPRAS.rankOracle_query_bound line 11033
1047. lemma OAI.CommonBasesFPRAS.sum_eRk line 11042
1048. lemma OAI.CommonBasesFPRAS.dual_rank_nat line 11057
1049. def OAI.CommonBasesFPRAS.pairedDeficiencyOracle line 11071
1050. lemma OAI.CommonBasesFPRAS.paired_rank_nat line 11074
1051. lemma OAI.CommonBasesFPRAS.pairedDeficiencyOracle_correct line 11084
1052. def OAI.CommonBasesFPRAS.verifyCommonBase line 11097
1053. lemma OAI.CommonBasesFPRAS.verifyCommonBase_correct line 11099
1054. lemma OAI.CommonBasesFPRAS.verified_count_positive line 11118
1055. def OAI.CommonBasesFPRAS.oracleDeficiency line 11131
1056. def OAI.CommonBasesFPRAS.oracleAnneal line 11133
1057. def OAI.CommonBasesFPRAS.rationalHistoryPositive line 11135
1058. lemma OAI.CommonBasesFPRAS.rationalHistoryPositive_iff line 11137
1059. def OAI.CommonBasesFPRAS.oracleStepTree line 11147
1060. def OAI.CommonBasesFPRAS.oracleTraceTree line 11150
1061. def OAI.CommonBasesFPRAS.oracleRestartTree line 11153
1062. def OAI.CommonBasesFPRAS.oracleStartTree line 11159
1063. def OAI.CommonBasesFPRAS.oraclePhaseTree line 11161
1064. def OAI.CommonBasesFPRAS.oracleEstimate line 11166
1065. def OAI.CommonBasesFPRAS.oracleGuard line 11170
1066. def OAI.CommonBasesFPRAS.oracleWitnessTree line 11172
1067. def OAI.CommonBasesFPRAS.oracleAlgorithmTree line 11175
1068. lemma OAI.CommonBasesFPRAS.oracleDeficiency_eq line 11182
1069. lemma OAI.CommonBasesFPRAS.oracleAnneal_eq line 11185
1070. lemma OAI.CommonBasesFPRAS.oracleStepTree_eq line 11188
1071. lemma OAI.CommonBasesFPRAS.oracleTraceTree_eq line 11192
1072. lemma OAI.CommonBasesFPRAS.oracleRestartTree_eq line 11196
1073. lemma OAI.CommonBasesFPRAS.oracleStartTree_eq line 11203
1074. lemma OAI.CommonBasesFPRAS.oraclePhaseTree_eq line 11207
1075. lemma OAI.CommonBasesFPRAS.oracleEstimate_eq line 11212
1076. lemma OAI.CommonBasesFPRAS.oracleGuard_eq line 11216
1077. lemma OAI.CommonBasesFPRAS.oracleWitnessTree_eq line 11223
1078. theorem OAI.CommonBasesFPRAS.oracleAlgorithmTree_eq line 11227
1079. lemma OAI.CommonBasesFPRAS.RatBound.add line 11237
1080. lemma OAI.CommonBasesFPRAS.RatBound.bits line 11248
1081. lemma OAI.CommonBasesFPRAS.RatBound.binary_add line 11255
1082. lemma OAI.CommonBasesFPRAS.RatBound.binary_mul line 11260
1083. lemma OAI.CommonBasesFPRAS.RatBound.binary_div line 11262
1084. lemma OAI.CommonBasesFPRAS.RatBound.binary_list_sum line 11264
1085. lemma OAI.CommonBasesFPRAS.RatBound.binary_prod line 11274
1086. lemma OAI.CommonBasesFPRAS.rationalEmpirical_binary_bound line 11282
1087. lemma OAI.CommonBasesFPRAS.rho_observable_binary line 11291
1088. lemma OAI.CommonBasesFPRAS.rationalRatio_binary_bound line 11300
1089. lemma OAI.CommonBasesFPRAS.historySample_length_le line 11320
1090. def OAI.CommonBasesFPRAS.outputWordBound line 11328
1091. lemma OAI.CommonBasesFPRAS.rationalEstimate_binary_bound line 11330
1092. lemma OAI.CommonBasesFPRAS.rationalGuard_binary_bound line 11342
1093. def OAI.CommonBasesFPRAS.bitResourceParameter line 11351
1094. def OAI.CommonBasesFPRAS.fairBitCount line 11353
1095. lemma OAI.CommonBasesFPRAS.polynomial_recipe_bounds line 11357
1096. theorem OAI.CommonBasesFPRAS.fairBitCount_polynomial line 11415
1097. def OAI.CommonBasesFPRAS.oracleFairOutput line 11439
1098. lemma OAI.CommonBasesFPRAS.oracleFairOutput_eq line 11443
1099. def OAI.CommonBasesFPRAS.oracleAmplifiedOutput line 11451
1100. def OAI.CommonBasesFPRAS.oracleBoundedOutput line 11454
1101. lemma OAI.CommonBasesFPRAS.oracleBoundedOutput_eq line 11460
1102. lemma OAI.CommonBasesFPRAS.commonBaseCount_empty line 11468
1103. theorem OAI.CommonBasesFPRAS.oracle_bounded_fair_experiment line 11478
1104. def OAI.CommonBasesFPRAS.wordPlainEquiv line 11503
1105. def OAI.CommonBasesFPRAS.sortedMemberEquiv line 11522
1106. def OAI.CommonBasesFPRAS.canonicalPlainEnumeration line 11533
1107. def OAI.CommonBasesFPRAS.canonicalExchangeEnumeration line 11536
1108. inductive OAI.CommonBasesFPRAS.DrawTree.Reindexed line 11548
1109. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.refl line 11552
1110. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.symm line 11556
1111. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.bind line 11563
1112. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.map line 11569
1113. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.expectation line 11571
1114. def OAI.CommonBasesFPRAS.DrawTree.uniformVia line 11579
1115. lemma OAI.CommonBasesFPRAS.DrawTree.uniformVia_reindexed line 11583
1116. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.fits line 11592
1117. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.all line 11602
1118. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.run_expectation line 11609
1119. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.run_observable line 11626
1120. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.optionBind line 11637
1121. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.iterate line 11644
1122. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.sample line 11649
1123. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.history line 11654
1124. lemma OAI.CommonBasesFPRAS.hittingTree_reindexed line 11661
1125. def OAI.CommonBasesFPRAS.canonicalMetropolis line 11677
1126. lemma OAI.CommonBasesFPRAS.canonicalMetropolis_reindexed line 11685
1127. def OAI.CommonBasesFPRAS.canonicalStepTree line 11698
1128. def OAI.CommonBasesFPRAS.canonicalTraceTree line 11700
1129. def OAI.CommonBasesFPRAS.canonicalRestartTree line 11703
1130. def OAI.CommonBasesFPRAS.canonicalStartTree line 11709
1131. def OAI.CommonBasesFPRAS.canonicalPhaseTree line 11711
1132. def OAI.CommonBasesFPRAS.canonicalWitnessTree line 11716
1133. def OAI.CommonBasesFPRAS.canonicalAlgorithmTree line 11718
1134. lemma OAI.CommonBasesFPRAS.canonicalStepTree_reindexed line 11721
1135. lemma OAI.CommonBasesFPRAS.canonicalTraceTree_reindexed line 11724
1136. lemma OAI.CommonBasesFPRAS.canonicalRestartTree_reindexed line 11727
1137. lemma OAI.CommonBasesFPRAS.canonicalStartTree_reindexed line 11733
1138. lemma OAI.CommonBasesFPRAS.canonicalPhaseTree_reindexed line 11736
1139. lemma OAI.CommonBasesFPRAS.canonicalWitnessTree_reindexed line 11743
1140. lemma OAI.CommonBasesFPRAS.canonicalAlgorithmTree_reindexed line 11749
1141. lemma OAI.CommonBasesFPRAS.uniformAverage_independent_eq line 11758
1142. def OAI.CommonBasesFPRAS.canonicalFairOutput line 11783
1143. def OAI.CommonBasesFPRAS.canonicalAmplifiedOutput line 11787
1144. def OAI.CommonBasesFPRAS.canonicalBoundedOutput line 11790
1145. lemma OAI.CommonBasesFPRAS.canonicalAlgorithmTree_to_rational line 11801
1146. lemma OAI.CommonBasesFPRAS.canonicalAlgorithmTree_fits line 11806
1147. lemma OAI.CommonBasesFPRAS.canonicalFairOutput_all line 11811
1148. lemma OAI.CommonBasesFPRAS.canonicalFairOutput_law line 11828
1149. lemma OAI.CommonBasesFPRAS.canonicalAmplifiedOutput_law line 11835
1150. lemma OAI.CommonBasesFPRAS.canonicalAmplifiedOutput_all line 11842
1151. theorem OAI.CommonBasesFPRAS.canonical_bounded_fair_experiment line 11859
1152. def OAI.CommonBasesFPRAS.bitMatrixEquiv line 11894
1153. def OAI.CommonBasesFPRAS.fourBitEquiv line 11897
1154. def OAI.CommonBasesFPRAS.bankWordEquiv line 11902
1155. def OAI.CommonBasesFPRAS.flatFPRASOutput line 11912
1156. def OAI.CommonBasesFPRAS.paddedFPRASOutput line 11915
1157. lemma OAI.CommonBasesFPRAS.paddedFPRASOutput_law line 11918
1158. lemma OAI.CommonBasesFPRAS.uniformAverage_indicator_card line 11927
1159. theorem OAI.CommonBasesFPRAS.padded_fair_experiment line 11932
1160. inductive OAI.CommonBasesFPRAS.OracleDraw line 11957
1161. def OAI.CommonBasesFPRAS.OracleDraw.bind line 11963
1162. def OAI.CommonBasesFPRAS.OracleDraw.map line 11967
1163. def OAI.CommonBasesFPRAS.OracleDraw.lift line 11968
1164. def OAI.CommonBasesFPRAS.OracleDraw.resolve line 11971
1165. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_bind line 11975
1166. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_map line 11981
1167. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_lift line 11983
1168. def OAI.CommonBasesFPRAS.OracleDraw.Queries line 11988
1169. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_mono line 11992
1170. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_bind line 11999
1171. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_map line 12010
1172. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_lift line 12012
1173. def OAI.CommonBasesFPRAS.OracleDraw.run line 12017
1174. lemma OAI.CommonBasesFPRAS.OracleDraw.run_resolve line 12030
1175. lemma OAI.CommonBasesFPRAS.OracleDraw.run_queries line 12046
1176. def OAI.CommonBasesFPRAS.greedyEffect line 12069
1177. lemma OAI.CommonBasesFPRAS.greedyEffect_resolve line 12073
1178. lemma OAI.CommonBasesFPRAS.greedyEffect_queries line 12078
1179. def OAI.CommonBasesFPRAS.rankEffect line 12084
1180. lemma OAI.CommonBasesFPRAS.rankEffect_resolve line 12086
1181. lemma OAI.CommonBasesFPRAS.rankEffect_queries line 12089
1182. def OAI.CommonBasesFPRAS.deficiencyEffect line 12093
1183. lemma OAI.CommonBasesFPRAS.deficiencyEffect_resolve line 12096
1184. lemma OAI.CommonBasesFPRAS.deficiencyEffect_queries line 12100
1185. def OAI.CommonBasesFPRAS.OracleDraw.optionBind line 12111
1186. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_optionBind line 12113
1187. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_optionBind line 12116
1188. def OAI.CommonBasesFPRAS.OracleDraw.iterate line 12122
1189. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_iterate line 12125
1190. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_iterate line 12130
1191. def OAI.CommonBasesFPRAS.OracleDraw.sample line 12135
1192. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_sample line 12138
1193. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_sample line 12146
1194. def OAI.CommonBasesFPRAS.OracleDraw.hitting line 12153
1195. lemma OAI.CommonBasesFPRAS.OracleDraw.resolve_hitting line 12156
1196. lemma OAI.CommonBasesFPRAS.OracleDraw.queries_hitting line 12163
1197. def OAI.CommonBasesFPRAS.OracleDraw.traverse line 12171
1198. lemma OAI.CommonBasesFPRAS.OracleDraw.traverse_resolve line 12174
1199. lemma OAI.CommonBasesFPRAS.OracleDraw.traverse_queries line 12179
1200. def OAI.CommonBasesFPRAS.exchangeEffect line 12190
1201. lemma OAI.CommonBasesFPRAS.exchangeEffect_resolve line 12200
1202. lemma OAI.CommonBasesFPRAS.exchangeEffect_queries line 12207
1203. def OAI.CommonBasesFPRAS.stepEffect line 12217
1204. lemma OAI.CommonBasesFPRAS.stepEffect_resolve line 12223
1205. lemma OAI.CommonBasesFPRAS.stepEffect_queries line 12231
1206. def OAI.CommonBasesFPRAS.traceEffect line 12249
1207. lemma OAI.CommonBasesFPRAS.traceEffect_resolve line 12252
1208. lemma OAI.CommonBasesFPRAS.traceEffect_queries line 12255
1209. def OAI.CommonBasesFPRAS.restartEffect line 12258
1210. lemma OAI.CommonBasesFPRAS.restartEffect_resolve line 12264
1211. lemma OAI.CommonBasesFPRAS.restartEffect_queries line 12270
1212. def OAI.CommonBasesFPRAS.startEffect line 12277
1213. def OAI.CommonBasesFPRAS.phaseEffect line 12279
1214. lemma OAI.CommonBasesFPRAS.phaseEffect_resolve line 12284
1215. def OAI.CommonBasesFPRAS.witnessEffect line 12291
1216. lemma OAI.CommonBasesFPRAS.witnessEffect_resolve line 12293
1217. def OAI.CommonBasesFPRAS.ratioEffect line 12306
1218. lemma OAI.CommonBasesFPRAS.ratioEffect_resolve line 12310
1219. lemma OAI.CommonBasesFPRAS.ratioEffect_queries line 12319
1220. lemma OAI.CommonBasesFPRAS.historySample_length_bound line 12324
1221. def OAI.CommonBasesFPRAS.estimateProductEffect line 12334
1222. lemma OAI.CommonBasesFPRAS.estimateProductEffect_resolve line 12338
1223. lemma OAI.CommonBasesFPRAS.estimateProductEffect_queries line 12346
1224. def OAI.CommonBasesFPRAS.estimateEffect line 12358
1225. lemma OAI.CommonBasesFPRAS.estimateEffect_resolve line 12360
1226. lemma OAI.CommonBasesFPRAS.estimateEffect_queries line 12363
1227. def OAI.CommonBasesFPRAS.guardEffect line 12366
1228. lemma OAI.CommonBasesFPRAS.guardEffect_resolve line 12368
1229. lemma OAI.CommonBasesFPRAS.guardEffect_queries line 12374
1230. def OAI.CommonBasesFPRAS.finishEffect line 12380
1231. lemma OAI.CommonBasesFPRAS.finishEffect_resolve line 12382
1232. def OAI.CommonBasesFPRAS.historyFinishEffect line 12388
1233. lemma OAI.CommonBasesFPRAS.historyFinishEffect_resolve line 12391
1234. def OAI.CommonBasesFPRAS.queryAlgorithm line 12399
1235. lemma OAI.CommonBasesFPRAS.queryAlgorithm_resolve line 12400
1236. def OAI.CommonBasesFPRAS.phaseQueryBound line 12409
1237. lemma OAI.CommonBasesFPRAS.phaseEffect_queries line 12411
1238. lemma OAI.CommonBasesFPRAS.witnessEffect_queries line 12430
1239. lemma OAI.CommonBasesFPRAS.finishEffect_queries line 12437
1240. lemma OAI.CommonBasesFPRAS.historyFinishEffect_queries line 12449
1241. def OAI.CommonBasesFPRAS.oracleQueryBound line 12458
1242. lemma OAI.CommonBasesFPRAS.queryAlgorithm_queries line 12459
1243. lemma OAI.CommonBasesFPRAS.capped_queryAlgorithm line 12461
1244. lemma OAI.CommonBasesFPRAS.oracleQueryBound_le line 12469
1245. theorem OAI.CommonBasesFPRAS.allQueries_polynomial line 12483
1246. def OAI.CommonBasesFPRAS.queryFairOutput line 12518
1247. lemma OAI.CommonBasesFPRAS.queryFairOutput_value line 12523
1248. lemma OAI.CommonBasesFPRAS.queryFairOutput_queries line 12528
1249. def OAI.CommonBasesFPRAS.queryAmplifiedOutput line 12532
1250. lemma OAI.CommonBasesFPRAS.queryAmplifiedOutput_value line 12536
1251. lemma OAI.CommonBasesFPRAS.queryAmplifiedOutput_queries line 12540
1252. def OAI.CommonBasesFPRAS.queryBoundedOutput line 12546
1253. lemma OAI.CommonBasesFPRAS.queryBoundedOutput_value line 12551
1254. lemma OAI.CommonBasesFPRAS.queryBoundedOutput_queries line 12558
1255. def OAI.CommonBasesFPRAS.paddedQueryOutput line 12565
1256. lemma OAI.CommonBasesFPRAS.paddedQueryOutput_value line 12568
1257. theorem OAI.CommonBasesFPRAS.query_fair_experiment line 12573
1258. def OAI.CommonBasesFPRAS.workConfig line 12597
1259. def OAI.CommonBasesFPRAS.pairRegisters line 12599
1260. lemma OAI.CommonBasesFPRAS.pairRegisters_a line 12601
1261. lemma OAI.CommonBasesFPRAS.pairRegisters_b line 12603
1262. lemma OAI.CommonBasesFPRAS.pairRegisters_update_a line 12605
1263. lemma OAI.CommonBasesFPRAS.pairRegisters_update_b line 12613
1264. lemma OAI.CommonBasesFPRAS.execution_add line 12616
1265. def OAI.CommonBasesFPRAS.incrementProgram line 12625
1266. def OAI.CommonBasesFPRAS.leadingOnes line 12633
1267. def OAI.CommonBasesFPRAS.carryTail line 12637
1268. lemma OAI.CommonBasesFPRAS.leadingOnes_le line 12641
1269. lemma OAI.CommonBasesFPRAS.replicate_append_false line 12645
1270. lemma OAI.CommonBasesFPRAS.increment_carry line 12648
1271. lemma OAI.CommonBasesFPRAS.increment_restore line 12671
1272. def OAI.CommonBasesFPRAS.incrementBits line 12686
1273. lemma OAI.CommonBasesFPRAS.incrementBits_correct line 12687
1274. theorem OAI.CommonBasesFPRAS.increment_block line 12698
1275. def OAI.CommonBasesFPRAS.Instruction.relabel line 12717
1276. def OAI.CommonBasesFPRAS.relabelConfig line 12723
1277. lemma OAI.CommonBasesFPRAS.machineStep_relabel line 12725
1278. lemma OAI.CommonBasesFPRAS.machineStep_none_pre line 12744
1279. lemma OAI.CommonBasesFPRAS.machineStep_none_not_halt line 12749
1280. lemma OAI.CommonBasesFPRAS.execution_relabel line 12754
1281. lemma OAI.CommonBasesFPRAS.execution_relabel_before_halt line 12763
1282. def OAI.CommonBasesFPRAS.firstLabel line 12777
1283. def OAI.CommonBasesFPRAS.secondLabel line 12778
1284. def OAI.CommonBasesFPRAS.lastLabel line 12779
1285. def OAI.CommonBasesFPRAS.concatProgram line 12781
1286. lemma OAI.CommonBasesFPRAS.concatProgram_first line 12784
1287. lemma OAI.CommonBasesFPRAS.concatProgram_second line 12790
1288. lemma OAI.CommonBasesFPRAS.concat_first_run line 12793
1289. lemma OAI.CommonBasesFPRAS.concat_second_run line 12799
1290. def OAI.CommonBasesFPRAS.restartControl line 12805
1291. lemma OAI.CommonBasesFPRAS.link_exit line 12807
1292. theorem OAI.CommonBasesFPRAS.concat_run line 12812
1293. def OAI.CommonBasesFPRAS.tripleRegisters line 12826
1294. lemma OAI.CommonBasesFPRAS.tripleRegisters_a line 12828
1295. lemma OAI.CommonBasesFPRAS.tripleRegisters_b line 12831
1296. lemma OAI.CommonBasesFPRAS.tripleRegisters_d line 12834
1297. lemma OAI.CommonBasesFPRAS.tripleRegisters_update_a line 12837
1298. lemma OAI.CommonBasesFPRAS.tripleRegisters_update_b line 12848
1299. lemma OAI.CommonBasesFPRAS.tripleRegisters_update_d line 12857
1300. def OAI.CommonBasesFPRAS.copyConfig line 12861
1301. def OAI.CommonBasesFPRAS.copyProgram line 12863
1302. lemma OAI.CommonBasesFPRAS.copy_scan line 12874
1303. lemma OAI.CommonBasesFPRAS.copy_restore line 12889
1304. theorem OAI.CommonBasesFPRAS.copy_block line 12906
1305. def OAI.CommonBasesFPRAS.sumDigit line 12918
1306. def OAI.CommonBasesFPRAS.sumCarry line 12919
1307. def OAI.CommonBasesFPRAS.addDigits line 12920
1308. def OAI.CommonBasesFPRAS.addCost line 12927
1309. lemma OAI.CommonBasesFPRAS.addDigits_value line 12934
1310. lemma OAI.CommonBasesFPRAS.addDigits_length_cost line 12951
1311. def OAI.CommonBasesFPRAS.addConfig line 12973
1312. def OAI.CommonBasesFPRAS.addProgram line 12975
1313. lemma OAI.CommonBasesFPRAS.add_build line 12994
1314. lemma OAI.CommonBasesFPRAS.add_restore line 13044
1315. theorem OAI.CommonBasesFPRAS.addition_block line 13060
1316. lemma OAI.CommonBasesFPRAS.addDigits_length_max line 13080
1317. lemma OAI.CommonBasesFPRAS.workReg_ne line 13101
1318. lemma OAI.CommonBasesFPRAS.workReg_ne01 line 13108
1319. lemma OAI.CommonBasesFPRAS.workReg_ne02 line 13109
1320. lemma OAI.CommonBasesFPRAS.workReg_ne03 line 13110
1321. lemma OAI.CommonBasesFPRAS.workReg_ne04 line 13111
1322. lemma OAI.CommonBasesFPRAS.workReg_ne10 line 13112
1323. lemma OAI.CommonBasesFPRAS.workReg_ne12 line 13113
1324. lemma OAI.CommonBasesFPRAS.workReg_ne13 line 13114
1325. lemma OAI.CommonBasesFPRAS.workReg_ne14 line 13115
1326. lemma OAI.CommonBasesFPRAS.workReg_ne20 line 13116
1327. lemma OAI.CommonBasesFPRAS.workReg_ne21 line 13117
1328. lemma OAI.CommonBasesFPRAS.workReg_ne23 line 13118
1329. lemma OAI.CommonBasesFPRAS.workReg_ne24 line 13119
1330. lemma OAI.CommonBasesFPRAS.workReg_ne30 line 13120
1331. lemma OAI.CommonBasesFPRAS.workReg_ne31 line 13121
1332. lemma OAI.CommonBasesFPRAS.workReg_ne32 line 13122
1333. lemma OAI.CommonBasesFPRAS.workReg_ne34 line 13123
1334. lemma OAI.CommonBasesFPRAS.workReg_ne40 line 13124
1335. lemma OAI.CommonBasesFPRAS.workReg_ne41 line 13125
1336. lemma OAI.CommonBasesFPRAS.workReg_ne42 line 13126
1337. lemma OAI.CommonBasesFPRAS.workReg_ne43 line 13127
1338. def OAI.CommonBasesFPRAS.mulRegisters line 13129
1339. lemma OAI.CommonBasesFPRAS.mulRegisters_copy_in line 13132
1340. lemma OAI.CommonBasesFPRAS.mulRegisters_copy_out line 13137
1341. lemma OAI.CommonBasesFPRAS.mulRegisters_add_in line 13142
1342. lemma OAI.CommonBasesFPRAS.mulRegisters_add_out line 13147
1343. lemma OAI.CommonBasesFPRAS.mulRegisters_update0 line 13152
1344. lemma OAI.CommonBasesFPRAS.mulRegisters_update1 line 13156
1345. def OAI.CommonBasesFPRAS.mulBody line 13161
1346. def OAI.CommonBasesFPRAS.mulBodyConfig line 13162
1347. def OAI.CommonBasesFPRAS.mulBodyCost line 13164
1348. lemma OAI.CommonBasesFPRAS.mulBody_exit line 13166
1349. lemma OAI.CommonBasesFPRAS.mulBody_run line 13168
1350. lemma OAI.CommonBasesFPRAS.mulBodyCost_bound line 13190
1351. def OAI.CommonBasesFPRAS.mulBodyLabel line 13198
1352. def OAI.CommonBasesFPRAS.mulProgram line 13199
1353. def OAI.CommonBasesFPRAS.mulConfig line 13204
1354. lemma OAI.CommonBasesFPRAS.mulProgram_body line 13206
1355. lemma OAI.CommonBasesFPRAS.mulProgram_body_run line 13212
1356. def OAI.CommonBasesFPRAS.mulDigits line 13223
1357. def OAI.CommonBasesFPRAS.mulCost line 13227
1358. lemma OAI.CommonBasesFPRAS.mulDigits_value line 13232
1359. lemma OAI.CommonBasesFPRAS.mulDigits_length line 13239
1360. lemma OAI.CommonBasesFPRAS.mulCost_bound line 13247
1361. lemma OAI.CommonBasesFPRAS.mul_run line 13263
1362. theorem OAI.CommonBasesFPRAS.multiplication_block line 13299
1363. def OAI.CommonBasesFPRAS.coinWord line 13310
1364. lemma OAI.CommonBasesFPRAS.coinWord_length line 13313
1365. lemma OAI.CommonBasesFPRAS.coinWord_ofFn line 13317
1366. def OAI.CommonBasesFPRAS.randomConfig line 13328
1367. def OAI.CommonBasesFPRAS.randomProgram line 13330
1368. theorem OAI.CommonBasesFPRAS.random_bank_block line 13338
1369. lemma OAI.CommonBasesFPRAS.bitResourceParameter_le_target line 13356
1370. lemma OAI.CommonBasesFPRAS.fairBitCount_le_target line 13360
1371. lemma OAI.CommonBasesFPRAS.queryCount_le_target line 13364
1372. theorem OAI.CommonBasesFPRAS.query_experiment_target_scale line 13372
1373. lemma OAI.CommonBasesFPRAS.uniformAverage_bitEmbedding line 13390
1374. def OAI.CommonBasesFPRAS.clockPosition line 13409
1375. lemma OAI.CommonBasesFPRAS.clockPosition_injective line 13411
1376. def OAI.CommonBasesFPRAS.clockWord line 13418
1377. lemma OAI.CommonBasesFPRAS.clockWord_law line 13420
1378. def OAI.CommonBasesFPRAS.clockQueryOutput line 13423
1379. lemma OAI.CommonBasesFPRAS.clockQueryOutput_value line 13426
1380. lemma OAI.CommonBasesFPRAS.clockQueryOutput_law line 13431
1381. theorem OAI.CommonBasesFPRAS.clock_query_experiment line 13440
1382. def OAI.CommonBasesFPRAS.wordOracle line 13471
1383. def OAI.CommonBasesFPRAS.wordGreedy line 13473
1384. def OAI.CommonBasesFPRAS.greedyTime line 13476
1385. def OAI.CommonBasesFPRAS.greedyWork line 13479
1386. def OAI.CommonBasesFPRAS.greedyCalls line 13482
1387. lemma OAI.CommonBasesFPRAS.greedyTime_bound line 13485
1388. lemma OAI.CommonBasesFPRAS.greedyWork_bound line 13489
1389. lemma OAI.CommonBasesFPRAS.greedyCalls_bound line 13493
1390. lemma OAI.CommonBasesFPRAS.wordGreedy_length line 13497
1391. def OAI.CommonBasesFPRAS.greedyRegisters line 13503
1392. lemma OAI.CommonBasesFPRAS.greedyRegisters_update0 line 13505
1393. lemma OAI.CommonBasesFPRAS.greedyRegisters_update1 line 13508
1394. lemma OAI.CommonBasesFPRAS.greedyRegisters_update2 line 13511
1395. lemma OAI.CommonBasesFPRAS.greedyRegisters_update4 line 13514
1396. def OAI.CommonBasesFPRAS.greedyConfig line 13517
1397. def OAI.CommonBasesFPRAS.greedyCopy₁ line 13519
1398. def OAI.CommonBasesFPRAS.greedyCopy₂ line 13520
1399. def OAI.CommonBasesFPRAS.greedyProgram line 13521
1400. lemma OAI.CommonBasesFPRAS.greedy_copy₁ line 13538
1401. lemma OAI.CommonBasesFPRAS.greedy_copy₂ line 13545
1402. lemma OAI.CommonBasesFPRAS.greedyRegisters_copy₁ line 13552
1403. lemma OAI.CommonBasesFPRAS.greedyRegisters_copy₁_out line 13557
1404. lemma OAI.CommonBasesFPRAS.greedyRegisters_copy₂ line 13562
1405. lemma OAI.CommonBasesFPRAS.greedyRegisters_copy₂_out line 13567
1406. lemma OAI.CommonBasesFPRAS.greedy_copy₁_run line 13572
1407. lemma OAI.CommonBasesFPRAS.greedy_copy₂_run line 13584
1408. lemma OAI.CommonBasesFPRAS.greedy_clear line 13596
1409. lemma OAI.CommonBasesFPRAS.greedy_query_run line 13609
1410. lemma OAI.CommonBasesFPRAS.greedy_true_body line 13622
1411. lemma OAI.CommonBasesFPRAS.greedy_false_body line 13644
1412. theorem OAI.CommonBasesFPRAS.greedy_machine_run line 13652
1413. def OAI.CommonBasesFPRAS.wordSet line 13679
1414. lemma OAI.CommonBasesFPRAS.wordSet_zero_succ line 13680
1415. lemma OAI.CommonBasesFPRAS.wordSet_bit line 13684
1416. lemma OAI.CommonBasesFPRAS.wordSet_zero_subset line 13698
1417. lemma OAI.CommonBasesFPRAS.wordSet_ofFn line 13709
1418. lemma OAI.CommonBasesFPRAS.wordSet_empty line 13712
1419. lemma OAI.CommonBasesFPRAS.wordSet_zeros line 13713
1420. theorem OAI.CommonBasesFPRAS.wordGreedy_basis line 13718
1421. lemma OAI.CommonBasesFPRAS.incrementBits_length line 13770
1422. def OAI.CommonBasesFPRAS.popcountBits line 13777
1423. def OAI.CommonBasesFPRAS.popcountTime line 13780
1424. lemma OAI.CommonBasesFPRAS.popcount_value line 13783
1425. lemma OAI.CommonBasesFPRAS.popcountTime_bound line 13788
1426. def OAI.CommonBasesFPRAS.popcountConfig line 13801
1427. def OAI.CommonBasesFPRAS.popcountLabel line 13803
1428. def OAI.CommonBasesFPRAS.popcountProgram line 13804
1429. lemma OAI.CommonBasesFPRAS.popcount_increment line 13809
1430. lemma OAI.CommonBasesFPRAS.greedyRegisters_increment_in line 13816
1431. lemma OAI.CommonBasesFPRAS.greedyRegisters_increment_out line 13820
1432. lemma OAI.CommonBasesFPRAS.popcount_increment_run line 13825
1433. theorem OAI.CommonBasesFPRAS.popcount_run line 13837
1434. lemma OAI.CommonBasesFPRAS.count_ofFn line 13867
1435. lemma OAI.CommonBasesFPRAS.wordSet_card line 13874
1436. lemma OAI.CommonBasesFPRAS.wordGreedy_rank line 13884
1437. def OAI.CommonBasesFPRAS.rankProgram line 13899
1438. def OAI.CommonBasesFPRAS.rankConfig line 13900
1439. def OAI.CommonBasesFPRAS.rankBits line 13902
1440. def OAI.CommonBasesFPRAS.rankTime line 13904
1441. def OAI.CommonBasesFPRAS.rankWork line 13906
1442. lemma OAI.CommonBasesFPRAS.rankTime_bound line 13908
1443. lemma OAI.CommonBasesFPRAS.rankWork_bound line 13915
1444. lemma OAI.CommonBasesFPRAS.rank_run line 13922
1445. theorem OAI.CommonBasesFPRAS.matroid_rank_machine line 13943
1446. def OAI.CommonBasesFPRAS.compareBits line 13968
1447. lemma OAI.CommonBasesFPRAS.compareBits_correct line 13973
1448. lemma OAI.CommonBasesFPRAS.compareBits_lt line 13990
1449. def OAI.CommonBasesFPRAS.compareConfig line 13993
1450. def OAI.CommonBasesFPRAS.compareProgram line 13995
1451. theorem OAI.CommonBasesFPRAS.comparison_run line 14007
1452. theorem OAI.CommonBasesFPRAS.comparison_block line 14047
1453. def OAI.CommonBasesFPRAS.subBorrow line 14054
1454. def OAI.CommonBasesFPRAS.subDigits line 14055
1455. def OAI.CommonBasesFPRAS.subCost line 14062
1456. lemma OAI.CommonBasesFPRAS.subDigits_value line 14069
1457. lemma OAI.CommonBasesFPRAS.subDigits_length_cost line 14092
1458. def OAI.CommonBasesFPRAS.subConfig line 14114
1459. def OAI.CommonBasesFPRAS.subProgram line 14116
1460. lemma OAI.CommonBasesFPRAS.sub_build line 14135
1461. lemma OAI.CommonBasesFPRAS.sub_restore line 14184
1462. theorem OAI.CommonBasesFPRAS.subtraction_block line 14200
1463. lemma OAI.CommonBasesFPRAS.execution_relabel_before_any_halt line 14228
1464. lemma OAI.CommonBasesFPRAS.execution_of_output line 14242
1465. lemma OAI.CommonBasesFPRAS.execution_extend_output line 14248
1466. lemma OAI.CommonBasesFPRAS.workReg_ne05 line 14260
1467. lemma OAI.CommonBasesFPRAS.workReg_ne06 line 14261
1468. lemma OAI.CommonBasesFPRAS.workReg_ne15 line 14262
1469. lemma OAI.CommonBasesFPRAS.workReg_ne16 line 14263
1470. lemma OAI.CommonBasesFPRAS.workReg_ne25 line 14264
1471. lemma OAI.CommonBasesFPRAS.workReg_ne26 line 14265
1472. lemma OAI.CommonBasesFPRAS.workReg_ne35 line 14266
1473. lemma OAI.CommonBasesFPRAS.workReg_ne36 line 14267
1474. lemma OAI.CommonBasesFPRAS.workReg_ne45 line 14268
1475. lemma OAI.CommonBasesFPRAS.workReg_ne46 line 14269
1476. lemma OAI.CommonBasesFPRAS.workReg_ne50 line 14270
1477. lemma OAI.CommonBasesFPRAS.workReg_ne51 line 14271
1478. lemma OAI.CommonBasesFPRAS.workReg_ne52 line 14272
1479. lemma OAI.CommonBasesFPRAS.workReg_ne53 line 14273
1480. lemma OAI.CommonBasesFPRAS.workReg_ne54 line 14274
1481. lemma OAI.CommonBasesFPRAS.workReg_ne56 line 14275
1482. lemma OAI.CommonBasesFPRAS.workReg_ne60 line 14276
1483. lemma OAI.CommonBasesFPRAS.workReg_ne61 line 14277
1484. lemma OAI.CommonBasesFPRAS.workReg_ne62 line 14278
1485. lemma OAI.CommonBasesFPRAS.workReg_ne63 line 14279
1486. lemma OAI.CommonBasesFPRAS.workReg_ne64 line 14280
1487. lemma OAI.CommonBasesFPRAS.workReg_ne65 line 14281
1488. def OAI.CommonBasesFPRAS.divRegisters line 14282
1489. lemma OAI.CommonBasesFPRAS.divRegisters_copyR_in line 14285
1490. lemma OAI.CommonBasesFPRAS.divRegisters_copyR_out line 14290
1491. lemma OAI.CommonBasesFPRAS.divRegisters_copyD_in line 14295
1492. lemma OAI.CommonBasesFPRAS.divRegisters_copyD_out line 14300
1493. lemma OAI.CommonBasesFPRAS.divRegisters_compare_in line 14305
1494. lemma OAI.CommonBasesFPRAS.divRegisters_compare_out line 14310
1495. lemma OAI.CommonBasesFPRAS.divRegisters_copyS_in line 14315
1496. lemma OAI.CommonBasesFPRAS.divRegisters_copyS_out line 14320
1497. lemma OAI.CommonBasesFPRAS.divRegisters_sub_in line 14325
1498. lemma OAI.CommonBasesFPRAS.divRegisters_sub_out line 14330
1499. lemma OAI.CommonBasesFPRAS.divRegisters_update0 line 14335
1500. lemma OAI.CommonBasesFPRAS.divRegisters_update2 line 14340
1501. lemma OAI.CommonBasesFPRAS.divRegisters_update3 line 14345
1502. def OAI.CommonBasesFPRAS.divCopies line 14350
1503. def OAI.CommonBasesFPRAS.divCheck line 14351
1504. def OAI.CommonBasesFPRAS.divSubtract line 14352
1505. def OAI.CommonBasesFPRAS.divCopiesConfig line 14353
1506. def OAI.CommonBasesFPRAS.divCheckConfig line 14354
1507. def OAI.CommonBasesFPRAS.divSubtractConfig line 14355
1508. lemma OAI.CommonBasesFPRAS.divCopies_exit line 14356
1509. lemma OAI.CommonBasesFPRAS.divSubtract_exit line 14358
1510. lemma OAI.CommonBasesFPRAS.divCopies_run line 14360
1511. def OAI.CommonBasesFPRAS.divCheckCost line 14381
1512. lemma OAI.CommonBasesFPRAS.divCheck_run line 14382
1513. def OAI.CommonBasesFPRAS.divSubtractCost line 14403
1514. lemma OAI.CommonBasesFPRAS.divSubtract_run line 14404
1515. def OAI.CommonBasesFPRAS.divisionCheckLabel line 14427
1516. def OAI.CommonBasesFPRAS.divisionSubLabel line 14429
1517. def OAI.CommonBasesFPRAS.divisionProgram line 14430
1518. def OAI.CommonBasesFPRAS.divisionConfig line 14441
1519. lemma OAI.CommonBasesFPRAS.division_check_table line 14443
1520. lemma OAI.CommonBasesFPRAS.division_sub_table line 14456
1521. lemma OAI.CommonBasesFPRAS.division_check_run line 14465
1522. lemma OAI.CommonBasesFPRAS.division_sub_run line 14475
1523. def OAI.CommonBasesFPRAS.divisionRemainder line 14487
1524. def OAI.CommonBasesFPRAS.divisionDigit line 14489
1525. def OAI.CommonBasesFPRAS.divisionDigitCost line 14490
1526. lemma OAI.CommonBasesFPRAS.division_digit_run line 14492
1527. def OAI.CommonBasesFPRAS.divisionWords line 14517
1528. def OAI.CommonBasesFPRAS.divisionCost line 14520
1529. theorem OAI.CommonBasesFPRAS.division_machine_run line 14524
1530. lemma OAI.CommonBasesFPRAS.binaryValue_append line 14536
1531. def OAI.CommonBasesFPRAS.streamValue line 14544
1532. lemma OAI.CommonBasesFPRAS.streamValue_eq line 14547
1533. lemma OAI.CommonBasesFPRAS.division_step_math line 14555
1534. lemma OAI.CommonBasesFPRAS.divisionWords_invariant line 14568
1535. theorem OAI.CommonBasesFPRAS.divisionWords_correct line 14586
1536. lemma OAI.CommonBasesFPRAS.subDigits_length line 14595
1537. lemma OAI.CommonBasesFPRAS.divisionRemainder_length line 14606
1538. lemma OAI.CommonBasesFPRAS.divCheckCost_bound line 14612
1539. lemma OAI.CommonBasesFPRAS.divSubtractCost_bound line 14619
1540. lemma OAI.CommonBasesFPRAS.divisionDigitCost_bound line 14627
1541. lemma OAI.CommonBasesFPRAS.divisionCost_bound line 14633
1542. theorem OAI.CommonBasesFPRAS.division_block line 14648
1543. def OAI.CommonBasesFPRAS.Instruction.renameRegisters line 14667
1544. def OAI.CommonBasesFPRAS.renameProgram line 14673
1545. def OAI.CommonBasesFPRAS.renameConfig line 14675
1546. lemma OAI.CommonBasesFPRAS.rename_update line 14677
1547. lemma OAI.CommonBasesFPRAS.machineStep_rename line 14684
1548. theorem OAI.CommonBasesFPRAS.execution_rename_before_halt line 14703
1549. def OAI.CommonBasesFPRAS.bitFrame line 14718
1550. lemma OAI.CommonBasesFPRAS.bitFrame_length line 14721
1551. lemma OAI.CommonBasesFPRAS.bitFrame_append line 14725
1552. lemma OAI.CommonBasesFPRAS.bitFrame_reverse_cons line 14730
1553. def OAI.CommonBasesFPRAS.framePackProgram line 14735
1554. def OAI.CommonBasesFPRAS.frameConfig line 14743
1555. lemma OAI.CommonBasesFPRAS.frame_pack_scan line 14745
1556. theorem OAI.CommonBasesFPRAS.frame_pack_block line 14761
1557. def OAI.CommonBasesFPRAS.frameUnpackProgram line 14774
1558. theorem OAI.CommonBasesFPRAS.frame_unpack_block line 14782
1559. theorem OAI.CommonBasesFPRAS.frame_unpack_packed line 14800
1560. abbrev OAI.CommonBasesFPRAS.MachineCode.Registers line 14810
1561. structure OAI.CommonBasesFPRAS.MachineCode.Block line 14811
1562. def OAI.CommonBasesFPRAS.MachineCode.state line 14816
1563. def OAI.CommonBasesFPRAS.MachineCode.Runs line 14819
1564. def OAI.CommonBasesFPRAS.MachineCode.skip line 14824
1565. lemma OAI.CommonBasesFPRAS.MachineCode.runs_skip line 14825
1566. def OAI.CommonBasesFPRAS.MachineCode.seq line 14830
1567. lemma OAI.CommonBasesFPRAS.MachineCode.runs_seq line 14838
1568. def OAI.CommonBasesFPRAS.MachineCode.push line 14857
1569. lemma OAI.CommonBasesFPRAS.MachineCode.runs_push line 14861
1570. inductive OAI.CommonBasesFPRAS.MachineCode.Test line 14867
1571. def OAI.CommonBasesFPRAS.MachineCode.Test.instruction line 14872
1572. def OAI.CommonBasesFPRAS.MachineCode.Test.result line 14878
1573. def OAI.CommonBasesFPRAS.MachineCode.Test.queries line 14888
1574. def OAI.CommonBasesFPRAS.MachineCode.Test.work line 14892
1575. lemma OAI.CommonBasesFPRAS.MachineCode.test_step line 14897
1576. def OAI.CommonBasesFPRAS.MachineCode.noLabel line 14924
1577. def OAI.CommonBasesFPRAS.MachineCode.yesLabel line 14926
1578. lemma OAI.CommonBasesFPRAS.MachineCode.noLabel_exit line 14928
1579. lemma OAI.CommonBasesFPRAS.MachineCode.yesLabel_exit line 14930
1580. def OAI.CommonBasesFPRAS.MachineCode.fork line 14933
1581. lemma OAI.CommonBasesFPRAS.MachineCode.fork_head line 14943
1582. lemma OAI.CommonBasesFPRAS.MachineCode.fork_no line 14946
1583. lemma OAI.CommonBasesFPRAS.MachineCode.fork_yes line 14951
1584. lemma OAI.CommonBasesFPRAS.MachineCode.fork_run_no line 14957
1585. lemma OAI.CommonBasesFPRAS.MachineCode.fork_run_yes line 14980
1586. def OAI.CommonBasesFPRAS.loopLabel line 15008
1587. def OAI.CommonBasesFPRAS.repeatProgram line 15010
1588. lemma OAI.CommonBasesFPRAS.repeatProgram_body line 15014
1589. lemma OAI.CommonBasesFPRAS.loopLabel_last line 15018
1590. def OAI.CommonBasesFPRAS.loopConfig line 15019
1591. lemma OAI.CommonBasesFPRAS.repeatProgram_pop line 15021
1592. lemma OAI.CommonBasesFPRAS.repeatProgram_empty line 15026
1593. def OAI.CommonBasesFPRAS.loopState line 15031
1594. def OAI.CommonBasesFPRAS.loopSum line 15034
1595. theorem OAI.CommonBasesFPRAS.repeat_block line 15038
1596. lemma OAI.CommonBasesFPRAS.loopSum_le line 15067
1597. def OAI.CommonBasesFPRAS.reverseProgram line 15076
1598. def OAI.CommonBasesFPRAS.reverseConfig line 15082
1599. theorem OAI.CommonBasesFPRAS.reverse_block line 15084
1600. def OAI.CommonBasesFPRAS.clearProgram line 15098
1601. def OAI.CommonBasesFPRAS.clearConfig line 15099
1602. theorem OAI.CommonBasesFPRAS.clear_block line 15101
1603. def OAI.CommonBasesFPRAS.moveProgram line 15113
1604. def OAI.CommonBasesFPRAS.moveConfig line 15114
1605. lemma OAI.CommonBasesFPRAS.triple_pair_ab line 15116
1606. lemma OAI.CommonBasesFPRAS.triple_pair_bd line 15120
1607. theorem OAI.CommonBasesFPRAS.move_block line 15124
1608. def OAI.CommonBasesFPRAS.MachineCode.reverse line 15151
1609. def OAI.CommonBasesFPRAS.MachineCode.clear line 15153
1610. def OAI.CommonBasesFPRAS.MachineCode.move line 15155
1611. def OAI.CommonBasesFPRAS.MachineCode.pack line 15157
1612. def OAI.CommonBasesFPRAS.MachineCode.unpack line 15159
1613. lemma OAI.CommonBasesFPRAS.MachineCode.runs_reverse line 15169
1614. lemma OAI.CommonBasesFPRAS.MachineCode.runs_clear line 15176
1615. lemma OAI.CommonBasesFPRAS.MachineCode.runs_move line 15183
1616. lemma OAI.CommonBasesFPRAS.MachineCode.runs_pack line 15190
1617. lemma OAI.CommonBasesFPRAS.MachineCode.runs_unpack line 15197
1618. lemma OAI.CommonBasesFPRAS.MachineCode.runs_unpack_packed line 15212
1619. def OAI.CommonBasesFPRAS.MachineCode.repeatBlock line 15219
1620. abbrev OAI.CommonBasesFPRAS.MachineCode.Word line 15224
1621. def OAI.CommonBasesFPRAS.MachineCode.regs line 15226
1622. lemma OAI.CommonBasesFPRAS.MachineCode.regs_zero line 15228
1623. lemma OAI.CommonBasesFPRAS.MachineCode.regs_one line 15229
1624. lemma OAI.CommonBasesFPRAS.MachineCode.regs_two line 15230
1625. lemma OAI.CommonBasesFPRAS.MachineCode.regs_eight line 15231
1626. lemma OAI.CommonBasesFPRAS.MachineCode.update_regs_zero line 15232
1627. lemma OAI.CommonBasesFPRAS.MachineCode.update_regs_one line 15234
1628. lemma OAI.CommonBasesFPRAS.MachineCode.update_regs_two line 15236
1629. lemma OAI.CommonBasesFPRAS.MachineCode.update_regs_eight line 15238
1630. def OAI.CommonBasesFPRAS.MachineCode.pair line 15241
1631. lemma OAI.CommonBasesFPRAS.MachineCode.pair_length line 15242
1632. def OAI.CommonBasesFPRAS.MachineCode.Computes line 15245
1633. def OAI.CommonBasesFPRAS.MachineCode.Bounded line 15249
1634. lemma OAI.CommonBasesFPRAS.MachineCode.computes_skip line 15252
1635. lemma OAI.CommonBasesFPRAS.MachineCode.computes_seq line 15254
1636. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_seq line 15259
1637. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_mono line 15265
1638. def OAI.CommonBasesFPRAS.MachineCode.copy line 15270
1639. lemma OAI.CommonBasesFPRAS.MachineCode.runs_copy line 15271
1640. def OAI.CommonBasesFPRAS.MachineCode.duplicate line 15280
1641. lemma OAI.CommonBasesFPRAS.MachineCode.computes_duplicate line 15281
1642. lemma OAI.CommonBasesFPRAS.MachineCode.split_pair line 15291
1643. lemma OAI.CommonBasesFPRAS.MachineCode.make_pair line 15296
1644. lemma OAI.CommonBasesFPRAS.MachineCode.move_one_zero line 15301
1645. def OAI.CommonBasesFPRAS.MachineCode.first line 15307
1646. def OAI.CommonBasesFPRAS.MachineCode.second line 15308
1647. lemma OAI.CommonBasesFPRAS.MachineCode.computes_first line 15309
1648. lemma OAI.CommonBasesFPRAS.MachineCode.computes_second line 15319
1649. lemma OAI.CommonBasesFPRAS.MachineCode.save_zero line 15328
1650. lemma OAI.CommonBasesFPRAS.MachineCode.restore_one line 15333
1651. lemma OAI.CommonBasesFPRAS.MachineCode.pack_zero_one line 15338
1652. def OAI.CommonBasesFPRAS.MachineCode.swap line 15344
1653. lemma OAI.CommonBasesFPRAS.MachineCode.computes_swap line 15345
1654. def OAI.CommonBasesFPRAS.MachineCode.left line 15358
1655. lemma OAI.CommonBasesFPRAS.MachineCode.computes_left line 15361
1656. def OAI.CommonBasesFPRAS.MachineCode.right line 15383
1657. lemma OAI.CommonBasesFPRAS.MachineCode.computes_right line 15384
1658. def OAI.CommonBasesFPRAS.MachineCode.parallel line 15391
1659. def OAI.CommonBasesFPRAS.MachineCode.fanout line 15392
1660. def OAI.CommonBasesFPRAS.MachineCode.stripZeros line 15394
1661. def OAI.CommonBasesFPRAS.MachineCode.stripCost line 15398
1662. lemma OAI.CommonBasesFPRAS.MachineCode.strip_length line 15402
1663. lemma OAI.CommonBasesFPRAS.MachineCode.strip_cost_le line 15406
1664. lemma OAI.CommonBasesFPRAS.MachineCode.strip_append line 15410
1665. def OAI.CommonBasesFPRAS.MachineCode.normalWord line 15417
1666. lemma OAI.CommonBasesFPRAS.MachineCode.normal_length line 15418
1667. lemma OAI.CommonBasesFPRAS.MachineCode.normalWord_cons line 15420
1668. lemma OAI.CommonBasesFPRAS.MachineCode.binaryValue_bits line 15427
1669. lemma OAI.CommonBasesFPRAS.MachineCode.normalWord_eq_bits line 15434
1670. lemma OAI.CommonBasesFPRAS.MachineCode.normalWord_value line 15451
1671. lemma OAI.CommonBasesFPRAS.MachineCode.normalWord_bits line 15453
1672. def OAI.CommonBasesFPRAS.MachineCode.stripCode line 15456
1673. lemma OAI.CommonBasesFPRAS.MachineCode.runs_strip line 15463
1674. def OAI.CommonBasesFPRAS.MachineCode.normalCode line 15481
1675. def OAI.CommonBasesFPRAS.MachineCode.normalCost line 15482
1676. lemma OAI.CommonBasesFPRAS.MachineCode.normalCost_le line 15483
1677. lemma OAI.CommonBasesFPRAS.MachineCode.computes_normalCode line 15489
1678. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_normalCode line 15500
1679. def OAI.CommonBasesFPRAS.MachineCode.addBlock line 15506
1680. def OAI.CommonBasesFPRAS.MachineCode.addTime line 15507
1681. lemma OAI.CommonBasesFPRAS.MachineCode.runs_add line 15508
1682. lemma OAI.CommonBasesFPRAS.MachineCode.addTime_le line 15517
1683. def OAI.CommonBasesFPRAS.MachineCode.addCode line 15522
1684. lemma OAI.CommonBasesFPRAS.MachineCode.computes_add line 15523
1685. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_add line 15537
1686. def OAI.CommonBasesFPRAS.MachineCode.mulBlock line 15544
1687. lemma OAI.CommonBasesFPRAS.MachineCode.mulRegisters_regs line 15545
1688. lemma OAI.CommonBasesFPRAS.MachineCode.runs_mul line 15547
1689. lemma OAI.CommonBasesFPRAS.MachineCode.clear_zero line 15556
1690. lemma OAI.CommonBasesFPRAS.MachineCode.move_two_zero line 15559
1691. def OAI.CommonBasesFPRAS.MachineCode.mulCode line 15564
1692. def OAI.CommonBasesFPRAS.MachineCode.mulTime line 15565
1693. lemma OAI.CommonBasesFPRAS.MachineCode.computes_mul line 15567
1694. lemma OAI.CommonBasesFPRAS.MachineCode.mulTime_le line 15585
1695. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_mul line 15592
1696. lemma OAI.CommonBasesFPRAS.MachineCode.computes_parallel line 15596
1697. lemma OAI.CommonBasesFPRAS.MachineCode.computes_fanout line 15603
1698. def OAI.CommonBasesFPRAS.MachineCode.prependCode line 15611
1699. lemma OAI.CommonBasesFPRAS.MachineCode.computes_prepend line 15614
1700. def OAI.CommonBasesFPRAS.MachineCode.constCode line 15625
1701. lemma OAI.CommonBasesFPRAS.MachineCode.computes_const line 15626
1702. def OAI.CommonBasesFPRAS.MachineCode.selectCode line 15633
1703. lemma OAI.CommonBasesFPRAS.MachineCode.computes_select line 15634
1704. def OAI.CommonBasesFPRAS.MachineCode.queryCode line 15656
1705. lemma OAI.CommonBasesFPRAS.MachineCode.computes_query line 15657
1706. def OAI.CommonBasesFPRAS.MachineCode.quadRegs line 15675
1707. lemma OAI.CommonBasesFPRAS.MachineCode.quadRegs_zero line 15676
1708. lemma OAI.CommonBasesFPRAS.MachineCode.quadRegs_one line 15677
1709. lemma OAI.CommonBasesFPRAS.MachineCode.quadRegs_two line 15678
1710. lemma OAI.CommonBasesFPRAS.MachineCode.quadRegs_three line 15679
1711. lemma OAI.CommonBasesFPRAS.MachineCode.quadRegs_nil line 15680
1712. lemma OAI.CommonBasesFPRAS.MachineCode.update_quad_zero line 15682
1713. lemma OAI.CommonBasesFPRAS.MachineCode.update_quad_one line 15684
1714. lemma OAI.CommonBasesFPRAS.MachineCode.update_quad_two line 15686
1715. lemma OAI.CommonBasesFPRAS.MachineCode.update_quad_three line 15688
1716. lemma OAI.CommonBasesFPRAS.MachineCode.divRegisters_quad line 15690
1717. def OAI.CommonBasesFPRAS.MachineCode.divBlock line 15693
1718. lemma OAI.CommonBasesFPRAS.MachineCode.runs_div line 15694
1719. lemma OAI.CommonBasesFPRAS.MachineCode.div_prepare line 15704
1720. lemma OAI.CommonBasesFPRAS.MachineCode.div_finish line 15717
1721. def OAI.CommonBasesFPRAS.MachineCode.rawDivCode line 15735
1722. def OAI.CommonBasesFPRAS.MachineCode.divResult line 15738
1723. def OAI.CommonBasesFPRAS.MachineCode.rawDivTime line 15739
1724. lemma OAI.CommonBasesFPRAS.MachineCode.computes_rawDiv line 15741
1725. lemma OAI.CommonBasesFPRAS.MachineCode.divisionWords_length line 15754
1726. lemma OAI.CommonBasesFPRAS.MachineCode.divResult_length line 15764
1727. lemma OAI.CommonBasesFPRAS.MachineCode.rawDivTime_le line 15767
1728. def OAI.CommonBasesFPRAS.MachineCode.divCode line 15774
1729. def OAI.CommonBasesFPRAS.MachineCode.normalizedResult line 15775
1730. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_div line 15776
1731. lemma OAI.CommonBasesFPRAS.MachineCode.normalizedResult_pos line 15790
1732. def OAI.CommonBasesFPRAS.MachineCode.cmpLabel line 15795
1733. def OAI.CommonBasesFPRAS.MachineCode.cmpBlock line 15796
1734. lemma OAI.CommonBasesFPRAS.MachineCode.cmpBlock_body line 15803
1735. lemma OAI.CommonBasesFPRAS.MachineCode.runs_cmp line 15811
1736. def OAI.CommonBasesFPRAS.MachineCode.cmpCode line 15826
1737. lemma OAI.CommonBasesFPRAS.MachineCode.computes_cmp line 15827
1738. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_cmp line 15836
1739. def OAI.CommonBasesFPRAS.MachineCode.loopAccum line 15840
1740. theorem OAI.CommonBasesFPRAS.MachineCode.runs_repeat line 15844
1741. lemma OAI.CommonBasesFPRAS.MachineCode.loopAccum_le line 15887
1742. lemma OAI.CommonBasesFPRAS.MachineCode.save_one line 15896
1743. def OAI.CommonBasesFPRAS.MachineCode.iterationBody line 15902
1744. lemma OAI.CommonBasesFPRAS.MachineCode.iteration_body line 15903
1745. def OAI.CommonBasesFPRAS.MachineCode.iterateCode line 15913
1746. lemma OAI.CommonBasesFPRAS.MachineCode.computes_iterate line 15914
1747. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_iterate line 15932
1748. def OAI.CommonBasesFPRAS.MachineCode.words line 15947
1749. lemma OAI.CommonBasesFPRAS.MachineCode.words_length line 15950
1750. def OAI.CommonBasesFPRAS.MachineCode.foldWords line 15955
1751. def OAI.CommonBasesFPRAS.MachineCode.foldCharge line 15958
1752. lemma OAI.CommonBasesFPRAS.MachineCode.runs_repeat_cons line 15962
1753. lemma OAI.CommonBasesFPRAS.MachineCode.unpack_one_two line 15986
1754. lemma OAI.CommonBasesFPRAS.MachineCode.pack_two_zero line 15991
1755. lemma OAI.CommonBasesFPRAS.MachineCode.save_one_with_two line 15996
1756. def OAI.CommonBasesFPRAS.MachineCode.listBody line 16002
1757. lemma OAI.CommonBasesFPRAS.MachineCode.list_body line 16004
1758. lemma OAI.CommonBasesFPRAS.MachineCode.list_loop line 16016
1759. def OAI.CommonBasesFPRAS.MachineCode.foldCode line 16039
1760. lemma OAI.CommonBasesFPRAS.MachineCode.computes_fold line 16040
1761. def OAI.CommonBasesFPRAS.MachineCode.reverseCode line 16055
1762. lemma OAI.CommonBasesFPRAS.MachineCode.computes_reverse line 16056
1763. def OAI.CommonBasesFPRAS.MachineCode.boolListBlock line 16066
1764. lemma OAI.CommonBasesFPRAS.MachineCode.boolList_push line 16078
1765. lemma OAI.CommonBasesFPRAS.MachineCode.runs_boolList line 16079
1766. def OAI.CommonBasesFPRAS.MachineCode.boolListCode line 16094
1767. lemma OAI.CommonBasesFPRAS.MachineCode.computes_boolList line 16095
1768. def OAI.CommonBasesFPRAS.MachineCode.consWordCode line 16105
1769. lemma OAI.CommonBasesFPRAS.MachineCode.computes_consWord line 16107
1770. def OAI.CommonBasesFPRAS.MachineCode.consListCode line 16115
1771. lemma OAI.CommonBasesFPRAS.MachineCode.computes_consList line 16116
1772. def OAI.CommonBasesFPRAS.MachineCode.appendCode line 16121
1773. lemma OAI.CommonBasesFPRAS.MachineCode.computes_append line 16122
1774. def OAI.CommonBasesFPRAS.MachineCode.subBlock line 16131
1775. def OAI.CommonBasesFPRAS.MachineCode.subTime line 16132
1776. lemma OAI.CommonBasesFPRAS.MachineCode.runs_sub line 16133
1777. def OAI.CommonBasesFPRAS.MachineCode.subCode line 16145
1778. lemma OAI.CommonBasesFPRAS.MachineCode.computes_sub line 16146
1779. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_sub line 16164
1780. def OAI.CommonBasesFPRAS.MachineCode.rankPrep line 16171
1781. lemma OAI.CommonBasesFPRAS.MachineCode.runs_rankPrep line 16181
1782. lemma OAI.CommonBasesFPRAS.MachineCode.update_regs_three_empty line 16198
1783. lemma OAI.CommonBasesFPRAS.MachineCode.greedyRegisters_regs line 16200
1784. def OAI.CommonBasesFPRAS.MachineCode.readyRank line 16203
1785. def OAI.CommonBasesFPRAS.MachineCode.rankCode line 16204
1786. def OAI.CommonBasesFPRAS.MachineCode.rankWord line 16205
1787. lemma OAI.CommonBasesFPRAS.MachineCode.popcountBits_length line 16207
1788. lemma OAI.CommonBasesFPRAS.MachineCode.rankBits_length line 16219
1789. lemma OAI.CommonBasesFPRAS.MachineCode.computes_rank line 16223
1790. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_rank line 16246
1791. lemma OAI.CommonBasesFPRAS.MachineCode.rankWord_correct line 16257
1792. lemma OAI.CommonBasesFPRAS.MachineCode.rankWord_eq_rankOracle line 16267
1793. inductive OAI.CommonBasesFPRAS.MachineCode.DataType line 16275
1794. def OAI.CommonBasesFPRAS.MachineCode.Value line 16280
1795. def OAI.CommonBasesFPRAS.MachineCode.encode line 16288
1796. def OAI.CommonBasesFPRAS.MachineCode.width line 16296
1797. inductive OAI.CommonBasesFPRAS.MachineCode.Expression line 16298
1798. def OAI.CommonBasesFPRAS.MachineCode.compile line 16322
1799. def OAI.CommonBasesFPRAS.MachineCode.evalFold line 16346
1800. def OAI.CommonBasesFPRAS.MachineCode.evaluate line 16354
1801. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_fanout line 16391
1802. lemma OAI.CommonBasesFPRAS.MachineCode.bounded_select line 16397
1803. lemma OAI.CommonBasesFPRAS.MachineCode.computes_bounded line 16403
1804. lemma OAI.CommonBasesFPRAS.MachineCode.evalFold_loop line 16407
1805. lemma OAI.CommonBasesFPRAS.MachineCode.evalFold_bounded line 16447
1806. theorem OAI.CommonBasesFPRAS.MachineCode.compile_correct line 16459
1807. def OAI.CommonBasesFPRAS.MachineCode.foldValue line 16621
1808. def OAI.CommonBasesFPRAS.MachineCode.run line 16625
1809. lemma OAI.CommonBasesFPRAS.MachineCode.evalFold_forget line 16649
1810. lemma OAI.CommonBasesFPRAS.MachineCode.evaluate_forget line 16663
1811. lemma OAI.CommonBasesFPRAS.MachineCode.compile_run line 16692
1812. def OAI.CommonBasesFPRAS.MachineCode.Expression.onLeft line 16707
1813. def OAI.CommonBasesFPRAS.MachineCode.Expression.onRight line 16709
1814. def OAI.CommonBasesFPRAS.MachineCode.Expression.swap line 16711
1815. def OAI.CommonBasesFPRAS.MachineCode.Expression.letIn line 16712
1816. def OAI.CommonBasesFPRAS.MachineCode.Expression.applyIf line 16714
1817. def OAI.CommonBasesFPRAS.MachineCode.Expression.boolNot line 16717
1818. def OAI.CommonBasesFPRAS.MachineCode.Expression.boolAnd line 16718
1819. def OAI.CommonBasesFPRAS.MachineCode.Expression.natEqZero line 16719
1820. def OAI.CommonBasesFPRAS.MachineCode.Expression.natSub line 16720
1821. def OAI.CommonBasesFPRAS.MachineCode.Expression.natDivRem line 16721
1822. def OAI.CommonBasesFPRAS.MachineCode.Expression.natDiv line 16723
1823. def OAI.CommonBasesFPRAS.MachineCode.Expression.natMod line 16724
1824. def OAI.CommonBasesFPRAS.MachineCode.Expression.listReverse line 16726
1825. def OAI.CommonBasesFPRAS.MachineCode.Expression.mapStep line 16728
1826. def OAI.CommonBasesFPRAS.MachineCode.Expression.mapWith line 16732
1827. def OAI.CommonBasesFPRAS.MachineCode.Expression.listLength line 16735
1828. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordLength line 16737
1829. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordRepeatStep line 16739
1830. def OAI.CommonBasesFPRAS.MachineCode.Expression.unary line 16743
1831. lemma OAI.CommonBasesFPRAS.MachineCode.foldValue_eq_foldl line 16748
1832. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_boolNot line 16757
1833. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_boolAnd line 16759
1834. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natEqZero line 16761
1835. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natSub line 16763
1836. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natDivRem line 16768
1837. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natDiv line 16771
1838. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natMod line 16774
1839. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_listReverse line 16777
1840. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_mapStep line 16783
1841. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_mapWith line 16788
1842. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_listLength line 16799
1843. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordLength line 16808
1844. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordRepeatStep line 16810
1845. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.unary_value line 16813
1846. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_unary line 16832
1847. lemma OAI.CommonBasesFPRAS.MachineCode.width_pair line 16839
1848. lemma OAI.CommonBasesFPRAS.MachineCode.width_nil line 16841
1849. lemma OAI.CommonBasesFPRAS.MachineCode.width_cons line 16842
1850. lemma OAI.CommonBasesFPRAS.MachineCode.list_length_le_width line 16845
1851. def OAI.CommonBasesFPRAS.MachineCode.FoldSafe line 16851
1852. def OAI.CommonBasesFPRAS.MachineCode.Safe line 16855
1853. lemma OAI.CommonBasesFPRAS.MachineCode.safe_input line 16865
1854. lemma OAI.CommonBasesFPRAS.MachineCode.safe_output line 16868
1855. def OAI.CommonBasesFPRAS.MachineCode.chargeBound line 16873
1856. lemma OAI.CommonBasesFPRAS.MachineCode.evalFold_charge line 16880
1857. lemma OAI.CommonBasesFPRAS.MachineCode.charge_primitive line 16909
1858. lemma OAI.CommonBasesFPRAS.MachineCode.evaluate_charge line 16911
1859. def OAI.CommonBasesFPRAS.MachineCode.chargeDegree line 17042
1860. def OAI.CommonBasesFPRAS.MachineCode.chargeCoefficient line 17049
1861. lemma OAI.CommonBasesFPRAS.MachineCode.monomial_add_bound line 17056
1862. lemma OAI.CommonBasesFPRAS.MachineCode.monomial_fold_bound line 17067
1863. lemma OAI.CommonBasesFPRAS.MachineCode.chargeBound_polynomial line 17079
1864. lemma OAI.CommonBasesFPRAS.MachineCode.evaluate_polynomial line 17088
1865. lemma OAI.CommonBasesFPRAS.MachineCode.foldSafe_mono line 17094
1866. lemma OAI.CommonBasesFPRAS.MachineCode.safe_mono line 17100
1867. lemma OAI.CommonBasesFPRAS.MachineCode.safe_compose line 17119
1868. lemma OAI.CommonBasesFPRAS.MachineCode.safe_both line 17131
1869. lemma OAI.CommonBasesFPRAS.MachineCode.foldSafe_invariant line 17153
1870. lemma OAI.CommonBasesFPRAS.MachineCode.foldValue_invariant line 17162
1871. lemma OAI.CommonBasesFPRAS.MachineCode.safe_fold_invariant line 17175
1872. inductive OAI.CommonBasesFPRAS.MachineCode.SizePolynomial line 17185
1873. def OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.eval line 17191
1874. def OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.degree line 17196
1875. def OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.coefficient line 17200
1876. lemma OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.monotone line 17205
1877. lemma OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.bound line 17212
1878. def OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.subst line 17229
1879. lemma OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.eval_subst line 17234
1880. def OAI.CommonBasesFPRAS.MachineCode.Controlled line 17238
1881. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_input line 17240
1882. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_compose line 17246
1883. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_both line 17258
1884. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_branch line 17266
1885. lemma OAI.CommonBasesFPRAS.MachineCode.width_nat line 17288
1886. lemma OAI.CommonBasesFPRAS.MachineCode.width_word line 17289
1887. lemma OAI.CommonBasesFPRAS.MachineCode.width_bool line 17290
1888. lemma OAI.CommonBasesFPRAS.MachineCode.width_unit line 17291
1889. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_mono line 17292
1890. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_le_value line 17294
1891. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_add line 17297
1892. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_mul line 17306
1893. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_binaryValue line 17313
1894. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_bool line 17316
1895. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_append line 17322
1896. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_reverse line 17327
1897. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_member line 17332
1898. def OAI.CommonBasesFPRAS.MachineCode.Atomic line 17342
1899. def OAI.CommonBasesFPRAS.MachineCode.constantWidth line 17346
1900. lemma OAI.CommonBasesFPRAS.MachineCode.safe_atomic line 17349
1901. lemma OAI.CommonBasesFPRAS.MachineCode.atomic_width line 17353
1902. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_atomic line 17436
1903. lemma OAI.CommonBasesFPRAS.MachineCode.foldSafe_prefix line 17442
1904. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_fold line 17457
1905. lemma OAI.CommonBasesFPRAS.MachineCode.mod_double_lt line 17492
1906. lemma OAI.CommonBasesFPRAS.MachineCode.mod_size_lt line 17498
1907. def OAI.CommonBasesFPRAS.MachineCode.gcdStep line 17509
1908. def OAI.CommonBasesFPRAS.MachineCode.gcdSteps line 17510
1909. lemma OAI.CommonBasesFPRAS.MachineCode.gcdSteps_zero line 17513
1910. lemma OAI.CommonBasesFPRAS.MachineCode.gcdSteps_done line 17517
1911. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.NN line 17535
1912. def OAI.CommonBasesFPRAS.MachineCode.Expression.sortPair line 17537
1913. def OAI.CommonBasesFPRAS.MachineCode.Expression.gcdStepCode line 17538
1914. def OAI.CommonBasesFPRAS.MachineCode.Expression.gcdCode line 17541
1915. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_sortPair line 17545
1916. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_gcdStepCode line 17549
1917. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.fold_gcdStepCode line 17553
1918. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_gcdCode line 17563
1919. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_onLeft line 17597
1920. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_onRight line 17599
1921. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_swap line 17601
1922. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_letIn line 17602
1923. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_applyIf line 17604
1924. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_boolNot line 17607
1925. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_boolAnd line 17608
1926. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_natEqZero line 17609
1927. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_natSub line 17610
1928. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_natDivRem line 17611
1929. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_natDiv line 17612
1930. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_natMod line 17613
1931. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_listReverse line 17614
1932. lemma OAI.CommonBasesFPRAS.MachineCode.foldl_succ line 17628
1933. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_listLength line 17632
1934. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordLength line 17650
1935. lemma OAI.CommonBasesFPRAS.MachineCode.gcdSteps_max line 17652
1936. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_gcdStep line 17661
1937. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_gcd line 17662
1938. def OAI.CommonBasesFPRAS.MachineCode.PolySafe line 17689
1939. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_of_controlled line 17692
1940. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_mono line 17700
1941. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_compose line 17704
1942. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_both line 17716
1943. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_fold line 17725
1944. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_controlled line 17744
1945. lemma OAI.CommonBasesFPRAS.MachineCode.run_mapStep_partial line 17749
1946. lemma OAI.CommonBasesFPRAS.MachineCode.fold_mapStep_bound line 17754
1947. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_mapStep line 17773
1948. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_mapFold line 17775
1949. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_mapWith line 17813
1950. def OAI.CommonBasesFPRAS.MachineCode.rationalPair line 17824
1951. def OAI.CommonBasesFPRAS.MachineCode.normalizePair line 17825
1952. lemma OAI.CommonBasesFPRAS.MachineCode.rationalPair_div line 17827
1953. lemma OAI.CommonBasesFPRAS.MachineCode.rationalPair_value line 17833
1954. lemma OAI.CommonBasesFPRAS.MachineCode.rationalPair_den line 17842
1955. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_applyIf line 17845
1956. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_letIn line 17849
1957. def OAI.CommonBasesFPRAS.MachineCode.Expression.normalizeRat line 17854
1958. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratCross line 17860
1959. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratAdd line 17863
1960. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratMul line 17865
1961. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratDiv line 17868
1962. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratLess line 17869
1963. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratMinOne line 17871
1964. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_normalizeRat line 17873
1965. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_normalizeRat_pair line 17888
1966. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratCross line 17892
1967. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratAdd_raw line 17894
1968. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratMul_raw line 17898
1969. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratDiv_raw line 17902
1970. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratAdd line 17906
1971. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratMul line 17915
1972. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratDiv line 17922
1973. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratLess line 17930
1974. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratMinOne line 17940
1975. def OAI.CommonBasesFPRAS.MachineCode.Expression.iterateWord line 17958
1976. def OAI.CommonBasesFPRAS.MachineCode.Expression.iterateNat line 17960
1977. def OAI.CommonBasesFPRAS.MachineCode.Expression.fromList line 17963
1978. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.foldValue_iterate line 17966
1979. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_iterateWord line 17975
1980. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_iterateNat line 17980
1981. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_fromList line 17988
1982. def OAI.CommonBasesFPRAS.MachineCode.Expression.rangeStepCode line 17996
1983. def OAI.CommonBasesFPRAS.MachineCode.Expression.rangeCode line 17998
1984. def OAI.CommonBasesFPRAS.MachineCode.Expression.rangeStep line 18001
1985. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.rangeStep_iterate line 18002
1986. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_rangeCode line 18006
1987. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.SplitState line 18012
1988. def OAI.CommonBasesFPRAS.MachineCode.Expression.splitStep line 18013
1989. def OAI.CommonBasesFPRAS.MachineCode.Expression.splitAtCode line 18019
1990. def OAI.CommonBasesFPRAS.MachineCode.Expression.takeCode line 18022
1991. def OAI.CommonBasesFPRAS.MachineCode.Expression.dropCode line 18023
1992. def OAI.CommonBasesFPRAS.MachineCode.Expression.splitStepValue line 18025
1993. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_splitStep line 18027
1994. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.fold_splitStep line 18038
1995. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_splitAtCode line 18049
1996. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_takeCode line 18059
1997. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_dropCode line 18063
1998. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_compose line 18068
1999. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_both line 18071
2000. def OAI.CommonBasesFPRAS.MachineCode.Expression.headD line 18079
2001. def OAI.CommonBasesFPRAS.MachineCode.Expression.getDCode line 18080
2002. def OAI.CommonBasesFPRAS.MachineCode.Expression.boolOr line 18083
2003. def OAI.CommonBasesFPRAS.MachineCode.Expression.natEqual line 18084
2004. def OAI.CommonBasesFPRAS.MachineCode.Expression.listAll line 18086
2005. def OAI.CommonBasesFPRAS.MachineCode.Expression.filterStep line 18088
2006. def OAI.CommonBasesFPRAS.MachineCode.Expression.filterWith line 18092
2007. def OAI.CommonBasesFPRAS.MachineCode.Expression.foldLast line 18096
2008. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.foldLast_append line 18099
2009. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.foldLast_reverse line 18104
2010. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_headD line 18109
2011. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_getDCode line 18120
2012. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_boolOr line 18132
2013. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natEqual line 18134
2014. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_listAll line 18144
2015. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_filterStep line 18158
2016. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_filterWith line 18167
2017. def OAI.CommonBasesFPRAS.MachineCode.Expression.powStepCode line 18185
2018. def OAI.CommonBasesFPRAS.MachineCode.Expression.powCode line 18186
2019. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_powCode line 18188
2020. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratPowCode line 18199
2021. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratPowCode line 18201
2022. lemma OAI.CommonBasesFPRAS.MachineCode.width_take line 18214
2023. lemma OAI.CommonBasesFPRAS.MachineCode.width_drop line 18219
2024. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_fromList line 18224
2025. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_splitStep line 18238
2026. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_splitFold line 18239
2027. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_splitAt line 18253
2028. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_take line 18258
2029. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_drop line 18260
2030. lemma OAI.CommonBasesFPRAS.MachineCode.fold_fst_mem line 18262
2031. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_headD line 18271
2032. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_getD line 18287
2033. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_boolOr line 18292
2034. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_natEqual line 18293
2035. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_listAll line 18294
2036. def OAI.CommonBasesFPRAS.MachineCode.wordDouble line 18304
2037. lemma OAI.CommonBasesFPRAS.MachineCode.wordDouble_length_le line 18305
2038. lemma OAI.CommonBasesFPRAS.MachineCode.wordDouble_fold_length_le line 18307
2039. lemma OAI.CommonBasesFPRAS.MachineCode.wordDouble_prefix_length_le line 18311
2040. lemma OAI.CommonBasesFPRAS.MachineCode.fold_wordDouble line 18315
2041. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordRepeatStep line 18320
2042. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_wordRepeatFold line 18321
2043. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_unary line 18351
2044. abbrev OAI.CommonBasesFPRAS.MachineCode.StateData line 18367
2045. def OAI.CommonBasesFPRAS.MachineCode.representedState line 18369
2046. lemma OAI.CommonBasesFPRAS.MachineCode.representedState_inl line 18371
2047. lemma OAI.CommonBasesFPRAS.MachineCode.representedState_inr line 18373
2048. lemma OAI.CommonBasesFPRAS.MachineCode.representedState_preinl line 18375
2049. lemma OAI.CommonBasesFPRAS.MachineCode.representedState_preinr line 18377
2050. lemma OAI.CommonBasesFPRAS.MachineCode.wordSet_not line 18379
2051. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordGet line 18389
2052. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordNot line 18391
2053. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordCountStep line 18393
2054. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordCount line 18394
2055. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordGet line 18396
2056. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordNot line 18400
2057. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordCount line 18406
2058. def OAI.CommonBasesFPRAS.MachineCode.Expression.deficiencyCode line 18424
2059. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_deficiencyCode line 18428
2060. lemma OAI.CommonBasesFPRAS.MachineCode.deficiencyCode_source line 18438
2061. abbrev OAI.CommonBasesFPRAS.MachineCode.Optional line 18453
2062. abbrev OAI.CommonBasesFPRAS.MachineCode.RandomRows line 18454
2063. def OAI.CommonBasesFPRAS.MachineCode.optionData line 18456
2064. lemma OAI.CommonBasesFPRAS.MachineCode.foldValue_append line 18459
2065. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ident line 18467
2066. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_fst line 18469
2067. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_snd line 18471
2068. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_constant line 18473
2069. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_reverse line 18475
2070. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_toNat line 18477
2071. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_less line 18479
2072. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordTake line 18482
2073. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordDrop line 18483
2074. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordTake line 18484
2075. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordDrop line 18488
2076. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.RejectState line 18493
2077. def OAI.CommonBasesFPRAS.MachineCode.Expression.rejectStep line 18494
2078. def OAI.CommonBasesFPRAS.MachineCode.Expression.rejectCode line 18499
2079. def OAI.CommonBasesFPRAS.MachineCode.Expression.rejectValue line 18502
2080. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_rejectStep line 18506
2081. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.fold_reject line 18513
2082. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_rejectCode line 18526
2083. lemma OAI.CommonBasesFPRAS.MachineCode.binaryValue_ofFn_reverse line 18535
2084. lemma OAI.CommonBasesFPRAS.MachineCode.ofFn_bitPrefix line 18545
2085. lemma OAI.CommonBasesFPRAS.MachineCode.rejectValue_ofFn line 18552
2086. lemma OAI.CommonBasesFPRAS.MachineCode.rejectValue_prefix line 18564
2087. abbrev OAI.CommonBasesFPRAS.MachineCode.BankData line 18574
2088. abbrev OAI.CommonBasesFPRAS.MachineCode.Bank line 18575
2089. lemma OAI.CommonBasesFPRAS.MachineCode.rejectValue_lt line 18576
2090. def OAI.CommonBasesFPRAS.MachineCode.bankEval line 18586
2091. lemma OAI.CommonBasesFPRAS.MachineCode.bankEval_bind line 18594
2092. lemma OAI.CommonBasesFPRAS.MachineCode.bankEval_map line 18607
2093. def OAI.CommonBasesFPRAS.MachineCode.bankEncode line 18613
2094. lemma OAI.CommonBasesFPRAS.MachineCode.bankEncode_succ line 18615
2095. lemma OAI.CommonBasesFPRAS.MachineCode.bankEval_run line 18618
2096. def OAI.CommonBasesFPRAS.MachineCode.zeroValue line 18652
2097. def OAI.CommonBasesFPRAS.MachineCode.optionalValue line 18659
2098. def OAI.CommonBasesFPRAS.MachineCode.decodeOptional line 18660
2099. lemma OAI.CommonBasesFPRAS.MachineCode.decode_optionalValue line 18661
2100. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect line 18664
2101. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.clog_two_size_pred line 18666
2102. def OAI.CommonBasesFPRAS.MachineCode.Expression.clogCode line 18676
2103. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_clogCode line 18677
2104. def OAI.CommonBasesFPRAS.MachineCode.Effect.pure line 18688
2105. def OAI.CommonBasesFPRAS.MachineCode.Effect.fail line 18689
2106. def OAI.CommonBasesFPRAS.MachineCode.Effect.bind line 18691
2107. def OAI.CommonBasesFPRAS.MachineCode.Effect.keep line 18696
2108. def OAI.CommonBasesFPRAS.MachineCode.Effect.letIn line 18702
2109. def OAI.CommonBasesFPRAS.MachineCode.Effect.draw line 18705
2110. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_pure line 18710
2111. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_fail line 18716
2112. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_bind line 18718
2113. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_keep line 18726
2114. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_draw line 18732
2115. def OAI.CommonBasesFPRAS.MachineCode.Effect.Realizes line 18741
2116. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_pure line 18746
2117. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_bind line 18752
2118. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_keep line 18769
2119. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_letIn line 18782
2120. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_draw line 18789
2121. def OAI.CommonBasesFPRAS.MachineCode.Effect.map line 18805
2122. def OAI.CommonBasesFPRAS.MachineCode.Effect.precompose line 18806
2123. def OAI.CommonBasesFPRAS.MachineCode.Effect.choose line 18808
2124. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_precompose line 18811
2125. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_precompose line 18816
2126. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_choose line 18824
2127. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_map line 18832
2128. def OAI.CommonBasesFPRAS.MachineCode.iterateM line 18841
2129. lemma OAI.CommonBasesFPRAS.MachineCode.iterateM_some line 18844
2130. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_iterateNatM line 18850
2131. def OAI.CommonBasesFPRAS.MachineCode.Effect.loopStep line 18873
2132. def OAI.CommonBasesFPRAS.MachineCode.Effect.repeatCode line 18875
2133. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_loopStep_none line 18877
2134. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_loopStep_some line 18879
2135. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_repeat line 18882
2136. def OAI.CommonBasesFPRAS.MachineCode.Effect.treeRepeat line 18888
2137. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_repeat line 18891
2138. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.trans line 18914
2139. lemma OAI.CommonBasesFPRAS.DrawTree.uniformVia_reindexed_via line 18922
2140. def OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw line 18930
2141. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.Realizes.law line 18933
2142. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.reindex line 18936
2143. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_bind line 18941
2144. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_letIn line 18950
2145. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_precompose line 18959
2146. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_map line 18965
2147. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_choose line 18972
2148. lemma OAI.CommonBasesFPRAS.DrawTree.bind_leaf line 18986
2149. lemma OAI.CommonBasesFPRAS.DrawTree.map_bind line 18990
2150. lemma OAI.CommonBasesFPRAS.DrawTree.bind_map line 18994
2151. lemma OAI.CommonBasesFPRAS.DrawTree.map_map line 18996
2152. def OAI.CommonBasesFPRAS.MachineCode.optionEncode line 19003
2153. lemma OAI.CommonBasesFPRAS.MachineCode.optionEncode_none line 19005
2154. lemma OAI.CommonBasesFPRAS.MachineCode.optionEncode_some line 19007
2155. def OAI.CommonBasesFPRAS.MachineCode.Effect.someCode line 19011
2156. def OAI.CommonBasesFPRAS.MachineCode.Effect.noneCode line 19013
2157. def OAI.CommonBasesFPRAS.MachineCode.Effect.optionContinue line 19014
2158. def OAI.CommonBasesFPRAS.MachineCode.Effect.optionBind line 19016
2159. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_some line 19019
2160. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_none line 19023
2161. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_optionContinue line 19026
2162. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_optionBind line 19038
2163. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_repeat line 19048
2164. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.treeRepeat_succ_last line 19060
2165. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.treeRepeat_option line 19070
2166. def OAI.CommonBasesFPRAS.MachineCode.Effect.iterateCode line 19077
2167. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_iterate line 19079
2168. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_reparam line 19091
2169. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_post line 19095
2170. lemma OAI.CommonBasesFPRAS.MachineCode.foldValue_iterateM line 19102
2171. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_iterateNat line 19109
2172. lemma OAI.CommonBasesFPRAS.MachineCode.iterateM_total line 19193
2173. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_le line 19198
2174. lemma OAI.CommonBasesFPRAS.MachineCode.width_range line 19207
2175. lemma OAI.CommonBasesFPRAS.MachineCode.width_rangeState line 19211
2176. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_rangeStep line 19216
2177. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_rangeCode line 19217
2178. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordRange line 19259
2179. lemma OAI.CommonBasesFPRAS.MachineCode.run_filterStep_partial line 19268
2180. lemma OAI.CommonBasesFPRAS.MachineCode.fold_filterStep_bound line 19275
2181. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_filterStep line 19296
2182. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_filterFold line 19298
2183. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_filterWith line 19311
2184. def OAI.CommonBasesFPRAS.MachineCode.stateEncode line 19319
2185. lemma OAI.CommonBasesFPRAS.MachineCode.stateEncode_left_length line 19321
2186. lemma OAI.CommonBasesFPRAS.MachineCode.stateEncode_right_length line 19323
2187. lemma OAI.CommonBasesFPRAS.MachineCode.stateEncode_repr line 19325
2188. lemma OAI.CommonBasesFPRAS.MachineCode.stateEncode_get_left line 19329
2189. lemma OAI.CommonBasesFPRAS.MachineCode.stateEncode_get_right line 19331
2190. def OAI.CommonBasesFPRAS.MachineCode.Expression.boolXor line 19336
2191. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_boolXor line 19337
2192. def OAI.CommonBasesFPRAS.MachineCode.Expression.singleAt line 19340
2193. def OAI.CommonBasesFPRAS.MachineCode.Expression.fullAt line 19342
2194. def OAI.CommonBasesFPRAS.MachineCode.Expression.emptyAt line 19344
2195. def OAI.CommonBasesFPRAS.MachineCode.Expression.singleValue line 19347
2196. def OAI.CommonBasesFPRAS.MachineCode.Expression.fullValue line 19348
2197. def OAI.CommonBasesFPRAS.MachineCode.Expression.emptyValue line 19349
2198. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_singleAt line 19350
2199. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_fullAt line 19355
2200. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_emptyAt line 19360
2201. def OAI.CommonBasesFPRAS.MachineCode.Expression.plainValue line 19367
2202. def OAI.CommonBasesFPRAS.MachineCode.Expression.plainCode line 19368
2203. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_plainCode line 19370
2204. lemma OAI.CommonBasesFPRAS.MachineCode.singleValue_source line 19379
2205. lemma OAI.CommonBasesFPRAS.MachineCode.fullValue_source line 19384
2206. lemma OAI.CommonBasesFPRAS.MachineCode.emptyValue_source line 19389
2207. lemma OAI.CommonBasesFPRAS.MachineCode.plainValue_source line 19395
2208. lemma OAI.CommonBasesFPRAS.MachineCode.plainCode_source line 19410
2209. abbrev OAI.CommonBasesFPRAS.MachineCode.DefectInput line 19414
2210. def OAI.CommonBasesFPRAS.MachineCode.Expression.defectAt line 19417
2211. def OAI.CommonBasesFPRAS.MachineCode.Expression.defectAtValue line 19422
2212. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_defectAt line 19424
2213. def OAI.CommonBasesFPRAS.MachineCode.Expression.defectValue line 19438
2214. def OAI.CommonBasesFPRAS.MachineCode.Expression.defectCode line 19440
2215. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_defectCode line 19443
2216. lemma OAI.CommonBasesFPRAS.MachineCode.slotPair_inj line 19457
2217. lemma OAI.CommonBasesFPRAS.MachineCode.slotPair_mem line 19458
2218. lemma OAI.CommonBasesFPRAS.MachineCode.defect_paired_iff line 19459
2219. lemma OAI.CommonBasesFPRAS.MachineCode.defectValue_source line 19474
2220. lemma OAI.CommonBasesFPRAS.MachineCode.defectCode_source line 19511
2221. abbrev OAI.CommonBasesFPRAS.MachineCode.SampleData line 19516
2222. abbrev OAI.CommonBasesFPRAS.MachineCode.HistoryData line 19517
2223. def OAI.CommonBasesFPRAS.MachineCode.Expression.countWith line 19520
2224. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_countWith line 19522
2225. def OAI.CommonBasesFPRAS.MachineCode.Expression.countPlainCode line 19529
2226. def OAI.CommonBasesFPRAS.MachineCode.Expression.countDefectCode line 19531
2227. def OAI.CommonBasesFPRAS.MachineCode.Expression.countPlainValue line 19532
2228. def OAI.CommonBasesFPRAS.MachineCode.Expression.countDefectValue line 19533
2229. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_countPlainCode line 19534
2230. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_countDefectCode line 19538
2231. def OAI.CommonBasesFPRAS.MachineCode.Expression.learningRatioCode line 19543
2232. def OAI.CommonBasesFPRAS.MachineCode.Expression.learningRatio line 19545
2233. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.learningRatio_nonneg line 19546
2234. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_learningRatio line 19548
2235. def OAI.CommonBasesFPRAS.MachineCode.Expression.weightStep line 19554
2236. def OAI.CommonBasesFPRAS.MachineCode.Expression.weightUpdate line 19559
2237. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.weightUpdate_nonneg line 19561
2238. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_weightStep line 19567
2239. def OAI.CommonBasesFPRAS.MachineCode.Expression.historyWeightValue line 19579
2240. def OAI.CommonBasesFPRAS.MachineCode.Expression.historyWeightCode line 19581
2241. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.fold_weightStep line 19583
2242. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_historyWeightCode line 19592
2243. def OAI.CommonBasesFPRAS.MachineCode.sampleEncode line 19599
2244. def OAI.CommonBasesFPRAS.MachineCode.historyEncode line 19600
2245. lemma OAI.CommonBasesFPRAS.MachineCode.countPlainValue_source line 19601
2246. lemma OAI.CommonBasesFPRAS.MachineCode.countDefectValue_source line 19604
2247. lemma OAI.CommonBasesFPRAS.MachineCode.weightUpdate_source line 19609
2248. lemma OAI.CommonBasesFPRAS.MachineCode.historyWeight_source line 19621
2249. lemma OAI.CommonBasesFPRAS.MachineCode.historyWeightCode_source line 19638
2250. def OAI.CommonBasesFPRAS.MachineCode.Expression.listAppend line 19646
2251. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_listAppend line 19648
2252. def OAI.CommonBasesFPRAS.MachineCode.Expression.productStep line 19661
2253. def OAI.CommonBasesFPRAS.MachineCode.Expression.productCode line 19664
2254. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_productStep line 19666
2255. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_productCode line 19674
2256. def OAI.CommonBasesFPRAS.MachineCode.Expression.indexPairs line 19690
2257. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_indexPairs line 19691
2258. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_listAppend line 19700
2259. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_map_pair line 19714
2260. lemma OAI.CommonBasesFPRAS.MachineCode.width_list_product line 19728
2261. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_productStep line 19741
2262. lemma OAI.CommonBasesFPRAS.MachineCode.fold_productStep line 19746
2263. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_productCode line 19754
2264. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordGet line 19773
2265. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordNot line 19777
2266. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordCountStep line 19783
2267. lemma OAI.CommonBasesFPRAS.MachineCode.fold_wordCount_bound line 19784
2268. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordCount line 19792
2269. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_deficiency line 19807
2270. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_normalizeRat line 19816
2271. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratCross line 19820
2272. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratAdd line 19821
2273. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratMul line 19825
2274. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratDiv line 19829
2275. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratLess line 19833
2276. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratMinOne line 19834
2277. lemma OAI.CommonBasesFPRAS.MachineCode.iterateM_succ_last line 19836
2278. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_repeat_succ_last line 19848
2279. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_repeat_succ_last line 19861
2280. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseRepeat line 19872
2281. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.phaseRepeat_bind line 19875
2282. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_phaseRepeat line 19880
2283. def OAI.CommonBasesFPRAS.MachineCode.Effect.hitStepCode line 19894
2284. def OAI.CommonBasesFPRAS.MachineCode.Effect.hitFinish line 19896
2285. def OAI.CommonBasesFPRAS.MachineCode.Effect.hittingCode line 19898
2286. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect.SearchState line 19901
2287. def OAI.CommonBasesFPRAS.MachineCode.Effect.searchStep line 19902
2288. def OAI.CommonBasesFPRAS.MachineCode.Effect.searchFinish line 19906
2289. def OAI.CommonBasesFPRAS.MachineCode.Effect.searchEncode line 19909
2290. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.searchRepeat_done line 19913
2291. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.searchRepeat_finish line 19918
2292. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_hitStep line 19930
2293. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_hitting line 19953
2294. def OAI.CommonBasesFPRAS.MachineCode.Expression.optionMapCode line 19972
2295. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_optionMapCode line 19974
2296. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_recode line 19984
2297. def OAI.CommonBasesFPRAS.MachineCode.Effect.withContext line 19991
2298. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_withContext line 19993
2299. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_optionMap line 20003
2300. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_optionRecode line 20017
2301. def OAI.CommonBasesFPRAS.MachineCode.Expression.defectPairsValue line 20035
2302. def OAI.CommonBasesFPRAS.MachineCode.Expression.defectPairsCode line 20037
2303. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_defectPairsCode line 20039
2304. def OAI.CommonBasesFPRAS.MachineCode.Expression.chainValue line 20047
2305. def OAI.CommonBasesFPRAS.MachineCode.Expression.chainCode line 20048
2306. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_chainCode line 20050
2307. def OAI.CommonBasesFPRAS.MachineCode.Expression.multiplierValue line 20058
2308. def OAI.CommonBasesFPRAS.MachineCode.Expression.multiplierCode line 20061
2309. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_multiplierCode line 20066
2310. lemma OAI.CommonBasesFPRAS.MachineCode.mem_defectPairsValue line 20081
2311. lemma OAI.CommonBasesFPRAS.MachineCode.defectPairs_nonempty_source line 20091
2312. lemma OAI.CommonBasesFPRAS.MachineCode.chainValue_source line 20105
2313. lemma OAI.CommonBasesFPRAS.MachineCode.multiplierValue_source line 20123
2314. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_append line 20146
2315. def OAI.CommonBasesFPRAS.MachineCode.Expression.updateAt line 20149
2316. def OAI.CommonBasesFPRAS.MachineCode.Expression.updateWord line 20152
2317. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_updateAt line 20154
2318. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_updateWord line 20159
2319. def OAI.CommonBasesFPRAS.MachineCode.Expression.splitWord line 20180
2320. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_splitWord line 20182
2321. def OAI.CommonBasesFPRAS.MachineCode.Expression.exchangeWord line 20190
2322. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_exchangeWord line 20193
2323. def OAI.CommonBasesFPRAS.MachineCode.Expression.exchangeSetCode line 20201
2324. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_exchangeSetCode line 20203
2325. def OAI.CommonBasesFPRAS.MachineCode.combinedEncode line 20214
2326. def OAI.CommonBasesFPRAS.MachineCode.position line 20215
2327. lemma OAI.CommonBasesFPRAS.MachineCode.position_lt line 20216
2328. lemma OAI.CommonBasesFPRAS.MachineCode.position_inj line 20217
2329. lemma OAI.CommonBasesFPRAS.MachineCode.combinedEncode_length line 20219
2330. lemma OAI.CommonBasesFPRAS.MachineCode.combinedEncode_get line 20221
2331. lemma OAI.CommonBasesFPRAS.MachineCode.combinedEncode_update line 20230
2332. lemma OAI.CommonBasesFPRAS.MachineCode.exchangeSetCode_source line 20246
2333. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.historyWeightValue_nonneg line 20262
2334. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.multiplierValue_nonneg line 20271
2335. def OAI.CommonBasesFPRAS.MachineCode.Expression.rhoCode line 20278
2336. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.rationalRho_nonneg line 20282
2337. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_rhoCode line 20289
2338. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.WeightContext line 20308
2339. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.WeightInput line 20309
2340. def OAI.CommonBasesFPRAS.MachineCode.Expression.annealCode line 20311
2341. def OAI.CommonBasesFPRAS.MachineCode.Expression.weightCode line 20314
2342. lemma OAI.CommonBasesFPRAS.MachineCode.rationalHistory_nonnegative line 20318
2343. lemma OAI.CommonBasesFPRAS.MachineCode.annealCode_source line 20337
2344. lemma OAI.CommonBasesFPRAS.MachineCode.weightCode_source line 20354
2345. def OAI.CommonBasesFPRAS.MachineCode.Effect.bernoulliCode line 20372
2346. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bernoulliCode_source line 20374
2347. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.AcceptanceInput line 20394
2348. def OAI.CommonBasesFPRAS.MachineCode.Expression.acceptanceCode line 20395
2349. lemma OAI.CommonBasesFPRAS.MachineCode.acceptanceCode_source line 20400
2350. def OAI.CommonBasesFPRAS.MachineCode.Expression.memberPositions line 20424
2351. def OAI.CommonBasesFPRAS.MachineCode.Expression.membersCode line 20425
2352. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_membersCode line 20427
2353. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.memberPositions_nodup line 20435
2354. lemma OAI.CommonBasesFPRAS.MachineCode.mem_memberPositions_source line 20439
2355. def OAI.CommonBasesFPRAS.MachineCode.memberPositionEquiv line 20445
2356. def OAI.CommonBasesFPRAS.MachineCode.memberListEquiv line 20458
2357. lemma OAI.CommonBasesFPRAS.MachineCode.memberListEquiv_position line 20461
2358. def OAI.CommonBasesFPRAS.MachineCode.Effect.uniformList line 20469
2359. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.uniformVia_size line 20472
2360. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.realizes_uniformList line 20479
2361. lemma OAI.CommonBasesFPRAS.MachineCode.combinedEncode_compl line 20510
2362. def OAI.CommonBasesFPRAS.MachineCode.exchangePositions line 20514
2363. def OAI.CommonBasesFPRAS.MachineCode.Expression.exchangePositionsCode line 20516
2364. lemma OAI.CommonBasesFPRAS.MachineCode.run_exchangePositionsCode line 20518
2365. lemma OAI.CommonBasesFPRAS.MachineCode.exchangePositions_nodup line 20523
2366. lemma OAI.CommonBasesFPRAS.MachineCode.memberPositionEquiv_val line 20526
2367. def OAI.CommonBasesFPRAS.MachineCode.exchangePositionEquiv line 20530
2368. def OAI.CommonBasesFPRAS.MachineCode.exchangeListEquiv line 20548
2369. lemma OAI.CommonBasesFPRAS.MachineCode.exchangeListEquiv_val line 20551
2370. def OAI.CommonBasesFPRAS.MachineCode.Effect.proposal line 20559
2371. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.proposal_source line 20560
2372. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect.OfferInput line 20572
2373. def OAI.CommonBasesFPRAS.MachineCode.Effect.acceptancePrep line 20574
2374. def OAI.CommonBasesFPRAS.MachineCode.Effect.offerCore line 20576
2375. def OAI.CommonBasesFPRAS.MachineCode.Effect.offerCode line 20580
2376. def OAI.CommonBasesFPRAS.MachineCode.Effect.activeStepCode line 20583
2377. def OAI.CommonBasesFPRAS.MachineCode.Effect.stepCode line 20586
2378. lemma OAI.CommonBasesFPRAS.MachineCode.offerCore_source line 20601
2379. lemma OAI.CommonBasesFPRAS.MachineCode.offerCode_source line 20629
2380. lemma OAI.CommonBasesFPRAS.MachineCode.activeStepCode_source line 20640
2381. lemma OAI.CommonBasesFPRAS.MachineCode.stepCode_source line 20649
2382. lemma OAI.CommonBasesFPRAS.MachineCode.binaryValue_injective_length line 20670
2383. lemma OAI.CommonBasesFPRAS.MachineCode.binaryValue_replicate_false line 20684
2384. lemma OAI.CommonBasesFPRAS.MachineCode.padded_range line 20689
2385. def OAI.CommonBasesFPRAS.MachineCode.Expression.paddedBitsCode line 20701
2386. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_paddedBitsCode line 20703
2387. def OAI.CommonBasesFPRAS.MachineCode.Expression.plainDecodeCode line 20724
2388. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.plainDecodeCode_source line 20725
2389. def OAI.CommonBasesFPRAS.MachineCode.Effect.plainCode line 20741
2390. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.plainCode_source line 20743
2391. def OAI.CommonBasesFPRAS.MachineCode.Effect.storedStepPrep line 20765
2392. def OAI.CommonBasesFPRAS.MachineCode.Effect.storedStepCode line 20768
2393. def OAI.CommonBasesFPRAS.MachineCode.Effect.traceCode line 20770
2394. lemma OAI.CommonBasesFPRAS.MachineCode.rationalHistory_map line 20774
2395. lemma OAI.CommonBasesFPRAS.MachineCode.historyEncode_take line 20777
2396. lemma OAI.CommonBasesFPRAS.MachineCode.storedStepCode_source line 20788
2397. lemma OAI.CommonBasesFPRAS.MachineCode.traceCode_source line 20803
2398. def OAI.CommonBasesFPRAS.MachineCode.Effect.withOptionContext line 20822
2399. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_withOptionContext line 20825
2400. abbrev OAI.CommonBasesFPRAS.MachineCode.RestartContext line 20840
2401. abbrev OAI.CommonBasesFPRAS.MachineCode.RestartState line 20841
2402. abbrev OAI.CommonBasesFPRAS.MachineCode.RestartInput line 20842
2403. def OAI.CommonBasesFPRAS.MachineCode.Effect.traceAtPrep line 20845
2404. def OAI.CommonBasesFPRAS.MachineCode.Effect.traceAtCode line 20849
2405. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartTickPrep line 20851
2406. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartTick line 20854
2407. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartPrep line 20857
2408. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartCode line 20860
2409. lemma OAI.CommonBasesFPRAS.MachineCode.traceAtCode_source line 20874
2410. lemma OAI.CommonBasesFPRAS.MachineCode.restartTick_source line 20880
2411. lemma OAI.CommonBasesFPRAS.MachineCode.canonicalRestart_phaseRepeat line 20892
2412. lemma OAI.CommonBasesFPRAS.MachineCode.restartCode_source line 20912
2413. def OAI.CommonBasesFPRAS.MachineCode.Expression.allRange line 20932
2414. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_allRange line 20934
2415. lemma OAI.CommonBasesFPRAS.MachineCode.rationalPair_pos line 20945
2416. def OAI.CommonBasesFPRAS.MachineCode.Expression.pairPositiveCode line 20952
2417. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_pairPositiveCode line 20954
2418. def OAI.CommonBasesFPRAS.MachineCode.Expression.slotRowCode line 20966
2419. def OAI.CommonBasesFPRAS.MachineCode.Expression.slotsPositiveCode line 20969
2420. def OAI.CommonBasesFPRAS.MachineCode.Expression.prefixPositiveCode line 20971
2421. def OAI.CommonBasesFPRAS.MachineCode.Expression.historyPositiveCode line 20973
2422. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_slotRowCode line 20976
2423. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_slotsPositiveCode line 20982
2424. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_prefixPositiveCode line 20988
2425. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_historyPositiveCode line 20993
2426. lemma OAI.CommonBasesFPRAS.MachineCode.rationalHistory_inactive line 21003
2427. lemma OAI.CommonBasesFPRAS.MachineCode.rationalHistoryPositive_slots line 21012
2428. lemma OAI.CommonBasesFPRAS.MachineCode.historyPositiveCode_source line 21024
2429. lemma OAI.CommonBasesFPRAS.DrawTree.Reindexed.lift_map line 21045
2430. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_unmap line 21066
2431. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleTick line 21074
2432. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleFinish line 21076
2433. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleCode line 21078
2434. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleTickTree line 21081
2435. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.sampleRepeat_finish line 21083
2436. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_sampleTick line 21100
2437. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_sample line 21110
2438. abbrev OAI.CommonBasesFPRAS.MachineCode.AlgorithmParams line 21134
2439. abbrev OAI.CommonBasesFPRAS.MachineCode.PhaseInput line 21135
2440. def OAI.CommonBasesFPRAS.MachineCode.params line 21136
2441. def OAI.CommonBasesFPRAS.MachineCode.Expression.mapEach line 21139
2442. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_mapEach line 21141
2443. def OAI.CommonBasesFPRAS.MachineCode.Effect.retainOption line 21148
2444. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_retainOption line 21151
2445. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseRestartPrep line 21163
2446. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseRestartCode line 21166
2447. def OAI.CommonBasesFPRAS.MachineCode.Effect.startCode line 21167
2448. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseStepPrep line 21168
2449. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseStepCode line 21170
2450. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseSamplePrep line 21172
2451. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseSampleCode line 21174
2452. def OAI.CommonBasesFPRAS.MachineCode.Effect.positiveTest line 21176
2453. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseCode line 21177
2454. def OAI.CommonBasesFPRAS.MachineCode.Effect.witnessCode line 21179
2455. lemma OAI.CommonBasesFPRAS.MachineCode.phaseRestartCode_source line 21188
2456. lemma OAI.CommonBasesFPRAS.MachineCode.startCode_source line 21197
2457. lemma OAI.CommonBasesFPRAS.MachineCode.phaseStepCode_source line 21203
2458. lemma OAI.CommonBasesFPRAS.MachineCode.phaseSampleCode_source line 21212
2459. lemma OAI.CommonBasesFPRAS.MachineCode.positiveTest_source line 21228
2460. lemma OAI.CommonBasesFPRAS.MachineCode.phaseCode_source line 21230
2461. lemma OAI.CommonBasesFPRAS.MachineCode.witnessCode_source line 21244
2462. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_mapWith_source line 21258
2463. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratSumCode line 21278
2464. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratProductCode line 21279
2465. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratSumCode line 21280
2466. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ratProductCode line 21294
2467. def OAI.CommonBasesFPRAS.MachineCode.Expression.natRatCode line 21309
2468. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natRatCode line 21310
2469. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_add_max line 21316
2470. def OAI.CommonBasesFPRAS.MachineCode.pairHeight line 21324
2471. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_pos line 21325
2472. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_fst line 21326
2473. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_snd line 21327
2474. lemma OAI.CommonBasesFPRAS.MachineCode.width_le_pairHeight line 21328
2475. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_le_width line 21336
2476. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_normalize line 21340
2477. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_ratAdd_raw line 21349
2478. lemma OAI.CommonBasesFPRAS.MachineCode.pairHeight_ratMul_raw line 21362
2479. lemma OAI.CommonBasesFPRAS.MachineCode.run_ratAdd_height line 21374
2480. lemma OAI.CommonBasesFPRAS.MachineCode.run_ratMul_height line 21381
2481. lemma OAI.CommonBasesFPRAS.MachineCode.fold_pairHeight line 21389
2482. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_pairFold line 21406
2483. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratSum line 21417
2484. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_ratProduct line 21422
2485. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_boolXor line 21479
2486. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_singleAt line 21480
2487. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_fullAt line 21481
2488. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_emptyAt line 21482
2489. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_plainCode line 21483
2490. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_defectAt line 21487
2491. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_defectCode line 21493
2492. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_countWith line 21497
2493. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_countPlain line 21499
2494. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_countDefect line 21505
2495. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_learningRatio line 21510
2496. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_weightStep line 21515
2497. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_indexPairs line 21519
2498. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordIndexPairs line 21522
2499. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_defectPairs line 21530
2500. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_chainCode line 21535
2501. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_updateAt line 21540
2502. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_updateWord line 21541
2503. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_splitWord line 21545
2504. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_exchangeWord line 21546
2505. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_exchangeSet line 21550
2506. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_membersCode line 21555
2507. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_exchangePositions line 21556
2508. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordTake line 21561
2509. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_wordDrop line 21562
2510. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_clog line 21563
2511. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_rejectStep line 21564
2512. lemma OAI.CommonBasesFPRAS.MachineCode.fold_reject_width line 21568
2513. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_rejectFold line 21584
2514. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_reject line 21598
2515. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_pure line 21603
2516. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_fail line 21605
2517. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_bind line 21606
2518. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_keep line 21608
2519. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_letIn line 21610
2520. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_draw line 21613
2521. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_optionMap line 21620
2522. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_mapEach line 21622
2523. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_precompose line 21625
2524. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_map line 21628
2525. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_choose line 21631
2526. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_withContext line 21634
2527. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_retainOption line 21639
2528. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_bernoulli line 21662
2529. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_uniformList line 21663
2530. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_proposal line 21664
2531. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_someCode line 21668
2532. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_noneCode line 21670
2533. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.controlled_optionBind line 21671
2534. lemma OAI.CommonBasesFPRAS.MachineCode.bits_length_pow line 21675
2535. lemma OAI.CommonBasesFPRAS.MachineCode.powStep_iterate line 21683
2536. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_powStep line 21687
2537. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_powCode line 21688
2538. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_ratPowCode line 21744
2539. lemma OAI.CommonBasesFPRAS.MachineCode.run_both_parts line 21775
2540. lemma OAI.CommonBasesFPRAS.MachineCode.width_fst line 21789
2541. lemma OAI.CommonBasesFPRAS.MachineCode.width_snd line 21791
2542. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_ratPowerAfter line 21793
2543. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_preControlled line 21804
2544. lemma OAI.CommonBasesFPRAS.MachineCode.bankEval_rest_suffix line 21812
2545. lemma OAI.CommonBasesFPRAS.MachineCode.bankEval_rest_width line 21826
2546. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.outputs line 21834
2547. lemma OAI.CommonBasesFPRAS.MachineCode.width_optionalValue line 21842
2548. lemma OAI.CommonBasesFPRAS.MachineCode.width_optionEncode line 21850
2549. lemma OAI.CommonBasesFPRAS.MachineCode.learningRatio_height line 21859
2550. lemma OAI.CommonBasesFPRAS.MachineCode.run_weightStep_raw line 21870
2551. lemma OAI.CommonBasesFPRAS.MachineCode.weightStep_height line 21883
2552. lemma OAI.CommonBasesFPRAS.MachineCode.fold_weight_height line 21896
2553. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_weightFold line 21912
2554. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_historyWeight line 21922
2555. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_multiplier line 21926
2556. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_rho line 21934
2557. lemma OAI.CommonBasesFPRAS.MachineCode.run_deficiency_le line 21935
2558. def OAI.CommonBasesFPRAS.MachineCode.weightSmall line 21944
2559. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_anneal line 21946
2560. lemma OAI.CommonBasesFPRAS.MachineCode.polySafe_weight line 21967
2561. abbrev OAI.CommonBasesFPRAS.MachineCode.OraclePredicate line 21973
2562. def OAI.CommonBasesFPRAS.MachineCode.OracleSafe line 21975
2563. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_lift line 21977
2564. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_controlled line 21979
2565. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_mono line 21987
2566. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_reparam line 21991
2567. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_compose line 21995
2568. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_both line 22005
2569. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_post line 22013
2570. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_pull line 22020
2571. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_input_bound line 22026
2572. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_applyIf line 22030
2573. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_fold line 22060
2574. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_iterateNat line 22080
2575. def OAI.CommonBasesFPRAS.MachineCode.Effect.bankScope line 22165
2576. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.scope_width line 22167
2577. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_scope_fst line 22177
2578. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_scope_controlled line 22184
2579. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_pure line 22188
2580. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_precompose line 22196
2581. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_keep line 22210
2582. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_bind line 22217
2583. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.output_some line 22247
2584. lemma OAI.CommonBasesFPRAS.DrawTree.All.mono line 22264
2585. lemma OAI.CommonBasesFPRAS.DrawTree.all_bind_of_all line 22269
2586. lemma OAI.CommonBasesFPRAS.DrawTree.all_map_of_all line 22275
2587. lemma OAI.CommonBasesFPRAS.MachineCode.bankEval_all line 22282
2588. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.outputs_all line 22299
2589. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.output_some_all line 22311
2590. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.run_bound line 22326
2591. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.RealizesLaw.rest_width line 22350
2592. def OAI.CommonBasesFPRAS.MachineCode.Effect.BankMonotone line 22359
2593. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_pure line 22362
2594. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_fail line 22367
2595. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_bind line 22371
2596. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_keep_value line 22384
2597. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.run_keep_some line 22392
2598. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_keep line 22405
2599. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_letIn line 22413
2600. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_precompose line 22416
2601. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_map line 22424
2602. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_choose line 22426
2603. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.bank_draw line 22436
2604. abbrev OAI.CommonBasesFPRAS.MachineCode.Attribute line 22444
2605. def OAI.CommonBasesFPRAS.MachineCode.Attribute.Mono line 22445
2606. def OAI.CommonBasesFPRAS.MachineCode.AttrSafe line 22447
2607. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_controlled line 22449
2608. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_mono line 22452
2609. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_compose line 22455
2610. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_both line 22467
2611. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_post line 22470
2612. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_pull line 22473
2613. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_branch line 22479
2614. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_applyIf line 22496
2615. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect.EffectSafe line 22507
2616. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_pure line 22509
2617. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_precompose line 22519
2618. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_keep line 22534
2619. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_bind line 22540
2620. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_letIn line 22575
2621. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_controlled line 22586
2622. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_choose line 22588
2623. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_letControlled line 22593
2624. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_mapControlled line 22596
2625. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_preControlled line 22600
2626. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_withContext line 22603
2627. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_retainOption line 22607
2628. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_some line 22611
2629. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_loopStep line 22616
2630. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_repeat_scoped line 22632
2631. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_repeat_law line 22682
2632. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_mapControlled line 22707
2633. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_letControlled line 22714
2634. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_withContext line 22720
2635. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_retainOption line 22725
2636. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_withOptionContext line 22730
2637. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_attr line 22737
2638. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_effectAttr line 22747
2639. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_choose line 22760
2640. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_letIn line 22768
2641. def OAI.CommonBasesFPRAS.MachineCode.Effect.optionScope line 22781
2642. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.optionScope_encode line 22783
2643. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.optionScope_width line 22789
2644. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_optionContinue line 22803
2645. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_optionBind line 22834
2646. def OAI.CommonBasesFPRAS.MachineCode.contextAttr line 22843
2647. def OAI.CommonBasesFPRAS.MachineCode.weightAttr line 22844
2648. lemma OAI.CommonBasesFPRAS.MachineCode.contextAttr_mono line 22845
2649. lemma OAI.CommonBasesFPRAS.MachineCode.weightAttr_mono line 22846
2650. lemma OAI.CommonBasesFPRAS.MachineCode.attr_weight line 22847
2651. def OAI.CommonBasesFPRAS.MachineCode.acceptanceAttr line 22849
2652. lemma OAI.CommonBasesFPRAS.MachineCode.acceptanceAttr_mono line 22850
2653. lemma OAI.CommonBasesFPRAS.MachineCode.attr_acceptance line 22851
2654. def OAI.CommonBasesFPRAS.MachineCode.Effect.offerAttr line 22865
2655. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.offerAttr_mono line 22866
2656. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_offerCore line 22867
2657. def OAI.CommonBasesFPRAS.MachineCode.Effect.pairOfferAttr line 22879
2658. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.pairOfferAttr_mono line 22880
2659. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_offer line 22881
2660. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_activeStep line 22891
2661. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_step line 22897
2662. lemma OAI.CommonBasesFPRAS.MachineCode.width_stateEncode line 22912
2663. lemma OAI.CommonBasesFPRAS.MachineCode.width_sampleEncode line 22915
2664. lemma OAI.CommonBasesFPRAS.MachineCode.width_observation line 22923
2665. lemma OAI.CommonBasesFPRAS.MachineCode.width_history_observed line 22931
2666. structure OAI.CommonBasesFPRAS.MachineCode.SamplerModel line 22945
2667. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.tau line 22957
2668. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.cap line 22958
2669. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.Bounded line 22959
2670. abbrev OAI.CommonBasesFPRAS.MachineCode.SamplerModel.Hist line 22961
2671. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.histValue line 22962
2672. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.weightContext line 22964
2673. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.weightValue line 22966
2674. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.restartContext line 22968
2675. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.restartValue line 22970
2676. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.phaseValue line 22972
2677. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.width_histValue line 22974
2678. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.width_weightValue line 22982
2679. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.width_restartValue line 22994
2680. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.width_phaseValue line 23010
2681. def OAI.CommonBasesFPRAS.MachineCode.sourceWidthPoly line 23028
2682. lemma OAI.CommonBasesFPRAS.MachineCode.eval_sourceWidthPoly line 23031
2683. def OAI.CommonBasesFPRAS.MachineCode.weightScope line 23034
2684. lemma OAI.CommonBasesFPRAS.MachineCode.weightScope_width line 23037
2685. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_step line 23043
2686. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_storedStep line 23049
2687. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_storedStep line 23061
2688. lemma OAI.CommonBasesFPRAS.DrawTree.all_of_forall line 23071
2689. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_hitStep line 23081
2690. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect.SearchData line 23100
2691. def OAI.CommonBasesFPRAS.MachineCode.Effect.searchScope line 23101
2692. def OAI.CommonBasesFPRAS.MachineCode.Effect.searchInputScope line 23102
2693. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.searchScope_width line 23106
2694. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.searchEncode_scope line 23113
2695. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_repeatHit line 23120
2696. def OAI.CommonBasesFPRAS.MachineCode.Effect.traceScope line 23154
2697. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.traceScope_width line 23156
2698. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_trace line 23164
2699. lemma OAI.CommonBasesFPRAS.MachineCode.attr_rangeCode line 23179
2700. lemma OAI.CommonBasesFPRAS.MachineCode.attr_powCode line 23181
2701. lemma OAI.CommonBasesFPRAS.MachineCode.attr_paddedBits line 23185
2702. lemma OAI.CommonBasesFPRAS.MachineCode.attr_plainDecode line 23195
2703. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_plain line 23199
2704. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_plain line 23213
2705. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.Bounded.mono line 23223
2706. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartScope line 23229
2707. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.restartScope_width line 23232
2708. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_traceAt line 23237
2709. def OAI.CommonBasesFPRAS.MachineCode.Effect.traceRepeatScope line 23247
2710. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartOptWidth line 23250
2711. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.restartOptWidth_bound line 23252
2712. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_repeatTrace line 23260
2713. def OAI.CommonBasesFPRAS.MachineCode.Effect.iterateTraceScope line 23291
2714. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.iterateTraceScope_width line 23293
2715. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_iterateTrace line 23301
2716. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_restartTick line 23311
2717. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.restartInput line 23330
2718. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.width_restartInput line 23332
2719. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartRepeatScope line 23349
2720. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_restartRepeat line 23352
2721. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartInputScope line 23374
2722. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.restartInputScope_width line 23377
2723. def OAI.CommonBasesFPRAS.MachineCode.Effect.restartAfterPlainScope line 23381
2724. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.restartAfterPlainScope_width line 23384
2725. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_restart line 23394
2726. def OAI.CommonBasesFPRAS.MachineCode.SamplerModel.phaseState line 23419
2727. lemma OAI.CommonBasesFPRAS.MachineCode.SamplerModel.width_phaseState line 23422
2728. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseScope line 23432
2729. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.phaseScope_width line 23434
2730. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_phaseRestart line 23439
2731. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_start line 23454
2732. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseStateScope line 23457
2733. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.phaseStateScope_width line 23460
2734. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_phaseStep line 23464
2735. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.repeatSample_length line 23480
2736. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect.SampleNodeData line 23491
2737. abbrev OAI.CommonBasesFPRAS.MachineCode.Effect.SampleAccData line 23492
2738. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleAccValue line 23493
2739. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleAccWidth line 23496
2740. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.sampleAccValue_width line 23499
2741. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleAccScope line 23516
2742. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.sampleAccScope_width line 23520
2743. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_sampleTick line 23524
2744. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleRepeatScope line 23534
2745. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_sampleRepeat line 23537
2746. def OAI.CommonBasesFPRAS.MachineCode.Effect.sampleInputScope line 23562
2747. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.sampleInputScope_width line 23564
2748. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_sampleCode line 23572
2749. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_phaseSample line 23581
2750. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_mapStep line 23598
2751. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_mapFold line 23611
2752. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_mapWith line 23665
2753. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_allRange line 23675
2754. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_pairPositive line 23695
2755. lemma OAI.CommonBasesFPRAS.MachineCode.attr_slotRow line 23699
2756. lemma OAI.CommonBasesFPRAS.MachineCode.attr_slotsPositive line 23707
2757. lemma OAI.CommonBasesFPRAS.MachineCode.attr_prefixPositive line 23715
2758. lemma OAI.CommonBasesFPRAS.MachineCode.attr_historyPositive line 23723
2759. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_chooseScoped line 23755
2760. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.oracleSafe_some line 23763
2761. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.attr_positiveTest line 23767
2762. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_positiveTest line 23773
2763. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_phaseNone line 23779
2764. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_phase line 23781
2765. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_witness line 23797
2766. def OAI.CommonBasesFPRAS.MachineCode.Expression.weightedPlainCode line 23808
2767. def OAI.CommonBasesFPRAS.MachineCode.Expression.weightedListCode line 23811
2768. def OAI.CommonBasesFPRAS.MachineCode.Expression.weightedMeanCode line 23813
2769. def OAI.CommonBasesFPRAS.MachineCode.Expression.plainMeanCode line 23815
2770. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratioCode line 23817
2771. lemma OAI.CommonBasesFPRAS.MachineCode.weightedPlain_nonneg line 23823
2772. lemma OAI.CommonBasesFPRAS.MachineCode.weightedPlainCode_source line 23829
2773. lemma OAI.CommonBasesFPRAS.MachineCode.weightedListCode_source line 23841
2774. lemma OAI.CommonBasesFPRAS.MachineCode.weightedMeanCode_source line 23847
2775. lemma OAI.CommonBasesFPRAS.MachineCode.plainMeanCode_source line 23861
2776. lemma OAI.CommonBasesFPRAS.MachineCode.ratioCode_source line 23871
2777. def OAI.CommonBasesFPRAS.MachineCode.Effect.historyTickCode line 23893
2778. def OAI.CommonBasesFPRAS.MachineCode.Effect.historyTickTree line 23897
2779. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.optionRepeat_none line 23899
2780. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.iterate_history line 23904
2781. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_historyTickCode line 23916
2782. def OAI.CommonBasesFPRAS.MachineCode.Effect.historyCode line 23929
2783. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.law_historyCode line 23931
2784. def OAI.CommonBasesFPRAS.MachineCode.Expression.historyAtCode line 23944
2785. def OAI.CommonBasesFPRAS.MachineCode.Expression.ratioAtCode line 23945
2786. def OAI.CommonBasesFPRAS.MachineCode.Expression.estimateCode line 23948
2787. def OAI.CommonBasesFPRAS.MachineCode.Expression.guardCode line 23952
2788. lemma OAI.CommonBasesFPRAS.MachineCode.historyAtCode_source line 23957
2789. lemma OAI.CommonBasesFPRAS.MachineCode.ratio_nonnegative line 23965
2790. lemma OAI.CommonBasesFPRAS.MachineCode.ratioAtCode_source line 23984
2791. lemma OAI.CommonBasesFPRAS.MachineCode.estimateCode_source line 23992
2792. lemma OAI.CommonBasesFPRAS.MachineCode.guardCode_source line 24022
2793. def OAI.CommonBasesFPRAS.MachineCode.Effect.finalGuardCode line 24042
2794. def OAI.CommonBasesFPRAS.MachineCode.Effect.algorithmHistoryCode line 24044
2795. def OAI.CommonBasesFPRAS.MachineCode.Effect.algorithmCode line 24046
2796. lemma OAI.CommonBasesFPRAS.MachineCode.algorithmHistoryCode_source line 24053
2797. lemma OAI.CommonBasesFPRAS.MachineCode.finalGuardCode_source line 24064
2798. lemma OAI.CommonBasesFPRAS.MachineCode.algorithmCode_source line 24074
2799. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.history_length line 24087
2800. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_historyTick line 24102
2801. def OAI.CommonBasesFPRAS.MachineCode.Effect.phaseOptWidth line 24105
2802. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.phaseOptWidth_bound line 24107
2803. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.historyTick_source line 24122
2804. def OAI.CommonBasesFPRAS.MachineCode.Effect.historyRepeatScope line 24134
2805. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_historyRepeat line 24136
2806. def OAI.CommonBasesFPRAS.MachineCode.Effect.historyInputScope line 24173
2807. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.historyInputScope_width line 24175
2808. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_historyCode line 24185
2809. def OAI.CommonBasesFPRAS.MachineCode.Effect.algorithmScope line 24193
2810. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.algorithmScope_width line 24195
2811. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_algorithmHistory line 24201
2812. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_fst line 24212
2813. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_snd line 24222
2814. lemma OAI.CommonBasesFPRAS.MachineCode.attrSafe_shift line 24233
2815. lemma OAI.CommonBasesFPRAS.MachineCode.attr_anneal line 24238
2816. lemma OAI.CommonBasesFPRAS.MachineCode.attr_weightedPlain line 24240
2817. lemma OAI.CommonBasesFPRAS.MachineCode.attr_weightedList line 24251
2818. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_plainMean line 24260
2819. lemma OAI.CommonBasesFPRAS.MachineCode.attr_weightedMean line 24263
2820. lemma OAI.CommonBasesFPRAS.MachineCode.attr_ratio line 24268
2821. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_historyAt line 24272
2822. lemma OAI.CommonBasesFPRAS.MachineCode.attr_ratioAt line 24273
2823. lemma OAI.CommonBasesFPRAS.MachineCode.attr_pow line 24280
2824. def OAI.CommonBasesFPRAS.MachineCode.estimatorAttr line 24284
2825. lemma OAI.CommonBasesFPRAS.MachineCode.estimatorAttr_mono line 24286
2826. lemma OAI.CommonBasesFPRAS.MachineCode.attr_estimate line 24288
2827. lemma OAI.CommonBasesFPRAS.MachineCode.attr_guard line 24310
2828. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_optionMap line 24318
2829. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_guard line 24340
2830. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_finalGuard line 24346
2831. lemma OAI.CommonBasesFPRAS.MachineCode.Effect.safe_algorithm line 24362
2832. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_mapStep line 24384
2833. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_mapFold line 24398
2834. lemma OAI.CommonBasesFPRAS.MachineCode.oracleSafe_mapWith line 24442
2835. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.InsertState line 24458
2836. def OAI.CommonBasesFPRAS.MachineCode.Expression.insertStep line 24459
2837. def OAI.CommonBasesFPRAS.MachineCode.Expression.insertInit line 24464
2838. def OAI.CommonBasesFPRAS.MachineCode.Expression.insertRatCode line 24467
2839. def OAI.CommonBasesFPRAS.MachineCode.Expression.sortRatCode line 24469
2840. def OAI.CommonBasesFPRAS.MachineCode.Expression.medianCode line 24471
2841. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_insertStep line 24474
2842. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_insertRatCode line 24482
2843. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_sortRatCode line 24508
2844. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_medianCode line 24527
2845. lemma OAI.CommonBasesFPRAS.MachineCode.run_insertStep_raw line 24543
2846. lemma OAI.CommonBasesFPRAS.MachineCode.insertFold_width line 24550
2847. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_insertStep line 24564
2848. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_insertFold line 24565
2849. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_insertRat line 24578
2850. lemma OAI.CommonBasesFPRAS.MachineCode.insertRat_width line 24581
2851. lemma OAI.CommonBasesFPRAS.MachineCode.sortFold_width line 24595
2852. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_sortFold line 24610
2853. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_sortRat line 24619
2854. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_median line 24622
2855. def OAI.CommonBasesFPRAS.MachineCode.Expression.optionalRatCode line 24628
2856. def OAI.CommonBasesFPRAS.MachineCode.Expression.singleCode line 24629
2857. def OAI.CommonBasesFPRAS.MachineCode.Expression.amplifiedCode line 24631
2858. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_optionalRatCode line 24633
2859. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_singleCode line 24636
2860. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_amplifiedCode line 24646
2861. lemma OAI.CommonBasesFPRAS.MachineCode.safe_single line 24669
2862. def OAI.CommonBasesFPRAS.MachineCode.amplificationScope line 24672
2863. lemma OAI.CommonBasesFPRAS.MachineCode.amplificationScope_width line 24674
2864. lemma OAI.CommonBasesFPRAS.MachineCode.safe_amplified line 24682
2865. abbrev OAI.CommonBasesFPRAS.MachineCode.FrozenData line 24710
2866. def OAI.CommonBasesFPRAS.MachineCode.frozenValue line 24711
2867. def OAI.CommonBasesFPRAS.MachineCode.Expression.natPow line 24715
2868. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_natPow line 24718
2869. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_natPow line 24723
2870. def OAI.CommonBasesFPRAS.MachineCode.Expression.sumE line 24728
2871. def OAI.CommonBasesFPRAS.MachineCode.Expression.prodE line 24729
2872. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_sumE line 24730
2873. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_prodE line 24733
2874. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_sumE line 24736
2875. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_prodE line 24738
2876. def OAI.CommonBasesFPRAS.MachineCode.Expression.ceilDivCode line 24741
2877. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_ceilDivCode line 24743
2878. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_ceilDivCode line 24750
2879. def OAI.CommonBasesFPRAS.MachineCode.Expression.lengthNatCode line 24755
2880. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_lengthNatCode line 24756
2881. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_lengthNatCode line 24760
2882. def OAI.CommonBasesFPRAS.MachineCode.Expression.annealLengthCode line 24765
2883. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_annealLengthCode line 24767
2884. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_annealLengthCode line 24770
2885. def OAI.CommonBasesFPRAS.MachineCode.Expression.sampleCountCode line 24772
2886. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_sampleCountCode line 24776
2887. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_sampleCountCode line 24781
2888. def OAI.CommonBasesFPRAS.MachineCode.Expression.tauCode line 24801
2889. def OAI.CommonBasesFPRAS.MachineCode.Expression.capCode line 24804
2890. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_tauCode line 24807
2891. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_capCode line 24812
2892. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_tauCode line 24819
2893. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_capCode line 24823
2894. def OAI.CommonBasesFPRAS.MachineCode.Expression.chunkValues line 24829
2895. def OAI.CommonBasesFPRAS.MachineCode.Expression.chunkStep line 24831
2896. def OAI.CommonBasesFPRAS.MachineCode.Expression.chunksCode line 24833
2897. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_chunkStep line 24835
2898. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_chunksCode line 24841
2899. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.chunkValues_zero line 24848
2900. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.chunkValues_succ line 24849
2901. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.chunkValues_flatten line 24856
2902. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.chunkValues_ofFn line 24864
2903. lemma OAI.CommonBasesFPRAS.MachineCode.controlled_chunkStep line 24872
2904. lemma OAI.CommonBasesFPRAS.MachineCode.attr_chunksCode line 24875
2905. lemma OAI.CommonBasesFPRAS.MachineCode.ceil_nat_ratio line 24886
2906. lemma OAI.CommonBasesFPRAS.MachineCode.inverse_ceiling_input line 24898
2907. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenN line 24909
2908. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenL line 24910
2909. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenE line 24912
2910. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenSamples line 24913
2911. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenParams line 24915
2912. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenReps line 24918
2913. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.Recipe3 line 24921
2914. def OAI.CommonBasesFPRAS.MachineCode.Expression.drawsCode line 24922
2915. def OAI.CommonBasesFPRAS.MachineCode.Expression.wordBoundCode line 24928
2916. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenRecipe3 line 24933
2917. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenDraws line 24934
2918. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenWordBound line 24935
2919. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.BankShape line 24936
2920. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.PreparedData line 24937
2921. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenPrepared line 24938
2922. def OAI.CommonBasesFPRAS.MachineCode.Expression.bitCountCode line 24940
2923. def OAI.CommonBasesFPRAS.MachineCode.Expression.frozenBitCount line 24942
2924. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenN line 24944
2925. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenL line 24946
2926. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenE line 24951
2927. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenSamples line 24955
2928. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenParams line 24959
2929. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenReps line 24963
2930. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_drawsCode line 24967
2931. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_wordBoundCode line 24972
2932. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenRecipe3 line 24976
2933. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenPrepared line 24979
2934. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_bitCountCode line 24986
2935. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_frozenBitCount line 24990
2936. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenN line 24994
2937. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenL line 24995
2938. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenE line 25001
2939. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenSamples line 25005
2940. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenParams line 25012
2941. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenReps line 25020
2942. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_drawsCode line 25024
2943. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_wordBoundCode line 25029
2944. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenRecipe3 line 25033
2945. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenPrepared line 25039
2946. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_bitCountCode line 25047
2947. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_frozenBitCount line 25048
2948. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.Shape3 line 25054
2949. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.Shape4 line 25055
2950. def OAI.CommonBasesFPRAS.MachineCode.Expression.rowsCode line 25057
2951. def OAI.CommonBasesFPRAS.MachineCode.Expression.bankCode line 25059
2952. def OAI.CommonBasesFPRAS.MachineCode.Expression.banksCode line 25062
2953. def OAI.CommonBasesFPRAS.MachineCode.Expression.shape4Code line 25066
2954. def OAI.CommonBasesFPRAS.MachineCode.Expression.reshapeCode line 25068
2955. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_rowsCode line 25070
2956. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_bankCode line 25074
2957. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_banksCode line 25083
2958. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.run_shape4Code line 25094
2959. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.controlled_shape4Code line 25096
2960. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.attr_rowsCode line 25097
2961. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.attr_bankCode line 25100
2962. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.attr_banksCode line 25120
2963. lemma OAI.CommonBasesFPRAS.MachineCode.Expression.attr_reshapeCode line 25140
2964. def OAI.CommonBasesFPRAS.MachineCode.Expression.preambleCode line 25148
2965. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.RawData line 25150
2966. abbrev OAI.CommonBasesFPRAS.MachineCode.Expression.AmplifyInput line 25151
2967. def OAI.CommonBasesFPRAS.MachineCode.Expression.reshapePrepared line 25152
2968. def OAI.CommonBasesFPRAS.MachineCode.Expression.finishCode line 25154
2969. def OAI.CommonBasesFPRAS.MachineCode.Expression.postambleCode line 25156
2970. lemma OAI.CommonBasesFPRAS.MachineCode.safe_preamble line 25158
2971. def OAI.CommonBasesFPRAS.MachineCode.rawScope line 25167
2972. lemma OAI.CommonBasesFPRAS.MachineCode.algorithmScope_mono line 25170
2973. lemma OAI.CommonBasesFPRAS.MachineCode.safe_reshapePrepared line 25174
2974. def OAI.CommonBasesFPRAS.MachineCode.finishScope line 25184
2975. lemma OAI.CommonBasesFPRAS.MachineCode.safe_finish line 25186
2976. lemma OAI.CommonBasesFPRAS.MachineCode.safe_postamble line 25199
2977. def OAI.CommonBasesFPRAS.MachineCode.coinPush line 25213
2978. lemma OAI.CommonBasesFPRAS.MachineCode.runs_coinPush line 25214
2979. def OAI.CommonBasesFPRAS.MachineCode.sampledWord line 25223
2980. lemma OAI.CommonBasesFPRAS.MachineCode.sampledWord_length line 25226
2981. lemma OAI.CommonBasesFPRAS.MachineCode.sampledWord_get line 25230
2982. lemma OAI.CommonBasesFPRAS.MachineCode.sampledWord_ofFn line 25244
2983. lemma OAI.CommonBasesFPRAS.MachineCode.runs_coinLoop line 25251
2984. lemma OAI.CommonBasesFPRAS.MachineCode.runs_pack_any line 25276
2985. lemma OAI.CommonBasesFPRAS.MachineCode.runs_move_any line 25286
2986. def OAI.CommonBasesFPRAS.MachineCode.sixRegs line 25303
2987. def OAI.CommonBasesFPRAS.MachineCode.inputPack line 25306
2988. def OAI.CommonBasesFPRAS.MachineCode.inputTime line 25309
2989. lemma OAI.CommonBasesFPRAS.MachineCode.runs_inputPack line 25312
2990. lemma OAI.CommonBasesFPRAS.MachineCode.inputTime_bound line 25350
2991. lemma OAI.CommonBasesFPRAS.MachineCode.frozen_width line 25354
2992. lemma OAI.CommonBasesFPRAS.MachineCode.initialConfig_state line 25359
2993. def OAI.CommonBasesFPRAS.MachineCode.preparedValue line 25364
2994. def OAI.CommonBasesFPRAS.MachineCode.rawValue line 25368
2995. def OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.pow line 25373
2996. lemma OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.eval_pow line 25376
2997. def OAI.CommonBasesFPRAS.MachineCode.masterParameter line 25382
2998. def OAI.CommonBasesFPRAS.MachineCode.atomPoly line 25384
2999. def OAI.CommonBasesFPRAS.MachineCode.tauPoly line 25385
3000. def OAI.CommonBasesFPRAS.MachineCode.capPoly line 25388
3001. def OAI.CommonBasesFPRAS.MachineCode.fairPoly line 25390
3002. def OAI.CommonBasesFPRAS.MachineCode.sourceEnvelope line 25391
3003. def OAI.CommonBasesFPRAS.MachineCode.scopeEnvelope line 25393
3004. lemma OAI.CommonBasesFPRAS.MachineCode.master_pos line 25394
3005. lemma OAI.CommonBasesFPRAS.MachineCode.rank_le_ground line 25396
3006. lemma OAI.CommonBasesFPRAS.MachineCode.master_fields line 25401
3007. lemma OAI.CommonBasesFPRAS.MachineCode.atom_ge line 25407
3008. lemma OAI.CommonBasesFPRAS.MachineCode.recipe_atom_bounds line 25411
3009. lemma OAI.CommonBasesFPRAS.MachineCode.envelope_parameters line 25435
3010. lemma OAI.CommonBasesFPRAS.MachineCode.width_six line 25472
3011. lemma OAI.CommonBasesFPRAS.MachineCode.width_frozen line 25479
3012. lemma OAI.CommonBasesFPRAS.MachineCode.width_prepared_bound line 25484
3013. lemma OAI.CommonBasesFPRAS.MachineCode.scopeEnvelope_ge line 25503
3014. lemma OAI.CommonBasesFPRAS.MachineCode.rawValue_scope line 25506
3015. lemma OAI.CommonBasesFPRAS.MachineCode.frozen_preamble_scope line 25525
3016. lemma OAI.CommonBasesFPRAS.MachineCode.compile_safe_bound line 25542
3017. def OAI.CommonBasesFPRAS.MachineCode.compiledMajorant line 25556
3018. lemma OAI.CommonBasesFPRAS.MachineCode.compile_majorant line 25559
3019. lemma OAI.CommonBasesFPRAS.MachineCode.frozen_uniform_safe line 25567
3020. lemma OAI.CommonBasesFPRAS.MachineCode.SizePolynomial.monomial_bound line 25581
3021. def OAI.CommonBasesFPRAS.MachineCode.outRegs line 25591
3022. def OAI.CommonBasesFPRAS.MachineCode.outputPack line 25592
3023. def OAI.CommonBasesFPRAS.MachineCode.outputTime line 25593
3024. lemma OAI.CommonBasesFPRAS.MachineCode.runs_outputPack line 25594
3025. lemma OAI.CommonBasesFPRAS.MachineCode.outputTime_bound line 25608
3026. lemma OAI.CommonBasesFPRAS.MachineCode.runs_coinLoop_regs line 25611
3027. lemma OAI.CommonBasesFPRAS.MachineCode.runs_randomPack line 25618
3028. def OAI.CommonBasesFPRAS.MachineCode.pipeline line 25624
3029. def OAI.CommonBasesFPRAS.MachineCode.pipelineTime line 25627
3030. lemma OAI.CommonBasesFPRAS.MachineCode.runs_pipeline line 25629
3031. def OAI.CommonBasesFPRAS.MachineCode.physicalWord line 25658
3032. lemma OAI.CommonBasesFPRAS.MachineCode.sampledWord_physical line 25660
3033. def OAI.CommonBasesFPRAS.MachineCode.physicalPosition line 25667
3034. lemma OAI.CommonBasesFPRAS.MachineCode.physicalPosition_injective line 25669
3035. lemma OAI.CommonBasesFPRAS.MachineCode.physicalWord_finite line 25678
3036. lemma OAI.CommonBasesFPRAS.MachineCode.physicalWord_law line 25683
3037. def OAI.CommonBasesFPRAS.MachineCode.terminalState line 25688
3038. lemma OAI.CommonBasesFPRAS.MachineCode.runs_terminal line 25690
3039. lemma OAI.CommonBasesFPRAS.MachineCode.input_state line 25699
3040. lemma OAI.CommonBasesFPRAS.MachineCode.terminal_rational line 25702
3041. def OAI.CommonBasesFPRAS.MachineCode.pipelineBudget line 25707
3042. lemma OAI.CommonBasesFPRAS.MachineCode.pipeline_budget line 25708
3043. lemma OAI.CommonBasesFPRAS.MachineCode.pipeline_budgeted line 25718
3044. lemma OAI.CommonBasesFPRAS.MachineCode.pipeline_budgeted_length line 25762
3045. def OAI.CommonBasesFPRAS.MachineCode.totalResourcePoly line 25781
3046. lemma OAI.CommonBasesFPRAS.MachineCode.totalResourcePoly_budget line 25784
3047. def OAI.CommonBasesFPRAS.MachineCode.fprasBlock line 25799
3048. def OAI.CommonBasesFPRAS.MachineCode.treeBankOutput line 25803
3049. def OAI.CommonBasesFPRAS.MachineCode.treeBanksOutput line 25805
3050. lemma OAI.CommonBasesFPRAS.MachineCode.treeBankOutput_all line 25807
3051. lemma OAI.CommonBasesFPRAS.MachineCode.treeBanksOutput_all line 25818
3052. lemma OAI.CommonBasesFPRAS.MachineCode.reindexed_bank_law line 25831
3053. lemma OAI.CommonBasesFPRAS.MachineCode.reindexed_banks_law line 25838
3054. lemma OAI.CommonBasesFPRAS.MachineCode.canonicalTree_all line 25848
3055. lemma OAI.CommonBasesFPRAS.MachineCode.bitMatrix_apply line 25861
3056. lemma OAI.CommonBasesFPRAS.MachineCode.ofFn_bitMatrix line 25863
3057. lemma OAI.CommonBasesFPRAS.MachineCode.chunks_bitMatrix line 25875
3058. lemma OAI.CommonBasesFPRAS.MachineCode.run_banksCode_four line 25878
3059. lemma OAI.CommonBasesFPRAS.MachineCode.ofFn_finCongr line 25885
3060. lemma OAI.CommonBasesFPRAS.MachineCode.run_reshapeCode_four line 25889
3061. lemma OAI.CommonBasesFPRAS.MachineCode.run_reshapeCode_cast line 25895
3062. def OAI.CommonBasesFPRAS.MachineCode.bankReshapeEquiv line 25903
3063. lemma OAI.CommonBasesFPRAS.MachineCode.run_reshapeCode_equiv line 25906
3064. lemma OAI.CommonBasesFPRAS.MachineCode.reshape_count line 25911
3065. def OAI.CommonBasesFPRAS.MachineCode.reshapeWordEquiv line 25921
3066. lemma OAI.CommonBasesFPRAS.MachineCode.run_reshapeCode_source line 25926
3067. lemma OAI.CommonBasesFPRAS.MachineCode.run_preamble_generic line 25937
3068. lemma OAI.CommonBasesFPRAS.MachineCode.run_preambleCode line 25944
3069. lemma OAI.CommonBasesFPRAS.MachineCode.run_reshapePrepared_generic line 25949
3070. lemma OAI.CommonBasesFPRAS.MachineCode.run_reshapePrepared line 25954
3071. def OAI.CommonBasesFPRAS.MachineCode.OutputCertificate line 25962
3072. lemma OAI.CommonBasesFPRAS.MachineCode.output_certificate line 25969
3073. lemma OAI.CommonBasesFPRAS.MachineCode.encode_natPair line 26021
3074. lemma OAI.CommonBasesFPRAS.MachineCode.encode_rawValue line 26022
3075. lemma OAI.CommonBasesFPRAS.MachineCode.width_natPair line 26024
3076. lemma OAI.CommonBasesFPRAS.MachineCode.frozen_machine line 26027
3077. lemma OAI.CommonBasesFPRAS.MachineCode.physical_accuracy line 26070
3078. theorem OAI.common_bases_fpras line 26093

      Distinct definitions of this name: ComparatorChallenges/CommonBasesFPRAS.lean:128 (same statement text; different proof or body). Qualify references as OAI.common_bases_fpras@path.