OAI/Computability/TypeSystem/Channels.lean

GitHub source file

245 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.Labelled.LogicSetup.neg_equivalent line 11
2. theorem OAI.PureTypeSystem.Labelled.LogicSetup.sign_equivalent line 16
3. structure OAI.PureTypeSystem.Labelled.DoubleCode line 23
4. def OAI.PureTypeSystem.Labelled.DoubleCode.rename line 28
5. def OAI.PureTypeSystem.Labelled.DoubleCode.subst line 29
6. def OAI.PureTypeSystem.Labelled.DoubleCode.carrier line 30
7. def OAI.PureTypeSystem.Labelled.DoubleCode.emb line 31
8. def OAI.PureTypeSystem.Labelled.DoubleCode.bit line 33
9. def OAI.PureTypeSystem.Labelled.DoubleCode.eval line 35
10. def OAI.PureTypeSystem.Labelled.DoubleCode.recover line 36
11. structure OAI.PureTypeSystem.Labelled.DoubleCode.Formed line 41
12. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.rename line 46
13. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.sorted line 50
14. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.mode line 51
15. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.emb_typed line 53
16. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.eval_formula line 58
17. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bit_formula line 63
18. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.rec_formula line 67
19. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.emb_evaluation line 72
20. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.emb_bit line 90
21. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.emb_recovery line 103
22. structure OAI.PureTypeSystem.Labelled.ChannelCode line 124

    Source documentation

    The fixed odd paths of the first (and later probe) observation channel.

    structure ChannelCode (S : Type u) where
    …

23. def OAI.PureTypeSystem.Labelled.ChannelCode.rename line 131
24. def OAI.PureTypeSystem.Labelled.ChannelCode.subst line 133
25. def OAI.PureTypeSystem.Labelled.ChannelCode.logicalType line 135
26. def OAI.PureTypeSystem.Labelled.ChannelCode.rawType line 136
27. def OAI.PureTypeSystem.Labelled.ChannelCode.predicateType line 137
28. def OAI.PureTypeSystem.Labelled.ChannelCode.toRaw line 138
29. def OAI.PureTypeSystem.Labelled.ChannelCode.toLog line 139
30. def OAI.PureTypeSystem.Labelled.ChannelCode.round line 140
31. def OAI.PureTypeSystem.Labelled.ChannelCode.eval line 141
32. def OAI.PureTypeSystem.Labelled.ChannelCode.pred line 142
33. structure OAI.PureTypeSystem.Labelled.ChannelCode.Formed line 147
34. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.rename line 154
35. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.logical_sorted line 161
36. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.raw_sorted line 162
37. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.predicate_sorted line 163
38. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.logical_mode line 164
39. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.raw_mode line 165
40. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.predicate_mode line 166
41. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.toRaw_typed line 168
42. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.toLog_typed line 172
43. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.round_typed line 176
44. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.eval_formula line 181
45. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.pred_typed line 187
46. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.primitive_round line 193
47. theorem OAI.PureTypeSystem.Labelled.ChannelCode.Formed.pred_evaluation line 207
48. theorem OAI.PureTypeSystem.Labelled.DataWrapper.Formed.of_secondary_path line 220
49. structure OAI.PureTypeSystem.Labelled.ChannelSetup line 231

    Source documentation

    All roles use fixed path syntax selected once from the forbidden configuration. In particular the shared raw wrapper is not reselected when constructing a query, bundle, or the second channel.

    structure ChannelSetup {Γ : List (Expr S)} {γ : Nat → Mode} {C : Set (Set S)}
        (L : LogicSetup P Γ γ C) where
    …

    Mentions: OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.Mode, OAI.PureTypeSystem.Labelled.LogicSetup

