matita/contribs/assembly/freescale/medium_tests_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                           Progetto FreeScale                           *)
  17 (*                                                                        *)
  18 (* Sviluppato da:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/medium_tests_tools.ma".
  28
  29 (* ***************** *)
  30 (* assiomi e teoremi *)
  31 (* ***************** *)
  32
  33 axiom get_set_clk_desc :
  34  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.
  35   get_clk_desc m t (set_clk_desc m t s clk) = clk.
  36
  37 axiom set_set_clk_desc :
  38  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk1,clk2.
  39   set_clk_desc m t (set_clk_desc m t s clk1) clk2 =
  40   set_clk_desc m t s clk2.
  41
  42 axiom memory_filter_read_set_clk_desc :
  43  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀addr.∀clk.
  44   memory_filter_read m t (set_clk_desc m t s clk) addr =
  45   memory_filter_read m t s addr.
  46
  47 axiom filtered_inc_set_clk_desc :
  48  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀w.
  49   filtered_inc_w16 m t (set_clk_desc m t s clk) w =
  50   filtered_inc_w16 m t s w.
  51
  52 axiom filtered_plus_set_clk_desc :
  53  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀w.∀n.
  54   filtered_plus_w16 m t (set_clk_desc m t s clk) w n =
  55   filtered_plus_w16 m t s w n.
  56
  57 axiom filtered_plus_set_mem_desc :
  58  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀mem.∀w.∀n.
  59   filtered_plus_w16 m t (set_mem_desc m t s mem) w n =
  60   filtered_plus_w16 m t s w n.
  61
  62 axiom filtered_plus_and_inc :
  63  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀w.∀n.
  64   filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n =
  65   filtered_plus_w16 m t s w (S n).
  66
  67 axiom get_alu_set_clk_desc :
  68  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.
  69   alu m t (set_clk_desc m t s clk) =
  70   alu m t s.
  71
  72 axiom get_chk_desc_set_clk_desc :
  73  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.
  74   get_chk_desc m t (set_clk_desc m t s clk) =
  75   get_chk_desc m t s.
  76
  77 axiom get_chk_desc_set_mem_desc :
  78  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀mem.
  79   get_chk_desc m t (set_mem_desc m t s mem) =
  80   get_chk_desc m t s.
  81
  82 axiom get_mem_desc_set_clk_desc :
  83  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.
  84   get_mem_desc m t (set_clk_desc m t s clk) =
  85   get_mem_desc m t s.
  86
  87 axiom set_clk_desc_set_mem_desc :
  88  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀mem.
  89   set_mem_desc m t (set_clk_desc m t s clk) mem =
  90   set_clk_desc m t (set_mem_desc m t s mem) clk.
  91
  92 axiom set_clk_desc_set_alu :
  93  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀alu.
  94   set_alu m t (set_clk_desc m t s clk) alu =
  95   set_clk_desc m t (set_alu m t s alu) clk.
  96
  97 axiom set_clk_desc_set_z_flag :
  98  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀z.
  99   set_z_flag m t (set_clk_desc m t s clk) z =
 100   set_clk_desc m t (set_z_flag m t s z) clk.
 101
 102 axiom set_clk_desc_setweak_n_flag :
 103  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀n.
 104   setweak_n_flag m t (set_clk_desc m t s clk) n =
 105   set_clk_desc m t (setweak_n_flag m t s n) clk.
 106
 107 axiom set_clk_desc_setweak_v_flag :
 108  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀v.
 109   setweak_v_flag m t (set_clk_desc m t s clk) v =
 110   set_clk_desc m t (setweak_v_flag m t s v) clk.
 111
 112 axiom set_clk_desc_set_pc_reg :
 113  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀clk.∀pc.
 114   set_pc_reg m t (set_clk_desc m t s clk) pc =
 115   set_clk_desc m t (set_pc_reg m t s pc) clk.
 116
 117 axiom set_clk_f_set_clk_desc :
 118  ∀m:mcu_type.∀t:memory_impl.∀s:any_status m t.∀f.
 119   (get_clk_desc m t s = None ?) →
 120   (set_clk_desc m t (f s) (None ?) = (f s)).
 121
 122 axiom w16h_of_make_word16 :
 123  ∀bh,bl:byte8.
 124   w16h (mk_word16 bh bl) = bh.
 125
 126 axiom MSB16_of_make_word16 :
 127  ∀bh,bl:byte8.
 128   MSB_w16 (mk_word16 bh bl) = MSB_b8 bh.
 129
 130 lemma execute_HCS08_LDHX_maIMM2 :
 131  ∀t:memory_impl.∀s:any_status HCS08 t.∀bhigh,blow:byte8.
 132   (get_clk_desc HCS08 t s = None ?) →
 133   (memory_filter_read HCS08 t s (get_pc_reg HCS08 t s) = Some ? 〈x4,x5〉) →
 134   (memory_filter_read HCS08 t s (filtered_inc_w16 HCS08 t s
 135                                  (get_pc_reg HCS08 t s)) = Some ? bhigh) →
 136   (memory_filter_read HCS08 t s (filtered_inc_w16 HCS08 t s
 137                                  (filtered_inc_w16 HCS08 t s
 138                                   (get_pc_reg HCS08 t s))) = Some ? blow)
 139   → (execute HCS08 t (TickOK ? s) 3 =
 140     TickOK ? (set_pc_reg HCS08 t
 141               (setweak_v_flag HCS08 t
 142                (setweak_n_flag HCS08 t
 143                 (set_z_flag HCS08 t
 144                  (set_alu HCS08 t s
 145                   (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉))
 146                 (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉))
 147                (MSB_w16 〈bhigh:blow〉))
 148               false)
 149              (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3))).
 150
 151  intros;
 152  whd in ⊢ (? ? % ?);
 153  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 154  rewrite > H;
 155
 156  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 157  whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 158  rewrite > H1;
 159
 160  whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 161  change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
 162   (match (quadrupleT (any_opcode HCS08) ??? LDHX MODE_IMM2 〈x4,x5〉 〈x0,x3〉) with
 163    [quadrupleT pseudo mode _ tot_clk ⇒ match eq_b8 〈x0,x1〉 tot_clk with
 164     [ true ⇒ tick_execute HCS08 t s pseudo mode (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))
 165     | false ⇒ TickOK (any_status HCS08 t) (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 pseudo mode tot_clk (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))]]);
 166  change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
 167   (match eq_b8 〈x0,x1〉 〈x0,x3〉 with
 168    [ true ⇒ tick_execute HCS08 t s (anyOP HCS08 LDHX) MODE_IMM2 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))
 169    | 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)))))]);
 170  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 171
 172  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)))));
 173  change in ⊢ (? ? % ?) with
 174   (match 2 with
 175    [ O ⇒ TickOK ? status1
 176    | S (n':nat) ⇒ execute HCS08 t (tick HCS08 t status1) n']);
 177  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
 178  unfold status1 in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_. ? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?);
 179  rewrite > (get_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)))));
 180  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
 181  normalize in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? (? ? ? ? (? ? (? ? ? ? ? ? % ? ? ? ?)))) ?] ?);
 182  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.%] ?);
 183
 184  unfold status1 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? (? ? ? % ?)) ?] ?);
 185  rewrite > (set_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)))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))
 186   in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? (? ? %) ?] ?);
 187  letin status2 ≝ (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
 188
 189  change in ⊢ (? ? % ?) with
 190   (match 1 with
 191    [ O ⇒ TickOK ? status2
 192    | S (n':nat) ⇒ execute HCS08 t (tick HCS08 t status2) n']);
 193  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
 194  unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.  ? ? ? match ? ? ? % in option return ? with [_⇒?|_⇒?] ?] ?);
 195  rewrite > (get_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
 196  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
 197  change in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match % in option return ? with [_⇒?|_⇒?] ?] ?) with
 198   (execute_LDHX HCS08 t status2 MODE_IMM2
 199  (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)));
 200  whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match % in option return ? with [_⇒?|_⇒?] ?] ?);
 201  whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_.? ? ? match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 202
 203  unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 204  rewrite > (memory_filter_read_set_clk_desc HCS08 t s (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))
 205   in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 206  rewrite > H2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 207  whd in ⊢ (? ? match ? in nat return ? with [_⇒? |_⇒λ_. ? ? ? match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 208
 209  unfold status2 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 210  rewrite > (filtered_inc_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))
 211   in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match ? ? ? ? % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 212  rewrite > (memory_filter_read_set_clk_desc HCS08 t s (filtered_inc_w16 HCS08 t s (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))
 213   in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 214  rewrite > H3 in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_. ? ? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ?] ?);
 215
 216  whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
 217  change in ⊢ (? ? % ?) with
 218   (TickOK ?
 219   (set_clk_desc HCS08 t
 220    (set_pc_reg HCS08 t
 221     (setweak_v_flag HCS08 t
 222      (setweak_n_flag HCS08 t
 223       (set_z_flag HCS08 t
 224        (set_alu HCS08 t status2
 225         (set_indX_16_reg_HC08 (alu HCS08 t status2) 〈bhigh:blow〉))
 226        (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉))
 227       (MSB_w16 〈bhigh:blow〉)) false)
 228     (filtered_plus_w16 HCS08 t status2
 229      (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) 2))
 230    (None ?)));
 231
 232  unfold status2 in ⊢ (? ? (? ? (? ? ? (? ? ? ? (? ? ? % ? ?)) ?)) ?);
 233  rewrite > (filtered_plus_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)) 2);
 234  rewrite > (filtered_plus_and_inc HCS08 t s (get_pc_reg HCS08 t s) 2);
 235  unfold status2 in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? (? ? ? %) ?)) ?) ?) ?) ?) ?)) ?);
 236  rewrite > (get_alu_set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))
 237   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? % ?)) ?) ?) ?) ?) ?)) ?);
 238  unfold status2 in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? % ?) ?) ?) ?) ?) ?)) ?);
 239  rewrite > (set_clk_desc_set_alu HCS08 t s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉))
 240   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? % ?) ?) ?) ?) ?)) ?);
 241  rewrite > (set_clk_desc_set_z_flag HCS08 t (set_alu HCS08 t s (set_indX_16_reg_HC08 (alu HCS08 t s) 〈bhigh:blow〉)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (eq_w16 〈bhigh:blow〉 〈〈x0,x0〉:〈x0,x0〉〉));
 242  rewrite > (set_clk_desc_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〉〉)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (MSB_w16 〈bhigh:blow〉));
 243  rewrite > (set_clk_desc_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〉)) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) false);
 244  rewrite > (set_clk_desc_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) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))) (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3));
 245  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 ?));
 246  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 ⊢ (? ? (? ? %) ?);
 247  [2: elim H; reflexivity ]
 248  reflexivity.
 249 qed.
 250
 251 definition execute_HCS08_STHX_maSP1_aux ≝
 252  λs:any_status HCS08 MEM_TREE.λblow:byte8.
 253   TickOK ? (set_pc_reg HCS08 MEM_TREE
 254             (setweak_v_flag HCS08 MEM_TREE
 255              (setweak_n_flag HCS08 MEM_TREE
 256               (set_z_flag HCS08 MEM_TREE
 257                (set_mem_desc HCS08 MEM_TREE s
 258                 (mt_update byte8
 259                  (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s)
 260                   (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)
 261                   (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))
 262                  (succ_w16
 263                   (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉))
 264                  (indX_low_reg_HC08 (alu HCS08 MEM_TREE s))))
 265                (eq_w16 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE s)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE s))〉 〈〈x0,x0〉:〈x0,x0〉〉))
 266               (MSB_b8 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s))))
 267              false)
 268             (filtered_plus_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) 3)).
 269
 270 lemma execute_HCS08_STHX_maSP1 :
 271  ∀s:any_status HCS08 MEM_TREE.∀blow:byte8.
 272   (get_clk_desc HCS08 MEM_TREE s = None ?) →
 273   (memory_filter_read HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) = Some ? 〈x9,xE〉) →
 274   (memory_filter_read HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s
 275                                  (get_pc_reg HCS08 MEM_TREE s)) = Some ? 〈xF,xF〉) →
 276   (memory_filter_read HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s
 277                                  (filtered_inc_w16 HCS08 MEM_TREE s
 278                                   (get_pc_reg HCS08 MEM_TREE s))) = Some ? blow) →
 279   (chk_get MEM_TREE (get_chk_desc HCS08 MEM_TREE s)
 280              (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) =
 281    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) →
 282   (chk_get MEM_TREE (get_chk_desc HCS08 MEM_TREE s)
 283              (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) =
 284    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) →
 285    (execute HCS08 MEM_TREE (TickOK ? s) 5 = execute_HCS08_STHX_maSP1_aux s blow).
 286
 287  intros;
 288  whd in ⊢ (? ? % ?);
 289  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 290  rewrite > H;
 291
 292  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 293  whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 294  rewrite > H1;
 295
 296  whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 297  rewrite > H2 in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 298  whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 299  change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
 300   (match quadrupleT ???? (anyOP HCS08 STHX) MODE_SP1 〈〈x9,xE〉:〈xF,xF〉〉 〈x0,x5〉 with [ quadrupleT pseudo mode _ tot_clk ⇒ match eq_b8 〈x0,x1〉 tot_clk with [true⇒tick_execute HCS08 MEM_TREE s pseudo mode (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) |false⇒ TickOK (any_status HCS08 MEM_TREE) (set_clk_desc HCS08 MEM_TREE s (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 〈x0,x1〉 pseudo mode tot_clk (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))]]);
 301  change in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
 302   (match eq_b8 〈x0,x1〉 〈x0,x5〉 with [true⇒ tick_execute HCS08 MEM_TREE s (anyOP HCS08 STHX) MODE_SP1 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) |false⇒ TickOK (any_status HCS08 MEM_TREE) (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))]);
 303  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 304
 305  letin status1 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE  s (get_pc_reg HCS08 MEM_TREE s))))));
 306  change in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (status1);
 307  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status1) 4);
 308
 309  whd in ⊢ (? ? % ?);
 310  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 311  unfold status1 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 312  rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) ) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 313  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 314  unfold status1 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 315  rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 316  letin status2 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
 317  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status2) 3);
 318
 319  whd in ⊢ (? ? % ?);
 320  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 321  unfold status2 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 322  rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 323  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 324  unfold status2 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 325  rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x2〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 326
 327  letin status3 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
 328  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status3) 2);
 329
 330  whd in ⊢ (? ? % ?);
 331  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 332  unfold status3 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 333  rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 334  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 335  unfold status3 in ⊢ (? ? match ? ? (? ? ? % ?) in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 336  rewrite > (set_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x3〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match ? ? % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 337
 338  letin status4 ≝ (set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
 339  change in ⊢ (? ? % ?) with (execute HCS08 MEM_TREE (TickOK ? status4) 1);
 340
 341  whd in ⊢ (? ? % ?);
 342  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 343  unfold status4 in ⊢ (? ? match match ? ? ? % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 344  rewrite > (get_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 345  whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 346  change in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (execute_STHX HCS08 MEM_TREE status4 MODE_SP1 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))));
 347  whd in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 348  whd in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 349  unfold status4 in ⊢ (? ? match match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 350  rewrite > (memory_filter_read_set_clk_desc HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 351   in ⊢ (? ? match match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 352  rewrite > H3 in ⊢ (? ? match match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 353
 354  whd in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:?.%) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 355  whd in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:?.match % in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 356  whd in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:?.match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 357  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 358   in ⊢ (? ? match match match match ? in option return ? with [_⇒? |_⇒λ_. (λoffs:?.match match match ? ? ? (? ? ? (? (? %) ?)) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 359  rewrite > (get_chk_desc_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 360   in ⊢ (? ? match match match match ? in option return ? with [_⇒?|_⇒λ_.(λoffs:? .match match match ? ? ? (? ? % ?) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?]) ?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 361  change in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
 362   (match match match getn_array8T o0 memory_type (chk_get MEM_TREE (get_chk_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) in memory_type return λm.(option (Prod16T (Prod16T (Prod16T (Prod16T byte8))))) with [MEM_READ_ONLY⇒ Some (Prod16T (Prod16T (Prod16T (Prod16T byte8)))) (get_mem_desc HCS08 MEM_TREE status4) |MEM_READ_WRITE⇒ Some (Prod16T (Prod16T (Prod16T (Prod16T byte8)))) (mt_update byte8 (get_mem_desc HCS08 MEM_TREE status4) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉) (w16h 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE status4)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))〉)) |MEM_OUT_OF_BOUND⇒None (Prod16T (Prod16T (Prod16T (Prod16T byte8))))] in option return λo.(option (any_status HCS08 MEM_TREE)) with [None⇒None (any_status HCS08 MEM_TREE) |Some x⇒ (λmem.Some (any_status HCS08 MEM_TREE) (set_mem_desc HCS08 MEM_TREE status4 mem)) x] in option return λo.(option (Prod (any_status HCS08 MEM_TREE) word16)) with [None⇒None (Prod (any_status HCS08 MEM_TREE) word16) |Some x⇒ (λtmps1.opt_map (any_status HCS08 MEM_TREE) (Prod (any_status HCS08 MEM_TREE) word16) (memory_filter_write HCS08 MEM_TREE tmps1 (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉)) (w16l 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE status4)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))〉)) (λtmps2.Some (Prod (any_status HCS08 MEM_TREE) word16) (pair (any_status HCS08 MEM_TREE) word16 tmps2 (filtered_plus_w16 HCS08 MEM_TREE tmps2 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)))) x]);
 363  rewrite > H4 in ⊢ (? ? match match match match match match ? ? ? % in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 364
 365  whd in ⊢ (? ? match match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 366  rewrite > (get_mem_desc_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 367   in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? % ? ?)) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 368  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 369   in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? ? (? (? (? %) ?)))) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 370  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 371   in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? (? (? %) ?) ?)) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 372  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 373   in ⊢ (? ? match match match match ? ? (? ? ? ? (? ? ? ? (? (? ? (? %))))) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 374
 375  rewrite > (set_clk_desc_set_mem_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉) (w16h 〈(indX_high_reg_HC08 (alu HCS08 MEM_TREE s)):(indX_low_reg_HC08 (alu HCS08 MEM_TREE s))〉)) )
 376   in ⊢ (? ? match match match match ? ? % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 377  rewrite > (w16h_of_make_word16 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s)))
 378   in ⊢ (? ? match match match match ? ? (? ? ? (? ? ? ? (? ? ? ? %)) ?) in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 379  letin status5 ≝ (set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (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)))) (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 〈x0,x4〉 STHX MODE_SP1 〈x0,x5〉  (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))));
 380  change in ⊢ (? ? match match match match ? ? % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with (status5);
 381  change in ⊢ (? ? match match match % in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?) with
 382   (opt_map ?? (memory_filter_write HCS08 MEM_TREE status5 (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE status4)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE status4))) (λtmps2:any_status HCS08 MEM_TREE .Some ? (pair ?? tmps2 (filtered_plus_w16 HCS08 MEM_TREE tmps2 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1))));
 383  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 384   in ⊢ (? ? match match match ? ? ? (? ? ? ? ? (? %)) ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 385  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 386   in ⊢ (? ? match match match ? ? ? (? ? ? ? (? (? (? %) ?)) ?) ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 387
 388  whd in ⊢ (? ? match match match ? ? ? % ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 389  whd in ⊢ (? ? match match match ? ? ? match % in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 390  rewrite > (get_chk_desc_set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (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)))) (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 391   in ⊢ (? ? match match match ? ? ? match match ? ? ? (? ? % ?) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 392  rewrite > (get_chk_desc_set_mem_desc HCS08 MEM_TREE s (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))))
 393   in ⊢ (? ? match match match ? ? ? match match ? ? ? (? ? % ?) in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 394  rewrite > H5 in ⊢ (? ? match match match ? ? ? match match ? ? ? % in memory_type return ? with [_⇒?|_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] ? in option return ? with [_⇒?|_⇒?] in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 395
 396  whd in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
 397  whd in ⊢ (? ? % ?);
 398  rewrite > (filtered_plus_set_mem_desc HCS08 MEM_TREE status5 (mt_update byte8 (get_mem_desc HCS08 MEM_TREE status5) (succ_w16 (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) 〈〈x0,x0〉:blow〉)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s))) (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)
 399   in ⊢ (? ? (? ? (? ? ? (? ? ? ? %) ?)) ?);
 400  rewrite > (filtered_plus_set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (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)))) (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 〈x0,x4〉 STHX MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))) (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)
 401   in ⊢ (? ? (? ? (? ? ? (? ? ? ? %) ?)) ?);
 402  rewrite > (filtered_plus_set_mem_desc HCS08 MEM_TREE s (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))) (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))) 1)
 403   in ⊢ (? ? (? ? (? ? ? (? ? ? ? %) ?)) ?);
 404  rewrite > (filtered_plus_and_inc HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)) 1)
 405    in ⊢ (? ? (? ? (? ? ? (? ? ? ? %) ?)) ?);
 406  rewrite > (filtered_plus_and_inc HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) 2)
 407   in ⊢ (? ? (? ? (? ? ? (? ? ? ? %) ?)) ?);
 408  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 409   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? (? (? %) ?))) ?) ?) ?)) ?);
 410  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 411   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? (? ? (? %)))) ?) ?) ?)) ?);
 412  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 413   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? (? ? (? %)) ?)) ?) ?) ?) ?)) ?);
 414  rewrite > (get_alu_set_clk_desc HCS08 MEM_TREE s (Some ? (quintupleT ????? 〈x0,x4〉 (anyOP HCS08 STHX) MODE_SP1 〈x0,x5〉 (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s))))))
 415   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? (? (? %) ?) ?)) ?) ?) ?) ?)) ?);
 416  rewrite > (MSB16_of_make_word16 (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)) (indX_low_reg_HC08 (alu HCS08 MEM_TREE s)))
 417   in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? ? %) ?) ?) ?)) ?);  clearbody status;
 418  clearbody status;
 419  clearbody status1;
 420  clearbody status2;
 421  clearbody status3;
 422  clearbody status4;
 423
 424  cut (get_mem_desc HCS08 MEM_TREE (set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) (mk_word16 (mk_byte8 x0 x0) blow)) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)))) (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 (mk_byte8 x0 x4) STHX MODE_SP1 (mk_byte8 x0 x5) (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s)))))) = mt_update byte8 (get_mem_desc HCS08 MEM_TREE s) (plus_w16nc (sp_reg_HC08 (alu HCS08 MEM_TREE s)) (mk_word16 (mk_byte8 x0 x0) blow)) (indX_high_reg_HC08 (alu HCS08 MEM_TREE s)));
 425
 426  (* basta... *)
 427  [2: elim daemon ]
 428  rewrite > Hcut in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? ? % ? ?)) ?) ?) ?) ?) ?)) ?);
 429
 430  cut (set_mem_desc HCS08 MEM_TREE (set_clk_desc HCS08 MEM_TREE (set_mem_desc HCS08 MEM_TREE s (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)))) (Some (Prod5T byte8 (any_opcode HCS08) instr_mode byte8 word16) (quintupleT byte8 (any_opcode HCS08) instr_mode byte8 word16 〈x0,x4〉 STHX MODE_SP1 〈x0,x5〉  (filtered_inc_w16 HCS08 MEM_TREE s (filtered_inc_w16 HCS08 MEM_TREE s (get_pc_reg 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))) = 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))));
 431  [2: elim daemon ]
 432  rewrite > Hcut1 in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? % ?) ?) ?) ?) ?)) ?);
 433
 434  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)))
 435   in ⊢ (? ? (? ? %) ?);
 436  [2: elim H; reflexivity ]
 437  reflexivity.
 438 qed.