From c3af2d13846979d2614b5ae75c5d0e6b058f338f Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Sun, 15 Sep 2013 08:25:31 +0200 Subject: [PATCH] bitvector/power2: missing proofs added --- examples/bitvectors/power2.why | 29 +- examples/bitvectors/power2/why3session.xml | 425 ++++++++++++--------- 2 files changed, 242 insertions(+), 212 deletions(-) diff --git a/examples/bitvectors/power2.why b/examples/bitvectors/power2.why index 878e73d97..b9e98a43e 100644 --- a/examples/bitvectors/power2.why +++ b/examples/bitvectors/power2.why @@ -83,32 +83,9 @@ theory Pow2int use import int.EuclideanDivision -(* - lemma div_uniq: - forall x y q:int. - y > 0 /\ (exists r:int. x = q*y + r /\ 0 <= r < y) -> div x y = q - - lemma mod_uniq: - forall x y r:int. - y > 0 /\ (exists q:int. x = q*y + r /\ 0 <= r < y) -> mod x y = r - - lemma Div_double_aux: - forall x y:int. 0 < y <= x < 2*y -> - x = 1*y+(x-y) /\ 0 <= x-y < y - - lemma Div_double_aux2: - forall x y:int. 0 < y <= x < 2*y -> mod x y = x - y -*) - -(* - lemma Div_mult : - forall x y q:int. q > 0 -> - 0 < q*y <= x < (q+1)*y -> div x y = q - - lemma Div_mult_neg : - forall x y q:int. q > 0 -> - -(q+1)*y <= x < -q*y < 0 -> div x y = -(q+1) -*) + lemma Div_mult_inst: forall x z:int. + x > 0 -> + div (x * 1 + z) x = 1 + div z x lemma Div_double: forall x y:int. 0 < y <= x < 2*y -> div x y = 1 diff --git a/examples/bitvectors/power2/why3session.xml b/examples/bitvectors/power2/why3session.xml index 898a434aa..4f6cb5a66 100644 --- a/examples/bitvectors/power2/why3session.xml +++ b/examples/bitvectors/power2/why3session.xml @@ -15,18 +15,22 @@ version="2.4.1"/> + + + + + + + + + - + + + + + + + + + + - + @@ -3318,13 +3371,13 @@ -- GitLab