From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 26 Jul 2017 14:06:31 +0000 (+0200)
Subject: Added horrible problem, showing hard dependency on encodings
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f77b8aeb57b5ce0bcbc87a31a7f3dd74292e6d66;p=fireball-separation.git

Added horrible problem, showing hard dependency on encodings
---

diff --git a/ocaml/problems/encoding_horror b/ocaml/problems/encoding_horror
new file mode 100644
index 0000000..7e59102
--- /dev/null
+++ b/ocaml/problems/encoding_horror
@@ -0,0 +1,10 @@
+D z (y (x a b))
+C z (x BOMB)
+C z (_._.BOT)
+C y (x a b)
+
+#
+ - z must step
+ - x can't step
+ - x y can eat, but then a number applied to b must converge
+   (possible encoding numbers as `\lambda...\lambda. old_encoding`)