∀bh,bl:byte8.
MSB_w16 (mk_word16 bh bl) = MSB_b8 bh.
+(*
lemma execute_HCS08_LDHX_maIMM2 :
∀t:memory_impl.∀s:any_status HCS08 t.∀bhigh,blow:byte8.
(get_clk_desc HCS08 t s = None ?) →
[ true ⇒ tick_execute HCS08 t s (anyOP HCS08 LDHX) MODE_IMM2 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s))
| false ⇒ TickOK (any_status HCS08 t) (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))))]);
whd in ⊢ (? ? match % in tick_result return ? with [_⇒?|_⇒?|_⇒?] ?);
-
letin status1 ≝ (set_clk_desc HCS08 t s (Some ? (quintupleT ????? 〈x0,x1〉 (anyOP HCS08 LDHX) MODE_IMM2 〈x0,x3〉 (filtered_inc_w16 HCS08 t s (get_pc_reg HCS08 t s)))));
change in ⊢ (? ? % ?) with
(match 2 with
[2: elim H; reflexivity ]
reflexivity.
qed.
+*)