Changeset 3112 for src/ASM/ASM.ma


Ignore:
Timestamp:
Apr 9, 2013, 6:05:49 PM (7 years ago)
Author:
tranquil
Message:

added invariant that costlabels are only assigned to NOPs (not proved
yet, assembly has a new cases daemon)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r3104 r3112  
    12341234; oc_injective_costlabels :
    12351235  partial_injection … (λpc.lookup_opt … pc costlabels)
     1236; oc_costlabels_are_zero : (* this will imply that cost labels are only assigned to nops *)
     1237  ∀ppc,l.lookup_opt … ppc costlabels = Some ? l →
     1238  lookup … ppc cm (zero …) = zero …
    12361239}.
Note: See TracChangeset for help on using the changeset viewer.