- Timestamp:
- Jun 27, 2012, 1:40:29 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2109 r2114 101 101 special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d'). 102 102 #M #M' #cm #cm' #s #s' #w #w' 103 @list_addressing_mode_tags_elim_prop try %104 @list_addressing_mode_tags_elim_prop try %103 #d @(subaddressing_mode_elim … d) 104 #d' @(subaddressing_mode_elim … d') 105 105 #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 % 106 106 qed. … … 937 937 change with (add ???) in match (\snd (half_add ???)); 938 938 >set_arg_8_set_program_counter in ⊢ (???%); 939 [2,4,6,8: /2 / ]939 [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] 940 940 >program_counter_set_program_counter in ⊢ (???%); 941 941 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
Note: See TracChangeset
for help on using the changeset viewer.