Changeset 2158 for src/ASM

Timestamp:

Jul 6, 2012, 11:41:40 AM (8 years ago)

Author:

sacerdot

Message:

One less daemon.

File:

• src/ASM/Assembly.ma (modified) (2 diffs)

src/ASM/Assembly.ma

@@ -850 +850 @@
 qed.
 
-
-
 definition assembly:
     ∀p: pseudo_assembly_program.
@@ -958 +956 @@
     lapply (fst_snd_assembly_1_pseudoinstruction … p2) #EQpc_delta
     cut (pc_delta < 2^16)
-    [cases daemon (*CSC: DA FARE*) ] #pc_delta_ok check fst_eq
+    [ >EQpc_delta
+      @(eq_ind ?? (λp.λ_. |\snd p| < 2^16) ?? p2)
+      @assembly1_pseudoinstruction_lt_2_to_16 ] #pc_delta_ok
     cut (pc_delta = instruction_size lookup_labels sigma policy ppc (\snd hd))
     [ whd in match instruction_size; normalize nodelta