Changeset 944 for src

Timestamp:

Jun 13, 2011, 10:54:58 AM (10 years ago)

Author:

mulligan

Message:

split definition

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -1536 +1536 @@
     | ADDR11 _ ⇒ true
     | ADDR16 _ ⇒ true ].
-
-definition next_internal_pseudo_address_map ≝
- λM:internal_pseudo_address_map.
-  λs:PseudoStatus.
-   match \fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s)) with
+    
+definition next_internal_pseudo_address_map0 ≝
+  λfetched.
+  λM: internal_pseudo_address_map.
+  λs: PseudoStatus.
+   match fetched with
     [ Comment _ ⇒ Some ? M
     | Cost _ ⇒ Some … M
@@ -1565 +1566 @@
             None ?        
         | _ ⇒ (* TO BE COMPLETED *) Some ? M ]].
+  
+
+definition next_internal_pseudo_address_map ≝
+ λM:internal_pseudo_address_map.
+  λs:PseudoStatus.
+    next_internal_pseudo_address_map0 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s.
     
 definition status_of_pseudo_status:
@@ -2076 +2083 @@
   [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP
     #abs @⊥ normalize in abs; destruct (abs) ]
- * #labels #costs whd in ⊢ (? → ? → ??%? → ?) generalize in match (refl … (code_memory … ps))
+ * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ?)
+ generalize in match (refl … (code_memory … ps))
  cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta;
  generalize in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]) → ?) *; normalize nodelta;