Changeset 1587 for src/ASM/Interpret.ma

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:

• src/ASM/Interpret.ma (modified) (2 diffs)

src/ASM/Interpret.ma

@@ -638 +638 @@
                  let s ≝ add_ticks2 s in
                   s
-        ]. (*15s*)
+        ]. (*15s*) (*
     try (cases(other))
     try assumption (*20s*)
@@ -659 +659 @@
     try (normalize nodelta >set_arg_1_ignores_clock >clock_set_clock %)
     try (normalize nodelta >clock_set_clock >set_arg_16_ignores_clock >clock_set_clock %)
-    try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %)
+    try (normalize nodelta >set_arg_16_ignores_clock >clock_set_clock %) *) (* XXX: for convenience *)
     cases daemon
-qed.
-
-lemma write_at_stack_pointer_ignores_clock:
-  ∀M.∀s: PreStatus M.
-  ∀sp: Byte.
-    clock … (write_at_stack_pointer … s sp) = clock … s.
-  #M #s #sp
-  change with (let 〈nu, nl〉 ≝ split bool 4 4 (get_8051_sfr … s SFR_SP) in ?)
-   in match (write_at_stack_pointer ???);
-  normalize nodelta
-  cases(split bool 4 4 (get_8051_sfr … s SFR_SP))
-  #nu #nl normalize nodelta;
-  cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)))
-  normalize nodelta; %
 qed.