Changeset 2258 for src/ASM/Test.ma


Ignore:
Timestamp:
Jul 25, 2012, 1:47:01 PM (8 years ago)
Author:
sacerdot
Message:
  1. lemma generalized
  2. automation replaced with expansion to make everything faster
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Test.ma

    r2247 r2258  
    982982  ∀cm.
    983983  ∀ps.
    984   ∀addr: [[dptr]].
    985   ∀v: Word.
     984  ∀addr,addr': [[dptr]].
     985  ∀v,v': Word.
    986986  ∀M. ∀sigma. ∀policy. ∀s'.
    987987    status_of_pseudo_status M cm ps sigma policy = s' →
     988    v=v' → addr=addr' →
    988989      set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
    989       s' v addr =
     990      s' v' addr' =
    990991      status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy.
    991   #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl
     992  #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl
     993  <addr_refl #v_refl <v_refl
    992994  @(subaddressing_mode_elim … addr)
    993995  whd in match set_arg_16; normalize nodelta
Note: See TracChangeset for help on using the changeset viewer.