Changeset 993 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 17, 2011, 6:28:49 PM (9 years ago)
Author:
sacerdot
Message:

More Russell everywhere; getting closer to the goal.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r990 r993  
    10841084qed.
    10851085
     1086lemma snd_fetch_pseudo_instruction:
     1087 ∀l,ppc. \snd (fetch_pseudo_instruction l ppc) = \snd (half_add ? ppc (bitvector_of_nat ? 1)).
     1088 #l #ppc whd in ⊢ (??%?) whd in ⊢ (?? match % with [_ ⇒ ?]?) @pair_elim'
     1089 #lft #rgt @pair_elim' #x #y #_ @pair_elim' #a #b #_ normalize #H
     1090 generalize in match (pair_destruct_2 ????? H) normalize #K >K %
     1091qed.
     1092
    10861093definition instruction_matches_identifier ≝
    10871094  λy: Identifier.
Note: See TracChangeset for help on using the changeset viewer.