Changeset 2114


Ignore:
Timestamp:
Jun 27, 2012, 1:40:29 AM (5 years ago)
Author:
sacerdot
Message:

Proof repaired

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2109 r2114  
    101101        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
    102102  #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')
    105105  #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 %
    106106qed.
     
    937937        change with (add ???) in match (\snd (half_add ???));
    938938        >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/ ]
    940940        >program_counter_set_program_counter in ⊢ (???%);
    941941        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
Note: See TracChangeset for help on using the changeset viewer.