Changeset 1426 for src/ASM


Ignore:
Timestamp:
Oct 20, 2011, 2:08:39 PM (8 years ago)
Author:
boender
Message:

removed axiom

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1404 r1426  
    140140definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
    141141  λn,v. nat_of_bitvector_aux n O v.
    142 
    143 axiom 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  
     142   
    147143definition two_complement_negation ≝
    148144  λn: nat.
Note: See TracChangeset for help on using the changeset viewer.