]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
slight refactoring in the proof of strong normalization
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
1 name "basic_2_src"
2
3 table {
4    class "gray"
5    [ { "component" * } {
6         [ { "plane" * } {
7              [ "files" * ]
8           }
9         ]
10      }
11    ]
12    class "wine"
13    [ { "examples" * } {
14         [ { "terms with special features" * } {
15              [ "ex_sta_ldec" + "ex_cpr_omega" * ]
16           }
17         ]
18      }
19    ]
20    class "magenta"
21    [ { "" * } {
22         [ { "" * } {
23              [ "" * ]
24           }
25         ]
26      }
27    ]
28 (*   
29    [ { "higher order dynamic typing" * } {
30         [ { "higher order native type assignment" * } {
31              [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
32           }
33         ]
34      }
35    ]
36 *)
37    class "prune"
38    [ { "dynamic typing" * } {
39 (*
40         [ { "local env. ref. for native type assignment" * } {
41              [ "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ]
42           }
43         ]
44         [ { "native type assignment" * } {
45              [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
46           }
47         ]
48 *)
49         [ { "local env. ref. for stratified native validity" * } {
50              [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
51           }
52         ]
53         [ { "stratified native validity" * } {
54              [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
55              [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_scpes" + "snv_preserve" * ]
56           }
57         ]
58      }
59    ]
60    class "blue"
61    [ { "equivalence" * } {
62         [ { "decomposed extended equivalence" * } {
63              [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
64           }
65         ]
66         [ { "context-sensitive equivalence" * } {
67              [ "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
68           }
69         ]
70      }
71    ]
72    class "sky"
73    [ { "conversion" * } {
74         [ { "context-sensitive conversion" * } {
75              [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )" "cpc_cpc" * ]
76           }
77         ]
78      }
79    ]
80    class "cyan"
81    [ { "computation" * } {
82         [ { "evaluation for context-sensitive extended reduction" * } {
83              [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ]
84           }
85         ]
86         [ { "evaluation for context-sensitive reduction" * } {
87              [ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ]
88           }
89         ]
90         [ { "strongly normalizing \"big tree\" computation" * } {
91              [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ]
92           }
93         ]
94         [ { "strongly normalizing extended computation" * } {
95              [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
96              [ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
97              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ]
98              [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ]
99           }
100         ]
101         [ { "\"big tree\" parallel computation" * } {
102              [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ]
103              [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ]
104              [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" + "fpbu_fleq" * ]
105              [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ]
106           }
107         ]
108         [ { "decomposed extended computation" * } {
109              [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
110           }
111         ]
112         [ { "context-sensitive extended computation" * } {
113              [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
114              [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
115           }
116         ]
117         [ { "context-sensitive computation" * } {
118              [ "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ]
119              [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
120           }
121         ]
122         [ { "local env. ref. for generic reducibility" * } {
123              [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ]
124           }
125         ]
126         [ { "support for generic computation properties" * } {
127              [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
128           }
129         ]
130      }
131    ]
132    class "water"
133    [ { "reduction" * } {
134         [ { "\"big tree\" parallel reduction" * } {
135              [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_aaa" * ]
136           }
137         ]
138         [ { "normal forms for context-sensitive extended reduction" * } {
139              [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
140           }
141         ]
142         [ { "context-sensitive extended reduction" * } {
143              [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
144              [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
145           }
146         ]
147         [ { "irreducible forms for context-sensitive extended reduction" * } {
148              [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ]
149           }
150         ]
151         [ { "reducible forms for context-sensitive extended reduction" * } {
152              [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ]
153           }
154         ]
155         [ { "normal forms for context-sensitive reduction" * } {
156              [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
157           }
158         ]
159         [ { "context-sensitive reduction" * } {
160              [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ]
161              [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_llpx_sn" + "cpr_cir" * ]
162           }
163         ]
164         [ { "irreducible forms for context-sensitive reduction" * } {
165              [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ]
166           }
167         ]
168         [ { "reducible forms for context-sensitive reduction" * } {
169              [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ]
170           }
171         ]
172      }
173    ]
174    class "green"
175    [ { "unfold" * } {
176         [ { "unfold" * } {
177              [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ]
178           }
179         ]
180         [ { "iterated static type assignment" * } {
181              [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ]
182           }
183         ]
184      }
185    ]
186    class "grass"
187    [ { "static typing" * } {
188         [ { "local env. ref. for degree assignment" * } {
189              [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
190           }
191         ]
192         [ { "degree assignment" * } {
193              [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ]
194           }
195         ]
196         [ { "parameters" * } {
197              [ "sh" "sd" * ]
198           }
199         ]
200         [ { "local env. ref. for atomic arity assignment" * } {
201              [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
202           }
203         ]
204         [ { "atomic arity assignment" * } {
205              [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_fqus" + "aaa_lleq" + "aaa_aaa" * ]
206           }
207         ]
208         [ { "restricted local env. ref." * } {
209              [ "lsubr ( ? ⫃ ? )" "lsubr_lsubr" * ]
210           }
211         ]
212      }
213    ]
214    class "yellow"
215    [ { "multiple substitution" * } {
216         [ { "lazy equivalence" * } {
217              [ "fleq ( ⦃?,?,?⦄ ≡[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
218              [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_leq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ]
219           }
220         ]
221         [ { "lazy pointwise extension of a relation" * } {
222              [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
223           }
224         ]
225         [ { "pointwise union for local environments" * } {
226              [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ]
227           }
228         ]
229         [ { "context-sensitive exclusion from free variables" * } {
230              [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_append" + "frees_leq" + "frees_lift" * ]
231           }
232         ]
233         [ { "contxt-sensitive extended multiple substitution" * } {
234              [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ]
235           }
236         ]
237         [ { "iterated structural successor for closures" * } {
238              [ "fqus ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ]
239              [ "fqup ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
240           }
241         ]
242         [ { "iterated local env. slicing" * } {
243              [ "drops ( ⇩*[?,?] ? ≡ ? )" "drops_drop" + "drops_drops" * ]
244           }
245         ]
246         [ { "generic term relocation" * } {
247              [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
248              [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
249           }
250         ]
251         [ { "support for multiple relocation" * } {
252              [ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ]
253           }
254         ]
255      }
256    ]
257    class "orange"
258    [ { "substitution" * } {
259         [ { "structural successor for closures" * } {
260              [ "fquq ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊐⊐⸮ ⦃?,?,?⦄ )" * ]
261              [ "fqu ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" * ]
262           }
263         ]
264         [ { "global env. slicing" * } {
265              [ "gget ( ⇩[?] ? ≡ ? )" "gget_gget" * ]
266           }
267         ]
268         [ { "contxt-sensitive extended ordinary substitution" * } {
269              [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
270           }
271         ]
272         [ { "local env. ref. for extended substitution" * } {
273              [ "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
274           }
275         ]
276         [ { "pointwise extension of a relation" * } {
277              [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ]
278           }
279         ]
280         [ { "basic local env. slicing" * } {
281              [ "drop ( ⇩[?,?,?] ? ≡ ? )"  "drop_append" + "drop_leq" + "drop_drop" * ]
282           }
283         ]
284         [ { "basic term relocation" * } {
285              [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
286              [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_neq" + "lift_lift" * ]
287           }
288         ]
289      }
290    ]
291    class "red"
292    [ { "grammar" * } {
293         [ { "equivalence for local environments" * } {
294              [ "leq ( ? ⩬[?,?] ? )" "leq_leq" * ]
295           }
296         ]
297         [ { "same top term structure" * } {
298              [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ]
299           }
300         ]
301         [ { "closures" * } {
302              [ "cl_weight ( ♯{?,?,?} )" "cl_restricted_weight ( ♯{?,?} )" * ]
303           }
304         ]
305         [ { "internal syntax" * } {
306              [ "genv" * ]
307              [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" * ]
308              [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector ( Ⓐ?.? )" * ]
309              [ "item" * ]
310           }
311         ]
312         [ { "external syntax" * } {
313              [ "aarity" * ]
314           }
315         ]
316      }
317    ]
318 }
319
320 class "top"               { * }
321
322 class "capitalize italic" { 0 }
323
324 class "italic"            { 1 }