]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/problems/simple.evil2
Diverging problem + variation that steps on irrelevant arg
[fireball-separation.git] / ocaml / problems / simple.evil2
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)