Changeset 1928 for src/ASM/BitVector.ma


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r1890 r1928  
    209209qed.
    210210
     211corollary refl_iff_eq_bv_true:
     212  ∀n: nat.
     213  ∀x: BitVector n.
     214  ∀y: BitVector n.
     215    eq_bv n x y = true ↔ x = y.
     216  #n #x #y whd in match iff; normalize nodelta
     217  @conj /2/
     218qed.
     219
    211220axiom bitvector_of_string:
    212221  ∀n: nat.
Note: See TracChangeset for help on using the changeset viewer.