Changeset 1599 for src/ASM/Status.ma


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r1588 r1599  
    11081108lemma snd_fetch_pseudo_instruction:
    11091109 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
    1110  #l #ppc whd in ⊢ (??%?); whd in ⊢ (?? match % with [_ ⇒ ?]?); @pair_elim'
    1111  #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H
    1112  generalize in match (pair_destruct_2 ????? H); normalize #K >K %
     1110 #l #ppc whd in ⊢ (??(???%)?); @pair_elim
     1111 #lft #rgt @pair_elim #x #y #_ #_ %
    11131112qed.
    11141113
Note: See TracChangeset for help on using the changeset viewer.