OAI/Computability/TypeSystem/Diagonal.lean

GitHub source file

158 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.lift_subst line 10
2. def OAI.PureTypeSystem.Labelled.SpecializedCode.delta line 15
3. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.delta_rename line 17
4. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.delta_subst line 20
5. def OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredStep line 23
6. def OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredBody line 25
7. def OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPred line 27
8. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredStep_rename line 29
9. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredStep_subst line 33
10. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredBody_rename line 37
11. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredBody_subst line 41
12. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPredBody_instantiate line 45
13. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPred_rename line 48
14. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.shiftPred_subst line 52
15. def OAI.PureTypeSystem.Labelled.SpecializedCode.qStep line 57
16. def OAI.PureTypeSystem.Labelled.SpecializedCode.qBody line 59
17. def OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalQ line 61
18. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qStep_rename line 63
19. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qStep_subst line 67
20. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qBody_rename line 71
21. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qBody_subst line 75
22. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.qBody_instantiate line 79
23. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalQ_rename line 82
24. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalQ_subst line 85
25. def OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalBody line 88
26. def OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalPred line 90
27. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalBody_rename line 92
28. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalBody_subst line 96
29. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalBody_instantiate line 100
30. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalPred_rename line 103
31. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.diagonalPred_subst line 107
32. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.delta_typed line 122
33. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.delta_valid line 127
34. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.delta_congr line 132
35. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPredStep_formula line 141
36. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPredBody_family line 148
37. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_typed line 159
38. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_evaluation line 165
39. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qStep_formula line 184
40. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qBody_family line 193
41. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalQ_formula line 201
42. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalQ_intro line 209
43. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalQ_elim_one line 223
44. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalQ_elim line 234
45. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalBody_family line 247
46. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_typed line 252
47. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_evaluation line 257
48. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qConsequence_respect line 274
49. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.qStep_respect line 291
50. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalQ_respect line 313
51. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_exact line 335
52. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_respect line 346
53. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_extStep line 362
54. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_extAt line 382
55. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.diagonalPred_extensional line 393
56. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_exact line 410
57. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_respect line 427
58. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_extStep line 447
59. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_extAt line 471
60. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shiftPred_extensional line 485
61. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_wrong_tag line 505
62. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_to_tagged line 533
63. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.edge_from_tagged line 558
64. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.formEx_elim line 574
65. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.formEx_right_false line 592
66. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_left_forward line 613
67. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_left_backward line 639
68. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_right_forward line 655
69. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_right_backward line 669
70. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_respect line 691
71. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_gStep line 709
72. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_gAt line 730
73. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_propertyG line 744
74. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.part_good line 756
75. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_left_equivalent line 771
76. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pair_right_equivalent line 796
77. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_left line 818
78. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_right line 833
79. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rAll_intro line 856
80. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rAll_elim_one line 868
81. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyR_elim line 877
82. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_pred_compare_at line 901
83. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_pred_compare line 925
84. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_pred_extensional line 946
85. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_R_forward line 967
86. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_member_le line 986
87. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_member_imp line 1006
88. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_rStep line 1033
89. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_rAll line 1059
90. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_R_backward line 1079
91. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responsePair_R_equivalent line 1095
92. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.sb_law line 1125
93. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_compare_at line 1147
94. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_compare line 1167
95. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_predecessor line 1185
96. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.positive_shift_member line 1213
97. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.positive_shift_imp line 1226
98. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.positive_shift_step line 1248
99. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.positive_shift line 1269
100. def OAI.PureTypeSystem.Labelled.SpecializedCode.indStep line 1287
101. def OAI.PureTypeSystem.Labelled.SpecializedCode.indBody line 1289
102. def OAI.PureTypeSystem.Labelled.SpecializedCode.induction line 1291
103. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.indStep_rename line 1293
104. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.indStep_subst line 1297
105. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.indBody_rename line 1301
106. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.indBody_subst line 1305
107. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.indBody_instantiate line 1309
108. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.induction_rename line 1312
109. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.induction_subst line 1315
110. def OAI.PureTypeSystem.Labelled.SpecializedCode.wfStep line 1319
111. def OAI.PureTypeSystem.Labelled.SpecializedCode.wfBody line 1321
112. def OAI.PureTypeSystem.Labelled.SpecializedCode.wf line 1323
113. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wfStep_rename line 1325
114. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wfBody_rename line 1328
115. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wfStep_subst line 1332
116. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wfBody_subst line 1335
117. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wfBody_instantiate line 1339
118. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wf_rename line 1342
119. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.wf_subst line 1345
120. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.indStep_formula line 1359
121. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.indBody_family line 1367
122. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.induction_formula line 1375
123. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.induction_intro line 1381
124. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.induction_elim_one line 1393
125. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.induction_elim line 1402
126. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wfStep_formula line 1422
127. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wfBody_family line 1428
128. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_typed line 1434
129. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_primitive_evaluation line 1437
130. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_evaluation line 1444
131. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.indConsequence_respect line 1459
132. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.xComparison_rename line 1475
133. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.indStep_respect line 1481
134. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.induction_respect line 1501
135. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responseProbe_compare_at line 1522
136. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.responseProbe_compare line 1552
137. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_le_congr line 1578
138. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_validStep line 1596
139. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_validAt line 1616
140. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_valid line 1626
141. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wf_shift_evaluation line 1633
142. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_ind_member line 1653
143. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_ind_imp line 1665
144. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_ind_step line 1688
145. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.shift_induction line 1708
146. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.induction_builder line 1723
147. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.negative_ind_bottom line 1739
148. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.negative_ind_member line 1750
149. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.negative_ind_imp line 1765
150. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.negative_ind_step line 1780
151. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.negative_induction line 1792
152. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wfQ_member line 1807
153. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wfQ_imp line 1818
154. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wfQ_step line 1834
155. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.wfQ line 1847
156. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relational_bottom line 1857

     Source documentation

     The ambient bottom inhabitant, with actual encodings and no extensional equality or relational law supplied as a hypothesis.

     theorem relational_bottom : Proves P Γ γ L.bottom := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.Proves

157. def OAI.PureTypeSystem.Labelled.ChannelReturn.specialized line 1870
158. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.specialized_formed line 1871