50. def OAI.PureTypeSystem.Labelled.ChannelSetup.doubled line 265
51. theorem OAI.PureTypeSystem.Labelled.ChannelSetup.doubled_formed line 266
52. theorem OAI.PureTypeSystem.Labelled.ChannelSetup.exists_setup line 269
53. theorem OAI.PureTypeSystem.Labelled.LogicCode.subst_rename line 289
54. theorem OAI.PureTypeSystem.Labelled.LogicCode.rename_subst line 292
55. theorem OAI.PureTypeSystem.Labelled.DoubleCode.rename_comp line 298
56. theorem OAI.PureTypeSystem.Labelled.DoubleCode.instantiate_raise line 300
57. theorem OAI.PureTypeSystem.Labelled.DoubleCode.subst_rename line 302
58. theorem OAI.PureTypeSystem.Labelled.DoubleCode.rename_subst line 305
59. theorem OAI.PureTypeSystem.Labelled.DoubleCode.carrier_rename line 308
60. theorem OAI.PureTypeSystem.Labelled.DoubleCode.carrier_subst line 311
61. theorem OAI.PureTypeSystem.Labelled.DoubleCode.emb_rename line 314
62. theorem OAI.PureTypeSystem.Labelled.DoubleCode.emb_subst line 319
63. theorem OAI.PureTypeSystem.Labelled.DoubleCode.eval_rename line 325
64. theorem OAI.PureTypeSystem.Labelled.DoubleCode.eval_subst line 329
65. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bit_rename line 333
66. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bit_subst line 340
67. theorem OAI.PureTypeSystem.Labelled.DoubleCode.rec_rename line 347
68. theorem OAI.PureTypeSystem.Labelled.DoubleCode.rec_subst line 350
69. def OAI.PureTypeSystem.Labelled.DoubleCode.bitBody line 354
70. def OAI.PureTypeSystem.Labelled.DoubleCode.recBody line 356
71. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bitBody_instantiate line 358
72. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recBody_instantiate line 362
73. theorem OAI.PureTypeSystem.Labelled.DoubleCode.bitBody_rename line 371
74. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recBody_rename line 375
75. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bitBody_family line 386
76. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.recBody_family line 393
77. def OAI.PureTypeSystem.Labelled.DoubleCode.tower line 402
78. def OAI.PureTypeSystem.Labelled.DoubleCode.embed line 405
79. def OAI.PureTypeSystem.Labelled.DoubleCode.recoveryBody line 408
80. def OAI.PureTypeSystem.Labelled.DoubleCode.tagBody line 411
81. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tower_rename line 417
82. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tower_subst line 422
83. theorem OAI.PureTypeSystem.Labelled.DoubleCode.embed_rename line 427
84. theorem OAI.PureTypeSystem.Labelled.DoubleCode.embed_subst line 432
85. theorem OAI.PureTypeSystem.Labelled.DoubleCode.recoveryBody_rename line 437
86. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tagBody_rename line 443
87. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.tower_sorted line 460
88. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.tower_mode line 464
89. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.embed_typed line 469
90. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.recoveryBody_family line 476
91. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.tagBody_family line 482
92. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.embed_recovery line 490
93. theorem OAI.PureTypeSystem.Labelled.LogicCode.conj_instantiate_raise line 513
94. theorem OAI.PureTypeSystem.Labelled.LogicSetup.signed_sign line 519
95. theorem OAI.PureTypeSystem.Labelled.LogicSetup.signed_conj line 526
96. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.embed_tag line 538
97. def OAI.PureTypeSystem.Labelled.queryBits line 581

    Source documentation

    Nine distinct finite query strings. Index zero is the payload tag.

    def queryBits (q : Fin 9) : List Bool :=
    …

