Changeset 1404 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Oct 18, 2011, 3:39:56 PM (8 years ago)
Author:
boender
Message:
  • reworked + added
  • added an axiom to arithmetic, but should be provable
File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Arithmetic.ma

    r1207 r1404  
    141141  λn,v. nat_of_bitvector_aux n O v.
    142142
     143axiom bitvector_of_nat_ok:
     144  ∀n,x,y.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y.
     145(* if anyone wants to prove this... *)
     146 
    143147definition two_complement_negation ≝
    144148  λn: nat.
Note: See TracChangeset for help on using the changeset viewer.