OAI/Computability/TypeSystem/Specialization.lean

GitHub source file

282 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PureTypeSystem.Labelled.ObservationCode line 11

   Source documentation

   The exact three-copy observations at the special carrier.

   structure ObservationCode (S : Type u) where
   …

2. def OAI.PureTypeSystem.Labelled.ObservationCode.rename line 17
3. def OAI.PureTypeSystem.Labelled.ObservationCode.subst line 19
4. def OAI.PureTypeSystem.Labelled.ObservationCode.copies line 21
5. def OAI.PureTypeSystem.Labelled.ObservationCode.carrier line 22
6. def OAI.PureTypeSystem.Labelled.ObservationCode.tagged line 23
7. def OAI.PureTypeSystem.Labelled.ObservationCode.bitInner line 25
8. def OAI.PureTypeSystem.Labelled.ObservationCode.bitOuter line 26
9. def OAI.PureTypeSystem.Labelled.ObservationCode.observe line 27
10. def OAI.PureTypeSystem.Labelled.ObservationCode.observeBody line 29
11. def OAI.PureTypeSystem.Labelled.ObservationCode.compareBody line 32
12. def OAI.PureTypeSystem.Labelled.ObservationCode.compare line 34
13. def OAI.PureTypeSystem.Labelled.ObservationCode.ae line 36
14. theorem OAI.PureTypeSystem.Labelled.ObservationCode.rename_comp line 40
15. theorem OAI.PureTypeSystem.Labelled.ObservationCode.subst_rename line 42
16. theorem OAI.PureTypeSystem.Labelled.ObservationCode.rename_subst line 45
17. theorem OAI.PureTypeSystem.Labelled.ObservationCode.instantiate_raise line 48
18. theorem OAI.PureTypeSystem.Labelled.ObservationCode.copies_rename line 50
19. theorem OAI.PureTypeSystem.Labelled.ObservationCode.copies_subst line 51
20. theorem OAI.PureTypeSystem.Labelled.ObservationCode.carrier_rename line 52
21. theorem OAI.PureTypeSystem.Labelled.ObservationCode.carrier_subst line 56
22. theorem OAI.PureTypeSystem.Labelled.ObservationCode.tagged_rename line 60
23. theorem OAI.PureTypeSystem.Labelled.ObservationCode.tagged_subst line 64
24. theorem OAI.PureTypeSystem.Labelled.ObservationCode.bitInner_rename line 68
25. theorem OAI.PureTypeSystem.Labelled.ObservationCode.bitInner_subst line 72
26. theorem OAI.PureTypeSystem.Labelled.ObservationCode.bitOuter_rename line 76
27. theorem OAI.PureTypeSystem.Labelled.ObservationCode.bitOuter_subst line 80
28. theorem OAI.PureTypeSystem.Labelled.ObservationCode.observe_rename line 84
29. theorem OAI.PureTypeSystem.Labelled.ObservationCode.observe_subst line 88
30. theorem OAI.PureTypeSystem.Labelled.ObservationCode.observeBody_rename line 92
31. theorem OAI.PureTypeSystem.Labelled.ObservationCode.observeBody_subst line 96
32. theorem OAI.PureTypeSystem.Labelled.ObservationCode.compareBody_rename line 100
33. theorem OAI.PureTypeSystem.Labelled.ObservationCode.compareBody_subst line 104
34. theorem OAI.PureTypeSystem.Labelled.ObservationCode.compare_rename line 108
35. theorem OAI.PureTypeSystem.Labelled.ObservationCode.compare_subst line 112
36. theorem OAI.PureTypeSystem.Labelled.ObservationCode.ae_rename line 116
37. theorem OAI.PureTypeSystem.Labelled.ObservationCode.ae_subst line 120
38. theorem OAI.PureTypeSystem.Labelled.ObservationCode.observeBody_instantiate line 124
39. theorem OAI.PureTypeSystem.Labelled.ObservationCode.compareBody_instantiate line 127
40. def OAI.PureTypeSystem.Labelled.LogicCode.choices line 142

    Source documentation

    Right-associated finite disjunction used by the source query object.

    def choices (xs : List α) (mark property : α → Expr S) : Expr S :=
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr

41. theorem OAI.PureTypeSystem.Labelled.LogicCode.choices_nil line 145
42. theorem OAI.PureTypeSystem.Labelled.LogicCode.choices_cons line 146
43. theorem OAI.PureTypeSystem.Labelled.LogicCode.choices_rename line 149
44. theorem OAI.PureTypeSystem.Labelled.LogicCode.choices_subst line 156
45. theorem OAI.PureTypeSystem.Labelled.LogicSetup.choices_formula line 167
46. theorem OAI.PureTypeSystem.Labelled.LogicSetup.choices_false line 175
47. theorem OAI.PureTypeSystem.Labelled.LogicSetup.choices_select line 194
48. theorem OAI.PureTypeSystem.Labelled.LogicSetup.Family.choices line 227
49. def OAI.PureTypeSystem.Labelled.DoubleCode.realizationBody line 249

    Source documentation

    The source's seven structural branches; evaluation tag 7 is excluded.

    def realizationBody (U : DataWrapper S true) (L : LogicCode S) (T c : Expr S) (Q : Fin 7 → Expr S) :=
    …

    Mentions: OAI.PureTypeSystem.Labelled.DataWrapper, OAI.PureTypeSystem.Labelled.Expr

50. def OAI.PureTypeSystem.Labelled.DoubleCode.realization line 252
51. theorem OAI.PureTypeSystem.Labelled.DoubleCode.realizationBody_instantiate line 255
52. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.realizationBody_family line 277
53. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.realization_typed line 281
54. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.realization_evaluation line 287
55. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.realization_query_decoded line 296
56. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.realization_not_dummy line 324
57. structure OAI.PureTypeSystem.Labelled.SpecializedCode line 348
58. def OAI.PureTypeSystem.Labelled.SpecializedCode.rename line 353
59. def OAI.PureTypeSystem.Labelled.SpecializedCode.subst line 354
60. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rename_comp line 355
61. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.subst_rename line 357
62. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rename_subst line 359
63. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.instantiate_raise line 361
64. def OAI.PureTypeSystem.Labelled.SpecializedCode.relational line 363
65. def OAI.PureTypeSystem.Labelled.SpecializedCode.baseType line 364
66. def OAI.PureTypeSystem.Labelled.SpecializedCode.xType line 365
67. def OAI.PureTypeSystem.Labelled.SpecializedCode.yType line 366
68. def OAI.PureTypeSystem.Labelled.SpecializedCode.predType line 367
69. def OAI.PureTypeSystem.Labelled.SpecializedCode.xPredType line 368
70. def OAI.PureTypeSystem.Labelled.SpecializedCode.ev line 369
71. def OAI.PureTypeSystem.Labelled.SpecializedCode.gStep line 370
72. def OAI.PureTypeSystem.Labelled.SpecializedCode.gAtBody line 372
73. def OAI.PureTypeSystem.Labelled.SpecializedCode.gAt line 374
74. def OAI.PureTypeSystem.Labelled.SpecializedCode.gBody line 376
75. def OAI.PureTypeSystem.Labelled.SpecializedCode.propertyG line 378
76. def OAI.PureTypeSystem.Labelled.SpecializedCode.cStep line 380
77. def OAI.PureTypeSystem.Labelled.SpecializedCode.cAtBody line 382
78. def OAI.PureTypeSystem.Labelled.SpecializedCode.cAt line 384
79. def OAI.PureTypeSystem.Labelled.SpecializedCode.cBody line 386
80. def OAI.PureTypeSystem.Labelled.SpecializedCode.propertyC line 388
81. def OAI.PureTypeSystem.Labelled.SpecializedCode.eStep line 390
82. def OAI.PureTypeSystem.Labelled.SpecializedCode.eAtBody line 392
83. def OAI.PureTypeSystem.Labelled.SpecializedCode.eAt line 394
84. def OAI.PureTypeSystem.Labelled.SpecializedCode.eBody line 396
85. def OAI.PureTypeSystem.Labelled.SpecializedCode.propertyE line 398
86. def OAI.PureTypeSystem.Labelled.SpecializedCode.rPredStep line 400
87. def OAI.PureTypeSystem.Labelled.SpecializedCode.rPredBody line 402
88. def OAI.PureTypeSystem.Labelled.SpecializedCode.rPred line 404
89. def OAI.PureTypeSystem.Labelled.SpecializedCode.rStep line 406
90. def OAI.PureTypeSystem.Labelled.SpecializedCode.rBody line 408
91. def OAI.PureTypeSystem.Labelled.SpecializedCode.rAll line 410
92. def OAI.PureTypeSystem.Labelled.SpecializedCode.propertyR line 412
93. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.baseType_rename line 414
94. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.baseType_subst line 417
95. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.xType_rename line 420
96. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.xType_subst line 423
97. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.yType_rename line 426
98. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.yType_subst line 429
99. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.predType_rename line 432
100. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.predType_subst line 435
101. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.xPredType_rename line 438
102. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.xPredType_subst line 441
103. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.ev_rename line 444
104. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.ev_subst line 447
105. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gStep_rename line 450
106. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gStep_subst line 454
107. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gAtBody_rename line 458
108. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gAtBody_subst line 462
109. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gAtBody_instantiate line 466
110. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gAt_rename line 469
111. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gAt_subst line 473
112. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gBody_rename line 477
113. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gBody_subst line 481
114. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.gBody_instantiate line 485
115. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyG_rename line 488
116. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyG_subst line 492
117. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cStep_rename line 496
118. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cStep_subst line 500
119. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cAtBody_rename line 504
120. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cAtBody_subst line 508
121. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cAtBody_instantiate line 512
122. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cAt_rename line 515
123. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cAt_subst line 519
124. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cBody_rename line 523
125. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cBody_subst line 527
126. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.cBody_instantiate line 531
127. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyC_rename line 534
128. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyC_subst line 538
129. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eStep_rename line 542
130. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eStep_subst line 546
131. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eAtBody_rename line 550
132. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eAtBody_subst line 554
133. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eAtBody_instantiate line 558
134. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eAt_rename line 561
135. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eAt_subst line 565
136. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eBody_rename line 569
137. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eBody_subst line 573
138. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.eBody_instantiate line 577
139. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyE_rename line 580
140. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyE_subst line 584
141. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPredStep_rename line 588
142. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPredStep_subst line 592
143. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPredBody_rename line 596
144. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPredBody_subst line 600
145. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPredBody_instantiate line 604
146. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPred_rename line 607
147. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rPred_subst line 611
148. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rStep_rename line 615
149. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rStep_subst line 619
150. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rBody_rename line 623
151. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rBody_subst line 627
152. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rBody_instantiate line 631
153. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rAll_rename line 634
154. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.rAll_subst line 638
155. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyR_rename line 642
156. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyR_subst line 646
157. structure OAI.PureTypeSystem.Labelled.ObservationCode.Formed line 658
158. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.rename line 666
159. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.copies_formed line 669
160. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.carrier_sorted line 671
161. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.carrier_mode line 673
162. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.tagged_typed line 675
163. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.bitInner_formula line 679
164. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.bitOuter_formula line 682
165. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.observe_formula line 685
166. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.observeBody_family line 691
167. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compareBody_family line 698
168. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_formula line 703
169. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_formula line 711
170. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.tagged_observe line 720

     Source documentation

     The source's canonical O_i(x^t) evaluation is the genuine le(i,x).

     theorem tagged_observe {i x : Expr S} (t : Fin 3)
         (hi : HasType P Γ i (O.relational.channel.predicateType O.relational.probe.carrier)) (mi : WellModed γ i .data)
         (hx : HasType P Γ x (O.relational.channel.logicalType O.relational.probe.carrier)) (mx : WellModed γ x .data) :
         Equivalent P Γ γ (O.observe L.code KY.code KP.code i (O.tagged L.code t x))
           (O.relational.le L.code KY.code KP.code i x) := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Equivalent

171. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_intro line 739
172. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_elim line 761
173. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_intro line 774
174. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_elim line 789
175. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.carrier_typed_rename line 813
176. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_proof_rename line 818
177. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_refl line 824
178. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_symm line 832
179. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_trans line 846
180. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_refl line 866
181. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_symm line 874
182. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_trans line 885
183. theorem OAI.PureTypeSystem.Labelled.LogicSetup.iff_equivalent line 906
184. theorem OAI.PureTypeSystem.Labelled.LogicSetup.imp_equivalent line 913
185. theorem OAI.PureTypeSystem.Labelled.LogicSetup.conj_equivalent line 920
186. theorem OAI.PureTypeSystem.Labelled.LogicSetup.disj_congr line 927
187. theorem OAI.PureTypeSystem.Labelled.LogicSetup.signed_agree line 934
188. theorem OAI.PureTypeSystem.Labelled.LogicSetup.signed_disagree line 945
189. theorem OAI.PureTypeSystem.Labelled.LogicSetup.agreed_bits line 955
190. theorem OAI.PureTypeSystem.Labelled.LogicSetup.different_bits_left line 961
191. theorem OAI.PureTypeSystem.Labelled.LogicSetup.different_bits_right line 966
192. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.tagged_bitInner line 983
193. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.tagged_bitOuter line 988
194. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.compare_tagged line 993
195. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_tagged_same line 1022
196. theorem OAI.PureTypeSystem.Labelled.ObservationCode.Formed.ae_tagged_distinct line 1040
197. structure OAI.PureTypeSystem.Labelled.SpecializedCode.Formed line 1066
198. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rename line 1078
199. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.relational_formed line 1090
200. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.base_sorted line 1092
201. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.base_mode line 1093
202. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.y_sorted line 1094
203. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.y_mode line 1095
204. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.x_sorted line 1096
205. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.x_mode line 1097
206. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pred_sorted line 1098
207. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.pred_mode line 1099
208. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.ev_formula line 1101
209. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.tagged_typed line 1105
210. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gStep_formula line 1108
211. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gAtBody_family line 1115
212. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gAt_formula line 1129
213. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gBody_family line 1136
214. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_formula line 1147
215. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cStep_formula line 1153
216. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cAtBody_family line 1161
217. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cAt_formula line 1175
218. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cBody_family line 1182
219. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyC_formula line 1193
220. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eStep_formula line 1198
221. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eAtBody_family line 1207
222. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eAt_formula line 1221
223. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eBody_family line 1228
224. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyE_formula line 1239
225. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rPredStep_formula line 1244
226. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rPredBody_family line 1251
227. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rPred_typed line 1262
228. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rStep_formula line 1268
229. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rBody_family line 1277
230. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rAll_formula line 1288
231. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyR_formula line 1294
232. def OAI.PureTypeSystem.Labelled.SpecializedCode.property line 1305

     Source documentation

     The seven source structural tags G,C0,Cl,Cr,El,Er,R, in that order.

     def property (L : LogicCode S) (KY KP : QuantifierCode S) (t : Fin 7) (v : Expr S) :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierCode, OAI.PureTypeSystem.Labelled.Expr

