computation |
- evaluation for context-sensitive extended reduction |
+ evaluation for context-sensitive rt-reduction |
cpxe ( â¦?,?⦠⢠â¡*[?,?] ðâ¦?⦠) |
@@ -386,8 +453,8 @@
|
strongly normalizing qrst-computation |
- fsb ( �,?⦠⢠⦥[?,?] ? ) |
- fsb_alt ( �,?⦠⢠⦥⦥[?,?] ? ) |
+ fsb ( ⦥[?,?] �,?,?⦠) |
+ fsb_alt ( ⦥⦥[?,?] �,?,?⦠) |
fsb_aaa fsb_csx |
@@ -397,7 +464,7 @@
|
|
- strongly normalizing extended computation |
+ strongly normalizing rt-computation |
lcosx ( ? ⢠~â¬*[?,?,?] ? ) |
lcosx_cpx |
@@ -474,7 +541,7 @@
|
fpbs ( â¦?,?,?⦠â¥[?,?] â¦?,?,?⦠) |
fpbs_alt ( â¦?,?,?⦠â¥â¥[?,?] â¦?,?,?⦠) |
- fpbs_lift fpbs_fleq fpbs_aaa fpbs_fpbu fpbs_fpbc fpbs_fpbs |
+ fpbs_lift fpbs_aaa fpbs_fpb fpbs_fpbs |
|
@@ -483,7 +550,7 @@
|
- decomposed extended computation |
+ decomposed rt-computation |
scpds ( â¦?,?⦠⢠? â¢*â¡*[?,?,?] ? ) |
scpds_lift scpds_aaa scpds_scpds |
@@ -497,7 +564,7 @@
|
|
- context-sensitive extended computation |
+ context-sensitive rt-computation |
lpxs ( â¦?,?⦠⢠â¡*[?,?] ? ) |
lpxs_drop lpxs_lleq lpxs_aaa lpxs_cpxs lpxs_lpxs |
@@ -515,7 +582,7 @@
|
cpxs ( â¦?,?⦠⢠? â¡*[?,?] ? ) |
- cpxs_tsts cpxs_tsts_vector cpxs_leq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
+ cpxs_tsts cpxs_tsts_vector cpxs_lreq cpxs_lift cpxs_lleq cpxs_aaa cpxs_cpxs |
|
@@ -582,27 +649,9 @@
-
-
- |
-
-
- |
- fpbu ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
- fpbu_lift fpbu_lleq fpbu_fleq |
-
-
- |
+ fpbq ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
+ fpbq_alt ( â¦?,?,?⦠â½â½[?,?] â¦?,?,?⦠) |
+ fpbq_lift fpbq_aaa |
|
@@ -614,8 +663,8 @@
|
- fpb ( â¦?,?,?⦠â½[?,?] â¦?,?,?⦠) |
- fpb_lift fpb_aaa |
+ fpb ( â¦?,?,?⦠â»[?,?] â¦?,?,?⦠) |
+ fpb_lift fpb_lleq fpb_fleq |
|
@@ -627,7 +676,7 @@
|
- normal forms for context-sensitive extended reduction |
+ normal forms for context-sensitive rt-reduction |
cnx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
cnx_lift cnx_crx cnx_cix |
@@ -641,7 +690,7 @@
|
|
- context-sensitive extended reduction |
+ context-sensitive rt-reduction |
lpx ( â¦?,?⦠⢠â¡[?,?] ? ) |
lpx_drop lpx_frees lpx_lleq lpx_aaa |
@@ -659,7 +708,7 @@
|
cpx ( â¦?,?⦠⢠? â¡[?,?] ? ) |
- cpx_leq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix |
+ cpx_lreq cpx_lift cpx_llpx_sn cpx_lleq cpx_cix |
|
@@ -671,7 +720,7 @@
|
- irreducible forms for context-sensitive extended reduction |
+ irreducible forms for context-sensitive rt-reduction |
cix ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
cix_lift |
@@ -685,7 +734,7 @@
|
|
- reducible forms for context-sensitive extended reduction |
+ reducible forms for context-sensitive rt-reduction |
crx ( â¦?,?⦠⢠â¡[?,?] ðâ¦?⦠) |
crx_lift |
@@ -897,7 +946,7 @@
|
lleq ( ? â¡[?,?] ? ) |
- lleq_alt lleq_alt_rec lleq_leq lleq_drop lleq_fqus lleq_llor lleq_lleq |
+ lleq_alt lleq_alt_rec lleq_lreq lleq_drop lleq_fqus lleq_llor lleq_lleq |
|
@@ -911,7 +960,7 @@
lazy pointwise extension of a relation |
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 |
+ llpx_sn_alt llpx_sn_alt_rec llpx_sn_tc llpx_sn_lreq llpx_sn_drop llpx_sn_lpx_sn llpx_sn_frees llpx_sn_llor |
|
@@ -939,7 +988,7 @@
context-sensitive exclusion from free variables |
frees ( ? ⢠? ϵ ð
*[?]�⦠) |
- frees_append frees_leq frees_lift |
+ frees_append frees_lreq frees_lift |
|
@@ -951,7 +1000,7 @@
|
- contxt-sensitive extended multiple substitution |
+ contxt-sensitive multiple rt-substitution |
cpys ( â¦?,?⦠⢠? â¶*[?,?] ? ) |
cpys_alt ( â¦?,?⦠⢠? â¶â¶*[?,?] ? ) |
cpys_lift cpys_cpys |
@@ -1091,7 +1140,7 @@
|
- contxt-sensitive extended ordinary substitution |
+ contxt-sensitive ordinary rt-substitution |
cpy ( â¦?,?⦠⢠? â¶[?,?] ? ) |
cpy_lift cpy_nlift cpy_cpy |
@@ -1105,7 +1154,7 @@
|
|
- local env. ref. for extended substitution |
+ local env. ref. for rt-substitution |
lsuby ( ? â[?,?] ? ) |
lsuby_lsuby |
@@ -1135,7 +1184,7 @@
|
basic local env. slicing |
drop ( â¬[?,?,?] ? â¡ ? ) |
- drop_append drop_leq drop_drop |
+ drop_append drop_lreq drop_drop |
|
@@ -1176,8 +1225,8 @@