OAI/LinearAlgebra/MatrixFields/Histories/HistoryChildLaws.lean

GitHub source file

245 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatrixAllFields.MatrixMultiplication.Staggering.Capacity line 20
2. def OAI.MatrixAllFields.MatrixMultiplication.Staggering.totalCapacity line 22
3. def OAI.MatrixAllFields.MatrixMultiplication.Staggering.balanceFraction line 25
4. def OAI.MatrixAllFields.MatrixMultiplication.Staggering.thirdCapacity line 28
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.balanceFraction_pos line 31
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.sum_balanceFraction line 39
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.thirdCapacity_eq line 49
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.balanced line 57
9. def OAI.MatrixAllFields.MatrixMultiplication.Staggering.minCapacity line 63
10. def OAI.MatrixAllFields.MatrixMultiplication.Staggering.maxCapacity line 65
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.minCapacity_pos line 67
12. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.minCapacity_le_maxCapacity line 71
13. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.minCapacity_complement line 74
14. def OAI.MatrixAllFields.MatrixMultiplication.Staggering.boundaryDeficit line 79
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.boundaryDeficit_eq_ranges line 83
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.boundaryDeficit_nonneg line 96
17. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.finite_schedule_yield line 102
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Staggering.physical_order_unique line 110
19. def OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.lotTick line 141
20. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.lotTick_lt line 143
21. def OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.stageActive line 150
22. instance OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.(instance at line 153) line 153
23. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.stageActive_iff_unique_lot line 156
24. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.lot_active_at_its_tick line 172
25. def OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.tickCapacity line 178
26. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.tickCapacity_first line 183
27. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.tickCapacity_second line 189
28. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.tickCapacity_interior line 196
29. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.tickCapacity_penultimate line 205
30. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.tickCapacity_last line 211
31. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.sum_tick_minima line 217
32. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.finite_schedule_yield line 252
33. theorem OAI.MatrixAllFields.MatrixMultiplication.FiniteSchedule.fixed_lot_boundary_limit line 259
34. abbrev OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.PhysicalOrder line 296
35. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.card_physical_orders line 298
36. def OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.placementAmount line 301
37. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.placementAmount_eq line 303
38. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.sum_placementAmount line 306
39. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.placement_has_unique_order line 313
40. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.sum_selected_placement line 319
41. def OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.aggregateCapacity line 337
42. def OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.perPhysicalOrderCapacity line 340
43. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.perPhysicalOrderCapacity_apply line 346
44. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.perPhysicalOrderCapacity_eq line 359
45. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.minCapacity_mul line 367
46. theorem OAI.MatrixAllFields.MatrixMultiplication.PhysicalOrders.sum_physical_order_minima line 372
47. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Allocation line 403
48. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Placement line 408
49. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Initial line 409
50. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialShape line 411
51. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialShape_mem line 413
52. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.InitialPositive line 416
53. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ASplit line 418
54. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.AfterA line 419
55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aSplit line 421
56. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.halfShape line 424
57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aShape line 427
58. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aSplit_mem line 430
59. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aShape_mem line 433
60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageA_children_size line 437
61. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aShape_size line 440
62. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.APositive line 443
63. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.BSplit line 444
64. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.AfterB line 445
65. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bSplit line 447
66. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bShape line 450
67. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bSplit_mem line 453
68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bShape_mem line 456
69. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageB_children_size line 460
70. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bShape_size line 463
71. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.BPositive line 466
72. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.PartC line 467
73. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.AfterC line 468
74. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cParameterParent line 470
75. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cShapeParent line 471
76. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cSplit line 473
77. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cShape line 475
78. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cShape_zero line 478
79. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialPositiveFintype line 486
80. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aPositiveFintype line 489
81. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bPositiveFintype line 492
82. inductive OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.CanonicalHistory line 495
83. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.History line 503
84. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialAmount line 505
85. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aAmount line 506
86. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bAmount line 508
87. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.partAmount line 510
88. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cAmount line 512
89. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalAmount line 515
90. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.amount line 522
91. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialAmount_pos line 525
92. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.aAmount_pos line 528
93. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.bAmount_pos line 531
94. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.partAmount_pos line 534
95. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cAmount_nonneg line 537
96. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.amount_nonneg line 541
97. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.placement_amount_eq line 551
98. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.sum_placement_amount line 555
99. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initial_amount_sum line 562
100. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.root_mass_sum_lot line 568
101. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.a_transition line 574
102. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.b_transition line 581
103. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.part_transition line 588
104. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.c_transition line 592
105. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.population line 596
106. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.populationLength line 599
107. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.population_cast line 602
108. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.population_zero_iff line 607
109. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initial_population_sum line 612
110. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.a_population_transition line 621
111. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.b_population_transition line 629
112. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.part_population_transition line 637
113. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.c_population_transition line 645
114. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.a_half_counts_eq line 653
115. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.b_half_counts_eq line 659
116. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.c_half_counts_eq line 665
117. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialAncestor line 691
118. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ancestrySplits line 698
119. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ancestrySubdivisions line 707
120. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.historyKey line 712
121. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.placement_preserved line 719
122. inductive OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work line 723
123. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.source line 729
124. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.stage line 734
125. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.lot line 739
126. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.halfLength line 741
127. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.parentShape line 746
128. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.Branch line 751
129. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 756) line 756
130. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.child line 759
131. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.splitShape line 765
132. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.PlacedWork line 771
133. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Active line 772
134. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.active_tick_lt line 775
135. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchPopulation line 779
136. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchPopulation_half line 783
137. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchPopulation_sum line 796
138. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.terminal line 806
139. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.resident line 813
140. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.State line 821
141. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.terminal_carries line 823
142. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.work_source_resident line 832
143. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.a_child_resident line 842
144. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.c_child_resident line 846
145. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCounts line 869
146. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCounts_sum line 873
147. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCounts_positive line 879
148. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapeCounts_at line 892
149. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.parentShape_spec line 899
150. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.splitShape_spec line 908
151. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.splitShape_le line 915
152. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.splitShape_injective line 922
153. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchShape line 929
154. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchShape_injective line 932
155. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.jointCounts line 937
156. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeCounts line 941
157. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeParentShape line 944
158. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeHalfLength line 947
159. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.jointCounts_sum line 949
160. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.jointCounts_at line 954
161. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.jointCounts_support_sum line 960
162. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.jointCounts_support_le line 967
163. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapePositionMap line 975
164. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapePositionMap_injective line 982
165. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.shapePositionMap_surjective line 992
166. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchPositionEquiv line 1001
167. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.branchPositionEquiv_shape line 1009
168. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.rootShape line 1015
169. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialJointCounts line 1018
170. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialJointCounts_sum line 1023
171. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.initialJointCounts_support line 1029
172. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.priorityPermutation line 1056
173. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.PriorityLexLE line 1059
174. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 1063) line 1063
175. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.priorityPermutation_surjective line 1067
176. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.priorityPermutation_order line 1070
177. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBRepresentatives line 1074
178. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.readInPriority line 1077
179. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBPriorityIndex line 1079
180. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBPriority line 1083
181. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBPriority_finite_spec line 1085
182. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBPriority_reads_representative line 1092
183. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBPriority_lex_first line 1096
184. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageBPriority_233 line 1102
185. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cPriorityIndex line 1108
186. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCPriorityLabel line 1111
187. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCPriorityLabel_at_part line 1114
188. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.stageCPriorityLabel_remaining_order line 1118
189. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cPriority line 1123
190. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cPriority_at_part line 1126
191. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cPriority_at_part_two line 1130
192. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.cPriority_remaining_order line 1136
193. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.priority line 1141
194. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.priority_stageA line 1146
195. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.priority_stageB line 1149
196. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.priority_stageC line 1153
197. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.PlacedWork.physicalOrder line 1157
198. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.work_placement_for_order_unique line 1160
199. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.CanonicalActive line 1164
200. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ActiveOrder line 1167
201. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalActiveEquivOrder line 1170
202. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.workAmount line 1189
203. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeAggregateCapacity line 1192
204. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalTickCapacity line 1197
205. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalTickCapacity_eq_partition line 1203
206. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.physicalTickCapacity_eq_sixth line 1213
207. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.sum_physicalTick_minima line 1220
208. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.Statistic line 1248
209. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 1253) line 1253
210. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.(instance at line 1256) line 1256
211. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.statistic line 1258
212. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.statisticWeight line 1264
213. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.statistic_weight line 1271
214. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.childLaw line 1278
215. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.childLaw_nonnegative line 1285
216. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.childLaw_normalized line 1292
217. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.childLaw_outside_support line 1302
218. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalChildShape line 1313
219. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.canonicalChildShape_branchShape line 1316
220. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.Work.halfShape_mem line 1321
221. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.placedChildLawRat line 1338
222. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.childLawRat line 1343
223. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.rightChildLawRat line 1346
224. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.placedChildLawRat_branchShape line 1349
225. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.placedChildLawRat_nonnegative line 1356
226. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.placedChildLawRat_normalized_of_pos line 1361
227. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.childLaw line 1369
228. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.rightChildLaw line 1372
229. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.ActiveStatistic line 1375
230. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.activeStatistic line 1377
231. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.leftChildLaw line 1380
232. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.rightClassChildLaw line 1384
233. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.leftChildLaw_nonnegative line 1388
234. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.rightClassChildLaw_nonnegative line 1394
235. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.leftChildLaw_normalized_of_pos line 1400
236. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistory.rightClassChildLaw_normalized_of_pos line 1409
237. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.Statistic line 1425
238. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.statistic line 1427
239. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.leftLaw line 1430
240. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.rightLaw line 1433
241. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.leftLaw_nonnegative line 1436
242. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.rightLaw_nonnegative line 1440
243. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.leftLaw_normalized line 1444
244. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.rightLaw_normalized line 1450
245. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldHistoryChildLaws.singleton_typeWindow line 1456