Ignore:
Timestamp:
Aug 2, 2012, 1:58:14 PM (7 years ago)
Author:
sacerdot
Message:
  1. duplicated code erased
  2. POP case finished up to lemmas on read_at_stack_pointer
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/StatusProofsSplit.ma

    r2274 r2285  
    6464        c.
    6565  //
    66 qed.
    67 
    68 lemma get_8051_sfr_set_clock:
    69   ∀M: Type[0].
    70   ∀cm: M.
    71   ∀s: PreStatus M cm.
    72   ∀sfr: SFR8051.
    73   ∀t: Time.
    74     get_8051_sfr M cm (set_clock M cm s t) sfr =
    75       get_8051_sfr M cm s sfr.
    76   #M #cm #s #sfr #t %
    77 qed.
    78 
    79 lemma get_8051_sfr_set_program_counter:
    80   ∀M: Type[0].
    81   ∀cm: M.
    82   ∀s: PreStatus M cm.
    83   ∀pc: Word.
    84     get_8051_sfr M cm (set_program_counter M cm s pc) =
    85       get_8051_sfr M cm s.
    86   #M #cm #s #pc %
    8766qed.
    8867
Note: See TracChangeset for help on using the changeset viewer.