OAI/Computability/FiniteCompiler/UniformPaths.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

Uniform surface and path normalization with recursive compiler interfaces.

  1. theorem OAI.FiniteAlgebraicEnvelopes.Effect.primrec_sumElim line 11
  2. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_left line 22
  3. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_right line 24
  4. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_head line 26
  5. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_typeOf line 29
  6. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_shape line 36
  7. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_head? line 46
  8. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_left? line 52
  9. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_right? line 57
  10. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_heads line 63
  11. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_lefts line 65
  12. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_rights line 67
  13. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_encode line 69
  14. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_glue line 83
  15. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.cuts_fold line 98
  16. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_cuts line 104
  17. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_mem line 112
  18. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_decode line 115
  19. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_prepareChunk line 139
  20. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_prepareChunks line 145
  21. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_prepare line 149
  22. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.expand_map line 161
  23. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search_map line 167
  24. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.component_map line 174
  25. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.sectorList_map line 184
  26. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.universeList_map line 192
  27. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.step_map line 205
  28. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.mapHead_injective line 214
  29. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.stepBool_map line 222
  30. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.componentList_map line 235
  31. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.expand_ext_universe line 246
  32. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search_ext_universe line 254
  33. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.search_add_stable line 261
  34. theorem OAI.FiniteAlgebraicEnvelopes.Effect.Graph.component_ext_universe line 270
  35. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.universeList_ext_support line 287
  36. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.componentList_ext_support line 293
  37. def OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.representative line 300
  38. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.primrec_representative line 304
  39. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Uniform.primrec_entry line 326
  40. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Control.Uniform.primrec_success line 332
  41. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.internalPreprocess line 343
  42. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.preprocess line 351
  43. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_internalPreprocess line 359
  44. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.primrec_preprocess line 375
  45. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_prepareChunk_family line 406
  46. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_prepareChunks_family line 415
  47. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.Uniform.primrec_prepare_family line 421
  48. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.sectorPreprocess line 432
  49. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.preprocess line 435
  50. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_sectorPreprocess line 438
  51. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_preprocess line 443
  52. theorem OAI.FiniteAlgebraicEnvelopes.Effect.traverse_map_parameter line 453
  53. theorem OAI.FiniteAlgebraicEnvelopes.Effect.partrec_traverse_family line 459
  54. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Uniform.partrec_action line 469
  55. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Uniform.partrec_execute line 481
  56. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Uniform.partrec_partialSource line 489
  57. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_raw line 504
  58. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_rawLetters line 513
  59. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_readRaw line 523
  60. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_classify line 527
  61. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.primrec_realize line 533
  62. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.partialNormal line 537
  63. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.partrec_partialNormal line 543
  64. theorem OAI.FiniteAlgebraicEnvelopes.Effect.priorityList_map line 570
  65. theorem OAI.FiniteAlgebraicEnvelopes.Effect.priorityList_ext line 579
  66. theorem OAI.FiniteAlgebraicEnvelopes.Effect.minList_map line 586
  67. theorem OAI.FiniteAlgebraicEnvelopes.Effect.minList_ext line 601
  68. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.representative_map line 627
  69. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.representative_ext_support line 636
  70. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.representative_finite line 645
  71. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.Uniform.representative_finite_map line 653
  72. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.codedMachine line 677
  73. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.coded_initial line 681
  74. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.coded_transition line 684
  75. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_codedTransition line 691
  76. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.mem_support_iff line 701
  77. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.heads line 722
  78. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_heads line 725
  79. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.mem_heads_iff line 729
  80. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.heads_finset line 757
  81. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.codedRepresentative line 772
  82. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_codedRepresentative line 779
  83. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.finiteOrder line 791
  84. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.codedRepresentative_map line 797
  85. def OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.headMap line 826
  86. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.headMap_injective line 829
  87. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawSweep_map line 835
  88. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.rawNormal_map line 845
  89. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.quotaNormal_map line 850
  90. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.unmerge_map line 857
  91. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.pendingPreprocess_map line 869
  92. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.ofCleanup_map line 875
  93. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupNormal_map line 880
  94. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.cleanupPreprocess_map line 886
  95. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.internalPreprocess_map line 903
  96. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.preprocess_map line 919
  97. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.mapLetter line 934
  98. def OAI.FiniteAlgebraicEnvelopes.Compiler.Path.mapSector line 942
  99. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.typeOf_mapLetter line 946
  100. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.shape_map line 948
  101. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.mapLetter_injective line 951
  102. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.headed_map line 956
  103. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.encode_map line 959
  104. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.heads_map line 962
  105. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.lefts_map line 967
  106. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.rights_map line 971
  107. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.enter_mem_map line 975
  108. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.leave_mem_map line 981
  109. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.decode_map line 989
  110. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.glue_map line 1009
  111. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.cuts_map line 1014
  112. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepareChunk_map line 1025
  113. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Path.prepare_map line 1033
  114. def OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.mapKeep line 1045
  115. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.splitRun_map line 1050
  116. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.plan_map line 1056
  117. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.Action.partial_map line 1070
  118. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.execute_map line 1075
  119. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.RawRuns.partialSource_map line 1083
  120. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.unliteral_map line 1091
  121. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Scan.literal_map line 1093
  122. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.headMap line 1101
  123. def OAI.FiniteAlgebraicEnvelopes.Compiler.Word.letterMap line 1103
  124. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.headMap_injective line 1105
  125. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.letterMap_injective line 1107
  126. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.raw_map line 1111
  127. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.rawLetters_map line 1115
  128. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.readRaw_map line 1126
  129. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.classify_map line 1133
  130. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.realize_map line 1139
  131. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.sectorPreprocess_map line 1156
  132. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.preprocess_map line 1164
  133. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.partialNormal_map line 1172
  134. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Surface.Uniform.preprocess_specialize line 1205
  135. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.sectorPreprocess_specialize line 1214
  136. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.preprocess_specialize line 1220
  137. theorem OAI.FiniteAlgebraicEnvelopes.Compiler.Word.Uniform.partialNormal_specialize line 1226
  138. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.codedNormal line 1244
  139. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.partrec_codedNormal line 1248
  140. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.codedNormal_map line 1253
  141. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.surfaces line 1276
  142. def OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.letters line 1279
  143. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_surfaces line 1286
  144. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.primrec_letters line 1291
  145. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.mem_surfaces_iff line 1296
  146. theorem OAI.FiniteAlgebraicEnvelopes.MachineRealization.ParameterCode.mem_letters_iff line 1323