- Timestamp:
- Jun 13, 2011, 11:15:31 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r944 r945 2067 2067 // 2068 2068 qed. 2069 2070 lemma blah: 2071 ∀p: pseudo_instruction. 2072 ∀m: pseudo_internal_address_map. 2073 ∀s: PseudoStatus. 2074 ∀arg: Byte. 2075 next_internal_pseudo_address_map0 p m s (DIRECT arg) = Some ? → 2076 get_arg_8 (next_internal_pseudo_address_map0 p (internal_ram ? s) s (DIRECT arg)) = 2077 get_arg_8 (internal_ram ? s) (DIRECT arg). 2078 2079 map_address0 ... (DIRECT arg) = Some .. → 2080 get_arg_8 (map_address0 ... (internal_ram ...) (DIRECT arg) = 2081 get_arg_8 (internal_ram ...) (DIRECT arg) 2082 2083 ((if addressing_mode_ok M ps ACC_A∧addressing_mode_ok M ps (DIRECT ARG2) 2084 then Some internal_pseudo_address_map M 2085 else None internal_pseudo_address_map ) 2086 =Some internal_pseudo_address_map M') 2069 2087 2070 2088 lemma main_thm: … … 2227 2245 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2228 2246 (*|5: (* Call *)*) *) 2229 | (* Instruction *) -pi; *; normalize nodelta;2247 | (* Instruction *) -pi; whd in ⊢ (? → ??%? → ?) *; normalize nodelta; 2230 2248 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1] 2231 2249 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
Note: See TracChangeset
for help on using the changeset viewer.