]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Diverging problem + variation that steps on irrelevant arg
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Jun 2018 13:05:41 +0000 (15:05 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Jun 2018 15:01:36 +0000 (17:01 +0200)
ocaml/problems/simple.evil
ocaml/problems/simple.evil2 [new file with mode: 0644]

index ddf571850ba1d13553bd6b9ca8fee426eb3afb61..60c3bbf42df1312c8327d03b3d21dad38e52cb46 100644 (file)
@@ -13,11 +13,3 @@ $!
 D x (y1. x (y2. x (y3. x (y4. y1 y2 y3 y4))))\r
 C x (y1. x (y2. x (y3. x (y4. y1 y2 y3 y1))))\r
 C x (y1. x (y2. x (y3. x (y4. y1 y2 y1 y4))))\r
-\r
-$! the measure of the divergent is not sufficient\r
-D x y\r
-C x (y a)\r
-\r
-$! the measure of the divergent is badly not sufficient\r
-D x y\r
-C x (a. y (a b))\r
diff --git a/ocaml/problems/simple.evil2 b/ocaml/problems/simple.evil2
new file mode 100644 (file)
index 0000000..4036412
--- /dev/null
@@ -0,0 +1,15 @@
+$! the measure of the divergent is not sufficient
+D x y
+C x (y a)
+
+$! the measure of the divergent is badly not sufficient
+D x y
+C x (a. y (a b))
+
+$! stepping on useless arg
+D x0 x1
+C x9 (x0 x0) (x1 x7 x8)
+
+$! algorithm diverges!
+D x0 x1
+C x9 (x0 x0) (x1 x1 x8)