summaryrefslogtreecommitdiff
path: root/omega/examples/old_test/p5
diff options
context:
space:
mode:
Diffstat (limited to 'omega/examples/old_test/p5')
-rw-r--r--omega/examples/old_test/p58
1 files changed, 8 insertions, 0 deletions
diff --git a/omega/examples/old_test/p5 b/omega/examples/old_test/p5
new file mode 100644
index 0000000..ae7b242
--- /dev/null
+++ b/omega/examples/old_test/p5
@@ -0,0 +1,8 @@
+symbolic n;
+{[iw] -> [ir] :
+ 1 <= iw, ir <= 2n and iw=ir
+ and ! exists ( ik,jk : 1 <= ik <= 2n && 1 <= jk < n and
+ iw <= ik = ir and 2jk = ir )
+ and ! exists ( ik,jk : 1 <= ik <= 2n && 1 <= jk < n and
+ iw <= ik = ir and 2jk+1 = ir )
+ };