X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fmedium_tests_lemmas.ma;h=d59e885681ea7aeefee0ea775ed631bb920d4f76;hb=3e094922bf3fec6975fdbe6feceb509eaafe0563;hp=81505ac2615211999ab80f6060214f420baf4db1;hpb=661ffd4d7c77fce52fb2f2d96f1737be424af3f1;p=helm.git

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 81505ac26..d59e88568 100644
--- 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.