]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Simplified divergent problem
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2018 22:34:45 +0000 (00:34 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2018 22:34:45 +0000 (00:34 +0200)
C diverges in pure

ocaml/problems/simple.2 [new file with mode: 0644]

diff --git a/ocaml/problems/simple.2 b/ocaml/problems/simple.2
new file mode 100644 (file)
index 0000000..184b4fa
--- /dev/null
@@ -0,0 +1,3 @@
+$! simple: C diverges in pure (simplified from simple.1 (1))\r
+D v0 v1 (x. y. z. v2 y) (v5 v6)\r
+C v7 (v0 v1 v5 (x. x) (x. x) (x. x) (x. v8 v9)) (v0 v1 v5 (x. v2) v1 v5 (x. x)) (v8 v10 v5 (v5 v8 v6 v8 v5 (v5 v6) v8) v10 v10 v6)\r