98. theorem OAI.PureTypeSystem.Labelled.queryBits_length line 583
99. theorem OAI.PureTypeSystem.Labelled.queryBits_injective line 584
100. def OAI.PureTypeSystem.Labelled.queryTag line 588
101. theorem OAI.PureTypeSystem.Labelled.queryTag_ne_zero line 589
102. def OAI.PureTypeSystem.Labelled.DoubleCode.big line 594
103. def OAI.PureTypeSystem.Labelled.DoubleCode.bpType line 595
104. def OAI.PureTypeSystem.Labelled.DoubleCode.paramType line 596
105. def OAI.PureTypeSystem.Labelled.DoubleCode.tagged line 597
106. def OAI.PureTypeSystem.Labelled.DoubleCode.encodeBody line 599
107. def OAI.PureTypeSystem.Labelled.DoubleCode.encode line 604
108. def OAI.PureTypeSystem.Labelled.DoubleCode.mark line 606
109. def OAI.PureTypeSystem.Labelled.DoubleCode.query line 608
110. def OAI.PureTypeSystem.Labelled.DoubleCode.embedBody line 611
111. def OAI.PureTypeSystem.Labelled.DoubleCode.decoderBody line 613
112. def OAI.PureTypeSystem.Labelled.DoubleCode.decode line 615
113. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tagged_rename line 618
114. theorem OAI.PureTypeSystem.Labelled.DoubleCode.tagged_subst line 621
115. theorem OAI.PureTypeSystem.Labelled.DoubleCode.encodeBody_rename line 625
116. theorem OAI.PureTypeSystem.Labelled.DoubleCode.embedBody_instantiate line 632
117. theorem OAI.PureTypeSystem.Labelled.DoubleCode.embedBody_rename line 636
118. theorem OAI.PureTypeSystem.Labelled.DoubleCode.decoderBody_instantiate line 641
119. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.tagged_typed line 651
120. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bp_sorted line 656
121. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.bp_mode line 658
122. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.param_sorted line 660
123. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.param_mode line 662
124. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.encodeBody_family line 667
125. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.encode_typed line 674
126. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.embedBody_map line 680
127. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.decoderBody_family line 688
128. theorem OAI.PureTypeSystem.Labelled.DoubleCode.Formed.decode_typed line 694
129. theorem OAI.PureTypeSystem.Labelled.DataWrapper.apply_converts line 703
130. structure OAI.PureTypeSystem.Labelled.ProbeCode line 712

     Source documentation

     The A-independent syntax of the common probe type.

     structure ProbeCode (S : Type u) where
     …

131. def OAI.PureTypeSystem.Labelled.ProbeCode.rename line 724
132. def OAI.PureTypeSystem.Labelled.ProbeCode.subst line 727
133. def OAI.PureTypeSystem.Labelled.ProbeCode.doubled line 730
134. def OAI.PureTypeSystem.Labelled.ProbeCode.rawType line 731
135. def OAI.PureTypeSystem.Labelled.ProbeCode.paramType line 732
136. def OAI.PureTypeSystem.Labelled.ProbeCode.singleType line 733
137. def OAI.PureTypeSystem.Labelled.ProbeCode.funType line 734
138. def OAI.PureTypeSystem.Labelled.ProbeCode.domain line 735
139. def OAI.PureTypeSystem.Labelled.ProbeCode.body line 736
140. def OAI.PureTypeSystem.Labelled.ProbeCode.carrier line 738
141. theorem OAI.PureTypeSystem.Labelled.ProbeCode.doubled_rename line 740
142. theorem OAI.PureTypeSystem.Labelled.ProbeCode.doubled_subst line 741
143. theorem OAI.PureTypeSystem.Labelled.ProbeCode.rawType_rename line 743
144. theorem OAI.PureTypeSystem.Labelled.ProbeCode.rawType_subst line 746
145. theorem OAI.PureTypeSystem.Labelled.ProbeCode.paramType_rename line 749
146. theorem OAI.PureTypeSystem.Labelled.ProbeCode.paramType_subst line 753
147. theorem OAI.PureTypeSystem.Labelled.ProbeCode.singleType_rename line 757
148. theorem OAI.PureTypeSystem.Labelled.ProbeCode.singleType_subst line 760
149. theorem OAI.PureTypeSystem.Labelled.ProbeCode.funType_rename line 763
150. theorem OAI.PureTypeSystem.Labelled.ProbeCode.funType_subst line 766
151. theorem OAI.PureTypeSystem.Labelled.ProbeCode.instantiate_raise line 769
152. theorem OAI.PureTypeSystem.Labelled.ProbeCode.body_instantiate line 773
153. structure OAI.PureTypeSystem.Labelled.ProbeCode.Formed line 781
154. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.rename line 795
155. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.seed_sorted line 800
156. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.domain_sorted line 804
157. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.domain_mode line 805
158. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.raw_sorted line 806
159. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.raw_mode line 808
160. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.doubled_formed line 810
161. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.param_sorted line 811
162. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.param_mode line 813
163. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.single_sorted line 815
164. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.single_mode line 817
165. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.fun_sorted line 819
166. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.fun_mode line 822
167. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.body_sorted line 825
168. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.body_mode line 834
169. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.carrier_sorted line 840
170. theorem OAI.PureTypeSystem.Labelled.ProbeCode.Formed.carrier_mode line 845
171. def OAI.PureTypeSystem.Labelled.ChannelSetup.probe line 853
172. theorem OAI.PureTypeSystem.Labelled.ChannelSetup.probe_formed line 855
173. theorem OAI.PureTypeSystem.IsComponent.matched_return line 866

     Source documentation

     A secondary return can always be chosen with the outward parity.

     theorem matched_return (hC : IsComponent E C) {v w : V} {b : Bool}
         (hv : v ∈ C) (hw : w ∈ C) (hp : SignedPath E v w b) : SignedPath E w v b := by
     …

     Mentions: OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.SignedPath

