aboutsummaryrefslogtreecommitdiff
path: root/sample/245II.in
diff options
context:
space:
mode:
authorShinya Sato <shinnya.sato@gmail.com>2022-03-03 21:12:55 +0900
committerShinya Sato <shinnya.sato@gmail.com>2022-03-03 21:12:55 +0900
commitf19a057cfcfd77c5567ff8d536db84a40037f10d (patch)
treef661d617e12dcf695fde6eb3c3cc330354e1ce97 /sample/245II.in
parentc0efadbf4003cead718d09a887cff05103f3c377 (diff)
downloadinpla-f19a057cfcfd77c5567ff8d536db84a40037f10d.tar.gz
inpla-f19a057cfcfd77c5567ff8d536db84a40037f10d.zip
v0.8.1
Diffstat (limited to '')
-rw-r--r--sample/245II.in5
1 files changed, 0 insertions, 5 deletions
diff --git a/sample/245II.in b/sample/245II.in
index c71d45d..27910eb 100644
--- a/sample/245II.in
+++ b/sample/245II.in
@@ -3,10 +3,8 @@
// Rules
Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D;
D >< V => ;
-B(a,b,c) >< Z => a~c, b~Z;
B(a,x,e) >< Lam(b,c,y) => x~Lam(b,c,d), y~DB(a,d,e);
DB(a,b,c) >< V => a~c, b~V;
-C(x,y) >< Z => x~Z, y~Z;
C(x,y) >< Lam(s,t,u) =>
x~Lam(a,b,c), y~Lam(d,e,f),
s~Delta(a,d), t~Delta(b,e), u~C(c,f);
@@ -15,9 +13,6 @@ Delta(x,y) >< Delta(a,b) => x~a, y~b;
B(x,a,b) >< Delta(c,d) => x~CB(a,b,Delta(c,d));
Delta(a,b) >< CB(x,y,z) =>
x~Delta(c,d), y~Delta(e,f), z~Delta(B(a,c,e),B(b,d,f));
-Delta(x,y) >< S(z) =>
- x~S(a), y~S(b), z~Delta(a,b);
-Delta(x,y) >< Z => x~Z, y~Z;
Delta(x,y) >< V => x~V, y~V;
Delta(x,y) >< C(t,s) =>
x~C(a,b), y~C(c,d), t~Delta(b,d), s~Delta(a,c);