OAI/LinearAlgebra/MatrixMultiplication/Completion/Labels.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

Readable tensor completion and its finite arithmetic realization.

  1. def OAI.MatrixMultiplication.CompletionLabels.Leaf line 20
  2. instance OAI.MatrixMultiplication.CompletionLabels.leafFintype line 23
  3. def OAI.MatrixMultiplication.CompletionLabels.Coordinate line 27
  4. def OAI.MatrixMultiplication.CompletionLabels.coordinate line 32
  5. def OAI.MatrixMultiplication.CompletionLabels.ownerFlag line 37
  6. def OAI.MatrixMultiplication.CompletionLabels.leafColor line 42
  7. theorem OAI.MatrixMultiplication.CompletionLabels.leafColor_eq_iff line 45
  8. theorem OAI.MatrixMultiplication.CompletionLabels.complete_supported line 54
  9. def OAI.MatrixMultiplication.CompletionLabels.slot line 64
  10. def OAI.MatrixMultiplication.CompletionLabels.pattern line 69
  11. theorem OAI.MatrixMultiplication.CompletionLabels.slot_injective line 73
  12. theorem OAI.MatrixMultiplication.CompletionLabels.completed_color_iff line 86
  13. theorem OAI.MatrixMultiplication.CompletionLabels.pattern_mem line 99
  14. theorem OAI.MatrixMultiplication.CompletionLabels.pattern_eq_center line 113
  15. def OAI.MatrixMultiplication.CompletionLabels.centerRead line 121
  16. def OAI.MatrixMultiplication.CompletionLabels.outputRead line 125
  17. theorem OAI.MatrixMultiplication.CompletionLabels.centerRead_pattern line 129
  18. theorem OAI.MatrixMultiplication.CompletionLabels.outputRead_pattern line 141
  19. theorem OAI.MatrixMultiplication.CompletionLabels.raisedFlag_iff_output line 155
  20. def OAI.MatrixMultiplication.CompletionLabels.wordCoordinates line 180
  21. theorem OAI.MatrixMultiplication.CompletionLabels.word_ownerFlag line 184
  22. def OAI.MatrixMultiplication.CompletionLabels.packLeaf line 195
  23. theorem OAI.MatrixMultiplication.CompletionLabels.slot_packLeaf line 221
  24. theorem OAI.MatrixMultiplication.CompletionLabels.packLeaf_color line 228
  25. def OAI.MatrixMultiplication.CompletionLabels.conditionalLeafEquiv line 234
  26. def OAI.MatrixMultiplication.CompletionLabels.RetainedLeaf line 252
  27. instance OAI.MatrixMultiplication.CompletionLabels.retainedLeafFintype line 255
  28. def OAI.MatrixMultiplication.CompletionLabels.terminationFirstRead line 260
  29. def OAI.MatrixMultiplication.CompletionLabels.terminationSecondRead line 264
  30. theorem OAI.MatrixMultiplication.CompletionLabels.termination_readable line 268
  31. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.firstSide line 291
  32. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.secondSide line 296
  33. structure OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule line 301
  34. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.Label line 311
  35. instance OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.labelFintype line 313
  36. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.labels line 316
  37. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.labels_of_inactive line 319
  38. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.labels_of_active line 323
  39. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.labels_eq_iff line 327
  40. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.Complete line 336
  41. structure OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule line 343
  42. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.pairs line 360
  43. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.firstReader line 363
  44. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.secondReader line 368
  45. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.firstReader_readable line 373
  46. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.secondReader_readable line 383
  47. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.readers_off_branch line 393
  48. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.labelRecordOf_eq_prefix line 403
  49. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.label_eq_of_record_eq line 422
  50. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.completeRecord_injective line 433
  51. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.completeRecord_injective line 447
  52. def OAI.MatrixMultiplication.CompletionLabels.ownerPair line 462
  53. theorem OAI.MatrixMultiplication.CompletionLabels.ownerPair_first_mem line 467
  54. theorem OAI.MatrixMultiplication.CompletionLabels.ownerPair_second_mem line 472
  55. def OAI.MatrixMultiplication.CompletionLabels.patternSideRead line 477
  56. theorem OAI.MatrixMultiplication.CompletionLabels.patternSideRead_correct line 483
  57. theorem OAI.MatrixMultiplication.CompletionLabels.completion_pattern_readers line 505
  58. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.PrefixDetermined line 528
  59. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.canonicalActivate line 533
  60. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.NodeSchedule.canonicalActivate_correct line 539
  61. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.TopologicalSchedule.ofPrefixDetermined line 551
  62. structure OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program line 572
  63. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.Complete line 588
  64. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.pullback line 592
  65. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.pullback_complete line 607
  66. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.recode line 618
  67. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.recode_complete line 636
  68. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.single line 645
  69. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.appendLabel line 660
  70. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.takeArray line 663
  71. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.dropArray line 666
  72. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.append line 669
  73. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.append_labels_left line 711
  74. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.append_labels_right line 720
  75. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.append_complete line 730
  76. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.recordArray line 751
  77. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.recordArray_labelRecordOf line 757
  78. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.firstReader line 770
  79. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.secondReader line 775
  80. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.firstReader_readable line 780
  81. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.secondReader_readable line 787
  82. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.record_injective_on_context line 794
  83. def OAI.MatrixMultiplication.CompletionLabels.rootColor line 814
  84. def OAI.MatrixMultiplication.CompletionLabels.rootIndex line 816
  85. theorem OAI.MatrixMultiplication.CompletionLabels.rootColor_rootIndex line 821
  86. def OAI.MatrixMultiplication.CompletionLabels.completionView line 824
  87. def OAI.MatrixMultiplication.CompletionLabels.patternProgram line 828
  88. def OAI.MatrixMultiplication.CompletionLabels.decodePattern line 852
  89. theorem OAI.MatrixMultiplication.CompletionLabels.decodePattern_correct line 856
  90. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.powPast line 872
  91. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.powLabel line 880
  92. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.powLabel_at line 886
  93. def OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.pow line 898
  94. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.pow_labels line 933
  95. theorem OAI.MatrixMultiplication.CompletionLabels.TopologicalFlatten.Program.pow_complete line 938
  96. abbrev OAI.MatrixMultiplication.CompletionLabels.CompletionCode line 966
  97. def OAI.MatrixMultiplication.CompletionLabels.encodePattern line 968
  98. def OAI.MatrixMultiplication.CompletionLabels.decodePatternCode line 972
  99. theorem OAI.MatrixMultiplication.CompletionLabels.patternCode_roundtrip line 976
  100. def OAI.MatrixMultiplication.CompletionLabels.encodeOld line 981
  101. def OAI.MatrixMultiplication.CompletionLabels.decodeOld line 983
  102. theorem OAI.MatrixMultiplication.CompletionLabels.oldCode_roundtrip line 987
  103. def OAI.MatrixMultiplication.CompletionLabels.inheritedProgram line 992
  104. theorem OAI.MatrixMultiplication.CompletionLabels.inheritedProgram_complete line 1005
  105. def OAI.MatrixMultiplication.CompletionLabels.completionContextDecoder line 1019
  106. theorem OAI.MatrixMultiplication.CompletionLabels.completionContextDecoder_correct line 1023
  107. def OAI.MatrixMultiplication.CompletionLabels.completionProgram line 1046
  108. theorem OAI.MatrixMultiplication.CompletionLabels.completionProgram_complete line 1058
  109. def OAI.MatrixMultiplication.CompletionLabels.coordinateWord line 1072
  110. theorem OAI.MatrixMultiplication.CompletionLabels.coordinateWord_coordinate line 1077
  111. def OAI.MatrixMultiplication.CompletionLabels.completionLocalProgram line 1082
  112. theorem OAI.MatrixMultiplication.CompletionLabels.completionLocalProgram_complete line 1094
  113. structure OAI.MatrixMultiplication.CompletionLabels.ReadableTensor line 1107
  114. def OAI.MatrixMultiplication.CompletionLabels.ReadableTensor.raise line 1121
  115. def OAI.MatrixMultiplication.CompletionLabels.ReadableTensor.script line 1130
  116. def OAI.MatrixMultiplication.CompletionLabels.terminationSideRead line 1148
  117. theorem OAI.MatrixMultiplication.CompletionLabels.terminationSideRead_correct line 1154
  118. def OAI.MatrixMultiplication.CompletionLabels.terminationRoot line 1168
  119. def OAI.MatrixMultiplication.CompletionLabels.terminationInherited line 1184
  120. theorem OAI.MatrixMultiplication.CompletionLabels.terminationInherited_complete line 1191
  121. def OAI.MatrixMultiplication.CompletionLabels.terminationDecodeColor line 1202
  122. def OAI.MatrixMultiplication.CompletionLabels.terminationDecodeOld line 1206
  123. def OAI.MatrixMultiplication.CompletionLabels.terminationProgram line 1210
  124. theorem OAI.MatrixMultiplication.CompletionLabels.terminationProgram_complete line 1228
  125. theorem OAI.MatrixMultiplication.CompletionLabels.terminationProgram_context line 1250
  126. theorem OAI.MatrixMultiplication.CompletionLabels.terminationProgram_view line 1259
  127. theorem OAI.MatrixMultiplication.CompletionLabels.terminationRecord_injective line 1268