diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/success/Omega2.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/success/Omega2.v')
-rw-r--r-- | test-suite/success/Omega2.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v new file mode 100644 index 00000000..54b13702 --- /dev/null +++ b/test-suite/success/Omega2.v @@ -0,0 +1,28 @@ +Require Import ZArith Omega. + +(* Submitted by Yegor Bryukhov (#922) *) + +Open Scope Z_scope. + +Lemma Test46 : +forall v1 v2 v3 v4 v5 : Z, +((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) -> +9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) -> +((9 * v3) + (2 * v5)) + (5 * v2) = 3 * v4 -> +0 > 6 * v1 -> +(0 * v3) + (6 * v2) <> 2 -> +(0 * v3) + (5 * v5) <> ((4 * v2) + (8 * v2)) + (2 * v5) -> +7 * v3 > 5 * v5 -> +0 * v4 >= ((5 * v1) + (4 * v1)) + ((6 * v5) + (3 * v5)) -> +7 * v2 = ((3 * v2) + (6 * v5)) + (7 * v2) -> +0 * v3 > 7 * v1 -> +9 * v2 < 9 * v5 -> +(2 * v3) + (8 * v1) <= 5 * v4 -> +5 * v2 = ((5 * v1) + (0 * v5)) + (1 * v2) -> +0 * v5 <= 9 * v2 -> +((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9)) +-> False. +intros. +omega. +Qed. + |