Changeset 1515 for src/ASM/StatusProofs.ma

Timestamp:

Nov 18, 2011, 1:03:14 PM (9 years ago)

Author:

campbell

Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

• fix interpretation for - on positives
• move eq_nat_dec to a more appropriate place
• split out costs from other identifiers in ASM
• use identifier abstractions in back-end

File:

• src/ASM/StatusProofs.ma (modified) (1 diff)

src/ASM/StatusProofs.ma

@@ -182 +182 @@
 lemma get_8051_sfr_write_at_stack_pointer:
  ∀T,s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr T s y.
- #T #s #x #y whd in ⊢ (??%%) //
+ #T #s #x #y whd in ⊢ (??%%) >special_function_registers_8051_write_at_stack_pointer @refl
 qed.