Changeset 2147 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jul 3, 2012, 3:53:32 AM (7 years ago)
Author:
sacerdot
Message:

Theorem closed (up to one more lemma on overflow), but new proof obligation
for the assembly function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2146 r2147  
    730730         let 〈len,assembledi〉 ≝
    731731          assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in
     732         |assembledi| ≤ |assembled| ∧
    732733         ∀j:nat. ∀H: j < |assembledi|. ∀K.
    733734          nth_safe ? j assembledi H =
Note: See TracChangeset for help on using the changeset viewer.