reworked freescale stuff to put \m as a left parameter

[helm.git] / helm / software / matita / library / freescale / medium_tests_lemmas.ma

diff --git a/helm/software/matita/library/freescale/medium_tests_lemmas.ma b/helm/software/matita/library/freescale/medium_tests_lemmas.ma
index e708f57bcc0ff93d0a869a4210b2aaaae4076992..44f770ae34e67d41f50e9e7ca41ba948ee4a7f43 100644 (file)
--- a/helm/software/matita/library/freescale/medium_tests_lemmas.ma
+++ b/helm/software/matita/library/freescale/medium_tests_lemmas.ma
@@ -127,6 +127,7 @@ axiom MSB16_of_make_word16 :
  ∀bh,bl:byte8.
   MSB_w16 (mk_word16 bh bl) = MSB_b8 bh.
 
+(*
 lemma execute_HCS08_LDHX_maIMM2 :
  ∀t:memory_impl.∀s:any_status HCS08 t.∀bhigh,blow:byte8.
   (get_clk_desc HCS08 t s = None ?) →
@@ -168,7 +169,6 @@ lemma execute_HCS08_LDHX_maIMM2 :
    [ true ⇒ tick_execute HCS08 t s (anyOP HCS08 LDHX) MODE_IMM2 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))
    | false ⇒ TickOK (any_status HCS08 t) (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉     (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))]);
  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
-
  letin status1 ≝ (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
  change in ⊢ (? ? % ?) with
   (match 2 with 
@@ -436,3 +436,4 @@ lemma execute_HCS08_STHX_maSP1 :
  [2: elim H; reflexivity ]
  reflexivity.
 qed.
+*)