Changeset 2262

Timestamp:

07/25/12 17:54:59 (10 months ago)

Author:

mulligan

Message:

Changes from today.

Files:

• src/ASM/AssemblyProofSplit.ma (modified) (7 diffs)

src/ASM/AssemblyProofSplit.ma

@@ -917 +917 @@
   try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
   whd in match execute_1_preinstruction; normalize nodelta
-  [(*1,2: (* ADD and ADDC *)
+  [1,2: (* ADD and ADDC *)
     (* XXX: work on the right hand side *)
     (* XXX: switch to the left hand side *)
@@ -989 +989 @@
           >status_refl
           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
-          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
+          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
         |3:
           >status_refl
           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
-          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
+          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
         ]
       |2:
@@ -1003 +1003 @@
           >status_refl
           @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
-          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
+          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
         |3:
           >status_refl
           @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
-          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
+          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
         ]
       |3:
@@ -1031 +1031 @@
           @I
         |3:
-          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A)
-          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
+          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try %
           <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
         ]
@@ -2251 +2250 @@
     ]
   |*)43: (* POP *)
+    cases daemon
   |44:
     >EQP -P normalize nodelta
@@ -2417 +2417 @@
       ]
     ]
-  |47: (* POP *)
-  |48: (* XCH *)
-  |49: (* XCHD *)
-  |50: (* RET *)
-  |51: (* RETI *)
-  |52: (* NOP *)
+  |47: (* RETI *)
+    cases daemon
+  |48: (* NOP *)
     >EQP -P normalize nodelta
     #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
@@ -2432 +2429 @@
     @set_clock_status_of_pseudo_status %
   ]
-cases daemon
 qed.