- Timestamp:
- Jun 13, 2011, 1:46:41 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r942 r943 2229 2229 @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; 2230 2230 @(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 [ _ ⇒ ? | _ ⇒ ?])?)] 2232 2242 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)] 2233 2243 #result #flags
Note: See TracChangeset
for help on using the changeset viewer.