Changeset 904 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 8, 2011, 5:53:32 PM (9 years ago)

Author:

sacerdot

Message:

Cleanup.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -1014 +1014 @@
        sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
 
-lemma fetch_assembly_pseudo:
- ∀program,ppc,lookup_labels,lookup_datalabels.
-  ∀pi,code_memory,len,assembled,instructions,pc.
-   let expansion ≝ jump_expansion_policy program ppc in
-   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
-    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
-     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
-      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
-
-
 lemma rev_preserves_length:
  ∀A.∀l. length … (rev A l) = length … l.