From 49960d8950d001a372a0abde670a66ee60026957 Mon Sep 17 00:00:00 2001
From: Shinya Sato <shinnya.sato@gmail.com>
Date: Tue, 5 Mar 2024 18:19:27 +0900
Subject: v0.12.0

---
 sample/245II_new.in | 70 -----------------------------------------------------
 1 file changed, 70 deletions(-)
 delete mode 100644 sample/245II_new.in

(limited to 'sample/245II_new.in')

diff --git a/sample/245II_new.in b/sample/245II_new.in
deleted file mode 100644
index 2050179..0000000
--- a/sample/245II_new.in
+++ /dev/null
@@ -1,70 +0,0 @@
-// 245II in YALE encoding
-
-// Rules
-Lam(a,b,c) >< App(x,y) => a~x, b~y, c~D;
-D >< V => ;
-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) >< 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);
-C(x,y) >< V => x~V, y~V;
-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) >< 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);
-Delta(x,y) >< App(t,s) =>
-	x~App(a,b), y~App(c,d), t~Delta(a,c), s~Delta(b,d);
-Delta(x,y) >< Lam(t,s,u)=>
-	x~Lam(a,b,c), y~Lam(d,e,f),
-	t~Delta(a,d), s~Delta(b,e), u~Delta(c,f);
-DB(x,y,z) >< CB(t,s,u) =>
-	x~CB(d,e,u), y~CB(t,f,d), s~DB(e,f,z);
-C(x,y) >< CB(t,s,u) =>
-	x~CB(a,b,c), y~CB(d,e,f), 
-	t~Delta(a,d), s~C(b,e), u~C(c,f);
-D >< CB(a,b,c) => a~c, b~D;
-
-Eps >< Eps => ;
-Eps >< S(x) => x~Eps;
-Eps >< V => ;
-Eps >< D =>;
-Eps >< Delta(t,s) => t~Eps,s~Eps;
-Eps >< Lam(t,s,u) => t~Eps,s~Eps,u~Eps;
-Eps >< App(t,s) => t~Eps,s~Eps;
-Eps >< B(t,s,u) => t~Eps,s~Eps,u~Eps;
-Eps >< CB(t,s,u) => t~Eps,s~Eps,u~Eps;
-
-
-// Nets
-// lam x.x
-new(r) >< Id => r~Lam(i,i,V);
-
-// lam f. lam x. f(fx)
-new(r) >< Two => r~Lam(Lam(a,b,c),B(c,C(App(a,d),App(d,b)),V),V);
-
-// lam f. lam x. f(fx)
-new(r) >< Four => r~Lam(Lam(a,b,c), B(c,C(App(a,d), C(App(d, e), C(App(e, f), App(f, b)))), V), V);
-
-// lam f. lam x. f(fx)
-new(r) >< Five => r~Lam(Lam(a, b, c), B(c, C(App(a, d), C(App(d, e), C(App(e,f), C(App(f, g), App(g, b))))), V), V);
-
-
-// instances
-id1 << new(Id);
-id2 << new(Id);
-two << new(Two);
-four << new(Four);
-five << new(Five);
-
-
-// 245II
-two  ~ App(aux1, four);
-aux1 ~ App(aux2, five);
-aux2 ~ App(aux3, id1);
-aux3 ~ App(aux4, id2);
-aux4;
-exit;
-- 
cgit v1.2.3