OAI/LinearAlgebra/MatrixFields/Certificates/Four3_5_0.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw line 16
2. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound_0 line 55
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound_1 line 82
4. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound_2 line 109
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound_3 line 136
6. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound_4 line 163
7. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound_5 line 190
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Raw_sound line 217
9. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Den line 222
10. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Den_sound line 223
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Den_pos line 228
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Probs line 229
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Contains line 238
14. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Zero line 242
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Probs_sound line 245
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Half line 255
17. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Half_sound line 259
18. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Value line 286
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_1_5LogWitness line 287
20. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_1_5Log line 288
21. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_1_5Log_sound line 289
22. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_1_5 line 293
23. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_1_5_sound line 294
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_2_4LogWitness line 296
25. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_2_4Log line 297
26. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_2_4Log_sound line 298
27. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_2_4 line 302
28. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_2_4_sound line 303
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_3_4LogWitness line 305
30. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_3_4Log line 306
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_3_4Log_sound line 307
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_3_4 line 311
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_3_4_sound line 312
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_2LogWitness line 314
35. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_2Log line 315
36. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_2Log_sound line 316
37. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_2 line 320
38. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_2_sound line 321
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_3LogWitness line 323
40. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_3Log line 324
41. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_3Log_sound line 325
42. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_3 line 329
43. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_4_3_sound line 330
44. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_5_1LogWitness line 332
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_5_1Log line 333
46. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_5_1Log_sound line 334
47. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_5_1 line 338
48. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0E_5_1_sound line 339
49. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Terms line 341
50. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Terms_sound line 350
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Entropy line 361
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Entropy_sound line 362
53. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Labels line 364
54. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Labels_sound line 365
55. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Four line 370
56. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0Four_sound line 371
57. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Value line 373
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_4_0LogWitness line 374
59. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_4_0Log line 375
60. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_4_0Log_sound line 376
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_4_0 line 380
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_4_0_sound line 381
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_2_1LogWitness line 383
64. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_2_1Log line 384
65. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_2_1Log_sound line 385
66. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_2_1 line 389
67. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_2_1_sound line 390
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_3_1LogWitness line 392
69. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_3_1Log line 393
70. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_3_1Log_sound line 394
71. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_3_1 line 398
72. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_3_1_sound line 399
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_2LogWitness line 401
74. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_2Log line 402
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_2Log_sound line 403
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_2 line 407
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_2_sound line 408
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_3LogWitness line 410
79. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_3Log line 411
80. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_3Log_sound line 412
81. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_3 line 416
82. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_1_3_sound line 417
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_0_4LogWitness line 419
84. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_0_4Log line 420
85. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_0_4Log_sound line 421
86. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_0_4 line 425
87. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0E_0_4_sound line 426
88. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Terms line 428
89. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Terms_sound line 437
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Entropy line 448
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Entropy_sound line 449
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Mass line 451
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0Mass_sound line 452
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0MassTermLogWitness line 454
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0MassTermLog line 455
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0MassTermLog_sound line 456
97. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0MassTerm line 460
98. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0MassTerm_sound line 461
99. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0H line 463
100. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H0H_sound line 464
101. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Value line 466
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_1_5LogWitness line 467
103. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_1_5Log line 468
104. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_1_5Log_sound line 469
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_1_5 line 473
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_1_5_sound line 474
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_2_4LogWitness line 476
108. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_2_4Log line 477
109. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_2_4Log_sound line 478
110. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_2_4 line 482
111. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_2_4_sound line 483
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_3_4LogWitness line 485
113. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_3_4Log line 486
114. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_3_4Log_sound line 487
115. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_3_4 line 491
116. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_3_4_sound line 492
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_2LogWitness line 494
118. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_2Log line 495
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_2Log_sound line 496
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_2 line 500
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_2_sound line 501
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_3LogWitness line 503
123. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_3Log line 504
124. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_3Log_sound line 505
125. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_3 line 509
126. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_4_3_sound line 510
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_5_1LogWitness line 512
128. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_5_1Log line 513
129. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_5_1Log_sound line 514
130. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_5_1 line 518
131. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1E_5_1_sound line 519
132. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Terms line 521
133. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Terms_sound line 530
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Entropy line 541
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Entropy_sound line 542
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Mass line 544
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1Mass_sound line 545
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1MassTermLogWitness line 547
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1MassTermLog line 548
140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1MassTermLog_sound line 549
141. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1MassTerm line 553
142. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1MassTerm_sound line 554
143. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1H line 556
144. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H1H_sound line 557
145. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Value line 559
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2E_0_0Log line 560
147. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2E_0_0Log_sound line 561
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2E_0_0 line 563
149. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2E_0_0_sound line 564
150. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Terms line 566
151. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Terms_sound line 570
152. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Entropy line 581
153. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Entropy_sound line 582
154. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Mass line 584
155. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2Mass_sound line 585
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2MassTermLog line 587
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2MassTermLog_sound line 588
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2MassTerm line 590
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2MassTerm_sound line 591
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2H line 593
161. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.Z3_5_0H2H_sound line 594