Changeset 868


Ignore:
Timestamp:
May 31, 2011, 5:28:12 PM (8 years ago)
Author:
mulligan
Message:

more changes

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r867 r868  
    368368    P (JZ ? ?) ∧
    369369    P (JNZ ? ?) ∧
    370     P (JB ? (BIT_ADDR ?) ?)
     370    bitvector_elim 8 (λx. P (JB ? (BIT_ADDR x))).
    371371    P (JNB ? [[ bit_addr ]] ?) ∧
    372372    P (JBC ? [[ bit_addr ]] ?) ∧
  • src/ASM/BitVector.ma

    r744 r868  
    9191(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9292
     93definition eq_b ≝
     94  λb, c: bool.
     95    if b then
     96      c
     97    else
     98      notb c.
     99
    93100definition eq_bv ≝
    94101  λn: nat.
    95102  λb, c: BitVector n.
    96     eq_v bool n (λd, e.
    97       if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
    98         true
    99       else
    100         false) b c.
     103    eq_v bool n eq_b b c.
    101104
    102105lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
Note: See TracChangeset for help on using the changeset viewer.