174. structure OAI.PureTypeSystem.Labelled.ChannelReturn line 880

     Source documentation

     The parity-matched return is retained alongside, not substituted for, the fixed channel paths.

     structure ChannelReturn (K : ChannelSetup L) where
     …

     Mentions: OAI.PureTypeSystem.Labelled.ChannelSetup

175. theorem OAI.PureTypeSystem.Labelled.ChannelSetup.exists_setup_return line 885
176. def OAI.PureTypeSystem.Labelled.ChannelReturn.evenLoop line 907
177. def OAI.PureTypeSystem.Labelled.ChannelReturn.fourth line 909
178. def OAI.PureTypeSystem.Labelled.ChannelReturn.firstDouble line 910
179. def OAI.PureTypeSystem.Labelled.ChannelReturn.outerDouble line 911
180. def OAI.PureTypeSystem.Labelled.ChannelReturn.type line 913

     Source documentation

     Specific source A0: two fixed odd-pair detours followed by the matched return.

     def type : Expr S := R.route.apply (K.returnPath.apply (K.channel.raw.apply
     …

     Mentions: OAI.PureTypeSystem.Labelled.Expr

181. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.evenLoop_formed line 916
182. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.fourth_formed line 918
183. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.firstDouble_formed line 920
184. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.outerDouble_formed line 922
185. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.type_sorted line 925
186. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.type_mode line 929
187. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.evenLoop_apply line 933
188. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.fourth_apply line 935
189. theorem OAI.PureTypeSystem.Labelled.ChannelReturn.factorization line 939

     Source documentation

     The five odd segments have exactly the required endpoint, not merely an isomorphic or propositionally related placeholder type.

     theorem factorization :
         R.outerDouble.carrier (R.firstDouble.carrier (K.channel.raw.apply K.probe.carrier)) =
         K.channel.logicalType (K.initial.apply R.type) := by
     …

190. theorem OAI.PureTypeSystem.Labelled.ChannelCode.rename_comp line 955
191. theorem OAI.PureTypeSystem.Labelled.ChannelCode.instantiate_raise line 957
192. theorem OAI.PureTypeSystem.Labelled.ChannelCode.logicalType_rename line 959
193. theorem OAI.PureTypeSystem.Labelled.ChannelCode.logicalType_subst line 962
194. theorem OAI.PureTypeSystem.Labelled.ChannelCode.rawType_rename line 965
195. theorem OAI.PureTypeSystem.Labelled.ChannelCode.rawType_subst line 968
196. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predicateType_rename line 971
197. theorem OAI.PureTypeSystem.Labelled.ChannelCode.predicateType_subst line 974
198. theorem OAI.PureTypeSystem.Labelled.ChannelCode.toRaw_rename line 977
199. theorem OAI.PureTypeSystem.Labelled.ChannelCode.toRaw_subst line 980
200. theorem OAI.PureTypeSystem.Labelled.ChannelCode.toLog_rename line 983
201. theorem OAI.PureTypeSystem.Labelled.ChannelCode.toLog_subst line 986
202. theorem OAI.PureTypeSystem.Labelled.ChannelCode.round_rename line 989
203. theorem OAI.PureTypeSystem.Labelled.ChannelCode.round_subst line 992
204. theorem OAI.PureTypeSystem.Labelled.ChannelCode.eval_rename line 995
205. theorem OAI.PureTypeSystem.Labelled.ChannelCode.eval_subst line 999
206. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_formula_family line 1013

     Source documentation

     Data quantification using a uniform formula callback; the quantified annotation is still the original retained direct profile.

     theorem all_formula_family {I : Set S} (R : QuantifierRoute L.witnesses C L.base I)
         {T Q : Expr S} (hT : SortedAt P Γ T I) (mT : WellModed γ T .data)
         {s : S} (hs : HasType P Γ T (.sort s)) (hQ : L.Family T Q) :
         L.Formula (all R T Q) := all_formula R hT mT hs (hQ.opened hs)

     Mentions: OAI.PureTypeSystem.Labelled.QuantifierRoute, OAI.PureTypeSystem.Labelled.Expr, OAI.PureTypeSystem.Labelled.SortedAt, OAI.PureTypeSystem.Labelled.WellModed, OAI.PureTypeSystem.Labelled.HasType, OAI.PureTypeSystem.Labelled.LogicSetup.all, OAI.PureTypeSystem.Labelled.LogicSetup.all_formula

207. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_intro_future line 1018
208. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_elim_family line 1034
209. structure OAI.PureTypeSystem.Labelled.QuantifierCode line 1043

     Source documentation

     The two fixed proof paths implementing a direct-domain universal.

     structure QuantifierCode (S : Type u) where
     …

210. def OAI.PureTypeSystem.Labelled.QuantifierCode.rename line 1048
211. def OAI.PureTypeSystem.Labelled.QuantifierCode.subst line 1049
212. def OAI.PureTypeSystem.Labelled.QuantifierCode.all line 1050
213. theorem OAI.PureTypeSystem.Labelled.QuantifierCode.rename_comp line 1051
214. theorem OAI.PureTypeSystem.Labelled.QuantifierCode.instantiate_raise line 1053
215. theorem OAI.PureTypeSystem.Labelled.QuantifierCode.all_rename line 1055
216. theorem OAI.PureTypeSystem.Labelled.QuantifierCode.all_subst line 1059
217. def OAI.PureTypeSystem.Labelled.QuantifierRoute.code line 1067
218. theorem OAI.PureTypeSystem.Labelled.QuantifierRoute.code_rename line 1068
219. theorem OAI.PureTypeSystem.Labelled.LogicSetup.all_code line 1074
220. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_imp line 1083
221. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_neg line 1084
222. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_bottom line 1085
223. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_top line 1086
224. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_conj line 1087
225. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_disj line 1088
226. theorem OAI.PureTypeSystem.Labelled.LogicSetup.code_iff line 1089
227. theorem OAI.PureTypeSystem.Labelled.Expr.lifted_comp line 1096
228. theorem OAI.PureTypeSystem.Labelled.Expr.callback_rename line 1099
229. def OAI.PureTypeSystem.Labelled.LogicCode.guardBody line 1106
230. def OAI.PureTypeSystem.Labelled.LogicCode.guardAll line 1107
231. theorem OAI.PureTypeSystem.Labelled.LogicCode.guardBody_rename line 1108
232. theorem OAI.PureTypeSystem.Labelled.LogicCode.guardBody_instantiate line 1113
233. theorem OAI.PureTypeSystem.Labelled.LogicCode.guardAll_rename line 1116
234. theorem OAI.PureTypeSystem.Labelled.LogicSetup.guardAll_formula line 1128
235. theorem OAI.PureTypeSystem.Labelled.LogicSetup.guardAll_elim line 1132
236. theorem OAI.PureTypeSystem.Labelled.LogicSetup.guardAll_intro line 1142
237. theorem OAI.PureTypeSystem.Labelled.LogicSetup.cond_yes line 1170
238. theorem OAI.PureTypeSystem.Labelled.LogicSetup.cond_no line 1176
239. theorem OAI.PureTypeSystem.Labelled.LogicSetup.cond_top_yes line 1182
240. theorem OAI.PureTypeSystem.Labelled.LogicSetup.query_positive line 1187
241. theorem OAI.PureTypeSystem.Labelled.LogicSetup.query_negative line 1192
242. theorem OAI.PureTypeSystem.Labelled.LogicSetup.query_payload line 1197
243. theorem OAI.PureTypeSystem.Labelled.LogicSetup.equivalent_bottom_neg line 1205
244. theorem OAI.PureTypeSystem.Labelled.LogicSetup.equivalent_conj_neg line 1209
245. theorem OAI.PureTypeSystem.Labelled.LogicSetup.equivalent_conj_yes line 1214