]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
More diverging examples
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Jun 2018 13:26:59 +0000 (15:26 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 15 Jun 2018 15:01:36 +0000 (17:01 +0200)
ocaml/problems/simple.evil2

index 4036412f7279bf448b21b82a9ea177ce99939bfc..6bff97787b5fed7cb6650ba16b0e2346fd1b7ebf 100644 (file)
@@ -6,10 +6,17 @@ $! 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 x y x
+C x x x
+C y y y a
+
+$! algorithm diverges reaching the previous configuration!
+D x y
+C x x
+C y y a
 
-$! algorithm diverges!
-D x0 x1
-C x9 (x0 x0) (x1 x1 x8)
+$! stepping on useless arg
+D x y
+C x x
+C y a b