Changeset 932 for src

Timestamp:

Jun 10, 2011, 3:10:27 AM (9 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -1953 +1953 @@
        >ignore_clock
        @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
-       [1,2,3,4: XXX
-       >get_arg_8_set_program_counter try % [2:%]
-       >get_arg_8_set_program_counter [2:%]
-       >get_arg_8_set_program_counter [2:%]
-       >get_arg_8_set_code_memory
-       >get_arg_8_set_program_counter [2,4:%]
-       >get_arg_8_set_program_counter [2,4:%]
-       >get_arg_8_set_code_memory
-       cases (sub_8_with_carry (get_arg_8 … ps false arg1) (get_arg_8 … ps false arg2) ?(*false*)) #result #flags
-       *)#EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc'; %
+       [1,2,3,4: cases (half_add ???) #carry #result
+        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_to_eq … H2b) -newppc';
+        whd in ⊢ (??%%)
+         %
        >set_code_memory_set_flags >set_program_counter_set_flags >program_counter_set_flags %