diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-19 10:05:36 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-05-19 10:05:36 +0000 |
commit | 47d79dcb2247f42be9e5734e784e2ca9b18fd599 (patch) | |
tree | 22f81e1e637dd230006470705c3be405f4c2ab2e /test-suite/success/ROmega2.v | |
parent | a13575eeaf69ec3dadb9b3c6a3e365a7d8371390 (diff) |
tests de Romega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8832 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/ROmega2.v')
-rw-r--r-- | test-suite/success/ROmega2.v | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v new file mode 100644 index 000000000..9d47c9f65 --- /dev/null +++ b/test-suite/success/ROmega2.v @@ -0,0 +1,28 @@ +Require Import ZArith ROmega. + +(* 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. +(*romega.*) +Admitted. + |