Changeset 2154 for src

Timestamp:

Jul 5, 2012, 2:22:08 PM (8 years ago)

Author:

sacerdot

Message:

Code shuffled around.

Location:

src/ASM

Files:

• Arithmetic.ma (modified) (1 diff)
• Assembly.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -703 +703 @@
    nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
 
+axiom add_bitvector_of_nat:
+ ∀n,m1,m2.
+  bitvector_of_nat n (m1 + m2) =
+   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
+
 example add_SO:
   ∀n: nat.

src/ASM/Assembly.ma

@@ -712 +712 @@
      nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).
 
-
-(*CSC: move elsewhere*)
-axiom add_bitvector_of_nat:
- ∀n,m1,m2.
-  bitvector_of_nat n (m1 + m2) =
-   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
 
 lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels: