X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fproblems.ml;h=3c098b95ca4c226dcc9284844a007d063e67c833;hb=4627d2b89b5a96e09b1921e033a5c1d7dd50dbc6;hp=7f6f76ce2c362012e4a4e0e28235737eb92fe644;hpb=1bef432e151246cbcd9776da9cef4f0c038d387e;p=fireball-separation.git

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 7f6f76c..3c098b9 100644
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -318,7 +318,35 @@ let n2 () = magic_conv
 ] ["*"]
 ;;
 
-(* main ([p34]);; *)
+let n3 () = magic_conv
+(Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
+[
+"b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))";
+"c d e (f i) (e e) (g e) (k. l. e) (k. c (g (k (l. i)))) (c d e (k. k))";
+"f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (c d e (f i) (e e) (f (k. h))) (g e (b (k. i)) (e e (e e)))";
+"f (k. f) (k. f) (k. e) (c d e (f i) (e e) (g e)) (k. e e) (k. l. m. e) (k. e)";
+"g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f)";
+][
+"b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) a";
+"c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) a";
+"e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a";
+"f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a";
+"g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a";
+] ["*"];;
+
+(* ************************************************************************** *)
+
+let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];;
+let o2 () = magic_conv None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ["*"];;
+let o3 () = magic_conv
+ (Some"y (x a1 BOMB c) (x BOMB b1 d)")
+ [ "y (x a2 BOMB c) (x BOMB b1 d)";
+ "y (x a1 BOMB c) (x BOMB b2 d)";] [] ["*"];;
+let o4 () = magic_conv (Some"x BOMB a1 c")
+ [ "x y BOMB d"; "x BOMB a2 c" ] [] ["*"];;
+
+
+main [o1() ; o2(); o3(); o4();];;
 
 main ([
  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;
@@ -340,5 +368,6 @@ main ([
  m2 ;
 ] @ [
  n1 ;
- n2
+ n2 ;
+ n3
 ]));;