No longer used.

[helm.git] / helm / software / matita / contribs / assembly / freescale / medium_tests_lemmas.ma

diff --git a/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma b/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma
index 81505ac2615211999ab80f6060214f420baf4db1..d59e885681ea7aeefee0ea775ed631bb920d4f76 100644 (file)
--- a/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma
+++ b/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma
@@ -147,8 +147,8 @@ lemma execute_HCS08_LDHX_maIMM2 :
                (MSB_w16 〈bhigh:blow〉))
               false)
              (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3))).
-
- intros;
+elim daemon.
+(* intros;
  whd in ⊢ (? ? % ?);
  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > H;
@@ -245,7 +245,7 @@ lemma execute_HCS08_LDHX_maIMM2 :
  rewrite > (set_set_clk_desc HCS08 t (set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (None ?));
  rewrite > (set_clk_f_set_clk_desc HCS08 t s (λtmps.set_pc_reg HCS08 t (setweak_v_flag HCS08 t (setweak_n_flag HCS08 t (set_z_flag HCS08 t (set_alu HCS08 t tmps (set_indX_16_reg_HC08 (alu HCS08 t tmps) 〈bhigh:blow〉)) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_w16 〈bhigh:blow〉)) false) (filtered_plus_w16 HCS08 t tmps (get_pc_reg HCS08 t tmps) 3))) in ⊢ (? ? (? ? %) ?);
  [2: elim H; reflexivity ]
- reflexivity.
+ reflexivity.*)
 qed.
 
 definition execute_HCS08_STHX_maSP1_aux ≝
@@ -283,8 +283,8 @@ lemma execute_HCS08_STHX_maSP1 :
              (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) =
    array_8T ? MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE MEM_READ_WRITE) → 
    (execute HCS08 MEM_TREE (TickOK ? s) 5 = execute_HCS08_STHX_maSP1_aux s blow).
-
- intros;
+elim daemon.
+(* intros;
  whd in ⊢ (? ? % ?);
  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
  rewrite > H;
@@ -434,5 +434,5 @@ lemma execute_HCS08_STHX_maSP1 :
  rewrite > (set_clk_f_set_clk_desc HCS08 MEM_TREE s (λs.set_pc_reg HCS08 MEM_TREE (setweak_v_flag HCS08 MEM_TREE (setweak_n_flag HCS08 MEM_TREE (set_z_flag HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s))) (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s)))) (eq_w16 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE s)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE s))〉 〈〈x0,x0〉:〈x0,x0〉〉)) (MSB_b8 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))) false) (filtered_plus_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) 3)))
   in ⊢ (? ? (? ? %) ?);
  [2: elim H; reflexivity ]
- reflexivity.
+ reflexivity.*)
 qed.