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 ]
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 ]