]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
New failing test
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Jun 2018 09:19:49 +0000 (11:19 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 7 Jun 2018 09:19:49 +0000 (11:19 +0200)
ocaml/problems/simple.2

index 184b4fa2afd81ae564424b9be411f38465f1c641..f5bb2cef95efb0ecb244d8cf9cab4520940da3f9 100644 (file)
@@ -1,3 +1,10 @@
 $! simple: C diverges in pure (simplified from simple.1 (1))\r
 D v0 v1 (x. y. z. v2 y) (v5 v6)\r
 C v7 (v0 v1 v5 (x. x) (x. x) (x. x) (x. v8 v9)) (v0 v1 v5 (x. v2) v1 v5 (x. x)) (v8 v10 v5 (v5 v8 v6 v8 v5 (v5 v6) v8) v10 v10 v6)\r
+\r
+$! simple: il divergente non diverge\r
+D (((x7 x5) (x7 x5)) (x6. x4))(((((((x7 x5) (x7 x5)) ((x7 x5) (x1. (x6. ((x6 x3) (x9 (x6 x3))))))) (x6. x6)) x4) (x3. ((x0 x0) (x0 x2)))) (x4. (x6. x4)))\r
+C ((((((x6 x3) (x9 (x6 x3))) (x9. (x7. (x2. x3)))) (x4. (x6. ((x6 x3) (x9 (x6 x3)))))) x0) (x4. (x6. ((x6 x3) (x9 (x6 x3))))))\r
+C ((((((x7 x5) (x7 x5)) ((x7 x5) (x1. (x6. ((x6 x3) (x9 (x6 x3))))))) (x6. x6)) x4) (x0 (x4. (x7 x5))))\r
+C ((((((x8 (x4. (x7 x5))) (x0 x2)) (x1. (x6. ((x6 x3) (x9 (x6 x3)))))) (x3. (x9 (x6 x3)))) (((x0 x0) (x9 (x6 x3))) x1)) (x3. (x9 (x6 x3))))\r
+C (((((x7 x5) (x1. (x6. ((x6 x3) (x9 (x6 x3)))))) (x2. (x7. x4))) (((((((x7 x5) (x7 x5)) ((x7 x5) (x1. (x6. ((x6 x3) (x9 (x6 x3))))))) (x6. x6)) x4) (x3. ((x0 x0) (x0 x2)))) (x4. (x6. x4)))) (x3. (x6 (x7 x5))))\r