Changeset 1587 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Dec 5, 2011, 5:16:55 PM (8 years ago)
Author:
mulligan
Message:

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1582 r1587  
    638638                 let s ≝ add_ticks2 s in
    639639                  s
    640         ]. (*15s*)
     640        ]. (*15s*) (*
    641641    try (cases(other))
    642642    try assumption (*20s*)
     
    659659    try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %)
    660660    try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %)
    661     try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %)
     661    try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %) *) (* XXX: for convenience *)
    662662    cases daemon
    663 qed.
    664 
    665 lemma write_at_stack_pointer_ignores_clock:
    666   ∀M.∀s: PreStatus M.
    667   ∀sp: Byte.
    668     clock … (write_at_stack_pointer … s sp) = clock … s.
    669   #M #s #sp
    670   change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
    671    in match (write_at_stack_pointer ???);
    672   normalize nodelta
    673   cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
    674   #nu #nl normalize nodelta;
    675   cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
    676   normalize nodelta; %
    677663qed.
    678664
Note: See TracChangeset for help on using the changeset viewer.