OAI/Computability/WitnessedChoice/QuotedSyntax.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WitnessedChoice.RelationPools.Relation line 14
  2. def OAI.WitnessedChoice.RelationPools.graph line 16
  3. lemma OAI.WitnessedChoice.RelationPools.mem_graph line 18
  4. lemma OAI.WitnessedChoice.RelationPools.graph_injective line 22
  5. def OAI.WitnessedChoice.RelationPools.compose line 29
  6. lemma OAI.WitnessedChoice.RelationPools.mem_compose line 32
  7. lemma OAI.WitnessedChoice.RelationPools.compose_graph line 36
  8. def OAI.WitnessedChoice.RelationPools.localBound line 42
  9. def OAI.WitnessedChoice.RelationPools.localRelation line 44
  10. def OAI.WitnessedChoice.RelationPools.localPool line 48
  11. lemma OAI.WitnessedChoice.RelationPools.identity_mem_localPool line 52
  12. lemma OAI.WitnessedChoice.RelationPools.localPool_contains line 55
  13. lemma OAI.WitnessedChoice.RelationPools.localPool_card_le line 106
  14. def OAI.WitnessedChoice.RelationPools.rename line 119
  15. lemma OAI.WitnessedChoice.RelationPools.rename_graph line 122
  16. lemma OAI.WitnessedChoice.RelationPools.rename_compose line 135
  17. lemma OAI.WitnessedChoice.RelationPools.rename_localRelation line 148
  18. lemma OAI.WitnessedChoice.RelationPools.localPool_equivariant line 165
  19. def OAI.WitnessedChoice.edgeAtoms line 197
  20. def OAI.WitnessedChoice.configAtoms line 199
  21. def OAI.WitnessedChoice.edgeRow line 201
  22. def OAI.WitnessedChoice.vertexRow line 203
  23. def OAI.WitnessedChoice.edgeBlocks line 205
  24. def OAI.WitnessedChoice.vertexBlocks line 207
  25. def OAI.WitnessedChoice.blocks line 209
  26. def OAI.WitnessedChoice.tupleCode line 211
  27. def OAI.WitnessedChoice.parameterCode line 215
  28. lemma OAI.WitnessedChoice.smul_pair line 218
  29. lemma OAI.WitnessedChoice.tupleCode_fixed line 222
  30. lemma OAI.WitnessedChoice.parameterCode_fixed line 231
  31. def OAI.WitnessedChoice.PoolFilter line 241
  32. def OAI.WitnessedChoice.witnessPool line 244
  33. def OAI.WitnessedChoice.guardedSelection line 250
  34. lemma OAI.WitnessedChoice.one_mem_witnessPool line 255
  35. lemma OAI.WitnessedChoice.witnessPool_filter line 261
  36. theorem OAI.WitnessedChoice.guardedSelection_filtered line 274
  37. theorem OAI.WitnessedChoice.guardedSelection_invalid_filtered line 285
  38. lemma OAI.WitnessedChoice.composition_mem_witnessPool line 298
  39. lemma OAI.WitnessedChoice.witnessPool_card_le line 309
  40. def OAI.WitnessedChoice.BGS.pairCode line 352
  41. def OAI.WitnessedChoice.BGS.relationCode line 354
  42. lemma OAI.WitnessedChoice.BGS.pairCode_injective line 356
  43. lemma OAI.WitnessedChoice.BGS.pairCode_eq line 361
  44. lemma OAI.WitnessedChoice.BGS.relationCode_injective line 364
  45. lemma OAI.WitnessedChoice.BGS.elements_relationCode line 368
  46. lemma OAI.WitnessedChoice.BGS.relationCode_empty line 371
  47. lemma OAI.WitnessedChoice.BGS.relationCode_insert line 374
  48. lemma OAI.WitnessedChoice.BGS.relationCode_graph line 380
  49. def OAI.WitnessedChoice.BGS.partialRelations line 383
  50. lemma OAI.WitnessedChoice.BGS.tupleImage_cons line 389
  51. lemma OAI.WitnessedChoice.BGS.partialRelations_eq line 403
  52. lemma OAI.WitnessedChoice.BGS.Term.eval_partialPool line 428
  53. def OAI.WitnessedChoice.BGS.completeHF line 468
  54. lemma OAI.WitnessedChoice.BGS.Term.eval_completeRelation line 472
  55. lemma OAI.WitnessedChoice.BGS.mem_elements_relationCode line 526
  56. lemma OAI.WitnessedChoice.BGS.completeHF_tuple line 530
  57. lemma OAI.WitnessedChoice.BGS.Term.eval_identityRelation line 550
  58. lemma OAI.WitnessedChoice.BGS.Term.eval_localPool line 559
  59. structure OAI.WitnessedChoice.BGS.QuotedTerm line 582
  60. structure OAI.WitnessedChoice.BGS.QuotedFormula line 589
  61. def OAI.WitnessedChoice.BGS.QuotedTerm.var line 600
  62. def OAI.WitnessedChoice.BGS.QuotedTerm.empty line 602
  63. def OAI.WitnessedChoice.BGS.QuotedTerm.atoms line 604
  64. def OAI.WitnessedChoice.BGS.QuotedTerm.rename line 606
  65. def OAI.WitnessedChoice.BGS.QuotedTerm.up line 612
  66. def OAI.WitnessedChoice.BGS.QuotedTerm.double line 614
  67. def OAI.WitnessedChoice.BGS.QuotedTerm.union line 620
  68. def OAI.WitnessedChoice.BGS.QuotedTerm.unique line 626
  69. def OAI.WitnessedChoice.BGS.QuotedTerm.card line 632
  70. def OAI.WitnessedChoice.BGS.QuotedTerm.singleton line 638
  71. def OAI.WitnessedChoice.BGS.QuotedTerm.cup line 640
  72. def OAI.WitnessedChoice.BGS.QuotedTerm.pair line 642
  73. def OAI.WitnessedChoice.BGS.QuotedFormula.rename line 650
  74. def OAI.WitnessedChoice.BGS.QuotedFormula.up line 656
  75. def OAI.WitnessedChoice.BGS.QuotedFormula.eq line 658
  76. def OAI.WitnessedChoice.BGS.QuotedFormula.input line 666
  77. def OAI.WitnessedChoice.BGS.QuotedFormula.truth line 672
  78. def OAI.WitnessedChoice.BGS.QuotedFormula.neg line 674
  79. def OAI.WitnessedChoice.BGS.QuotedFormula.and line 680
  80. def OAI.WitnessedChoice.BGS.QuotedFormula.or line 686
  81. def OAI.WitnessedChoice.BGS.QuotedFormula.imp line 692
  82. def OAI.WitnessedChoice.BGS.QuotedFormula.iff line 694
  83. def OAI.WitnessedChoice.BGS.QuotedFormula.mem line 696
  84. def OAI.WitnessedChoice.BGS.QuotedFormula.existsIn line 705
  85. def OAI.WitnessedChoice.BGS.QuotedFormula.allIn line 713
  86. def OAI.WitnessedChoice.BGS.QuotedTerm.comprehend line 727
  87. def OAI.WitnessedChoice.BGS.QuotedTerm.map line 736
  88. def OAI.WitnessedChoice.BGS.QuotedTerm.bind line 738
  89. def OAI.WitnessedChoice.BGS.QuotedTerm.filter line 740
  90. def OAI.WitnessedChoice.BGS.QuotedTerm.inter line 742
  91. def OAI.WitnessedChoice.BGS.QuotedTerm.diff line 744
  92. def OAI.WitnessedChoice.BGS.QuotedTerm.cond line 746
  93. def OAI.WitnessedChoice.BGS.QuotedTerm.describe line 773
  94. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_var line 783
  95. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_empty line 785
  96. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_atoms line 787
  97. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_up line 789
  98. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_double line 791
  99. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_singleton line 793
  100. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_pair line 795
  101. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_filter line 797
  102. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_map line 801
  103. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_cup line 805
  104. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_bind line 809
  105. def OAI.WitnessedChoice.BGS.QuotedFormula.describe line 819
  106. def OAI.WitnessedChoice.BGS.QuotedFormula.allList line 827
  107. def OAI.WitnessedChoice.BGS.QuotedFormula.allSymbols line 831
  108. def OAI.WitnessedChoice.BGS.QuotedFormula.link line 834
  109. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_eq line 838
  110. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_input line 840
  111. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_up line 842
  112. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_mem line 844
  113. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_and line 846
  114. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_or line 848
  115. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_neg line 850
  116. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_imp line 852
  117. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_iff line 854
  118. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_allIn line 856
  119. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_existsIn line 859
  120. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_allList line 862
  121. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_allSymbols line 867
  122. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_link line 870
  123. lemma OAI.WitnessedChoice.BGS.inputHF_atoms line 876
  124. lemma OAI.WitnessedChoice.BGS.pair_mem_relationCode line 880
  125. lemma OAI.WitnessedChoice.BGS.all_stateCode line 885
  126. lemma OAI.WitnessedChoice.BGS.exists_stateCode line 888
  127. lemma OAI.WitnessedChoice.BGS.fin_cons_two line 901
  128. lemma OAI.WitnessedChoice.BGS.fin_cons_three line 903
  129. lemma OAI.WitnessedChoice.BGS.fin_cons_four line 905
  130. lemma OAI.WitnessedChoice.BGS.fin_cons_five line 907
  131. def OAI.WitnessedChoice.BGS.QuotedTerm.atomFilter line 913
  132. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_atomFilter line 923
  133. def OAI.WitnessedChoice.BGS.QuotedTerm.relation line 927
  134. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_relation line 944
  135. def OAI.WitnessedChoice.BGS.QuotedTerm.edgeAtoms line 949
  136. def OAI.WitnessedChoice.BGS.QuotedTerm.configAtoms line 951
  137. def OAI.WitnessedChoice.BGS.QuotedTerm.edgeRow line 953
  138. def OAI.WitnessedChoice.BGS.QuotedTerm.vertexRow line 955
  139. def OAI.WitnessedChoice.BGS.QuotedTerm.edgeBlocks line 957
  140. def OAI.WitnessedChoice.BGS.QuotedTerm.vertexBlocks line 959
  141. def OAI.WitnessedChoice.BGS.QuotedTerm.blocks line 961
  142. def OAI.WitnessedChoice.BGS.QuotedTerm.identity line 963
  143. def OAI.WitnessedChoice.BGS.QuotedTerm.localRelations line 969
  144. def OAI.WitnessedChoice.BGS.QuotedTerm.composition line 975
  145. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_edgeAtoms line 981
  146. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_configAtoms line 984
  147. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_edgeRow line 987
  148. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_vertexRow line 1000
  149. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_edgeBlocks line 1013
  150. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_vertexBlocks line 1021
  151. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_blocks line 1029
  152. lemma OAI.WitnessedChoice.BGS.QuotedTerm.meaning_composition line 1037
  153. def OAI.WitnessedChoice.BGS.FunctionalOnto line 1060
  154. lemma OAI.WitnessedChoice.BGS.functionalOnto_iff line 1063
  155. def OAI.WitnessedChoice.BGS.RawFilter line 1089
  156. lemma OAI.WitnessedChoice.BGS.rawFilter_graph line 1095
  157. lemma OAI.WitnessedChoice.BGS.rawFilter_iff line 1121
  158. def OAI.WitnessedChoice.BGS.QuotedFormula.functional line 1134
  159. def OAI.WitnessedChoice.BGS.QuotedFormula.onto line 1139
  160. def OAI.WitnessedChoice.BGS.QuotedFormula.preserves line 1142
  161. def OAI.WitnessedChoice.BGS.QuotedFormula.fixesBlocks line 1148
  162. def OAI.WitnessedChoice.BGS.QuotedFormula.fixesState line 1152
  163. def OAI.WitnessedChoice.BGS.QuotedFormula.filter line 1155
  164. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_functional line 1160
  165. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_onto line 1173
  166. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_preserves line 1177
  167. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_fixesBlocks line 1182
  168. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_fixesState line 1187
  169. lemma OAI.WitnessedChoice.BGS.QuotedFormula.meaning_filter line 1192