OAI/Computability/TypeSystem/Equivalence.lean

GitHub source file

180 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PureTypeSystem.Labelled.SpecializedCode.query line 12
2. def OAI.PureTypeSystem.Labelled.SpecializedCode.predCompare line 15
3. def OAI.PureTypeSystem.Labelled.SpecializedCode.qrStep line 17
4. def OAI.PureTypeSystem.Labelled.SpecializedCode.qrAtBody line 19
5. def OAI.PureTypeSystem.Labelled.SpecializedCode.qrAt line 21
6. def OAI.PureTypeSystem.Labelled.SpecializedCode.qrBody line 23
7. def OAI.PureTypeSystem.Labelled.SpecializedCode.queryRespect line 25
8. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.query_rename line 27
9. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.query_subst line 31
10. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.predCompare_rename line 35
11. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.predCompare_subst line 39
12. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrStep_rename line 43
13. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrStep_subst line 46
14. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrAtBody_rename line 49
15. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrAtBody_subst line 53
16. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrAt_rename line 57
17. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrAt_subst line 60
18. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrBody_rename line 63
19. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrBody_subst line 67
20. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.queryRespect_rename line 71
21. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.queryRespect_subst line 74
22. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrAtBody_instantiate line 77
23. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qrBody_instantiate line 81
24. def OAI.PureTypeSystem.Labelled.SpecializedCode.admissible line 85
25. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.predCompare_formula line 96
26. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qrStep_formula line 102
27. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qrAtBody_family line 109
28. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qrAt_formula line 117
29. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qrBody_family line 122
30. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.queryRespect_formula line 127
31. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.query_equivalent line 131
32. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qrStep_proves line 145
33. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qrAt_proves line 161
34. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.queryRespect_proves line 170
35. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.not_dummy_formula line 177
36. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.admissible_formula line 183
37. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.admissible_proves line 188
38. theorem OAI.PureTypeSystem.Labelled.LogicSetup.recover_equivalent line 212
39. def OAI.PureTypeSystem.Labelled.SpecializedCode.round line 222
40. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.round_rename line 223
41. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.round_typed line 234
42. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.middle_sorted line 239
43. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.middle_mode line 241
44. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.outer_eval_round line 244
45. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.bitOuter_round line 255
46. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.outer_recover_round line 259
47. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.bitInner_round line 271
48. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.observe_round line 277
49. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.ae_round line 288
50. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gAt_intro line 307
51. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gAt_elim line 320
52. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_intro line 330
53. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_elim_one line 342
54. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_elim line 351
55. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_round line 363
56. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_roundRespect line 371
57. def OAI.PureTypeSystem.Labelled.SpecializedCode.good line 399
58. def OAI.PureTypeSystem.Labelled.SpecializedCode.goodBody line 401
59. def OAI.PureTypeSystem.Labelled.SpecializedCode.relation line 403
60. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.goodBody_instantiate line 406
61. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.good_rename line 410
62. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.goodBody_rename line 414
63. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.relation_rename line 418
64. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.good_formula line 430
65. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.goodBody_family line 434
66. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.good_forward line 438
67. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.good_backward line 445
68. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.good_equivalent line 452
69. def OAI.PureTypeSystem.Labelled.SpecializedCode.queries line 478
70. def OAI.PureTypeSystem.Labelled.SpecializedCode.classPred line 480
71. def OAI.PureTypeSystem.Labelled.SpecializedCode.unionPred line 482
72. def OAI.PureTypeSystem.Labelled.SpecializedCode.isClass line 484
73. def OAI.PureTypeSystem.Labelled.SpecializedCode.edge line 486
74. def OAI.PureTypeSystem.Labelled.SpecializedCode.pairForm line 488
75. def OAI.PureTypeSystem.Labelled.SpecializedCode.pair line 490
76. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.queries_instantiate line 493
77. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.queries_rename line 496
78. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.isClass_eq line 499
79. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.edge_eq line 502
80. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.classPred_rename line 508
81. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.unionPred_rename line 513
82. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.isClass_rename line 518
83. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.edge_rename line 523
84. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.pairForm_rename line 528
85. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.pair_rename line 533
86. inductive OAI.PureTypeSystem.Labelled.ObservationFeature line 542
87. def OAI.PureTypeSystem.Labelled.ObservationFeature.rename line 545
88. def OAI.PureTypeSystem.Labelled.ObservationFeature.subst line 547
89. theorem OAI.PureTypeSystem.Labelled.ObservationFeature.rename_comp line 549
90. theorem OAI.PureTypeSystem.Labelled.ObservationFeature.subst_rename line 551
91. theorem OAI.PureTypeSystem.Labelled.ObservationFeature.rename_subst line 553
92. theorem OAI.PureTypeSystem.Labelled.ObservationFeature.instantiate_raise line 555
93. def OAI.PureTypeSystem.Labelled.SpecializedCode.feature line 560
94. def OAI.PureTypeSystem.Labelled.SpecializedCode.featureBody line 565
95. def OAI.PureTypeSystem.Labelled.SpecializedCode.featurePred line 567
96. def OAI.PureTypeSystem.Labelled.SpecializedCode.FeatureFormed line 569
97. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.feature_rename line 574
98. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.feature_subst line 578
99. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.featureBody_rename line 582
100. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.featureBody_instantiate line 587
101. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.featurePred_rename line 591
102. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.FeatureFormed.rename line 597
103. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_formula line 614
104. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.featureBody_family line 622
105. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_round line 629
106. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_respect line 637
107. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.featurePred_typed line 648
108. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.featurePred_evaluation line 655
109. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.featurePred_respect line 678
110. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_gStep line 693
111. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_gAt line 710
112. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_propertyG line 720
113. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.feature_good line 728
114. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_formula line 741
115. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_elim line 748
116. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_to_feature line 758
117. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_forward line 773
118. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_backward line 788
119. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.observation_equivalence line 808
120. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cAt_intro line 837
121. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cAt_elim line 851
122. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyC_intro line 861
123. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyC_elim line 869
124. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eAt_intro line 881
125. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eAt_elim line 895
126. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyE_intro line 905
127. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyE_elim line 913
128. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.queries_family line 933
129. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.classPred_typed line 937
130. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.unionPred_typed line 944
131. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.isClass_formula line 953
132. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_formula line 961
133. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pairForm_formula line 970
134. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_typed line 980
135. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_evaluation line 988
136. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_observation_evaluation line 998
137. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.union_evaluation line 1008
138. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.union_observation_evaluation line 1019
139. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_refl line 1043
140. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_symm line 1048
141. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_trans line 1055
142. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_congr line 1064
143. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_tagged_same line 1075
144. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_tagged_distinct line 1088
145. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_self line 1100
146. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_query line 1104
147. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_witness_elim line 1113
148. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_at_witness line 1138
149. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.class_witness_intro line 1167
150. theorem OAI.PureTypeSystem.Labelled.LogicSetup.select_disj_left line 1181
151. theorem OAI.PureTypeSystem.Labelled.LogicSetup.select_disj_right line 1186
152. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.tag_witness_incompatible line 1201
153. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.union_left_hit line 1215
154. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.union_right_hit line 1225
155. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_witness_core line 1235
156. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_query line 1273
157. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relation_observation_congr line 1289
158. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.union_at_witness line 1300
159. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_witness_intro line 1333
160. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_property_witness_elim line 1360
161. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_given_left_elim line 1388
162. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_classes_witness_elim line 1421
163. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_witness_elim line 1453
164. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_transport line 1485
165. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_congr line 1517
166. def OAI.PureTypeSystem.Labelled.SpecializedCode.formExBody line 1555
167. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.formExBody_instantiate line 1558
168. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.formExBody_rename line 1561
169. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.formExBody_family line 1576
170. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pairForm_eq line 1589
171. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.formEx_intro line 1596
172. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.formEx_congr line 1615
173. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pairForm_congr line 1638
174. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_evaluation_rounded line 1653
175. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_evaluation line 1664
176. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.comparison_intro line 1684
177. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.formEx_pred_congr line 1698
178. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pairForm_input_congr line 1718
179. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_input_evaluation_congr line 1735
180. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_comparison line 1754