]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems.ml
Fix: conv : x:min_int (.... y:1 ...) y was not considered for stepping
[fireball-separation.git] / ocaml / problems.ml
index 7f6f76ce2c362012e4a4e0e28235737eb92fe644..2a99a5c09180cb679a8cfe6dba65f738146526f7 100644 (file)
@@ -318,6 +318,22 @@ let n2 () = magic_conv
 ] ["*"]
 ;;
 
+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";
+] ["*"];;
+
 (* main ([p34]);; *)
 
 main ([
@@ -340,5 +356,6 @@ main ([
  m2 ;
 ] @ [
  n1 ;
- n2
+ n2 ;
+ n3
 ]));;