OAI/LinearAlgebra/MatrixFields/Certificates/Four3_0_5.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Contains line 238
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Zero line 242
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Probs_sound line 245
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Half line 255
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Half_sound line 259
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Value line 286
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_1_5LogWitness line 287
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_1_5Log line 288
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_1_5Log_sound line 289
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_1_5 line 293
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_1_5_sound line 294
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_2_4LogWitness line 296
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_2_4Log line 297
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_2_4Log_sound line 298
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_2_4 line 302
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_2_4_sound line 303
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_3_4LogWitness line 305
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_3_4Log line 306
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_3_4Log_sound line 307
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_3_4 line 311
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_3_4_sound line 312
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_2LogWitness line 314
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_2Log line 315
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_2Log_sound line 316
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_2 line 320
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_2_sound line 321
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_3LogWitness line 323
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_3Log line 324
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_3Log_sound line 325
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_3 line 329
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_4_3_sound line 330
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_5_1LogWitness line 332
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_5_1Log line 333
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_5_1Log_sound line 334
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_5_1 line 338
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5E_5_1_sound line 339
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Terms line 341
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Terms_sound line 350
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Entropy line 361
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Entropy_sound line 362
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Labels line 364
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Labels_sound line 365
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Four line 370
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5Four_sound line 371
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Value line 373
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_4_0LogWitness line 374
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_4_0Log line 375
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_4_0Log_sound line 376
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_4_0 line 380
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_4_0_sound line 381
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_2_1LogWitness line 383
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_2_1Log line 384
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_2_1Log_sound line 385
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_2_1 line 389
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_2_1_sound line 390
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_3_1LogWitness line 392
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_3_1Log line 393
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_3_1Log_sound line 394
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_3_1 line 398
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_3_1_sound line 399
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_2LogWitness line 401
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_2Log line 402
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_2Log_sound line 403
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_2 line 407
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_2_sound line 408
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_3LogWitness line 410
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_3Log line 411
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_3Log_sound line 412
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_3 line 416
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_1_3_sound line 417
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_0_4LogWitness line 419
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_0_4Log line 420
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_0_4Log_sound line 421
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_0_4 line 425
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0E_0_4_sound line 426
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Terms line 428
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Terms_sound line 437
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Entropy line 448
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Entropy_sound line 449
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Mass line 451
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0Mass_sound line 452
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0MassTermLogWitness line 454
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0MassTermLog line 455
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0MassTermLog_sound line 456
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0MassTerm line 460
98. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0MassTerm_sound line 461
99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0H line 463
100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H0H_sound line 464
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Value line 466
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1E_0_0Log line 467
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1E_0_0Log_sound line 468
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1E_0_0 line 470
105. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1E_0_0_sound line 471
106. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Terms line 473
107. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Terms_sound line 477
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Entropy line 488
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Entropy_sound line 489
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Mass line 491
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1Mass_sound line 492
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1MassTermLog line 494
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1MassTermLog_sound line 495
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1MassTerm line 497
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1MassTerm_sound line 498
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1H line 500
117. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H1H_sound line 501
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Value line 503
119. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_1_5LogWitness line 504
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_1_5Log line 505
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_1_5Log_sound line 506
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_1_5 line 510
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_1_5_sound line 511
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_2_4LogWitness line 513
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_2_4Log line 514
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_2_4Log_sound line 515
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_2_4 line 519
128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_2_4_sound line 520
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_3_4LogWitness line 522
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_3_4Log line 523
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_3_4Log_sound line 524
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_3_4 line 528
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_3_4_sound line 529
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_2LogWitness line 531
135. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_2Log line 532
136. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_2Log_sound line 533
137. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_2 line 537
138. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_2_sound line 538
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_3LogWitness line 540
140. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_3Log line 541
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_3Log_sound line 542
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_3 line 546
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_4_3_sound line 547
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_5_1LogWitness line 549
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_5_1Log line 550
146. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_5_1Log_sound line 551
147. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_5_1 line 555
148. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2E_5_1_sound line 556
149. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Terms line 558
150. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Terms_sound line 567
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Entropy line 578
152. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Entropy_sound line 579
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Mass line 581
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2Mass_sound line 582
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2MassTermLogWitness line 584
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2MassTermLog line 585
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2MassTermLog_sound line 586
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2MassTerm line 590
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2MassTerm_sound line 591
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2H line 593
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_0_5H2H_sound line 594