Ignore:
Timestamp:
Jun 13, 2011, 1:46:41 AM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r942 r943  
    22292229       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
    22302230       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
    2231        normalize nodelta; #MAP;(* [1,2:whd in MAP:(??(match % with [ _ ⇒ ?])?)]*)
     2231       normalize nodelta; #MAP;
     2232       [1: change in ⊢ (? → %) with
     2233        ((let 〈result,flags〉 ≝
     2234          add_8_with_carry
     2235           (get_arg_8 ? ps false ACC_A)
     2236           (get_arg_8 ?
     2237             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
     2238             false (DIRECT ARG2))
     2239           ? in ?) = ?)
     2240       [1,2: cut (addressing_mode_ok M ps (DIRECT ARG2) = true) [2:
     2241        [1,2:whd in MAP:(??(match % with [ _ ⇒ ? | _ ⇒ ?])?)]
    22322242       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    22332243       #result #flags
Note: See TracChangeset for help on using the changeset viewer.