source: src/ASM/AssemblyProofSplit.ma @ 2210

include "ASM/StatusProofsSplit.ma".

include alias "arithmetics/nat.ma".
include alias "basics/logic.ma".
include alias "ASM/BitVectorTrie.ma".

lemma fetch_many_singleton:
  ∀code_memory: BitVectorTrie Byte 16.
  ∀final_pc, start_pc: Word.
  ∀i: instruction.
    fetch_many code_memory final_pc start_pc [i] →
      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
start_pc.
  #code_memory #final_pc #start_pc #i * #new_pc
  #fetch_many_assm whd in fetch_many_assm;
  cases (eq_bv_eq … fetch_many_assm) assumption
qed.

include alias "ASM/Vector.ma".
include "ASM/Test.ma".

lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
  ∀M, cm, ps, sigma, x.
  ∀addr1: [[acc_a]].
    addressing_mode_ok pseudo_assembly_program M cm ps addr1=true → 
      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
  #M #cm #ps #sigma #x #addr1
  @(subaddressing_mode_elim … addr1)
  whd in ⊢ (??%? → ??%?);
  cases (\snd M)
  [1:
    //
  |2:
    #upper_lower #address normalize nodelta #absurd
    destruct(absurd) 
  ]
qed.

lemma addressing_mode_ok_to_snd_M_data:
  ∀M, cm, ps.
  ∀addr: [[acc_a]].
  addressing_mode_ok pseudo_assembly_program M cm ps addr = true →
    \snd M = data.
  #M #addr #ps #addr
  @(subaddressing_mode_elim … addr)
  whd in ⊢ (??%? → ?);
  cases (\snd M) normalize nodelta
  [2:
    * #address #absurd destruct(absurd)
  ]
  #_ %
qed.

lemma assoc_list_exists_true_to_assoc_list_lookup_Some:
  ∀A, B: Type[0].
  ∀e: A.
  ∀the_list: list (A × B).
  ∀eq_f: A → A → bool.
    assoc_list_exists A B e eq_f the_list = true →
      ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'.
  #A #B #e #the_list #eq_f elim the_list
  [1:
    whd in ⊢ (??%? → ?); #absurd destruct(absurd)
  |2:
    #hd #tl #inductive_hypothesis
    whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????);
    cases (eq_f (\fst hd) e) normalize nodelta
    [1:
      #_ %{(\snd hd)} %
    |2:
      @inductive_hypothesis
    ]
  ]
qed.

lemma assoc_list_exists_false_to_assoc_list_lookup_None:
  ∀A, B: Type[0].
  ∀e, e': A.
  ∀the_list, the_list': list (A × B).
  ∀eq_f: A → A → bool.
    e = e' →
    the_list = the_list' →
      assoc_list_exists A B e eq_f the_list = false →
        assoc_list_lookup A B e' eq_f the_list' = None ….
  #A #B #e #e' #the_list elim the_list
  [1:
    #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ %
  |2:
    #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl
    whd in ⊢ (??%? → ??%?); <e_refl
    cases (eq_f (\fst hd) e) normalize nodelta
    [1:
      #absurd destruct(absurd)
    |2:
      >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption
    ]
  ]
qed.

lemma sfr_psw_eq_to_bit_address_of_register_eq:
  ∀A: Type[0].
  ∀code_memory: A.
  ∀status, status', register_address.
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
      bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address.
  #A #code_memory #status #status' #register_address #sfr_psw_refl
  whd in match bit_address_of_register; normalize nodelta
  <sfr_psw_refl %
qed.

lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq:
  ∀A: Type[0].
  ∀code_memory: A.
  ∀status, status', register_address.
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
      low_internal_ram A code_memory status = low_internal_ram A code_memory status' →
        get_register A code_memory status register_address = get_register A code_memory status' register_address.
  #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl
  whd in match get_register; normalize nodelta <low_internal_ram_refl
  >(sfr_psw_eq_to_bit_address_of_register_eq … status status') //
qed.

lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr:
  ∀M', cm, status, status', sigma.
  ∀addr1: [[acc_a; registr; direct; indirect; data]]. (* XXX: expand as needed *)
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
    map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1.
  #M' #cm #status #status' #sigma #addr1 #sfr_refl
  @(subaddressing_mode_elim … addr1) try (#w #_ @I)
  [1: #_ @I ]
  #w whd in ⊢ (??%? → %);
  inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
  [1:
    #absurd destruct(absurd)
  |2:
    #_
    @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
    <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption
  ]
qed.

lemma not_b_c_to_b_not_c:
  ∀b, c: bool.
    (¬b) = c → b = (¬c).
  //
qed.
(* XXX: move above elsewhere *)

lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map:
  ∀M.
  ∀sigma.
  ∀sfr8051.
  ∀b.
    sfr8051 ≠ SFR_ACC_A →
      map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b.
  #M #sigma * #b
  [18:
    #relevant cases (absurd … (refl ??) relevant)
  ]
  #_ %
qed.

lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map:
  ∀M.
  ∀sigma: Word → Word.
  ∀w: BitVector 8.
  ∀b.
    w ≠ bitvector_of_nat … 224 →
      map_address_Byte_using_internal_pseudo_address_map M sigma w b = b.
  #M #sigma #w #b #w_neq_assm
  whd in ⊢ (??%?); inversion (sfr_of_Byte ?)
  [1:
    #sfr_of_Byte_refl %
  |2:
    * #sfr8051 #sfr_of_Byte_refl normalize nodelta try %
    @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map %
    #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl
    @(absurd ?? w_neq_assm)
    lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma
    whd in match sfr_of_Byte; normalize nodelta
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ]
    cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ]
    #absurd destruct(absurd)
qed.

lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map:
  ∀M, sigma, w, b.
    assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst  M) = false →
      map_internal_ram_address_using_pseudo_address_map M sigma w b = b.
  #M #sigma #w #b #assoc_list_exists_assm
  whd in ⊢ (??%?);
  >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %
qed.
    
lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:
  ∀M', cm.
  ∀sigma, status, status', b, b'.
  ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr]]. (* XXX: expand as needed *)
    get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →
    low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →
    b = b' →
    addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →
      map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.
  #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl
  @(subaddressing_mode_elim … addr1)
  [1:
    whd in ⊢ (??%? → ??%?); cases (\snd M')
    [1:
      normalize nodelta #_ %
    |2:
      * #address normalize nodelta #absurd destruct(absurd)
    ]
  |2,4:
    #w whd in ⊢ (??%? → ??%?);
    inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta
    [1,3:
      #absurd destruct(absurd)
    |2:
      #_
      <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)
      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)
      normalize nodelta %
    |4:
      #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm)
      -assoc_list_exists_assm #assoc_list_exists_assm
      <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)
      >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm)
      normalize nodelta %
    ]
  |3:
    #w whd in ⊢ (??%? → ??%?);
    @eq_bv_elim #eq_bv_refl normalize nodelta
    [1:
      #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm)
      #assoc_list_exists_refl #eq_accumulator_refl
      >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b)
      whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl)
      %
    |2:
      #assoc_list_exists_assm
      @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta
      cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl
      <head_head' inversion bit #bit_refl normalize nodelta
      >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl;
      [1:
        @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption
      |2:
        @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map
        <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm)
      ]
    ]
  |5,6:
    #w #_ %
  ]
qed.

