Changeset 943 for src

Timestamp:

Jun 13, 2011, 1:46:41 AM (9 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -2229 +2229 @@
        @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
        @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
-       normalize nodelta; #MAP;(* [1,2:whd in MAP:(??(match % with [ _ ⇒ ?])?)]*)
+       normalize nodelta; #MAP;
+       [1: change in ⊢ (? → %) with
+        ((let 〈result,flags〉 ≝
+          add_8_with_carry
+           (get_arg_8 ? ps false ACC_A)
+           (get_arg_8 ?
+             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
+             false (DIRECT ARG2))
+           ? in ?) = ?)
+       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
+        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
        #result #flags