Changeset 2111 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jun 26, 2012, 5:30:41 PM (8 years ago)
Author:
sacerdot
Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2108 r2111  
    189189  ∀b: BitVector n.
    190190    bitvector_of_nat n (nat_of_bitvector n b) = b.
     191
     192axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
    191193
    192194lemma nat_of_bitvector_aux_injective:
     
    689691    add … l r = add … r l.
    690692
     693axiom nat_of_bitvector_add:
     694 ∀n,v1,v2.
     695  nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
     696   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
     697
    691698example add_SO:
    692699  ∀n: nat.
Note: See TracChangeset for help on using the changeset viewer.