diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
| commit | be2a2fda89bba47d5342b7aebc10efd97f1d68b9 (patch) | |
| tree | 45a70ccd12dc139a53b49daba9c9821ffe2fd035 /test-suite/success/ROmega2.v | |
| parent | 763b05d3e66a0c0c49bad97434d891d22c1054dc (diff) | |
| parent | 72b9a7df489ea47b3e5470741fd39f6100d31676 (diff) | |
Merge commit 'upstream/8.1.pl1+dfsg'
Diffstat (limited to 'test-suite/success/ROmega2.v')
| -rw-r--r-- | test-suite/success/ROmega2.v | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index 9d47c9f6..a3be2898 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -4,6 +4,20 @@ Require Import ZArith ROmega. Open Scope Z_scope. + +(* First a simplified version used during debug of romega on Test46 *) +Lemma Test46_simplified : +forall v1 v2 v5 : Z, +0 = v2 + v5 -> +0 < v5 -> +0 < v2 -> +4*v2 <> 5*v1. +intros. +romega. +Qed. + + +(* The complete problem *) Lemma Test46 : forall v1 v2 v3 v4 v5 : Z, ((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) -> @@ -23,6 +37,5 @@ forall v1 v2 v3 v4 v5 : Z, ((7 * v1) + (1 * v3)) + ((2 * v3) + (1 * v3)) >= ((6 * v5) + (4)) + ((1) + (9)) -> False. intros. -(*romega.*) -Admitted. - +romega. +Qed. |