From 222f8b535ecae3cece6371773f700a2fc77c1bbb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick@luehne.de>
Date: Tue, 12 May 2020 04:33:52 +0200
Subject: [PATCH] Add specification for example 1

---
 examples/example-1.spec | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 examples/example-1.spec

diff --git a/examples/example-1.spec b/examples/example-1.spec
new file mode 100644
index 0000000..6c813c5
--- /dev/null
+++ b/examples/example-1.spec
@@ -0,0 +1,6 @@
+assert:
+	forall N
+	(
+		forall X (p(X) -> exists I exists M (I = M and I = X and I <= N))
+		-> forall X (q(X) -> exists I exists M (I = M and I = X and I <= 2 * N))
+	).