Changeset 1946 for src/ASM/Status.ma


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1882 r1946  
    11181118  λpc: Word.
    11191119    let 〈lbl, instr〉 ≝ nth (nat_of_bitvector ? pc) … code_mem ? in
    1120     let 〈flags, new_pc〉 ≝ half_add ? pc (bitvector_of_nat ? 1) in
     1120    let new_pc ≝ add ? pc (bitvector_of_nat ? 1) in
    11211121      〈instr, new_pc〉.
    11221122    cases not_implemented.
     
    11241124
    11251125lemma snd_fetch_pseudo_instruction:
    1126  ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
     1126 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = add ? ppc (bitvector_of_nat ? 1).
    11271127 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
    1128  #lft #rgt @pair_elim #x #y #_ #_ %
     1128 #lft #rgt #_ %
    11291129qed.
    11301130
Note: See TracChangeset for help on using the changeset viewer.