From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jun 2018 13:05:41 +0000 (+0200)
Subject: Diverging problem + variation that steps on irrelevant arg
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebefdb7061c74f40732633060af05204f519f2d6;p=fireball-separation.git

Diverging problem + variation that steps on irrelevant arg
---

diff --git a/ocaml/problems/simple.evil b/ocaml/problems/simple.evil
index ddf5718..60c3bbf 100644
--- a/ocaml/problems/simple.evil
+++ b/ocaml/problems/simple.evil
@@ -13,11 +13,3 @@ $!
 D x (y1. x (y2. x (y3. x (y4. y1 y2 y3 y4))))
 C x (y1. x (y2. x (y3. x (y4. y1 y2 y3 y1))))
 C x (y1. x (y2. x (y3. x (y4. y1 y2 y1 y4))))
-
-$! 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))
diff --git a/ocaml/problems/simple.evil2 b/ocaml/problems/simple.evil2
new file mode 100644
index 0000000..4036412
--- /dev/null
+++ b/ocaml/problems/simple.evil2
@@ -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)