Changeset 2114 for src

Timestamp:

Jun 27, 2012, 1:40:29 AM (8 years ago)

Author:

sacerdot

Message:

Proof repaired

File:

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

src/ASM/AssemblyProofSplit.ma

@@ -101 +101 @@
         special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
   #M #M' #cm #cm' #s #s' #w #w'
-  @list_addressing_mode_tags_elim_prop try %
-  @list_addressing_mode_tags_elim_prop try %
+  #d @(subaddressing_mode_elim … d)
+  #d' @(subaddressing_mode_elim … d')
   #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
 qed.
@@ -937 +937 @@
         change with (add ???) in match (\snd (half_add ???));
         >set_arg_8_set_program_counter in ⊢ (???%);
-        [2,4,6,8: /2/ ]
+        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
         >program_counter_set_program_counter in ⊢ (???%);
         >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')