Changeset 1587 for src/ASM/Interpret.ma
- Timestamp:
- Dec 5, 2011, 5:16:55 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Interpret.ma
r1582 r1587 638 638 let s ≝ add_ticks2 s in 639 639 s 640 ]. (*15s*) 640 ]. (*15s*) (* 641 641 try (cases(other)) 642 642 try assumption (*20s*) … … 659 659 try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %) 660 660 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 *) 662 662 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 #sp670 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 nodelta673 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; %677 663 qed. 678 664
Note: See TracChangeset
for help on using the changeset viewer.