From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 15 Jun 2018 12:10:19 +0000 (+0200)
Subject: Two problems where the measure does not decrease :-(
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9baecd2c43f39dd9c86b5a8f003bda19f821a66a;p=fireball-separation.git

Two problems where the measure does not decrease :-(
---

diff --git a/ocaml/problems/simple.evil b/ocaml/problems/simple.evil
index 60c3bbf..ddf5718 100644
--- a/ocaml/problems/simple.evil
+++ b/ocaml/problems/simple.evil
@@ -13,3 +13,11 @@ $!
 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))