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

more changes

File:
1 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 ]] ?) ∧
Note: See TracChangeset for help on using the changeset viewer.