From: Claudio Sacerdoti Coen Date: Thu, 31 May 2018 22:34:45 +0000 (+0200) Subject: Simplified divergent problem X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=428691717031468f6583a899fe8edbe58163428a;p=fireball-separation.git Simplified divergent problem C diverges in pure --- diff --git a/ocaml/problems/simple.2 b/ocaml/problems/simple.2 new file mode 100644 index 0000000..184b4fa --- /dev/null +++ b/ocaml/problems/simple.2 @@ -0,0 +1,3 @@ +$! simple: C diverges in pure (simplified from simple.1 (1)) +D v0 v1 (x. y. z. v2 y) (v5 v6) +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)