lemma match_nat_replace:
  ∀l, o, p, r, o', p': nat.
    l ≃ r →
    o ≃ o' →
    p ≃ p' →
      match l with [ O ⇒ o | S n ⇒ p ] = match r with [ O ⇒ o' | S n' ⇒ p' ].
  #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl %
qed.

lemma conjunction_split:
  ∀l, l', r, r': bool.
    l = l' → r = r' → (l ∧ r) = (l' ∧ r').
  #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl %
qed.

(*
lemma match_nat_status_of_pseudo_status:
  ∀M, cm, sigma, policy, s, s', s'', s'''.
  ∀n, n': nat.
    n = n' →
    status_of_pseudo_status M cm s' sigma policy = s →
    status_of_pseudo_status M cm s''' sigma policy = s'' →
      match n with [ O ⇒ s | S n' ⇒ s'' ] =
        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''']) sigma policy.
  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
  #n_refl #s_refl #s_refl' <n_refl <s_refl <s_refl'
  cases n normalize nodelta try % #n' %
qed.
*)

lemma main_lemma_preinstruction:
  ∀M, M': internal_pseudo_address_map.
  ∀preamble: preamble.
  ∀instr_list: list labelled_instruction.
  ∀cm: pseudo_assembly_program.
  ∀EQcm: cm = 〈preamble, instr_list〉.
  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
  ∀sigma: Word → Word.
  ∀policy: Word → bool.
  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
  ∀ps: PseudoStatus cm.
  ∀ppc: Word.
  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
  ∀labels: label_map.
  ∀costs: BitVectorTrie costlabel 16.
  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
  ∀newppc: Word.
  ∀lookup_labels: Identifier → Word.
  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
  ∀lookup_datalabels: Identifier → Word.
  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
  ∀instr: preinstruction Identifier.
  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
  ∀ticks: nat × nat.
  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
  ∀s: PreStatus pseudo_assembly_program cm.
  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
                  lookup_datalabels (Instruction instr)))) →
              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
                fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
                      status_of_pseudo_status M' cm s sigma policy).
    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
  (* XXX: takes about 45 minutes to type check! *)
  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
  [2: * // ]
  @(
  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
  match instr in preinstruction return λx. x = instr → Σs'.? with
        [ ADD addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) false in
            let cy_flag ≝ get_index' ? O  ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | ADDC addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) old_cy_flag in
            let cy_flag ≝ get_index' ? O ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | SUBB addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
                                                   (get_arg_8 … s false addr2) old_cy_flag in
            let cy_flag ≝ get_index' ? O ? flags in
            let ac_flag ≝ get_index' ? 1 ? flags in
            let ov_flag ≝ get_index' ? 2 ? flags in
            let s ≝ set_arg_8 … s ACC_A result in
              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
        | ANL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  let 〈addr1, addr2〉 ≝ l' in
                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 and_val
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 and_val
                ] 
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
               set_flags … s and_val (None ?) (get_ov_flag ?? s)
            ]
        | ORL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  let 〈addr1, addr2〉 ≝ l' in
                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 or_val
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                    set_arg_8 … s addr1 or_val
                ] 
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
               set_flags … s or_val (None ?) (get_ov_flag … s)
            ]
        | XRL addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l' ⇒
              let 〈addr1, addr2〉 ≝ l' in
              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                set_arg_8 … s addr1 xor_val
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
                set_arg_8 … s addr1 xor_val
            ]
        | INC addr ⇒ λinstr_refl.
            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
              [ ACC_A ⇒ λacc_a: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' ACC_A result
              | REGISTER r ⇒ λregister: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (REGISTER r) result
              | DIRECT d ⇒ λdirect: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (DIRECT d) result
              | INDIRECT i ⇒ λindirect: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
                 set_arg_8 … s' (INDIRECT i) result
              | DPTR ⇒ λdptr: True. λEQaddr.
                let s' ≝ add_ticks1 s in
                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
                let s ≝ set_8051_sfr … s' SFR_DPL bl in
                 set_8051_sfr … s' SFR_DPH bu
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
        | NOP ⇒ λinstr_refl.
           let s ≝ add_ticks2 s in
            s
        | DEC addr ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
             set_arg_8 … s addr result
        | MUL addr1 addr2 ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
           let product ≝ acc_a_nat * acc_b_nat in
           let ov_flag ≝ product ≥ 256 in
           let low ≝ bitvector_of_nat 8 (product mod 256) in
           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
           let s ≝ set_8051_sfr … s SFR_ACC_A low in
             set_8051_sfr … s SFR_ACC_B high
        | DIV addr1 addr2 ⇒ λinstr_refl.
           let s ≝ add_ticks1 s in
           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
             match acc_b_nat with
               [ O ⇒ set_flags … s false (None Bit) true
               | S o ⇒
                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
                   set_flags … s false (None Bit) false
               ]
        | DA addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
                let cy_flag ≝ get_index' ? O ? flags in
                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
                    let new_acc ≝ nu @@ acc_nl' in
                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
                  else
                    s
              else
                s
        | CLR addr ⇒ λinstr_refl.
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
              let s ≝ add_ticks1 s in
               set_arg_8 … s ACC_A (zero 8)
            | CARRY ⇒ λcarry: True.  λEQaddr.
              let s ≝ add_ticks1 s in
               set_arg_1 … s CARRY false
            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
              let s ≝ add_ticks1 s in
               set_arg_1 … s (BIT_ADDR b) false
            | _ ⇒ λother: False. ⊥
            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
        | CPL addr ⇒ λinstr_refl.
          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
                let s ≝ add_ticks1 s in
                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
                let new_acc ≝ negation_bv ? old_acc in
                 set_8051_sfr … s SFR_ACC_A new_acc
            | CARRY ⇒ λcarry: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let old_cy_flag ≝ get_arg_1 … s CARRY true in
                let new_cy_flag ≝ ¬old_cy_flag in
                 set_arg_1 … s CARRY new_cy_flag
            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
                let new_bit ≝ ¬old_bit in
                 set_arg_1 … s (BIT_ADDR b) new_bit
            | _ ⇒ λother: False. ?
            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
        | SETB b ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            set_arg_1 … s b false
        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_acc ≝ rotate_left … 1 old_acc in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_acc ≝ rotate_right … 1 old_acc in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_cy_flag ≝ get_index' ? O ? old_acc in
            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
            let s ≝ set_arg_1 … s CARRY new_cy_flag in
              set_8051_sfr … s SFR_ACC_A new_acc
        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_cy_flag ≝ get_cy_flag ?? s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
            let s ≝ set_arg_1 … s CARRY new_cy_flag in
              set_8051_sfr … s SFR_ACC_A new_acc
        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
            let s ≝ add_ticks1 s in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
            let new_acc ≝ nl @@ nu in
              set_8051_sfr … s SFR_ACC_A new_acc
        | PUSH addr ⇒ λinstr_refl.
            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
              [ DIRECT d ⇒ λdirect: True. λEQaddr.
                let s ≝ add_ticks1 s in
                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
                let s ≝ set_8051_sfr … s SFR_SP new_sp in
                  write_at_stack_pointer … s d
              | _ ⇒ λother: False. ⊥
              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
        | POP addr ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let contents ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
              set_arg_8 … s addr contents
        | XCH addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let old_addr ≝ get_arg_8 … s false addr2 in
            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
              set_arg_8 … s addr2 old_acc
        | XCHD addr1 addr2 ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
            let new_acc ≝ acc_nu @@ arg_nl in
            let new_arg ≝ arg_nu @@ acc_nl in
            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
              set_arg_8 … s addr2 new_arg
        | RET ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let high_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let low_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let new_pc ≝ high_bits @@ low_bits in
              set_program_counter … s new_pc
        | RETI ⇒ λinstr_refl.
            let s ≝ add_ticks1 s in
            let high_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let low_bits ≝ read_at_stack_pointer ?? s in
            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
            let s ≝ set_8051_sfr … s SFR_SP new_sp in
            let new_pc ≝ high_bits @@ low_bits in
              set_program_counter … s new_pc
        | MOVX addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          (* DPM: only copies --- doesn't affect I/O *)
          match addr with
            [ inl l ⇒
              let 〈addr1, addr2〉 ≝ l in
                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
            ]
        | MOV addr ⇒ λinstr_refl.
          let s ≝ add_ticks1 s in
          match addr with
            [ inl l ⇒
              match l with
                [ inl l' ⇒
                  match l' with
                    [ inl l'' ⇒
                      match l'' with
                        [ inl l''' ⇒
                          match l''' with
                            [ inl l'''' ⇒
                              let 〈addr1, addr2〉 ≝ l'''' in
                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                            | inr r'''' ⇒
                              let 〈addr1, addr2〉 ≝ r'''' in
                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                            ]
                        | inr r''' ⇒
                          let 〈addr1, addr2〉 ≝ r''' in
                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
                        ]
                    | inr r'' ⇒
                      let 〈addr1, addr2〉 ≝ r'' in
                       set_arg_16 … s (get_arg_16 … s addr2) addr1
                    ]
                | inr r ⇒
                  let 〈addr1, addr2〉 ≝ r in
                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
                ]
            | inr r ⇒
              let 〈addr1, addr2〉 ≝ r in
               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
            ]
          | JC addr ⇒ λinstr_refl.
                  if get_cy_flag ?? s then
                    let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                  else
                    let s ≝ add_ticks2 s in
                      s
            | JNC addr ⇒ λinstr_refl.
                  if ¬(get_cy_flag ?? s) then
                   let s ≝ add_ticks1 s in
                     set_program_counter … s (addr_of addr s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JB addr1 addr2 ⇒ λinstr_refl.
                  if get_arg_1 … s addr1 false then
                   let s ≝ add_ticks1 s in
                    set_program_counter … s (addr_of addr2 s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JNB addr1 addr2 ⇒ λinstr_refl.
                  if ¬(get_arg_1 … s addr1 false) then
                   let s ≝ add_ticks1 s in
                    set_program_counter … s (addr_of addr2 s)
                  else
                   let s ≝ add_ticks2 s in
                    s
            | JBC addr1 addr2 ⇒ λinstr_refl.
                  let s ≝ set_arg_1 … s addr1 false in
                    if get_arg_1 … s addr1 false then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr2 s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | JZ addr ⇒ λinstr_refl.
                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | JNZ addr ⇒ λinstr_refl.
                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
                     let s ≝ add_ticks1 s in
                      set_program_counter … s (addr_of addr s)
                    else
                     let s ≝ add_ticks2 s in
                      s
            | CJNE addr1 addr2 ⇒ λinstr_refl.
                  match addr1 with
                    [ inl l ⇒
                        let 〈addr1, addr2'〉 ≝ l in
                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
                            let s ≝ add_ticks1 s in
                            let s ≝ set_program_counter … s (addr_of addr2 s) in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                          else
                            let s ≝ add_ticks2 s in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                    | inr r' ⇒
                        let 〈addr1, addr2'〉 ≝ r' in
                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
                            let s ≝ add_ticks1 s in
                            let s ≝ set_program_counter … s (addr_of addr2 s) in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                          else
                            let s ≝ add_ticks2 s in
                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
                    ]
            | DJNZ addr1 addr2 ⇒ λinstr_refl.
              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
              let s ≝ set_arg_8 … s addr1 result in
                if ¬(eq_bv ? result (zero 8)) then
                 let s ≝ add_ticks1 s in
                  set_program_counter … s (addr_of addr2 s)
                else
                 let s ≝ add_ticks2 s in
                  s
           ] (refl … instr))
  try cases other
  try assumption (*20s*)
  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
  whd in match execute_1_preinstruction; normalize nodelta
  [35: (* XRL *)
    inversion addr
    [1:
      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
      >EQP -P normalize nodelta
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
      [2: normalize nodelta #absurd destruct(absurd) ]
      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?);
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      change with (set_arg_8 ????? = ?)
      @set_arg_8_status_of_pseudo_status try %
      >EQs >EQticks <instr_refl >addr_refl
      [1:
        @sym_eq @set_clock_status_of_pseudo_status
        [1:
          @sym_eq @set_program_counter_status_of_pseudo_status %
        |2:
          @eq_f2 %
        ]
      |2:
        @(subaddressing_mode_elim … acc_a) @I
      |3:
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
        [1:
          @(subaddressing_mode_elim … acc_a) %
        |4:
          @eq_f2
          @(pose … (set_clock ????)) #status #status_refl
          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
          [1:
            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
          |3:
            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
          |2:
            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
          |4:
            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
          ]
        |*:
          %
        ]
      ]
    |2:
      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
      >EQP -P normalize nodelta
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
      [2: normalize nodelta #absurd destruct(absurd) ]
      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?);
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      change with (set_arg_8 ????? = ?)
      @set_arg_8_status_of_pseudo_status try %
      >EQs >EQticks <instr_refl >addr_refl
      [1:
        @sym_eq @set_clock_status_of_pseudo_status
        [1:
          @sym_eq @set_program_counter_status_of_pseudo_status %
        |2:
          @eq_f2 %
        ]
      |2:
        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
        [1: @(subaddressing_mode_elim … direct) #w % ] %
      |3:
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
        [1:
          @(subaddressing_mode_elim … direct) #w %
        |4:
          @eq_f2
          @(pose … (set_clock ????)) #status #status_refl
          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
          [1:
            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
          |3:
            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
          |2:
            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
          |4:
            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
            [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ |*: % ]
          ]
        |*:
          %
        ]
      ]
    ]
  |4,5,6,7,8,9: (* INC and DEC *)
    cases daemon
  |42,44: (* RL and RR *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
    [2,4:
      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
      %
    ]
    @sym_eq @set_clock_status_of_pseudo_status
    [2,4:
      %
    ]
    @sym_eq @set_program_counter_status_of_pseudo_status %
  |43,45: (* RLC and RRC *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
    [2,4:
      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
      @eq_f2
      [1,3:
        @sym_eq
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
      |2,4:
        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
        @sym_eq @set_clock_status_of_pseudo_status %
      ]
    |1,3:
      @sym_eq @set_arg_1_status_of_pseudo_status try %
      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
    ]
  |1,2: (* ADD and ADDC *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    whd in ⊢ (??%?);
    normalize nodelta >EQs >EQticks <instr_refl
    @let_pair_in_status_of_pseudo_status
    [1,3:
      @eq_f3
      [1,2,4,5: 
        @(pose … (set_clock ????)) #status #status_refl
        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
        [1,5:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
          @(subaddressing_mode_elim … addr1) %
        |3,7:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
        |2,6:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
          @(subaddressing_mode_elim … addr1) %
        |4,8:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
          /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/
        ]
      |3: %
      |6:
        @sym_eq @(get_cy_flag_status_of_pseudo_status M')
        @sym_eq @set_clock_status_of_pseudo_status %
      ]
    |2,4:
      #result #flags @sym_eq
      @set_flags_status_of_pseudo_status try %
      @sym_eq @set_arg_8_status_of_pseudo_status try %
      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
    ]
  |3: (* SUB *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    whd in ⊢ (??%?);
    @(pair_replace ?????????? p)
    [1:
      @eq_f3
      normalize nodelta >EQs >EQticks <instr_refl
      [1:
        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
        @(get_arg_8_status_of_pseudo_status cm status … M')
        [1:
          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
        |2:
          >status_refl
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1)
          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
          @(subaddressing_mode_elim … addr1)
        |3:
          >status_refl
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1)
          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
          @(subaddressing_mode_elim … addr1)
        ]
      |2:
        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
        @(get_arg_8_status_of_pseudo_status cm status … M')
        [1:
          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
        |2:
          >status_refl
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2)
          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
          cases daemon (* XXX: ??? *)
        |3:
          >status_refl
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2)
          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          lapply addressing_mode_ok_assm_1 whd in match addressing_mode_ok; normalize nodelta
          cases daemon (* XXX: ??? *)
        ]
      |3:
        @(get_cy_flag_status_of_pseudo_status … M')
        @sym_eq @set_clock_status_of_pseudo_status
        [1:
          @sym_eq @set_program_counter_status_of_pseudo_status %
        |2:
          %
        ]
      ]
    |2:
      normalize nodelta
      @(pair_replace ?????????? p)
      [1:
        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
      |2:
        @set_flags_status_of_pseudo_status try %
        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
        [1:
          @sym_eq @set_clock_status_of_pseudo_status %
        |2:
          @I
        |3:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A)
          [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          whd in ⊢ (??%?);
          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
        ]
      ]
    ]
  |10: (* MUL *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
    [2:
      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
      @sym_eq
      [1:
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
        %
      |2:
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
      ]
    ]
    @sym_eq @set_8051_sfr_status_of_pseudo_status
    [2:
      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
      @eq_f @eq_f2 try % @eq_f2 @eq_f
      @sym_eq
      [1:
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
      |2:
        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
      ]
    ]
    @sym_eq @set_clock_status_of_pseudo_status
    [2:
      @eq_f %
    ]
    @sym_eq @set_program_counter_status_of_pseudo_status %
  |11,12: (* DIV *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    whd in ⊢ (??%?); normalize nodelta
    cases daemon (* XXX: need match_nat_replace but is not working! *)
  |13: (* DA *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    @(pair_replace ?????????? p)
    [1:
      @eq_f normalize nodelta >EQs >EQticks <instr_refl
      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    |2:
      @(pair_replace ?????????? p)
      [1:
        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
      |2:
        @(if_then_else_replace ???????? p1) normalize nodelta
        [1:
          cases (gtb ? 9)
          [1:
            %
          |2:
            change with (get_ac_flag ??? = get_ac_flag ???)
            @(get_ac_flag_status_of_pseudo_status M')
            @sym_eq @set_clock_status_of_pseudo_status
            >EQs >EQticks <instr_refl %
          ]
        |2:
          @(if_then_else_replace ???????? p1) normalize nodelta try %
          @(pair_replace ?????????? p2)
          [1:
            @eq_f3 try % normalize nodelta
            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
            whd in ⊢ (??%?);
            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
          |2:
            @(pair_replace ?????????? p2) try %
            @(pair_replace ?????????? p3) try %
            @(pair_replace ?????????? p3) try %
            @(if_then_else_replace ???????? p4) try % normalize nodelta
            @(if_then_else_replace ???????? p4) try % normalize nodelta
            @(pair_replace ?????????? p5) try %
            @(pair_replace ?????????? p5) try %
            @set_flags_status_of_pseudo_status try %
            [1:
              @eq_f @(get_ac_flag_status_of_pseudo_status M')
              @sym_eq @set_8051_sfr_status_of_pseudo_status
              [1:
                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
              |2:
                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
              ]
            |2:
              @(get_ov_flag_status_of_pseudo_status M')
              @sym_eq @set_8051_sfr_status_of_pseudo_status
              [1:
                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
              |2:
                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
              ]
            |3:
              @sym_eq @set_8051_sfr_status_of_pseudo_status
              [1:
                @sym_eq @set_clock_status_of_pseudo_status
                [1:
                  >EQs
                  @sym_eq @set_program_counter_status_of_pseudo_status %
                |2:
                  >EQs >EQticks <instr_refl %
                ]
              |2:
                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
              ]
            ]
          ]
        ]
      ]
    ]
  |14: (* DA *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    @(pair_replace ?????????? p)
    [1:
      @eq_f normalize nodelta >EQs >EQticks <instr_refl
      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    |2:
      @(pair_replace ?????????? p)
      [1:
        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
      |2:
        @(if_then_else_replace ???????? p1) normalize nodelta
        [1:
          cases (gtb ? 9)
          [1:
            %
          |2:
            change with (get_ac_flag ??? = get_ac_flag ???)
            @(get_ac_flag_status_of_pseudo_status M')
            @sym_eq @set_clock_status_of_pseudo_status
            >EQs >EQticks <instr_refl %
          ]
        |2:
          @(if_then_else_replace ???????? p1) normalize nodelta try %
          @(pair_replace ?????????? p2)
          [1:
            @eq_f3 try % normalize nodelta
            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
            whd in ⊢ (??%?);
            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
          |2:
            @(pair_replace ?????????? p2) try %
            @(pair_replace ?????????? p3) try %
            @(pair_replace ?????????? p3) try %
            @(if_then_else_replace ???????? p4) try % normalize nodelta
            @(if_then_else_replace ???????? p4) try % normalize nodelta
            @set_clock_status_of_pseudo_status
            [1:
              >EQs
              @sym_eq @set_program_counter_status_of_pseudo_status %
            |2:
              >EQs >EQticks <instr_refl %
            ]
          ]
        ]
      ]
    ]
  |15: (* DA *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    @(pair_replace ?????????? p)
    [1:
      @eq_f normalize nodelta >EQs >EQticks <instr_refl
      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    |2:
      @(pair_replace ?????????? p)
      [1:
        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
      |2:
        @(if_then_else_replace ???????? p1) normalize nodelta
        [1:
          cases (gtb ? 9)
          [1:
            %
          |2:
            change with (get_ac_flag ??? = get_ac_flag ???)
            @(get_ac_flag_status_of_pseudo_status M')
            @sym_eq @set_clock_status_of_pseudo_status
            >EQs >EQticks <instr_refl %
          ]
        |2:
          @(if_then_else_replace ???????? p1) normalize nodelta try %
          @set_clock_status_of_pseudo_status
          [1:
            >EQs
            @sym_eq @set_program_counter_status_of_pseudo_status %
          |2:
            >EQs >EQticks <instr_refl %
          ]
        ]
      ]
    ]
  |36: (* CLR *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    normalize nodelta #subaddressing_modein_witness
    @set_arg_8_status_of_pseudo_status try %
    [1:
      @sym_eq @set_clock_status_of_pseudo_status
      >EQs >EQticks <instr_refl %
    |2:
      whd in ⊢ (??%?);
      >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
      [2: <EQaddr % ] %
    ]
  |37: (* CLR *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    normalize nodelta #subaddressing_modein_witness
    @set_arg_1_status_of_pseudo_status try %
    @sym_eq @set_clock_status_of_pseudo_status
    >EQs >EQticks <instr_refl %
  |38: (* CLR *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    normalize nodelta #subaddressing_modein_witness
    @set_arg_1_status_of_pseudo_status try %
    [1:
      @sym_eq @set_clock_status_of_pseudo_status
      >EQs >EQticks <instr_refl %
    |*:
      (* XXX: ??? *)
      cases daemon
    ]
  |39: (* CPL *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    normalize nodelta #subaddressing_modein_witness
    @set_8051_sfr_status_of_pseudo_status
    [1:
      @sym_eq @set_clock_status_of_pseudo_status
      >EQs >EQticks <instr_refl %
    |2:
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data M' cm … addr addressing_mode_ok_assm_1)
      [2: <EQaddr % ] normalize nodelta @eq_f
      @(pose … (set_clock ????)) #status #status_refl
      @sym_eq @(get_8051_sfr_status_of_pseudo_status M' … status) >status_refl
      >EQs >EQticks <instr_refl try %
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addr addressing_mode_ok_assm_1)
      [2: <EQaddr % ] %
    ]
  |40: (* CPL *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    normalize nodelta #subaddressing_modein_witness
    @set_arg_1_status_of_pseudo_status try %
    [1:
      @eq_f @(get_arg_1_status_of_pseudo_status … M') try %
      @sym_eq @set_clock_status_of_pseudo_status
      >EQs >EQticks <instr_refl <EQaddr %
    |2:
      @sym_eq @set_clock_status_of_pseudo_status
      >EQs >EQticks <instr_refl <EQaddr %
    ]
  |41: (* CPL *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta
    generalize in match (subaddressing_modein ?? addr); <EQaddr in ⊢ (? → %);
    normalize nodelta #subaddressing_modein_witness
    @set_arg_1_status_of_pseudo_status
    [1:
      @eq_f
      @(pose … (set_clock ????)) #status #status_refl
      @(get_arg_1_status_of_pseudo_status … M' … status) try % >status_refl
      >EQs >EQticks <instr_refl <EQaddr
      [1:
        @sym_eq @set_clock_status_of_pseudo_status %
      |2:
        (* XXX: ??? *)
        cases daemon
      ]
    |2:
      @sym_eq @set_clock_status_of_pseudo_status
      >EQs >EQticks <instr_refl <EQaddr %
    |*:
      (* XXX: same as above, provable but tedious *)
      cases daemon
    ]
  |33: (* (* ANL *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta lapply instr_refl
    inversion addr
    [1:
      #addr' #addr_refl'
      inversion addr'
      #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
      whd in ⊢ (??%? → ?); normalize nodelta cases addr
      [1:
        #acc_a #others normalize nodelta
        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
        [2: normalize nodelta #absurd destruct(absurd) ]
        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
        [2: normalize nodelta #absurd destruct(absurd) ]
        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
        whd in ⊢ (??%?);
        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
        whd in ⊢ (??%?); normalize nodelta
        inversion addr #addr1 #addr2
        @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … acc_a)
        @(subaddressing_mode_elim … addr2)
        @set_arg_8_status_of_pseudo_status #addr_refl normalize nodelta try %
        [1:
          @sym_eq @set_clock_status_of_pseudo_status
          >EQs >EQticks <addr_refl <instr_refl
          [1:
            @sym_eq @set_program_counter_status_of_pseudo_status %
          |2:
            @eq_f2
            [1:
              >addr_refl @(subaddressing_mode_elim … addr1) %
            |2:
              @(clock_status_of_pseudo_status M')
              @sym_eq @set_program_counter_status_of_pseudo_status %
            ]
          ]
        |2:
          cases daemon (* XXX: matita dies here *)
        ]
      |2:
        #direct #others
        @pair_elim #direct' #others' #direct_others_refl' destruct(direct_others_refl') normalize nodelta
        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
        [2: normalize nodelta #absurd destruct(absurd) ]
        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
        [2: normalize nodelta #absurd destruct(absurd) ]
        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
        whd in ⊢ (??%?);
        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
        whd in ⊢ (??%?); normalize nodelta
        inversion addr #addr1 #addr2
        @(subaddressing_mode_elim … addr1) @(subaddressing_mode_elim … addr2)
        [1: #w |2: #w1 #w2 ] #addr_refl normalize nodelta
        @set_arg_8_status_of_pseudo_status
      ]
    |2:
      -addr #addr #instr_refl #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} lapply maps_assm
      whd in ⊢ (??%? → ?); normalize nodelta cases addr #carry #others normalize nodelta
      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
      [2: normalize nodelta #absurd destruct(absurd) ]
      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?);
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      whd in ⊢ (??%?); normalize nodelta
      inversion addr #addr1 #addr2 #addr_refl normalize nodelta
      @set_flags_status_of_pseudo_status try %
      [1:
        @conjunction_split
        [1:
          @(get_cy_flag_status_of_pseudo_status M')
          @sym_eq @set_clock_status_of_pseudo_status
          >EQs >EQticks <addr_refl <instr_refl %
        |2:
          >EQs >EQticks <addr_refl <instr_refl normalize nodelta
          (* XXX: can't get get_arg_1_status_of_pseudo_status to apply *)
          cases daemon
        ]
      |2:
        @(get_ov_flag_status_of_pseudo_status M')
        @sym_eq @set_clock_status_of_pseudo_status
        >EQs >EQticks <instr_refl <addr_refl %
      |3:
        @sym_eq @set_clock_status_of_pseudo_status
        >EQs >EQticks <instr_refl <addr_refl %
      ]
    ]
    whd in maps_assm:(??%%);
    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?); normalize nodelta *)
  |16: (* JC *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm
    whd in match expand_pseudo_instruction; normalize nodelta
    whd in match expand_relative_jump; normalize nodelta
    whd in match expand_relative_jump_internal; normalize nodelta
    @pair_elim #sj_possible #disp #sj_possible_disp_refl normalize nodelta
    inversion sj_possible #sj_possible_refl
    [1:
      #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?); normalize nodelta 
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      whd in ⊢ (??%?); normalize nodelta
      @(if_then_else_replace ???????? p) normalize nodelta
      [1:
        >EQs @(get_cy_flag_status_of_pseudo_status M')
        @sym_eq @set_program_counter_status_of_pseudo_status %
      |2:
        @(if_then_else_replace ???????? p) normalize nodelta try %
        >EQs >EQticks <instr_refl
        @set_program_counter_status_of_pseudo_status
        [1:
          >EQaddr_of normalize nodelta
          whd in match addr_of_relative; normalize nodelta
          whd in match (program_counter ???);
          check address_of_word_labels_code_mem_Some_hit
          >EQlookup_labels
          
          >sigma_increment_commutation
          whd in match assembly_1_pseudoinstruction; normalize nodelta
          whd in match expand_pseudo_instruction; normalize nodelta
          whd in match expand_relative_jump; normalize nodelta
          whd in match expand_relative_jump_internal; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl normalize nodelta normalize in match (length ??);
            lapply sigma_increment_commutation
            whd in match assembly_1_pseudoinstruction; normalize nodelta
            whd in match (length ??); normalize nodelta
            cases daemon
            (* XXX: missing invariant? *)
          ]
        |2:
          @sym_eq @set_clock_status_of_pseudo_status try %
          @eq_f2 try % whd in ⊢ (??%%);
          whd in match ticks_of0; normalize nodelta lapply sigma_increment_commutation
          whd in match assembly_1_pseudoinstruction; normalize nodelta
          whd in match expand_pseudo_instruction; normalize nodelta
          whd in match expand_relative_jump; normalize nodelta
          whd in match expand_relative_jump_internal; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            @eq_f2 try % >EQppc %
          |2:
            @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
            [1:
              @eq_f2 try % (* XXX: finish, use Jaap's invariant *)
              cases daemon
            |2:
              #_ >sj_possible_refl %
            ]
          ]
        ]
      ]
    |2:
      normalize nodelta >EQppc
      * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
      * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
      * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
      #fetch_many_assm whd in fetch_many_assm; %{2}
      change with (execute_1 ?? = ?)
      @(pose … (execute_1 ? (status_of_pseudo_status …)))
      #status_after_1 #EQstatus_after_1
      cases daemon (* XXX: ??? *)
    ]
  ] 
qed.

(*
  (* XXX: work on the left hand side *)
  (* XXX: switch to the right hand side *)
  normalize nodelta >EQs -s >EQticks -ticks
  whd in ⊢ (??%%);
  (* XXX: finally, prove the equality using sigma commutation *)
  cases daemon
  |11,12: (* DIV *)
  (* XXX: work on the right hand side *)
  normalize nodelta in p;
  >p normalize nodelta
  (* XXX: switch to the left hand side *)
  -instr_refl >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
  whd in ⊢ (??%?);
  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
  >(?: pose_assm = 0) normalize nodelta
  [2,4:
    <p >pose_refl
    cases daemon
  |1,3:
    (* XXX: switch to the right hand side *)
    >EQs -s >EQticks -ticks
    whd in ⊢ (??%%);
    (* XXX: finally, prove the equality using sigma commutation *)
    @split_eq_status try %
    cases daemon
  ]
  |13,14,15: (* DA *)
  (* XXX: work on the right hand side *)
  >p normalize nodelta
  >p1 normalize nodelta
  try (>p2 normalize nodelta
  try (>p3 normalize nodelta
  try (>p4 normalize nodelta
  try (>p5 normalize nodelta))))
  (* XXX: switch to the left hand side *)
  -instr_refl >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
  whd in ⊢ (??%?);
  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
  (* XXX: work on the left hand side *)
  @(pair_replace ?????????? p)
  [1,3,5:
    /demod/
    cases daemon
  |2,4,6:
    @(if_then_else_replace ???????? p1)
    [1,3,5:
      cases daemon
    |2,4:
      normalize nodelta
      @(pair_replace ?????????? p2)
      [1,3:
        cases daemon
      |2,4:
        normalize nodelta >p3 normalize nodelta
        >p4 normalize nodelta try >p5
      ]
    ]
  (* XXX: switch to the right hand side *)
  normalize nodelta >EQs -s >EQticks -ticks
  whd in ⊢ (??%%);
  (* XXX: finally, prove the equality using sigma commutation *)
  @split_eq_status try %
  cases daemon
  ]
  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
  (* XXX: work on the right hand side *)
  cases addr #addr' normalize nodelta
  [1,3:
    cases addr' #addr'' normalize nodelta
  ]
  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
  (* XXX: switch to the left hand side *)
  -instr_refl >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
  whd in ⊢ (??%?);
  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
  (* XXX: work on the left hand side *)
  (* XXX: switch to the right hand side *)
  normalize nodelta >EQs -s >EQticks -ticks
  whd in ⊢ (??%%);
  (* XXX: finally, prove the equality using sigma commutation *)
  cases daemon
  |47: (* MOV *)
  (* XXX: work on the right hand side *)
  cases addr -addr #addr normalize nodelta
  [1:
    cases addr #addr normalize nodelta
    [1:
      cases addr #addr normalize nodelta
      [1:
        cases addr #addr normalize nodelta
        [1:
          cases addr #addr normalize nodelta
        ]
      ]
    ]
  ]
  cases addr #lft #rgt normalize nodelta
  (* XXX: switch to the left hand side *)
  >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
  whd in ⊢ (??%?);
  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
  (* XXX: work on the left hand side *)
  (* XXX: switch to the right hand side *)
  normalize nodelta >EQs -s >EQticks -ticks
  whd in ⊢ (??%%);
  (* XXX: finally, prove the equality using sigma commutation *)
  cases daemon
  ]
*)


(*  [31,32: (* DJNZ *)
  (* XXX: work on the right hand side *)
  >p normalize nodelta >p1 normalize nodelta
  (* XXX: switch to the left hand side *)
  >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm
  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
  <EQppc in fetch_many_assm;
  whd in match (short_jump_cond ??);
  @pair_elim #sj_possible #disp
  @pair_elim #result #flags #sub16_refl
  @pair_elim #upper #lower #vsplit_refl
  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
  #sj_possible_pair destruct(sj_possible_pair)
  >p1 normalize nodelta
  [1,3:
    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    lapply maps_assm whd in ⊢ (??%? → ?);
    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
    (* XXX: work on the left hand side *)
    @(pair_replace ?????????? p) normalize nodelta
    [1,3:
      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
      >(get_arg_8_set_program_counter … true addr1)
      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
      @get_arg_8_pseudo_addressing_mode_ok assumption
    |2,4:
      >p1 normalize nodelta >EQs
      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
      >set_program_counter_status_of_pseudo_status
       whd in ⊢ (??%%);
      @split_eq_status
      [1,10:
        whd in ⊢ (??%%); >set_arg_8_set_program_counter
        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
        >low_internal_ram_set_program_counter
        [1:
          >low_internal_ram_set_program_counter
          (* XXX: ??? *)
        |2:
          >low_internal_ram_set_clock
          (* XXX: ??? *)
        ]
      |2,11:
        whd in ⊢ (??%%); >set_arg_8_set_program_counter
        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
        >high_internal_ram_set_program_counter
        [1:
          >high_internal_ram_set_program_counter
          (* XXX: ??? *)
        |2:
          >high_internal_ram_set_clock
          (* XXX: ??? *)
        ]
      |3,12:
        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
        >(external_ram_set_arg_8 ??? addr1)
        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
      |4,13:
        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
        [1:
          >program_counter_set_program_counter
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >set_clock_set_program_counter >program_counter_set_program_counter
          change with (add ??? = ?)
          (* XXX: ??? *)
        |2:
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >program_counter_set_program_counter
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >set_clock_set_program_counter >program_counter_set_program_counter
          >sigma_increment_commutation <EQppc
          whd in match (assembly_1_pseudoinstruction ??????);
          whd in match (expand_pseudo_instruction ??????);
          (* XXX: ??? *)
        ]
      |5,14:
        whd in match (special_function_registers_8051 ???);
        [1:
          >special_function_registers_8051_set_program_counter
          >special_function_registers_8051_set_clock
          >set_arg_8_set_program_counter in ⊢ (???%);
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >special_function_registers_8051_set_program_counter
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >special_function_registers_8051_set_program_counter
          @special_function_registers_8051_set_arg_8 assumption
        |2:
          >special_function_registers_8051_set_clock
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >special_function_registers_8051_set_program_counter
          >special_function_registers_8051_set_program_counter
          @special_function_registers_8051_set_arg_8 assumption
        ]
      |6,15:
        whd in match (special_function_registers_8052 ???);
        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
        [1:
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >set_arg_8_set_program_counter
          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
          >special_function_registers_8052_set_program_counter
          >special_function_registers_8052_set_program_counter
          @special_function_registers_8052_set_arg_8 assumption
        |2:
          whd in ⊢ (??%%);
          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
        ]
        (* XXX: we need special_function_registers_8052_set_arg_8 *)
      |7,16:
        whd in match (p1_latch ???);
        whd in match (p1_latch ???) in ⊢ (???%);
        (* XXX: we need p1_latch_8052_set_arg_8 *)
      |8,17:
        whd in match (p3_latch ???);
        whd in match (p3_latch ???) in ⊢ (???%);
        (* XXX: we need p3_latch_8052_set_arg_8 *)
      |9:
        >clock_set_clock
        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
        >EQticks <instr_refl @eq_f2
        [1:
          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
        |2:
          (* XXX: we need clock_set_arg_8 *)
        ]
      |18:
      ]
    ]
    (* XXX: switch to the right hand side *)
    normalize nodelta >EQs -s >EQticks -ticks
    cases (¬ eq_bv ???) normalize nodelta
    whd in ⊢ (??%%);
    (* XXX: finally, prove the equality using sigma commutation *)
    @split_eq_status try %
    [1,2,3,19,20,21,28,29,30:
      cases daemon (* XXX: axioms as above *)
    |4,13,22,31:
    |5,14,23,32:
    |6,15,24,33:
    |7,16,25,34:
    |8,17,26,35:
      whd in ⊢ (??%%);maps_assm
      
    |9,18,27,36:
      whd in ⊢ (??%%);
      whd in match (ticks_of_instruction ?); <instr_refl
      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
    ]
  |2,4:
    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
    [2, 4:
      cases daemon (* XXX: !!! *)
    ]
    normalize nodelta >EQppc
    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    #fetch_many_assm whd in fetch_many_assm; %{2}
    change with (execute_1 ?? = ?)
    @(pose … (execute_1 ? (status_of_pseudo_status …)))
    #status_after_1 #EQstatus_after_1
    <(?: ? = status_after_1)
    [3,6:
      >EQstatus_after_1 in ⊢ (???%);
      whd in ⊢ (???%);
      [1:
        <fetch_refl in ⊢ (???%);
      |2:
        <fetch_refl in ⊢ (???%);
      ]
      whd in ⊢ (???%);
      @(pair_replace ?????????? p)
      [1,3:
        cases daemon
      |2,4:
        normalize nodelta
        whd in match (addr_of_relative ????);
        cases (¬ eq_bv ???) normalize nodelta
        >set_clock_mk_Status_commutation
        whd in ⊢ (???%);
        change with (add ???) in match (\snd (half_add ???));
        >set_arg_8_set_program_counter in ⊢ (???%);
        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
        >program_counter_set_program_counter in ⊢ (???%);
        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
        [2,4,6,8:
          >bitvector_of_nat_sign_extension_equivalence
          [1,3,5,7:
            >EQintermediate_pc' %
          |*:
            repeat @le_S_S @le_O_n
          ]
        ]
        [1,3: % ]
      ]
    |1,4:
      skip
    ]
    [3,4:
      -status_after_1
      @(pose … (execute_1 ? (mk_PreStatus …)))
      #status_after_1 #EQstatus_after_1
      <(?: ? = status_after_1)
      [3,6:
        >EQstatus_after_1 in ⊢ (???%);
        whd in ⊢ (???%);
        (* XXX: matita bug with patterns across multiple goals *)
        [1:
          <fetch_refl'' in ⊢ (???%);
        |2:
          <fetch_refl'' in ⊢ (???%);
        ]
        [2: % |1: whd in ⊢ (???%); % ]
      |1,4:
        skip
      ]
      -status_after_1 whd in ⊢ (??%?);
      (* XXX: switch to the right hand side *)
      normalize nodelta >EQs -s >EQticks -ticks
      normalize nodelta whd in ⊢ (??%%);
    ]
    (* XXX: finally, prove the equality using sigma commutation *)
    @split_eq_status try %
    whd in ⊢ (??%%);
    cases daemon
  ]
  |30: (* CJNE *)
  (* XXX: work on the right hand side *)
  cases addr1 -addr1 #addr1 normalize nodelta
  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
  (* XXX: switch to the left hand side *)
  >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm

  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
  <EQppc in fetch_many_assm;
  whd in match (short_jump_cond ??);
  @pair_elim #sj_possible #disp
  @pair_elim #result #flags #sub16_refl
  @pair_elim #upper #lower #vsplit_refl
  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
  [1,3:
    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
    @(if_then_else_replace ???????? eq_bv_refl)
    [1,3,5,7:
      cases daemon
    |2,4,6,8:
      (* XXX: switch to the right hand side *)
      normalize nodelta >EQs -s >EQticks -ticks
      whd in ⊢ (??%%);
      (* XXX: finally, prove the equality using sigma commutation *)
      @split_eq_status try %
      [3,7,11,15:
        whd in ⊢ (??%?);
        [1,3:
          cases daemon
        |2,4:
          cases daemon
        ]
      ]
      cases daemon (* XXX *)
    ]
  |2,4:
    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
    [2, 4:
      cases daemon (* XXX: !!! *)
    ]
    normalize nodelta >EQppc
    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    #fetch_many_assm whd in fetch_many_assm; %{2}
    change with (execute_1 ?? = ?)
    @(pose … (execute_1 ? (status_of_pseudo_status …)))
    #status_after_1 #EQstatus_after_1
    <(?: ? = status_after_1)
    [2,5:
      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
    |3,6:
      >EQstatus_after_1 in ⊢ (???%);
      whd in ⊢ (???%);
      [1: <fetch_refl in ⊢ (???%);
      |2: <fetch_refl in ⊢ (???%);
      ]
      whd in ⊢ (???%);
      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
      whd in ⊢ (???%);
      whd in match (addr_of_relative ????);
      change with (add ???) in match (\snd (half_add ???));
      >set_clock_set_program_counter in ⊢ (???%);
      >program_counter_set_program_counter in ⊢ (???%);
      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
      [2,4,6,8:
        >bitvector_of_nat_sign_extension_equivalence
        [1,3,5,7:
          >EQintermediate_pc' %
        |*:
          repeat @le_S_S @le_O_n
        ]
      |1,5:
        %
      ]
    |1,4: skip
    ]
    [1,2,3,4:
      -status_after_1
      @(pose … (execute_1 ? (mk_PreStatus …)))
      #status_after_1 #EQstatus_after_1
      <(?: ? = status_after_1)
      [3,6,9,12:
        >EQstatus_after_1 in ⊢ (???%);
        whd in ⊢ (???%);
        (* XXX: matita bug with patterns across multiple goals *)
        [1: <fetch_refl'' in ⊢ (???%);
        |2: <fetch_refl'' in ⊢ (???%);
        |3: <fetch_refl'' in ⊢ (???%);
        |4: <fetch_refl'' in ⊢ (???%);
        ] %
      |1,4,7,10:
        skip
      ]
      -status_after_1 whd in ⊢ (??%?);
      (* XXX: switch to the right hand side *)
      normalize nodelta >EQs -s >EQticks -ticks
      whd in ⊢ (??%%);
    ]
    (* XXX: finally, prove the equality using sigma commutation *)
    @split_eq_status try %
    cases daemon
  ]
  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
  (* XXX: work on the right hand side *)
  >p normalize nodelta
  (* XXX: switch to the left hand side *)
  >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm
  
  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
  <EQppc in fetch_many_assm;
  whd in match (short_jump_cond ??);
  @pair_elim #sj_possible #disp
  @pair_elim #result #flags #sub16_refl
  @pair_elim #upper #lower #vsplit_refl
  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    (* XXX: work on the left hand side *)
    @(if_then_else_replace ???????? p) normalize nodelta
    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
      cases daemon
    ]
    (* XXX: switch to the right hand side *)
    normalize nodelta >EQs -s >EQticks -ticks
    whd in ⊢ (??%%);
    (* XXX: finally, prove the equality using sigma commutation *)
    @split_eq_status try %
    cases daemon
  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
      cases daemon (* XXX: !!! *)
    ]
    normalize nodelta >EQppc
    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    #fetch_many_assm whd in fetch_many_assm; %{2}
    change with (execute_1 ?? = ?)
    @(pose … (execute_1 ? (status_of_pseudo_status …)))
    #status_after_1 #EQstatus_after_1
    <(?: ? = status_after_1)
    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
      >EQstatus_after_1 in ⊢ (???%);
      whd in ⊢ (???%);
      [1: <fetch_refl in ⊢ (???%);
      |2: <fetch_refl in ⊢ (???%);
      |3: <fetch_refl in ⊢ (???%);
      |4: <fetch_refl in ⊢ (???%);
      |5: <fetch_refl in ⊢ (???%);
      |6: <fetch_refl in ⊢ (???%);
      |7: <fetch_refl in ⊢ (???%);
      |8: <fetch_refl in ⊢ (???%);
      |9: <fetch_refl in ⊢ (???%);
      |10: <fetch_refl in ⊢ (???%);
      |11: <fetch_refl in ⊢ (???%);
      |12: <fetch_refl in ⊢ (???%);
      |13: <fetch_refl in ⊢ (???%);
      |14: <fetch_refl in ⊢ (???%);
      ]
      whd in ⊢ (???%);
      @(if_then_else_replace ???????? p)
      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
        cases daemon
      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
        normalize nodelta
        whd in match (addr_of_relative ????);
        >set_clock_mk_Status_commutation
        [9,10:
          (* XXX: demodulation not working in this case *)
          >program_counter_set_arg_1 in ⊢ (???%);
          >program_counter_set_program_counter in ⊢ (???%);
        |*:
          /demod/
        ]
        whd in ⊢ (???%);
        change with (add ???) in match (\snd (half_add ???));
        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
          >bitvector_of_nat_sign_extension_equivalence
          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
            >EQintermediate_pc' %
          |*:
            repeat @le_S_S @le_O_n
          ]
        ]
        %
      ]
    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
      skip
    ]
    -status_after_1
    @(pose … (execute_1 ? (mk_PreStatus …)))
    #status_after_1 #EQstatus_after_1
    <(?: ? = status_after_1)
    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
      >EQstatus_after_1 in ⊢ (???%);
      whd in ⊢ (???%);
      (* XXX: matita bug with patterns across multiple goals *)
      [1: <fetch_refl'' in ⊢ (???%);
      |2: <fetch_refl' in ⊢ (???%);
      |3: <fetch_refl'' in ⊢ (???%);
      |4: <fetch_refl' in ⊢ (???%);
      |5: <fetch_refl'' in ⊢ (???%);
      |6: <fetch_refl' in ⊢ (???%);
      |7: <fetch_refl'' in ⊢ (???%);
      |8: <fetch_refl' in ⊢ (???%);
      |9: <fetch_refl'' in ⊢ (???%);
      |10: <fetch_refl' in ⊢ (???%);
      |11: <fetch_refl'' in ⊢ (???%);
      |12: <fetch_refl' in ⊢ (???%);
      |13: <fetch_refl'' in ⊢ (???%);
      |14: <fetch_refl' in ⊢ (???%);
      ]
      whd in ⊢ (???%);
      [9,10:
      |*:
        /demod/
      ] %
    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
      skip
    ]
    -status_after_1 whd in ⊢ (??%?);
    (* XXX: switch to the right hand side *)
    normalize nodelta >EQs -s >EQticks -ticks
    whd in ⊢ (??%%);
    (* XXX: finally, prove the equality using sigma commutation *)
    @split_eq_status try %
    [3,11,19,27,36,53,61:
      >program_counter_set_program_counter >set_clock_mk_Status_commutation
      [5: >program_counter_set_program_counter ]
      >EQaddr_of normalize nodelta
      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
      >create_label_cost_refl normalize nodelta #relevant @relevant
      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
      try assumption whd in match instruction_has_label; normalize nodelta
      <instr_refl normalize nodelta %
    |7,15,23,31,45,57,65:
      >set_clock_mk_Status_commutation >program_counter_set_program_counter
      whd in ⊢ (??%?); normalize nodelta
      >EQppc in fetch_many_assm; #fetch_many_assm
      [5:
        >program_counter_set_arg_1 >program_counter_set_program_counter
      ]
      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
      <bitvector_of_nat_sign_extension_equivalence
      [1,3,5,7,9,11,13:
        whd in ⊢ (???%); cases (half_add ???) normalize //
      |2,4,6,8,10,12,14:
        @assembly1_lt_128
        @le_S_S @le_O_n
      ]
    |*:
      cases daemon
    ]
  ]
  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
  (* XXX: work on the right hand side *)
  lapply (subaddressing_modein ???)
  <EQaddr normalize nodelta #irrelevant
  try (>p normalize nodelta)
  try (>p1 normalize nodelta)
  (* XXX: switch to the left hand side *)
  >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
  whd in ⊢ (??%?);
  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
  (* XXX: work on the left hand side *)
  [1,2,3,4,5:
    generalize in ⊢ (??(???(?%))?);
  |6,7,8,9,10,11:
    generalize in ⊢ (??(???(?%))?);
  |12:
    generalize in ⊢ (??(???(?%))?); 
  ]
  <EQaddr normalize nodelta #irrelevant
  try @(jmpair_as_replace ?????????? p)
  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
  (* XXX: switch to the right hand side *)
  normalize nodelta >EQs -s >EQticks -ticks
  whd in ⊢ (??%%);
  (* XXX: finally, prove the equality using sigma commutation *)
  try @split_eq_status try % whd in ⊢ (??%%);
  cases daemon
  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
  (* XXX: work on the right hand side *)
  >p normalize nodelta
  try (>p1 normalize nodelta)
  (* XXX: switch to the left hand side *)
  -instr_refl >EQP -P normalize nodelta
  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
  whd in ⊢ (??%?);
  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
  (* XXX: work on the left hand side *)
  @(pair_replace ?????????? p)
  [1,3,5,7,9,11,13,15,17:
    >set_clock_set_program_counter >set_clock_mk_Status_commutation
    >set_program_counter_mk_Status_commutation >clock_set_program_counter
    cases daemon
  |14,16,18:
    normalize nodelta
    @(pair_replace ?????????? p1)
    [1,3,5:
      >set_clock_mk_Status_commutation
      cases daemon
    ]
  ]
  (* XXX: switch to the right hand side *)
  normalize nodelta >EQs -s >EQticks -ticks
  whd in ⊢ (??%%);
  (* XXX: finally, prove the equality using sigma commutation *)
  try @split_eq_status try %
  cases daemon *)