Changeset 2154


Ignore:
Timestamp:
Jul 5, 2012, 2:22:08 PM (5 years ago)
Author:
sacerdot
Message:

Code shuffled around.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2149 r2154  
    703703   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
    704704
     705axiom add_bitvector_of_nat:
     706 ∀n,m1,m2.
     707  bitvector_of_nat n (m1 + m2) =
     708   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
     709
    705710example add_SO:
    706711  ∀n: nat.
  • src/ASM/Assembly.ma

    r2151 r2154  
    712712     nat_of_bitvector … pc + instruction_size lookup_labels sigma policy ppc instruction = 2^16).
    713713
    714 
    715 (*CSC: move elsewhere*)
    716 axiom add_bitvector_of_nat:
    717  ∀n,m1,m2.
    718   bitvector_of_nat n (m1 + m2) =
    719    add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
    720714
    721715lemma fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels:
Note: See TracChangeset for help on using the changeset viewer.