233. def OAI.PureTypeSystem.Labelled.SpecializedCode.propertyBody line 1315
234. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.property_rename line 1318
235. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.property_subst line 1321
236. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyBody_rename line 1324
237. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyBody_instantiate line 1329
238. def OAI.PureTypeSystem.Labelled.SpecializedCode.parameter line 1335

     Source documentation

     This is m0 itself, with no recursive occurrence in its seven properties.

     def parameter (L : LogicCode S) (KY KP : QuantifierCode S) :=
     …

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierCode

239. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.property_formula line 1346
240. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyBody_family line 1357
241. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.parameter_typed line 1362
242. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.parameter_not_dummy line 1373
243. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.parameter_query_decoded line 1384
244. theorem OAI.PureTypeSystem.Labelled.LogicSetup.guarded_equivalent_future line 1409

     Source documentation

     The source's guarded comparison builder, with a genuine proof binder.

     theorem guarded_equivalent_future (hA : L.Formula A) (hB : L.Formula B) (hD : L.Formula D)
         (hh : ∀ Δ δ (e : Embedding P Γ γ Δ δ), Proves P Δ δ (A.rename e.names) →
           Equivalent P Δ δ (B.rename e.names) (D.rename e.names)) :
         Equivalent P Γ γ (L.imp A B) (L.imp A D) := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.Embedding, OAI.PureTypeSystem.Labelled.Proves, OAI.PureTypeSystem.Labelled.Equivalent

245. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.v_typed_rename line 1435
246. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.y_typed_rename line 1439
247. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.x_typed_rename line 1443
248. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.comparison_rename line 1447
249. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.ev_compare line 1456
250. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gStep_respect line 1464
251. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cStep_respect line 1482
252. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eStep_respect line 1498
253. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.gAt_respect line 1516
254. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyG_respect line 1531
255. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.cAt_respect line 1544
256. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyC_respect line 1559
257. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.eAt_respect line 1572
258. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyE_respect line 1587
259. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.relational_rename line 1603
260. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.observation_rename line 1604
261. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rPred_evaluation line 1612
262. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rPred_compare_at line 1622
263. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rPred_respect line 1645
264. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rConsequence_respect line 1660
265. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rStep_respect line 1677
266. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.rAll_respect line 1698
267. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.propertyR_respect line 1711
268. def OAI.PureTypeSystem.Labelled.SpecializedCode.decoded line 1724
269. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.decoded_rename line 1727
270. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.property_respect line 1739
271. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.decoded_typed line 1753
272. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.decoded_at line 1762
273. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.decoded_compare line 1772
274. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.parameter_query_formula line 1787
275. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.Formed.parameter_query line 1796

     Source documentation

     Exact source q_t(P), from actual cancellation and the proved respect law.

     theorem parameter_query (t : Fin 7) {v : Expr S}
         (hv : HasType P Γ v B.predType) (mv : WellModed γ v .data) :
         Equivalent P Γ γ
           (B.relational.probe.doubled.query B.relational.predicate L.code t.castSucc (B.relational.probe.rawType B.type)
             (B.parameter L.code KY.code KP.code) v)
           (B.property L.code KY.code KP.code t v) := by
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.Equivalent

276. theorem OAI.PureTypeSystem.Labelled.DoubleCode.realizationBody_rename line 1816
277. theorem OAI.PureTypeSystem.Labelled.DoubleCode.realizationBody_subst line 1821
278. theorem OAI.PureTypeSystem.Labelled.DoubleCode.realization_rename line 1826
279. theorem OAI.PureTypeSystem.Labelled.DoubleCode.realization_subst line 1831
280. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.propertyBody_subst line 1839
281. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.parameter_rename line 1846
282. theorem OAI.PureTypeSystem.Labelled.SpecializedCode.parameter_subst line 1850