X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Fproblems%2Fp;fp=ocaml%2Fproblems%2Fp;h=6f1e0622cf6c636630114c87d6a9d3ac02969944;hb=7a5350448fac6b4e9ce894da1fc1815a68bdd5c1;hp=5e7283cbec99277c0bc13524f2fdfd094af0d2ed;hpb=4f1d4ac662d6aeb8e63ddcd4575f9ef6313a565b;p=fireball-separation.git

diff --git a/ocaml/problems/p b/ocaml/problems/p
index 5e7283c..6f1e062 100644
--- a/ocaml/problems/p
+++ b/ocaml/problems/p
@@ -1,85 +1,85 @@
-# p2
+$! p2
 N x y
   x z
   x (y z)
 
-# p4
+$! p4
 N x y
   x (a. a x)
   y (y z)
 
-# p5
+$! p5
 N a (x. x a) b
   b (x. x b) a
 
-# p6
+$! p6
 N a (x. x a) b
   b (x. x b) (c a)
 
-# p7
+$! p7
 N a (x. (x a) (a x x a) (x x) )
 
-# p8
+$! p8
 N x x (x x)
 
-# p9
+$! p9
 N x x (x x x) (x x (x x)) (x x (x x x)) x x
 
-# p10
+$! p10
 N x (y (x a b c))
 
-# p11
+$! p11
 N x x
   x (y.y)
 
-# p12
+$! p12
 N x x (x x)
   x x (x (y.y))
 
-# p13
+$! p13
 N x x (x x (x x x x x (x x)))
 
-# p14
+$! p14
 N a (a a (a (a a)) (a (a a)))
 
-# p15
+$! p15
 N a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))
 
-# p16:
+$! p16:
 N a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))
 
-# p17
+$! p17
 N b a
   b (c.a)
 
-# p18
+$! p18
 N a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))
   a a
   a (a a)
 
-# p19
+$! p19
 N a (a a) (a a a (a (a (a a) a)) a)
 
-# p20
+$! p20
 N a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))
 
-# p21
+$! p21
 N (((y z) (y z)) ((z (y z)) ((y z) (z z))))
   (((z z) x) (y z))
   ((z (y z)) ((y z) (z z)))
 
-# p22
+$! p22
 N ((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))
   ((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))
   (y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))
 
-# p23
-  (* diverging tests *) (* test p23 leads to test p24 *)
+$! p23
+# (* diverging tests *) (* test p23 leads to test p24 *)
 N z z z
   z (z z) (x. x)
 
-# p24
-  (* because of the last term, the magic number is 1 and we diverge
+$! p24
+# (* because of the last term, the magic number is 1 and we diverge
      but setting the magic number to 0 allows to solve the problem
      thus our strategy is incomplete *)
 N b b
@@ -87,8 +87,8 @@ N b b
   f b
   a (x.x)
 
-# p25
-  (* because of the last term, the magic number is 1 and we diverge
+$! p25
+# (* because of the last term, the magic number is 1 and we diverge
      but setting the magic number to 0 allows to solve the problem
      thus our strategy is incomplete *)
 N b b
@@ -96,48 +96,48 @@ N b b
   f b
   f (x.x)
 
-# p26
+$! p26
   (* BUG:
      0 (n (d (o.n) ...)))
      After instantiating n, the magic number (for d) should be 2, not 1! *)
 N (((x y) (z. (y. (y. z)))) (z. y))
   (((x y) x) (y y))
 
-# p27
+$! p27
 N (((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))
   ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))
   (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))
 
-# p28
+$! p28
 N ((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))
    (((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))
 
-# p29
+$! p29
 N ((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))
   (((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)
 
-# p30
+$! p30
 N ((b c) (b. (z a)))
   ((v (a. (z v))) ((y (b c)) ((z a) (v y))))
   ((v (v. c)) z)
   ((v y) (v (a. (z v))))
   ((y (b c)) ((z a) (v y)))
 
-# p31
+$! p31
 N  (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))
    ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))
    (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))
     (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))
       ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))
 
-# p32
+$! p32
 N (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))
   (((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)
   (((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))
   ((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))
   ((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))
 
-# p33
+$! p33
   (* Shows an error when the strategy that minimizes special_k is NOT used *)
 N ((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))
   ((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))
@@ -145,25 +145,25 @@ N ((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a
   (((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))
 #  (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
 
-# p34
+$! p34
 N b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a
   d (j. e) e (j. c f) (j. c j) b a
   d (j. e) e (j. c f) b (b c (b c) (j. c f)) a
   d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a
   d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a
 
-# p35
+$! p35
 N (((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))
   ((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))
   ((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))
 
-# p36
+$! p36
 N (((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))))))))
   (((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))
   (((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))
 
 
-# p37
+$! p37
   issue with eta-equality of terms in ps
 N x (a y) z
   x (a z. y z) w