Commit 99d25116 by ntmtuyen

parent 5efd8958
 ... ... @@ -273,9 +273,9 @@ Axiom to_nat_of_zero2 : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\ (* DO NOT EDIT BELOW *) Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), ((j < size)%Z /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)). Theorem to_nat_of_zero : forall (b:bv) (i:Z) (j:Z), (((j < size)%Z /\ (i <= j)%Z) /\ (0%Z <= i)%Z) -> ((forall (k:Z), ((k <= j)%Z /\ (i <= k)%Z) -> ((nth b k) = false)) -> ((to_nat_sub b j i) = 0%Z)). (* YOU MAY EDIT THE PROOF BELOW *) Open Scope Z_scope. intros b i j Hij. ... ...
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -287,14 +287,14 @@ Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z), Parameter from_int: Z -> bv. Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> Axiom Div_inf1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((int.EuclideanDivision.div x y) = 0%Z). Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z). Axiom Mod_0 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). Axiom Mod_01 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z y) = 1%Z). ... ... @@ -302,13 +302,13 @@ Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z Axiom Mod_neg1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), ((0%Z < i)%Z /\ (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z)) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), ((0%Z < i)%Z /\ (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z)) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\ (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n ... ... @@ -721,10 +721,7 @@ Axiom to_nat_sub_0_30 : forall (x:Z), (is_int32 x) -> Axiom jpxorx_pos : forall (x:Z), (0%Z <= x)%Z -> ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = true). Axiom jpxorx_neg : forall (x:Z), (x < 0%Z)%Z -> ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = false). Axiom from_int2c_to_nat_sub_gen : forall (i:Z), ((0%Z <= i)%Z /\ Axiom from_int2c_to_nat_sub_pos : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 31%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) -> ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x). ... ...
 ... ... @@ -287,14 +287,14 @@ Axiom to_nat_sub_footprint : forall (b1:bv) (b2:bv) (j:Z) (i:Z), Parameter from_int: Z -> bv. Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> Axiom Div_inf1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((int.EuclideanDivision.div x y) = 0%Z). Axiom Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) -> ((int.EuclideanDivision.div (-x)%Z y) = (-1%Z)%Z). Axiom Mod_0 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). Axiom Mod_01 : forall (y:Z), (~ (y = 0%Z)) -> ((int.EuclideanDivision.mod1 0%Z y) = 0%Z). Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z y) = 1%Z). ... ... @@ -302,13 +302,13 @@ Axiom Mod_1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 1%Z Axiom Mod_neg1y : forall (y:Z), (1%Z < y)%Z -> ((int.EuclideanDivision.mod1 (-1%Z)%Z y) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), ((0%Z < i)%Z /\ (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z)) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow : forall (x:Z) (i:Z), (((pow2 (i - 1%Z)%Z) <= x)%Z /\ (x < (pow2 i))%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = 1%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), ((0%Z < i)%Z /\ (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z)) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom Div_pow2 : forall (x:Z) (i:Z), (((-(pow2 i))%Z <= x)%Z /\ (x < (-(pow2 (i - 1%Z)%Z))%Z)%Z) -> ((int.EuclideanDivision.div x (pow2 (i - 1%Z)%Z)) = (-2%Z)%Z). Axiom nth_from_int_high_even : forall (n:Z) (i:Z), (((i < 32%Z)%Z /\ (0%Z <= i)%Z) /\ ((int.EuclideanDivision.mod1 (int.EuclideanDivision.div n ... ... @@ -721,10 +721,7 @@ Axiom to_nat_sub_0_30 : forall (x:Z), (is_int32 x) -> Axiom jpxorx_pos : forall (x:Z), (0%Z <= x)%Z -> ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = true). Axiom jpxorx_neg : forall (x:Z), (x < 0%Z)%Z -> ((nth (bw_xor (from_int 2147483648%Z) (from_int2c x)) 31%Z) = false). Axiom from_int2c_to_nat_sub_gen : forall (i:Z), ((0%Z <= i)%Z /\ Axiom from_int2c_to_nat_sub_pos : forall (i:Z), ((0%Z <= i)%Z /\ (i <= 31%Z)%Z) -> forall (x:Z), ((0%Z <= x)%Z /\ (x < (pow2 i))%Z) -> ((to_nat_sub (from_int2c x) (i - 1%Z)%Z 0%Z) = x). ... ... @@ -746,7 +743,7 @@ rewrite to_nat_sub_one;auto with zarith. replace (31-0) with 31 by omega. replace (31-1) with 30 by omega. rewrite to_nat_sub_0_30;auto. rewrite from_int2c_to_nat_sub_gen with (i:=31);auto with zarith. rewrite from_int2c_to_nat_sub_pos with (i:=31);auto with zarith. destruct H. split. exact H0. ... ...
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!