2017 April 16.
@@ -384,7 +392,7 @@
- conversion |
+ rt-conversion |
context-sensitive r-conversion |
cpc ( â¦?,?⦠⢠? â¬[?] ? ) |
cpc_cpc |
@@ -392,36 +400,6 @@
rt-computation |
uncounted context-sensitive rt-computation |
- lfsx ( ? ⢠â¬*[?,?,?] ðâ¦?⦠) |
- lfsx_fqup lfsx_lfpxs lfsx_lfsx |
-
-
-
-
- |
-
-
- |
- csx_vector ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
- csx_cnx_vector csx_csx_vector |
-
-
-
-
- |
-
-
- |
- csx ( â¦?,?⦠⢠â¬*[?,?] ðâ¦?⦠) |
- csx_simple csx_simple_theq csx_drops csx_lsubr csx_aaa csx_gcp csx_gcr csx_lfpx csx_cnx csx_cpxs csx_csx |
-
-
-
-
- |
-
-
- |
lfpxs ( â¦?,?⦠⢠â¬*[?,?] ? ) |
lfpxs_length lfpxs_drops lfpxs_fqup lfpxs_lfdeq lfpxs_aaa lfpxs_cpxs lfpxs_lfpxs |
@@ -459,6 +437,18 @@
lfpr ( â¦?,?⦠⢠â¡[?,?] ? ) |
lfpr_length lfpr_drops lfpr_fquq lfpr_fqup lfpr_frees lfpr_aaa lfpr_lfpx lfpr_lfpr |
+
+
+
+ |
+
+
+ |
+ cpr_ext ( â¦?,?⦠⢠? â¡[?] ? ) |
+
+
+ |
+
@@ -495,7 +485,19 @@
|
lfpx ( â¦?,?⦠⢠â¬[?,?] ? ) |
- lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_lfpx |
+ lfpx_length lfpx_drops lfpx_fqup lfpx_frees lfpx_lfdeq lfpx_aaa lfpx_cpx lfpx_lfpx |
+
+
+
+
+ |
+
+
+ |
+ cpx_ext ( â¦?,?⦠⢠? â¬[?] ? ) |
+
+
+ |
@@ -599,7 +601,7 @@
|
context-sensitive free variables |
lsubf ( â¦?,?⦠â«ð
* �,?⦠) |
- lsubf_frees |
+ lsubf_lsubr lsubf_frees lsubf_lsubf |
@@ -622,7 +624,7 @@
|
s-computation |
iterated structural successor for closures |
- fqus ( â¦?,?,?⦠â* â¦?,?,?⦠) |
+ fqus ( â¦?,?,?⦠â*[?] â¦?,?,?⦠) ( â¦?,?,?⦠â* â¦?,?,?⦠) |
fqus_weight fqus_drops fqus_fqup fqus_fqus |
@@ -632,13 +634,13 @@
|
- fqup ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
+ fqup ( â¦?,?,?⦠â+[?] â¦?,?,?⦠) ( â¦?,?,?⦠â+ â¦?,?,?⦠) |
fqup_weight fqup_drops fqup_fqup |
s-transition |
structural successor for closures |
- fquq ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
+ fquq ( â¦?,?,?⦠â⸮[?] â¦?,?,?⦠) ( â¦?,?,?⦠â⸮ â¦?,?,?⦠) |
fquq_length fquq_weight |
@@ -648,7 +650,7 @@
|
- fqu ( â¦?,?,?⦠â â¦?,?,?⦠) |
+ fqu ( â¦?,?,?⦠â[?] â¦?,?,?⦠) ( â¦?,?,?⦠â â¦?,?,?⦠) |
fqu_length fqu_weight |
@@ -667,7 +669,7 @@
drops ( â¬*[?,?] ? â¡ ? ) ( â¬*[?] ? â¡ ? ) |
- drops_lstar drops_weight drops_length drops_ceq drops_lexs drops_lreq drops_drops |
+ drops_lstar drops_weight drops_length drops_ext2 drops_lexs drops_lreq drops_drops |
@@ -731,9 +733,21 @@
|
|
- degree-based equivalence for terms |
- deq ( ? â¡[?,?] ? ) |
- deq_deq |
+ degree-based equivalence |
+ tdeq_ext ( ? â¡[?,?] ? ) ( ? ⢠? â¡[?,?] ? ) |
+
+
+ |
+
+
+
+
+ |
+
+
+ |
+ tdeq ( ? â¡[?,?] ? ) |
+ tdeq_tdeq |
@@ -818,10 +832,8 @@
|
binders for local environments |
- bind_ext2 |
-
-
- |
+ ext2 |
+ ext2_ext2 |
@@ -952,6 +964,6 @@
- Last update: Tue, 10 Oct 2017 22:45:09 +0200
+ Last update: Wed, 25 Oct 2017 21:44:35 +0200
|