1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/medium_tests_tools.ma".
29 (* ***************** *)
30 (* assiomi e teoremi *)
31 (* ***************** *)
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.
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.
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.
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.
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.
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.
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).
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) =
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) =
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) =
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) =
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.
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.
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.
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.
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.
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.
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)).
122 axiom w16h_of_make_word16 :
124 w16h (mk_word16 bh bl) = bh.
126 axiom MSB16_of_make_word16 :
128 MSB_w16 (mk_word16 bh bl) = MSB_b8 bh.
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
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〉))
149 (filtered_plus_w16 HCS08 t s (get_pc_reg HCS08 t s) 3))).
153 whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
156 whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
157 whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
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 [_⇒?|_⇒?|_⇒?] ?);
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
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 [_⇒?|_⇒λ_.%] ?);
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)))));
189 change in ⊢ (? ? % ?) 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 [_⇒?|_⇒?] ?] ?);
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 [_⇒?|_⇒?] ?] ?);
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 [_⇒?|_⇒?] ?] ?);
216 whd in ⊢ (? ? match ? in nat return ? with [_⇒?|_⇒λ_.? ? ? % ?] ?);
217 change in ⊢ (? ? % ?) with
219 (set_clk_desc HCS08 t
221 (setweak_v_flag HCS08 t
222 (setweak_n_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))
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 ]
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
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)))
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))))
268 (filtered_plus_w16 HCS08 MEM_TREE s (get_pc_reg HCS08 MEM_TREE s) 3)).
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).
289 whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
292 whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
293 whd in ⊢ (? ? match match % in fetch_result return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
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 [_⇒?|_⇒?|_⇒?] ?);
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);
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);
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 [_⇒?|_⇒?|_⇒?] ?);
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);
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 [_⇒?|_⇒?|_⇒?] ?);
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);
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 [_⇒?|_⇒?|_⇒?] ?);
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 [_⇒?|_⇒?|_⇒?] ?);
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 [_⇒?|_⇒?|_⇒?] ?);
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 [_⇒?|_⇒?|_⇒?] ?);
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 [_⇒?|_⇒?|_⇒?] ?);
396 whd in ⊢ (? ? match match % in option return ? with [_⇒?|_⇒?] in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
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;
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)));
428 rewrite > Hcut in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? ? (? ? % ? ?)) ?) ?) ?) ?) ?)) ?);
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))));
432 rewrite > Hcut1 in ⊢ (? ? (? ? (? ? ? (? ? ? (? ? ? (? ? ? (? ? ? % ?) ?) ?) ?) ?)) ?);
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 ]