source: src/ASM/AssemblyProofSplit.ma @ 2593

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".
(*include "ASM/Test2.ma".*)

(*CSC: move elsewhere*)
lemma not_b_c_to_b_not_c:
  ∀b, c: bool.
    (¬b) = c → b = (¬c).
  //
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.

(*CSC: move elsewhere*)
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 →
    (∀n. status_of_pseudo_status M cm (s''' n) sigma policy = s'' n) →
      match n with [ O ⇒ s | S n' ⇒ s'' n' ] =
        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' n'']) sigma policy.
  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
  #n_refl #s_refl #s_refl' <n_refl <s_refl
  cases n normalize nodelta try % #n' <(s_refl' n') %
qed.

lemma get_arg_8_status_of_pseudo_status':
  ∀cm,ps,l.
  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
  ∀M. ∀sigma. ∀policy. ∀s.
      s = status_of_pseudo_status M cm ps sigma policy →
      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr)
      = get_arg_8 … ps l addr →
      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
      s l addr = get_arg_8 … ps l addr.
 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
 try assumption %
qed.

lemma short_jump_cond_ok:
  ∀v1, v1', v2, v2': Word.
  ∀is_possible, offset.
    v1 = v1' → v2 = v2' →
    〈is_possible, offset〉 = short_jump_cond v1 v2 →
      is_possible → v2' = add 16 v1' (sign_extension offset).
  #v1 #v1' #v2 #v2' #is_possible #offset #v1_refl #v2_refl <v1_refl <v2_refl
  whd in match short_jump_cond; normalize nodelta
  @pair_elim #result #flags #sub16_refl
  @pair_elim #upper #lower #vsplit_refl
  inversion (get_index' bool ???) #get_index_refl normalize nodelta
  #relevant destruct(relevant) #relevant
  [1:
    @(sub_16_to_add_16_8_1 … flags)
  |2:
    @(sub_16_to_add_16_8_0 … flags)
  ]
  try assumption >sub16_refl
  <(eq_bv_eq … relevant)
  >(vsplit_ok … (sym_eq … vsplit_refl)) %
qed.

lemma set_clock_set_clock:
  ∀M, cm, s, t, t'.
    set_clock M cm (set_clock … cm s t) t' = set_clock … cm s t'.
  #M #cm #s #t #t' %
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 = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)).
  ∀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! *)
  ** #low #high #accA #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 → ? 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 → ? 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 → ? 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 addr ⇒ λ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.
            let s ≝ add_ticks1 s in
            let new_sp ≝ 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 (get_arg_8 … s false 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
  [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 (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    inversion (assert_data ?????) #addressing_mode_ok_assm_2
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
    letin M' ≝ (〈low,high,accA〉)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?);
    normalize nodelta >EQs >EQticks <instr_refl
    @let_pair_in_status_of_pseudo_status
    [1,3:
      @eq_f3
      [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M')
        [3,9:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
          @(subaddressing_mode_elim … addr1) %
        |6,12:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
        |2,8:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
          @(subaddressing_mode_elim … addr1) %
        |5,11:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
        |*: % ]
      |3:
        %
      |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ]
    |2,4:
      #result #flags @set_flags_status_of_pseudo_status try %
      @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: (* SUBB *)
    (* 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 (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    inversion (assert_data ?????) #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 … 〈low, high, accA〉)
        [1:
          >status_refl @set_clock_status_of_pseudo_status %
        |2:
          >status_refl
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
        |3:
          >status_refl
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
        ]
      |2:
        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
        @(get_arg_8_status_of_pseudo_status cm status … 〈low, high, accA〉)
        [1:
          >status_refl @set_clock_status_of_pseudo_status %
        |2:
          >status_refl
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
        |3:
          >status_refl
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
        ]
      |3:
        @(get_cy_flag_status_of_pseudo_status … 〈low, high, accA〉)
        @set_clock_status_of_pseudo_status
        [1:
          @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 %
        @(set_arg_8_status_of_pseudo_status … (refl …))
        [1:
          @set_clock_status_of_pseudo_status %
        |2:
          @I
        |3:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try %
          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
        ]
      ]
    ]
  |4: (* INC *)
    (* XXX: work on the right hand side *)
    (* XXX: switch to the left hand side *)
    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
    @(subaddressing_mode_elim … addr) normalize nodelta
    [1:
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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
      change with (set_arg_8 ??? ACC_A ? = ?)
      [2: @I ]
      @set_arg_8_status_of_pseudo_status try %
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
      @eq_f2 try % @sym_eq
      @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
    |2:
      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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
      change with (set_arg_8 ??? (REGISTER w) ? = ?)
      [2: @I ]
      @set_arg_8_status_of_pseudo_status try %
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1)
      [1: /2 by refl, eq_false_to_notb/ ] try %
      @eq_f2 try % @sym_eq
      @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
    |3:
      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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
      change with (set_arg_8 ??? (DIRECT w) ? = ?)
      [2: /2 by refl, eq_false_to_notb/ ]
      @set_arg_8_status_of_pseudo_status try %
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1)
      [1,2,3: % ]
      @eq_f2 try % @sym_eq
      @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
    |4:
      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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
      change with (set_arg_8 ??? (INDIRECT w) ? = ?)
      [2: /2 by refl, eq_false_to_notb/ ]
      @set_arg_8_status_of_pseudo_status try %
      [1:
        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
      |2:
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) try %
        @eq_f2 try % @sym_eq
        @(get_arg_8_status_of_pseudo_status' … 〈low, high, accA〉) try %
        [1:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
        |2:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
        ]
      ]
    |5:
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?);
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      whd in ⊢ (??%?);
      @let_pair_in_status_of_pseudo_status
      [1:
        @eq_f2 try %
        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
        @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl
        >EQs >EQticks %
      |2:
        #carry #bl @let_pair_in_status_of_pseudo_status
        [1:
          @eq_f3 try %
          @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
          @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl
          >EQs >EQticks %
        |2:
          #carry' #bu @set_8051_sfr_status_of_pseudo_status %
        ]
      ]
    ]
  |5: (* DEC *)
    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
    @(subaddressing_mode_elim … addr) normalize nodelta
    [1:
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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 ⊢ (??%?);
      @let_pair_in_status_of_pseudo_status
      [1:
        @eq_f3 try %
        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
        >EQs >EQticks try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
      |2:
        #result #flags
        @set_arg_8_status_of_pseudo_status try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
      ]
    |2:
      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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 ⊢ (??%?);
      @let_pair_in_status_of_pseudo_status
      [1:
        @eq_f3 try %
        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
        >EQs >EQticks try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
      |2:
        #result #flags
        @set_arg_8_status_of_pseudo_status try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
      ]
    |3:
      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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 ⊢ (??%?);
      @let_pair_in_status_of_pseudo_status
      [1:
        @eq_f3 try %
        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
        >EQs >EQticks try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
      |2:
        #result #flags
        @set_arg_8_status_of_pseudo_status try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
      ]
    |4:
      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) 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 ⊢ (??%?);
      @let_pair_in_status_of_pseudo_status
      [1:
        @eq_f3 try %
        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
        @(get_arg_8_status_of_pseudo_status … status … 〈low, high, accA〉) >status_refl -status_refl
        >EQs >EQticks try %
        [1:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
        |2:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
        ]
      |2:
        #result #flags
        @set_arg_8_status_of_pseudo_status try %
        [1:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
        |2:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
        ]
      ]
    ]
  |6: (* 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 (assert_data ?????) in maps_assm;
    @(subaddressing_mode_elim … addr1) #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    inversion (assert_data ?????) #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 ⊢ (??%?);
        whd in addressing_mode_ok_assm_1:(??%?); cases accA in addressing_mode_ok_assm_1;
        normalize nodelta [2: * #upper_lower #address #absurd destruct(absurd) ] #_ %
      |2:
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
      ]
    ]
    @set_8051_sfr_status_of_pseudo_status
    [2:
      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … ACC_A … addressing_mode_ok_assm_1)
      [2: /2 by refl, eq_false_to_notb/ ]
      @eq_f @eq_f2 try % @eq_f2 @eq_f
      @sym_eq
      [1:
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
        whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
        cases accA in addressing_mode_ok_assm_1;
        normalize nodelta [2: * #upper_lower #address #absurd destruct(absurd) ] #_ %
      |2:
        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
      ]
    ]
    @set_clock_status_of_pseudo_status
    [2:
      @eq_f %
    ]
    @set_program_counter_status_of_pseudo_status %
  |7,8: (* 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 (assert_data ?????) in maps_assm;
    @(subaddressing_mode_elim … addr1) #addressing_mode_ok_assm_1
    [2,4: normalize nodelta #absurd destruct(absurd) ]
    inversion (assert_data ?????) #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
    @(match_nat_status_of_pseudo_status 〈low, high, accA〉 cm sigma policy)
    [1,4:
      @eq_f
      @sym_eq @(pose … (set_clock ????)) #status #status_refl
      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl try %
    |2,5:
      @sym_eq @set_flags_status_of_pseudo_status %
    |3,6:
      #n @sym_eq @set_flags_status_of_pseudo_status try %
      @set_8051_sfr_status_of_pseudo_status
      [1,3:
        @set_8051_sfr_status_of_pseudo_status try %
        whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
        cases accA in addressing_mode_ok_assm_1; normalize nodelta
        [2,4: #address_entry #absurd destruct(absurd) ] #_
        @eq_f @eq_f2 %
      |2,4:
        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
        @(pose … (set_clock ????)) #status #status_refl
        @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low, high, accA〉 … status) >status_refl -status_refl try %
        whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
        cases accA in addressing_mode_ok_assm_1; normalize nodelta
        [2,4: #address_entry #absurd destruct(absurd) ] #_ %
      ]
    ]
  |9: (* 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 (assert_data ?????) in maps_assm;
    @(subaddressing_mode_elim … addr) #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 ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
      cases accA in addressing_mode_ok_assm_1; normalize nodelta
      [2: #address_entry #absurd destruct(absurd) ] #_ %
    |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 〈low, high, accA〉)
            @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 〈low, high, accA〉 … policy … (refl …))
            whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
            cases accA in addressing_mode_ok_assm_1; normalize nodelta
            [2: #address_entry #absurd destruct(absurd) ] #_
            >EQs >EQticks <instr_refl %
          |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_flags_status_of_pseudo_status try %
            [1:
              @eq_f @(get_ac_flag_status_of_pseudo_status 〈low, high, accA〉)
              @set_8051_sfr_status_of_pseudo_status
              [1:
                @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
              |2:
                whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
                cases accA in addressing_mode_ok_assm_1; normalize nodelta
                [2: #address_entry #absurd destruct(absurd) ] #_ %
              ]
            |2:
              @(get_ov_flag_status_of_pseudo_status 〈low, high, accA〉)
              @set_8051_sfr_status_of_pseudo_status
              [1:
                @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
              |2:
                whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
                cases accA in addressing_mode_ok_assm_1; normalize nodelta
                [2: #address_entry #absurd destruct(absurd) ] #_ %
              ]
            |3:
              @set_8051_sfr_status_of_pseudo_status
              [1:
                @set_clock_status_of_pseudo_status
                [1:
                  >EQs @set_program_counter_status_of_pseudo_status %
                |2:
                  >EQs >EQticks <instr_refl %
                ]
              |2:
                whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
                cases accA in addressing_mode_ok_assm_1; normalize nodelta
                [2: #address_entry #absurd destruct(absurd) ] #_ %
              ]
            ]
          ]
        ]
      ]
    ]
  |10: (* 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 (assert_data ?????) in maps_assm;
    @(subaddressing_mode_elim … addr) #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 ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
      cases accA in addressing_mode_ok_assm_1; normalize nodelta
      [2: #address_entry #absurd destruct(absurd) ] #_ %
    |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 〈low, high, accA〉)
            @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 〈low, high, accA〉 … policy … (refl …))
            whd in ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
            cases accA in addressing_mode_ok_assm_1; normalize nodelta
            [2: #address_entry #absurd destruct(absurd) ] #_ >EQs >EQticks <instr_refl %
          |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 @set_program_counter_status_of_pseudo_status %
            |2:
              >EQs >EQticks <instr_refl %
            ]
          ]
        ]
      ]
    ]
  |11: (* 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 (assert_data ?????) in maps_assm;
    @(subaddressing_mode_elim … addr) #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 ⊢ (??%?); whd in addressing_mode_ok_assm_1:(??%?);
      cases accA in addressing_mode_ok_assm_1; normalize nodelta
      [2: #address_entry #absurd destruct(absurd) ] #_ %
    |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 〈low, high, accA〉)
            @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 @set_program_counter_status_of_pseudo_status %
          |2:
            >EQs >EQticks <instr_refl %
          ]
        ]
      ]
    ]
  |12: (* JC *)
    >EQP -P normalize nodelta
    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
    >EQppc in ⊢ (% → ?);
    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    inversion sj_possible #sj_possible_refl normalize nodelta
    [1:
      #sigma_increment_commutation #maps_assm #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 ⊢ (??%?);
      @if_then_else_status_of_pseudo_status
      >EQs >EQticks <instr_refl normalize nodelta
      [1:
        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
      |2:
        @set_program_counter_status_of_pseudo_status
        [1:
          >EQaddr_of normalize nodelta
          whd in match addr_of_relative; normalize nodelta
          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
          [1:
            @sym_eq whd in ⊢ (??%?); >EQppc %
          |2:
            >EQlookup_labels %
          |3:
            >sj_possible_refl @I
          ]
        |2:
          @set_clock_status_of_pseudo_status try %
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      |3:
        @set_clock_status_of_pseudo_status try % @eq_f2 try %
        whd in match ticks_of0; normalize nodelta
        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
        [1:
          >EQppc %
        |2:
          >sj_possible_refl %
        ]
      ]
    |2:
      #sigma_increment_commutation #maps_assm
      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
      change with (execute 1 ?? = ?)
      whd in match execute_1; normalize nodelta
      whd in match execute_1'; normalize nodelta
      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
      whd in match execute_1_preinstruction; normalize nodelta
      @(if_then_else_replace ???????? p) normalize nodelta
      [1:
        >EQs
        whd in match get_cy_flag; normalize nodelta
        >special_function_registers_8051_set_program_counter
        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
        normalize #absurd destruct(absurd)
      |2:
        @(if_then_else_replace ???????? p) normalize nodelta try %
        change with (execute_1 ?? = ?) 
        whd in match execute_1; normalize nodelta
        whd in match execute_1'; normalize nodelta
        >program_counter_set_program_counter
        whd in match addr_of_relative; normalize nodelta
        >set_clock_set_program_counter >program_counter_set_program_counter
        <ljmp_fetch_refl
        change with (set_program_counter ???? = ?)
        >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter
        >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter
        >EQs >EQticks <instr_refl
        >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%);
        @set_program_counter_status_of_pseudo_status
        [1:
          >program_counter_set_program_counter
          whd in match compute_target_of_unconditional_jump; normalize nodelta
          >EQaddr_of normalize nodelta >EQlookup_labels %
        |2:
          >set_clock_set_clock
          @set_clock_status_of_pseudo_status try %
          /demod nohyps/
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      ]
    ]
  |13: (* JC *)
    >EQP -P normalize nodelta
    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
    >EQppc in ⊢ (% → ?);
    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    inversion sj_possible #sj_possible_refl normalize nodelta
    [1:
      #sigma_increment_commutation #maps_assm #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 ⊢ (??%?);
      @if_then_else_status_of_pseudo_status
      >EQs >EQticks <instr_refl normalize nodelta
      [1:
        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
      |2:
        @set_program_counter_status_of_pseudo_status
        [1:
          >EQaddr_of normalize nodelta
          whd in match addr_of_relative; normalize nodelta
          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
          [1:
            @sym_eq whd in ⊢ (??%?); >EQppc %
          |2:
            >EQlookup_labels %
          |3:
            >sj_possible_refl @I
          ]
        |2:
          @set_clock_status_of_pseudo_status try %
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      |3:
        @set_clock_status_of_pseudo_status try % @eq_f2 try %
        whd in match ticks_of0; normalize nodelta
        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
        [1:
          >EQppc %
        |2:
          >sj_possible_refl %
        ]
      ]
    |2:
      #sigma_increment_commutation #maps_assm
      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
      change with (execute 1 ?? = ?)
      whd in match execute_1; normalize nodelta
      whd in match execute_1'; normalize nodelta
      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
      whd in match execute_1_preinstruction; normalize nodelta
      @(if_then_else_replace ???????? p) normalize nodelta
      [1:
        >EQs
        whd in match get_cy_flag; normalize nodelta
        >special_function_registers_8051_set_program_counter
        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
        normalize #absurd destruct(absurd)
      |2:
        @(if_then_else_replace ???????? p) normalize nodelta try %
        change with (execute_1 ?? = ?) 
        whd in match execute_1; normalize nodelta
        whd in match execute_1'; normalize nodelta
        
        >set_clock_set_program_counter
        >program_counter_set_program_counter
        <sjmp_fetch_refl
        change with (set_program_counter ???? = ?)
        >set_clock_set_program_counter >set_clock_set_program_counter
        >set_program_counter_set_program_counter >set_program_counter_set_program_counter
        >EQs >EQticks <instr_refl
        >set_clock_set_program_counter >set_clock_set_clock
        @set_program_counter_status_of_pseudo_status
        [1:
          >program_counter_set_program_counter
          whd in match compute_target_of_unconditional_jump; normalize nodelta
          <(eq_bv_eq … ppc_eq_bv_refl) %
        |2:
          @set_clock_status_of_pseudo_status try % /demod nohyps/
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      ]
    ]
  |14: (* JNC *)
    >EQP -P normalize nodelta
    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
    >EQppc in ⊢ (% → ?);
    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    inversion sj_possible #sj_possible_refl normalize nodelta
    [1:
      #sigma_increment_commutation #maps_assm #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 ⊢ (??%?);
      @if_then_else_status_of_pseudo_status
      >EQs >EQticks <instr_refl normalize nodelta
      [1:
        @eq_f @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
      |2:
        @set_program_counter_status_of_pseudo_status
        [1:
          >EQaddr_of normalize nodelta
          whd in match addr_of_relative; normalize nodelta
          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
          [1:
            @sym_eq whd in ⊢ (??%?); >EQppc %
          |2:
            >EQlookup_labels %
          |3:
            >sj_possible_refl @I
          ]
        |2:
          @set_clock_status_of_pseudo_status try %
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      |3:
        @set_clock_status_of_pseudo_status try % @eq_f2 try %
        whd in match ticks_of0; normalize nodelta
        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
        [1:
          >EQppc %
        |2:
          >sj_possible_refl %
        ]
      ]
    |2:
      #sigma_increment_commutation #maps_assm
      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
      change with (execute 1 ?? = ?)
      whd in match execute_1; normalize nodelta
      whd in match execute_1'; normalize nodelta
      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
      whd in match execute_1_preinstruction; normalize nodelta
      @(if_then_else_replace ???????? p) normalize nodelta
      [1:
        @eq_f >EQs
        whd in match get_cy_flag; normalize nodelta
        >special_function_registers_8051_set_program_counter
        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
        normalize #absurd destruct(absurd)
      |2:
        @(if_then_else_replace ???????? p) normalize nodelta try %
        change with (execute_1 ?? = ?) 
        whd in match execute_1; normalize nodelta
        whd in match execute_1'; normalize nodelta
        >program_counter_set_program_counter
        whd in match addr_of_relative; normalize nodelta
        >set_clock_set_program_counter >program_counter_set_program_counter
        <ljmp_fetch_refl
        change with (set_program_counter ???? = ?)
        >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter
        >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter
        >EQs >EQticks <instr_refl
        >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%);
        @set_program_counter_status_of_pseudo_status
        [1:
          >program_counter_set_program_counter
          whd in match compute_target_of_unconditional_jump; normalize nodelta
          >EQaddr_of normalize nodelta >EQlookup_labels %
        |2:
          >set_clock_set_clock
          @set_clock_status_of_pseudo_status try %
          /demod nohyps/
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      ]
    ]
  |15: (* JNC *)
    >EQP -P normalize nodelta
    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
    >EQppc in ⊢ (% → ?);
    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    inversion sj_possible #sj_possible_refl normalize nodelta
    [1:
      #sigma_increment_commutation #maps_assm #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 ⊢ (??%?);
      @if_then_else_status_of_pseudo_status
      >EQs >EQticks <instr_refl normalize nodelta
      [1:
        @eq_f @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
      |2:
        @set_program_counter_status_of_pseudo_status
        [1:
          >EQaddr_of normalize nodelta
          whd in match addr_of_relative; normalize nodelta
          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
          [1:
            @sym_eq whd in ⊢ (??%?); >EQppc %
          |2:
            >EQlookup_labels %
          |3:
            >sj_possible_refl @I
          ]
        |2:
          @set_clock_status_of_pseudo_status try %
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      |3:
        @set_clock_status_of_pseudo_status try % @eq_f2 try %
        whd in match ticks_of0; normalize nodelta
        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
        [1:
          >EQppc %
        |2:
          >sj_possible_refl %
        ]
      ]
    |2:
      #sigma_increment_commutation #maps_assm
      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
      change with (execute 1 ?? = ?)
      whd in match execute_1; normalize nodelta
      whd in match execute_1'; normalize nodelta
      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
      whd in match execute_1_preinstruction; normalize nodelta
      @(if_then_else_replace ???????? p) normalize nodelta
      [1:
        @eq_f >EQs
        whd in match get_cy_flag; normalize nodelta
        >special_function_registers_8051_set_program_counter
        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
        normalize #absurd destruct(absurd)
      |2:
        @(if_then_else_replace ???????? p) normalize nodelta try %
        change with (execute_1 ?? = ?) 
        whd in match execute_1; normalize nodelta
        whd in match execute_1'; normalize nodelta
        
        >set_clock_set_program_counter
        >program_counter_set_program_counter
        <sjmp_fetch_refl
        change with (set_program_counter ???? = ?)
        >set_clock_set_program_counter >set_clock_set_program_counter
        >set_program_counter_set_program_counter >set_program_counter_set_program_counter
        >EQs >EQticks <instr_refl
        >set_clock_set_program_counter >set_clock_set_clock
        @set_program_counter_status_of_pseudo_status
        [1:
          >program_counter_set_program_counter
          whd in match compute_target_of_unconditional_jump; normalize nodelta
          <(eq_bv_eq … ppc_eq_bv_refl) %
        |2:
          @set_clock_status_of_pseudo_status try % /demod nohyps/
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      ]
    ]
  |16: (* JB *)
    >EQP -P normalize nodelta
    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
    >EQppc in ⊢ (% → ?);
    @pair_elim #sj_possible #disp #sj_possible_disp_refl
    inversion sj_possible #sj_possible_refl normalize nodelta
    @(subaddressing_mode_elim … addr1) #w
    [1:
      #sigma_increment_commutation #maps_assm #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 ⊢ (??%?);
      @if_then_else_status_of_pseudo_status
      >EQs >EQticks <instr_refl normalize nodelta
      [1:
        @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try % whd
        @vsplit_elim #bit_1 #seven_bits #bit_1_seven_bits_refl normalize nodelta
        inversion (head' bool ??) #head_refl' normalize nodelta
        @vsplit_elim #four_bits #three_bits #four_bits_three_bits_refl normalize nodelta
        whd in ⊢ (??%%); cases (sfr_of_Byte ?) normalize nodelta
      |2:
        @set_program_counter_status_of_pseudo_status
        [1:
          >EQaddr_of normalize nodelta
          whd in match addr_of_relative; normalize nodelta
          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
          [1:
            @sym_eq whd in ⊢ (??%?); >EQppc %
          |2:
            >EQlookup_labels %
          |3:
            >sj_possible_refl @I
          ]
        |2:
          @set_clock_status_of_pseudo_status try %
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      |3:
        @set_clock_status_of_pseudo_status try % @eq_f2 try %
        whd in match ticks_of0; normalize nodelta
        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
        [1:
          >EQppc %
        |2:
          >sj_possible_refl %
        ]
      ]
    |2:
      #sigma_increment_commutation #maps_assm
      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
      change with (execute 1 ?? = ?)
      whd in match execute_1; normalize nodelta
      whd in match execute_1'; normalize nodelta
      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
      whd in match execute_1_preinstruction; normalize nodelta
      @(if_then_else_replace ???????? p) normalize nodelta
      [1:
        @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉 … (BIT_ADDR w))
      
        @eq_f >EQs
        whd in match get_cy_flag; normalize nodelta
        >special_function_registers_8051_set_program_counter
        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
        normalize #absurd destruct(absurd)
      |2:
        @(if_then_else_replace ???????? p) normalize nodelta try %
        change with (execute_1 ?? = ?) 
        whd in match execute_1; normalize nodelta
        whd in match execute_1'; normalize nodelta
        >program_counter_set_program_counter
        whd in match addr_of_relative; normalize nodelta
        >set_clock_set_program_counter >program_counter_set_program_counter
        <ljmp_fetch_refl
        change with (set_program_counter ???? = ?)
        >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter
        >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter
        >EQs >EQticks <instr_refl
        >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%);
        @set_program_counter_status_of_pseudo_status
        [1:
          >program_counter_set_program_counter
          whd in match compute_target_of_unconditional_jump; normalize nodelta
          >EQaddr_of normalize nodelta >EQlookup_labels %
        |2:
          >set_clock_set_clock
          @set_clock_status_of_pseudo_status try %
          /demod nohyps/
          whd in match ticks_of0; normalize nodelta
          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
          [1:
            >EQppc %
          |2:
            >sj_possible_refl %
          ]
        ]
      ]
    ]
  |*)16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
    cases daemon
  |(*29,30: (* ANL and ORL *)
    inversion addr
    [1,3:
      *
      [1,3:
        #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 (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
        [2,4: normalize nodelta #absurd destruct(absurd) ]
        inversion (assert_data ?????) #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
        change with (set_arg_8 ????? = ?)
        @set_arg_8_status_of_pseudo_status try %
        >EQs >EQticks <instr_refl >addr_refl
        [1,4:
          @sym_eq @set_clock_status_of_pseudo_status
          [1,3:
            @sym_eq @set_program_counter_status_of_pseudo_status %
          |2,4:
            @eq_f2 %
          ]
        |2,5:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
        |3,6:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
          [1,5:
            @(subaddressing_mode_elim … acc_a) %
          |4,8:
            @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,5:
              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
            |3,7:
              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
            |2,6:
              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
            |4,8:
              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
            ]
          |*:
            %
          ]
        ]
      |2,4:
        #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 (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
        [2,4: normalize nodelta #absurd destruct(absurd) ]
        inversion (assert_data ?????) #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
        change with (set_arg_8 ????? = ?)
        @set_arg_8_status_of_pseudo_status try %
        >EQs >EQticks <instr_refl >addr_refl
        [1,4:
          @sym_eq @set_clock_status_of_pseudo_status
          [1,3:
            @sym_eq @set_program_counter_status_of_pseudo_status %
          |2,4:
            @eq_f2 %
          ]
        |2,5:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
        |3,6:
          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
          [1,5:
            @(subaddressing_mode_elim … direct) #w %
          |4,8:
            @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,5:
              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
            |3,7:
              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
            |2,6:
              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
            |4,8:
              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
            ]
          |*:
            %
          ]
        ]
      ]
    |2,4:
      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
      >EQP -P normalize nodelta
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2,4: normalize nodelta #absurd destruct(absurd) ]
      inversion (assert_data ?????) #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
      change with (set_flags ?????? = ?)
      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
      >EQs >EQticks <instr_refl >addr_refl
      @sym_eq @set_clock_status_of_pseudo_status %
    ]
  |31: (* 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 (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (assert_data ?????) #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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
          |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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
          ]
        |*:
          %
        ]
      ]
    |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 (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (assert_data ?????) #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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
          |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: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
          ]
        |*:
          %
        ]
      ]
    ]
  |32: (* CLR *)
    >EQP -P normalize nodelta lapply instr_refl
    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    [1,2:
      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [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
      [1:
        >EQs >EQticks <instr_refl
        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
        @set_arg_1_status_of_pseudo_status try %
        [1:
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
        |2:
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
        ]          
      |2:
        >EQs >EQticks <instr_refl
        change with (set_arg_8 ??? ACC_A ? = ?) try %
        @set_arg_8_status_of_pseudo_status try %
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
      ]
    |3:
      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?);
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      >EQs >EQticks <instr_refl
      change with (set_arg_1 ??? CARRY ? = ?) try %
      @set_arg_1_status_of_pseudo_status %
    ]
  |33: (* CPL *)
    >EQP -P normalize nodelta lapply instr_refl
    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    [1,2:
      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [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
      [1:
        >EQs >EQticks <instr_refl
        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
        @set_arg_1_status_of_pseudo_status
        [1:
          @eq_f
          @sym_eq @(pose … (set_clock ????)) #status #status_refl
          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
        |2:
          %
        |3:
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … true (refl …) addressing_mode_ok_assm_1) %
        |4:
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … (refl …) addressing_mode_ok_assm_1) %
        ]       
      |2:
        >EQs >EQticks <instr_refl
        change with (set_8051_sfr ????? = ?)
        @set_8051_sfr_status_of_pseudo_status try %
        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
        normalize nodelta @eq_f
        @(pose … (set_clock ????)) #status #status_refl
        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
      ]
    |3:
      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
      whd in ⊢ (??%?);
      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
      >EQs >EQticks <instr_refl
      change with (set_arg_1 ??? CARRY ? = ?) try %
      @set_arg_1_status_of_pseudo_status try %
      @eq_f
      @sym_eq @(pose … (set_clock ????)) #status #status_refl
      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
    ]
  |34,36: (* 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 (assert_data ?????) 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 %
  |35,37: (* 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 (assert_data ?????) 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) %
    ]
  |38: (* SWAP *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (assert_data ?????) 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 ⊢ (??%?);
    @(pair_replace ?????????? p)
    [1:
      @eq_f normalize nodelta
      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
      @(get_8051_sfr_status_of_pseudo_status … M' … status)
      [1:
        >status_refl -status_refl
        @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:
      @(pair_replace ?????????? p) normalize nodelta
      [1:
        %
      |2:
        @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) %
        ]
      ]      
    ]
  |39: (* MOV *)
    >EQP -P normalize nodelta
    inversion addr
    [1:
      #addr' normalize nodelta
      inversion addr'
      [1:
        #addr'' normalize nodelta
        inversion addr''
        [1:
          #addr''' normalize nodelta
          inversion addr'''
          [1:
            #addr'''' normalize nodelta
            inversion addr''''
            [1:
              normalize nodelta #acc_a_others
              cases acc_a_others #acc_a #others
              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
              whd in maps_assm:(??%%);
              inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
              [2: normalize nodelta #absurd destruct(absurd) ]
              inversion (assert_data ?????) #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 %
              [1:
                @sym_eq @set_clock_status_of_pseudo_status
                >EQs >EQticks <instr_refl >addr_refl %
              |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) % ]
                >EQs >EQticks <instr_refl >addr_refl
                [1,2:
                  %
                |3:
                  @(pose … (set_clock ????)) #status #status_refl
                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
                  [1:
                    @sym_eq @set_clock_status_of_pseudo_status %
                  |2:
                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
                  |3:
                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
                  ]
                ]
              ]
            |2:
              #others_others' cases others_others' #others #others' normalize nodelta
              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
              whd in maps_assm:(??%%);
              inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
              [2: normalize nodelta #absurd destruct(absurd) ]
              inversion (assert_data ?????) #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 try %
              [1:
                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
              |2:
                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
                [1:
                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
                |2,3:
                  %
                |4:
                  @(pose … (set_clock ????)) #status #status_refl
                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
                  [1:
                    @sym_eq @set_clock_status_of_pseudo_status %
                  |2:
                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
                  |3:
                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
                  ]
                ]
              ]
            ]
          |2:
            #direct_others cases direct_others #direct #others
            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
            whd in maps_assm:(??%%);
            inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
            [2: normalize nodelta #absurd destruct(absurd) ]
            inversion (assert_data ?????) #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 %
            |2:
              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
            |3:
              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
              [1:
                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
              |2,3:
                %
              |4:
                @(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 … others … addressing_mode_ok_assm_2)
                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
                |2:
                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
                ]
              ]
            ]
          ]
        |2:
          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
          #addr_refl'' #addr_refl' #addr_refl
          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
          whd in maps_assm:(??%%);
          inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
          [2: normalize nodelta #absurd destruct(absurd) ]
          inversion (assert_data ?????) #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_16 ????? = ?)
          @set_arg_16_status_of_pseudo_status try %
          >EQs >EQticks <instr_refl >addr_refl
          @sym_eq @set_clock_status_of_pseudo_status %
        ]
      |2:
        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
        #addr_refl' #addr_refl
        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
        whd in maps_assm:(??%%);
        inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
        [2: normalize nodelta #absurd destruct(absurd) ]
        inversion (assert_data ?????) #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_1 ????? = ?)
        @set_arg_1_status_of_pseudo_status
        >EQs >EQticks <instr_refl >addr_refl try %
        [1:
          @sym_eq @(pose … (set_clock ????)) #status #status_refl
          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
        |2,3:
          @(subaddressing_mode_elim … carry) @I
        ]
      ]
    |2:
      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
      #addr_refl
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (assert_data ?????) #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_1 ????? = ?)
      @set_arg_1_status_of_pseudo_status
      [1:
        >EQs >EQticks <instr_refl >addr_refl
        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
        @(subaddressing_mode_elim … carry) @I
      |2:
        >EQs >EQticks <instr_refl >addr_refl %
      |3,4:
        @(pose … (set_clock ????)) #status #status_refl
        [1:
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
        |2:
          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
        ]
        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
      ]
    ]
  |40: (* MOVX *)
    >EQP -P normalize nodelta
    inversion addr
    [1:
      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
      #addr_refl
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (assert_data ?????) #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 %
      |2:
        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
      |3:
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
        @(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 … others … addressing_mode_ok_assm_2)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
        |2:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
        ]
      ]
    |2:
      #others_acc_a cases others_acc_a #others #acc_a
      #addr_refl
      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
      whd in maps_assm:(??%%);
      inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
      [2: normalize nodelta #absurd destruct(absurd) ]
      inversion (assert_data ?????) #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
      >EQs >EQticks <instr_refl >addr_refl try %
      [1:
        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
      |2:
        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
        [1:
          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
        |2,3:
          %
        |4:
          @(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_2)
            [1: @(subaddressing_mode_elim … acc_a) % ] %
          |2:
            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
            [1: @(subaddressing_mode_elim … acc_a) % ] %
          ]
        ]
      ]
    ]
  |41: (* SETB *)
    >EQs >EQticks <instr_refl
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (assert_data ?????) 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
    change with (set_arg_1 ????? = ?)
    @set_arg_1_status_of_pseudo_status try %
    [1:
      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    |2:
      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
    ]
  |*)*)42: (* PUSH *)
    >EQP -P normalize nodelta lapply instr_refl
    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
    #sigma_increment_commutation
    whd in ⊢ (??%? → ?);
    @vsplit_elim #bit_one #seven_bits
    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
    cases bitone #bit_one_seven_bits_refl normalize nodelta
    [ @eq_bv_elim #seven_bits_refl normalize nodelta ]
    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in match execute_1_0; normalize nodelta
    whd in match execute_1_preinstruction; normalize nodelta
    >bit_one_seven_bits_refl
    [ >seven_bits_refl
      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
    | @write_at_stack_pointer_status_of_pseudo_status_sfr_not_accA [1:assumption]
    | @write_at_stack_pointer_status_of_pseudo_status_low ]
    [1,3,5: @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
      try %
      change with (add ??? = ?); @eq_f2 try %
      @(pose … (set_clock ????)) #status #status_refl
      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
    |*: >EQs /demod nohyps/ >add_commutative % ]
  |43: (* POP *)
  |*: cases daemon ]
    >EQP -P normalize nodelta lapply instr_refl
    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
    #sigma_increment_commutation
    whd in ⊢ (??%? → ?);
    @vsplit_elim #bit_one #seven_bits
    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
    cases bitone #bit_one_seven_bits_refl normalize nodelta
    [ @eq_bv_elim #seven_bits_refl normalize nodelta
      [2: inversion (lookup_from_internal_ram ??) normalize nodelta
          [2: #x #_ #abs destruct(abs)] #lookup_from_internal_ram_refl]]
    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in match execute_1_0; normalize nodelta
    whd in match execute_1_preinstruction; normalize nodelta
    @(pair_replace ?????????? p) >p normalize nodelta
    >bit_one_seven_bits_refl
    [1,3,5: <p @eq_f3 try %
      @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … s) try %
      @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl try %
      @eq_f2 try % @(subaddressing_mode_elim … addr) #y %
    |2: @set_arg_8_status_of_pseudo_status try %
      [1: @set_8051_sfr_status_of_pseudo_status try %
              @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl try %
              @eq_f2 try % @(subaddressing_mode_elim … addr) #y %
      | whd in ⊢ (??%?); 
        inversion (sfr_of_Byte ?) normalize nodelta
        [ #sfr_of_Byte_refl (*CSC: needs >read_at_stack_pointer_set_clock*) cases daemon
        | * normalize nodelta * #sfr_of_Byte_refl
          [18: @⊥ @(absurd ?? seven_bits_refl) >bit_one_seven_bits_refl
               @eq_sfr_of_Byte_accA_to_eq assumption
          |*: change with (read_at_stack_pointer ??? = ?)
              cases daemon (*CSC: needs >read_at_stack_pointer_set_clock*)]]]
    |3:
    |4:
    XXX
    ]
  |44:
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    inversion (assert_data ?????) #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 ????? = ?)
    >EQs >EQticks <instr_refl
    @set_arg_8_status_of_pseudo_status try %
    [1:
      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
      @(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 … addr2 … addressing_mode_ok_assm_2)
        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
      |2:
        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
      ]
    |2:
      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
      [1:
        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
      |*:
        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
        whd in match sfr_8051_index; normalize nodelta
        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
      ]
    |3:
      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
      [1:
        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
      |2:
        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
        whd in match sfr_8051_index; normalize nodelta
        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
      |3:
        @(pose … (set_clock ????)) #status #status_refl
        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
      ]
    ]
  |45: (* XCHD *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    inversion (assert_data ?????) #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 ⊢ (??%?);
    @(pair_replace ?????????? p) normalize nodelta
    >EQs >EQticks <instr_refl
    [1:
      @eq_f
      @sym_eq @(pose … (set_clock ????)) #status #status_refl
      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
    |2:
      @(pair_replace ?????????? p1) normalize nodelta
      >EQs >EQticks <instr_refl
      [1:
        @eq_f
        @sym_eq @(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 … addr2 … addressing_mode_ok_assm_2)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
        |2:
          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
        ]
      |2:
        @(pair_replace ?????????? p) normalize nodelta
        >EQs >EQticks <instr_refl
        [1:
          %
        |2:
          @(pair_replace ?????????? p1) normalize nodelta
          >EQs >EQticks <instr_refl
          [1:
            %
          |2:
            @set_arg_8_status_of_pseudo_status try %
            [1:
              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
            |2:
              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
              [1:
                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
              |2:
                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
                whd in match sfr_8051_index; normalize nodelta
                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
              ]
            |3:
              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
              [1:
                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
              |2:
                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
                whd in match sfr_8051_index; normalize nodelta
                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
              ]
            ]
          ]
        ]
      ]
    ]
  |46: (* RET *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
    [2: normalize nodelta #absurd destruct(absurd) ]
    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
    [2: normalize nodelta #absurd destruct(absurd) ]
    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    whd in ⊢ (??%?);
    @(pair_replace ?????????? p) normalize nodelta
    >EQs >EQticks <instr_refl
    [1:
      @eq_f3 try %
      @sym_eq @(pose … (set_clock ????)) #status #status_refl
      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
    |2:
      @(pair_replace ?????????? p1) normalize nodelta
      >EQs >EQticks <instr_refl
      [1:
        @eq_f3 try %
        @sym_eq @(pose … (set_clock ????)) #status #status_refl
        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
        [1:
          cases daemon
          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
        |2:
          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
          whd in match sfr_8051_index; normalize nodelta
          >get_index_v_set_index_hit
          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
          cases daemon
          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
        ]
      |2:
        cases daemon (* XXX *)
      ]
    ]
  |47: (* RETI *)
    cases daemon
  |48: (* NOP *)
    >EQP -P normalize nodelta
    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
    whd in maps_assm:(??%%);
    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
    whd in ⊢ (??%?);
    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
    change with (set_clock ???? = ?)
    @set_clock_status_of_pseudo_status %
  ]
qed.