diff --git a/examples/bitvectors/power2.why b/examples/bitvectors/power2.why index 878e73d9789c0bc9f17d4fbb44cdbe153de2b543..b9e98a43e4b36d54dd8bec6438d8e89ccd082cd0 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 898a434aae8e5c624439e2cd12fc9be4276a9a7d..4f6cb5a66f3ae5df3100d6e45268c042f52b29ea 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 @@