Changeset 1934 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
May 10, 2012, 3:37:07 PM (8 years ago)
Author:
boender
Message:
  • various & sundry moves of lemmas to better places
  • integrated Policy and Assembly
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1928 r1934  
    529529    full_add n b c false.
    530530
     531example half_add_SO:
     532 ∀pc.
     533 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
     534 cases daemon.
     535qed.
     536
    531537definition sign_bit : ∀n. BitVector n → bool ≝
    532538λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
Note: See TracChangeset for help on using the changeset viewer.