source: src/ASM/AssemblyProofSplit.ma @ 2284

Last change on this file since 2284 was 2284, checked in by sacerdot, 7 years ago

PUSH finished

File size: 117.7 KB
Line 
1include "ASM/StatusProofsSplit.ma".
2
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5include alias "ASM/BitVectorTrie.ma".
6
7lemma fetch_many_singleton:
8  ∀code_memory: BitVectorTrie Byte 16.
9  ∀final_pc, start_pc: Word.
10  ∀i: instruction.
11    fetch_many code_memory final_pc start_pc [i] →
12      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc.
13  #code_memory #final_pc #start_pc #i * #new_pc
14  #fetch_many_assm whd in fetch_many_assm;
15  cases (eq_bv_eq … fetch_many_assm) assumption
16qed.
17
18include alias "ASM/Vector.ma".
19include "ASM/Test.ma".
20(*include "ASM/Test2.ma".*)
21
22(*CSC: move elsewhere*)
23lemma not_b_c_to_b_not_c:
24  ∀b, c: bool.
25    (¬b) = c → b = (¬c).
26  //
27qed.
28 
29lemma match_nat_replace:
30  ∀l, o, p, r, o', p': nat.
31    l ≃ r →
32    o ≃ o' →
33    p ≃ p' →
34      match l with [ O ⇒ o | S n ⇒ p ] = match r with [ O ⇒ o' | S n' ⇒ p' ].
35  #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl %
36qed.
37
38(*CSC: move elsewhere*)
39lemma conjunction_split:
40  ∀l, l', r, r': bool.
41    l = l' → r = r' → (l ∧ r) = (l' ∧ r').
42  #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl %
43qed.
44
45lemma match_nat_status_of_pseudo_status:
46  ∀M, cm, sigma, policy, s, s', s'', s'''.
47  ∀n, n': nat.
48    n = n' →
49    status_of_pseudo_status M cm s' sigma policy = s →
50    (∀n. status_of_pseudo_status M cm (s''' n) sigma policy = s'' n) →
51      match n with [ O ⇒ s | S n' ⇒ s'' n' ] =
52        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' n'']) sigma policy.
53  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
54  #n_refl #s_refl #s_refl' <n_refl <s_refl
55  cases n normalize nodelta try % #n' <(s_refl' n') %
56qed.
57
58lemma get_arg_8_status_of_pseudo_status':
59  ∀cm,ps,l.
60  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
61  ∀M. ∀sigma. ∀policy. ∀s.
62      s = status_of_pseudo_status M cm ps sigma policy →
63      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
64      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr)
65      = get_arg_8 … ps l addr →
66      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
67      s l addr = get_arg_8 … ps l addr.
68 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
69 try assumption %
70qed.
71
72lemma short_jump_cond_ok:
73  ∀v1, v1', v2, v2': Word.
74  ∀is_possible, offset.
75    v1 = v1' → v2 = v2' →
76    〈is_possible, offset〉 = short_jump_cond v1 v2 →
77      is_possible → v2' = add 16 v1' (sign_extension offset).
78  #v1 #v1' #v2 #v2' #is_possible #offset #v1_refl #v2_refl <v1_refl <v2_refl
79  whd in match short_jump_cond; normalize nodelta
80  @pair_elim #result #flags #sub16_refl
81  @pair_elim #upper #lower #vsplit_refl
82  inversion (get_index' bool ???) #get_index_refl normalize nodelta
83  #relevant destruct(relevant) #relevant
84  [1:
85    @(sub_16_to_add_16_8_1 … flags)
86  |2:
87    @(sub_16_to_add_16_8_0 … flags)
88  ]
89  try assumption >sub16_refl
90  <(eq_bv_eq … relevant)
91  >(vsplit_ok … (sym_eq … vsplit_refl)) %
92qed.
93
94lemma set_clock_set_clock:
95  ∀M, cm, s, t, t'.
96    set_clock M cm (set_clock … cm s t) t' = set_clock … cm s t'.
97  #M #cm #s #t #t' %
98qed.
99
100lemma main_lemma_preinstruction:
101  ∀M, M': internal_pseudo_address_map.
102  ∀preamble: preamble.
103  ∀instr_list: list labelled_instruction.
104  ∀cm: pseudo_assembly_program.
105  ∀EQcm: cm = 〈preamble, instr_list〉.
106  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
107  ∀sigma: Word → Word.
108  ∀policy: Word → bool.
109  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
110  ∀ps: PseudoStatus cm.
111  ∀ppc: Word.
112  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
113  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
114  ∀labels: label_map.
115  ∀costs: BitVectorTrie costlabel 16.
116  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
117  ∀newppc: Word.
118  ∀lookup_labels: Identifier → Word.
119  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
120  ∀lookup_datalabels: Identifier → Word.
121  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
122  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
123  ∀instr: preinstruction Identifier.
124  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
125  ∀ticks: nat × nat.
126  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
127  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
128  ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)).
129  ∀s: PreStatus pseudo_assembly_program cm.
130  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
131  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
132  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
133              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
134                  lookup_datalabels (Instruction instr)))) →
135              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
136                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))
137                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
138                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
139                      status_of_pseudo_status M' cm s sigma policy).
140    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
141  (* XXX: takes about 45 minutes to type check! *)
142  ** #low #high #accA #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
143  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
144  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
145  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
146  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
147  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
148  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
149  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
150  [2: * // ]
151  @(
152  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
153  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
154  match instr in preinstruction return λx. x = instr → Σs'.? with
155        [ ADD addr1 addr2 ⇒ λinstr_refl.
156            let s ≝ add_ticks1 s in
157            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
158                                                   (get_arg_8 … s false addr2) false in
159            let cy_flag ≝ get_index' ? O ? flags in
160            let ac_flag ≝ get_index' ? 1 ? flags in
161            let ov_flag ≝ get_index' ? 2 ? flags in
162            let s ≝ set_arg_8 … s ACC_A result in
163              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
164        | ADDC addr1 addr2 ⇒ λinstr_refl.
165            let s ≝ add_ticks1 s in
166            let old_cy_flag ≝ get_cy_flag ?? s in
167            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
168                                                   (get_arg_8 … s false addr2) old_cy_flag in
169            let cy_flag ≝ get_index' ? O ? flags in
170            let ac_flag ≝ get_index' ? 1 ? flags in
171            let ov_flag ≝ get_index' ? 2 ? flags in
172            let s ≝ set_arg_8 … s ACC_A result in
173              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
174        | SUBB addr1 addr2 ⇒ λinstr_refl.
175            let s ≝ add_ticks1 s in
176            let old_cy_flag ≝ get_cy_flag ?? s in
177            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
178                                                   (get_arg_8 … s false addr2) old_cy_flag in
179            let cy_flag ≝ get_index' ? O ? flags in
180            let ac_flag ≝ get_index' ? 1 ? flags in
181            let ov_flag ≝ get_index' ? 2 ? flags in
182            let s ≝ set_arg_8 … s ACC_A result in
183              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
184        | ANL addr ⇒ λinstr_refl.
185          let s ≝ add_ticks1 s in
186          match addr with
187            [ inl l ⇒
188              match l with
189                [ inl l' ⇒
190                  let 〈addr1, addr2〉 ≝ l' in
191                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
192                    set_arg_8 … s addr1 and_val
193                | inr r ⇒
194                  let 〈addr1, addr2〉 ≝ r in
195                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
196                    set_arg_8 … s addr1 and_val
197                ]
198            | inr r ⇒
199              let 〈addr1, addr2〉 ≝ r in
200              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
201               set_flags … s and_val (None ?) (get_ov_flag ?? s)
202            ]
203        | ORL addr ⇒ λinstr_refl.
204          let s ≝ add_ticks1 s in
205          match addr with
206            [ inl l ⇒
207              match l with
208                [ inl l' ⇒
209                  let 〈addr1, addr2〉 ≝ l' in
210                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
211                    set_arg_8 … s addr1 or_val
212                | inr r ⇒
213                  let 〈addr1, addr2〉 ≝ r in
214                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
215                    set_arg_8 … s addr1 or_val
216                ]
217            | inr r ⇒
218              let 〈addr1, addr2〉 ≝ r in
219              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
220               set_flags … s or_val (None ?) (get_ov_flag … s)
221            ]
222        | XRL addr ⇒ λinstr_refl.
223          let s ≝ add_ticks1 s in
224          match addr with
225            [ inl l' ⇒
226              let 〈addr1, addr2〉 ≝ l' in
227              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
228                set_arg_8 … s addr1 xor_val
229            | inr r ⇒
230              let 〈addr1, addr2〉 ≝ r in
231              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
232                set_arg_8 … s addr1 xor_val
233            ]
234        | INC addr ⇒ λinstr_refl.
235            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with
236              [ ACC_A ⇒ λacc_a: True. λEQaddr.
237                let s' ≝ add_ticks1 s in
238                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
239                 set_arg_8 … s' ACC_A result
240              | REGISTER r ⇒ λregister: True. λEQaddr.
241                let s' ≝ add_ticks1 s in
242                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
243                 set_arg_8 … s' (REGISTER r) result
244              | DIRECT d ⇒ λdirect: True. λEQaddr.
245                let s' ≝ add_ticks1 s in
246                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
247                 set_arg_8 … s' (DIRECT d) result
248              | INDIRECT i ⇒ λindirect: True. λEQaddr.
249                let s' ≝ add_ticks1 s in
250                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
251                 set_arg_8 … s' (INDIRECT i) result
252              | DPTR ⇒ λdptr: True. λEQaddr.
253                let s' ≝ add_ticks1 s in
254                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
255                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
256                let s ≝ set_8051_sfr … s' SFR_DPL bl in
257                 set_8051_sfr … s' SFR_DPH bu
258              | _ ⇒ λother: False. ⊥
259              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
260        | NOP ⇒ λinstr_refl.
261           let s ≝ add_ticks2 s in
262            s
263        | DEC addr ⇒ λinstr_refl.
264           let s ≝ add_ticks1 s in
265           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
266             set_arg_8 … s addr result
267        | MUL addr1 addr2 ⇒ λinstr_refl.
268           let s ≝ add_ticks1 s in
269           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
270           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
271           let product ≝ acc_a_nat * acc_b_nat in
272           let ov_flag ≝ product ≥ 256 in
273           let low ≝ bitvector_of_nat 8 (product mod 256) in
274           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
275           let s ≝ set_8051_sfr … s SFR_ACC_A low in
276             set_8051_sfr … s SFR_ACC_B high
277        | DIV addr1 addr2 ⇒ λinstr_refl.
278           let s ≝ add_ticks1 s in
279           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
280           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
281             match acc_b_nat with
282               [ O ⇒ set_flags … s false (None Bit) true
283               | S o ⇒
284                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
285                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
286                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
287                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
288                   set_flags … s false (None Bit) false
289               ]
290        | DA addr ⇒ λinstr_refl.
291            let s ≝ add_ticks1 s in
292            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
293              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
294                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
295                let cy_flag ≝ get_index' ? O ? flags in
296                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
297                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
298                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
299                    let new_acc ≝ nu @@ acc_nl' in
300                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
301                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
302                  else
303                    s
304              else
305                s
306        | CLR addr ⇒ λinstr_refl.
307          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
308            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
309              let s ≝ add_ticks1 s in
310               set_arg_8 … s ACC_A (zero 8)
311            | CARRY ⇒ λcarry: True.  λEQaddr.
312              let s ≝ add_ticks1 s in
313               set_arg_1 … s CARRY false
314            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
315              let s ≝ add_ticks1 s in
316               set_arg_1 … s (BIT_ADDR b) false
317            | _ ⇒ λother: False. ⊥
318            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
319        | CPL addr ⇒ λinstr_refl.
320          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
321            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
322                let s ≝ add_ticks1 s in
323                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
324                let new_acc ≝ negation_bv ? old_acc in
325                 set_8051_sfr … s SFR_ACC_A new_acc
326            | CARRY ⇒ λcarry: True. λEQaddr.
327                let s ≝ add_ticks1 s in
328                let old_cy_flag ≝ get_arg_1 … s CARRY true in
329                let new_cy_flag ≝ ¬old_cy_flag in
330                 set_arg_1 … s CARRY new_cy_flag
331            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
332                let s ≝ add_ticks1 s in
333                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
334                let new_bit ≝ ¬old_bit in
335                 set_arg_1 … s (BIT_ADDR b) new_bit
336            | _ ⇒ λother: False. ?
337            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
338        | SETB b ⇒ λinstr_refl.
339            let s ≝ add_ticks1 s in
340            set_arg_1 … s b false
341        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
342            let s ≝ add_ticks1 s in
343            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
344            let new_acc ≝ rotate_left … 1 old_acc in
345              set_8051_sfr … s SFR_ACC_A new_acc
346        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
347            let s ≝ add_ticks1 s in
348            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
349            let new_acc ≝ rotate_right … 1 old_acc in
350              set_8051_sfr … s SFR_ACC_A new_acc
351        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
352            let s ≝ add_ticks1 s in
353            let old_cy_flag ≝ get_cy_flag ?? s in
354            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
355            let new_cy_flag ≝ get_index' ? O ? old_acc in
356            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
357            let s ≝ set_arg_1 … s CARRY new_cy_flag in
358              set_8051_sfr … s SFR_ACC_A new_acc
359        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
360            let s ≝ add_ticks1 s in
361            let old_cy_flag ≝ get_cy_flag ?? s in
362            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
363            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
364            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
365            let s ≝ set_arg_1 … s CARRY new_cy_flag in
366              set_8051_sfr … s SFR_ACC_A new_acc
367        | SWAP addr ⇒ λinstr_refl. (* DPM: always ACC_A *)
368            let s ≝ add_ticks1 s in
369            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
370            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
371            let new_acc ≝ nl @@ nu in
372              set_8051_sfr … s SFR_ACC_A new_acc
373        | PUSH addr ⇒ λinstr_refl.
374            let s ≝ add_ticks1 s in
375            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
376            let s ≝ set_8051_sfr … s SFR_SP new_sp in
377             write_at_stack_pointer … s (get_arg_8 … s false addr)
378        | POP addr ⇒ λinstr_refl.
379            let s ≝ add_ticks1 s in
380            let contents ≝ read_at_stack_pointer ?? s in
381            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
382            let s ≝ set_8051_sfr … s SFR_SP new_sp in
383              set_arg_8 … s addr contents
384        | XCH addr1 addr2 ⇒ λinstr_refl.
385            let s ≝ add_ticks1 s in
386            let old_addr ≝ get_arg_8 … s false addr2 in
387            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
388            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
389              set_arg_8 … s addr2 old_acc
390        | XCHD addr1 addr2 ⇒ λinstr_refl.
391            let s ≝ add_ticks1 s in
392            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
393            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
394            let new_acc ≝ acc_nu @@ arg_nl in
395            let new_arg ≝ arg_nu @@ acc_nl in
396            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
397              set_arg_8 … s addr2 new_arg
398        | RET ⇒ λinstr_refl.
399            let s ≝ add_ticks1 s in
400            let high_bits ≝ read_at_stack_pointer ?? s in
401            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
402            let s ≝ set_8051_sfr … s SFR_SP new_sp in
403            let low_bits ≝ read_at_stack_pointer ?? s in
404            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
405            let s ≝ set_8051_sfr … s SFR_SP new_sp in
406            let new_pc ≝ high_bits @@ low_bits in
407              set_program_counter … s new_pc
408        | RETI ⇒ λinstr_refl.
409            let s ≝ add_ticks1 s in
410            let high_bits ≝ read_at_stack_pointer ?? s in
411            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
412            let s ≝ set_8051_sfr … s SFR_SP new_sp in
413            let low_bits ≝ read_at_stack_pointer ?? s in
414            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
415            let s ≝ set_8051_sfr … s SFR_SP new_sp in
416            let new_pc ≝ high_bits @@ low_bits in
417              set_program_counter … s new_pc
418        | MOVX addr ⇒ λinstr_refl.
419          let s ≝ add_ticks1 s in
420          (* DPM: only copies --- doesn't affect I/O *)
421          match addr with
422            [ inl l ⇒
423              let 〈addr1, addr2〉 ≝ l in
424                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
425            | inr r ⇒
426              let 〈addr1, addr2〉 ≝ r in
427                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
428            ]
429        | MOV addr ⇒ λinstr_refl.
430          let s ≝ add_ticks1 s in
431          match addr with
432            [ inl l ⇒
433              match l with
434                [ inl l' ⇒
435                  match l' with
436                    [ inl l'' ⇒
437                      match l'' with
438                        [ inl l''' ⇒
439                          match l''' with
440                            [ inl l'''' ⇒
441                              let 〈addr1, addr2〉 ≝ l'''' in
442                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
443                            | inr r'''' ⇒
444                              let 〈addr1, addr2〉 ≝ r'''' in
445                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
446                            ]
447                        | inr r''' ⇒
448                          let 〈addr1, addr2〉 ≝ r''' in
449                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
450                        ]
451                    | inr r'' ⇒
452                      let 〈addr1, addr2〉 ≝ r'' in
453                       set_arg_16 … s (get_arg_16 … s addr2) addr1
454                    ]
455                | inr r ⇒
456                  let 〈addr1, addr2〉 ≝ r in
457                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
458                ]
459            | inr r ⇒
460              let 〈addr1, addr2〉 ≝ r in
461               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
462            ]
463          | JC addr ⇒ λinstr_refl.
464                  if get_cy_flag ?? s then
465                    let s ≝ add_ticks1 s in
466                      set_program_counter … s (addr_of addr s)
467                  else
468                    let s ≝ add_ticks2 s in
469                      s
470            | JNC addr ⇒ λinstr_refl.
471                  if ¬(get_cy_flag ?? s) then
472                   let s ≝ add_ticks1 s in
473                     set_program_counter … s (addr_of addr s)
474                  else
475                   let s ≝ add_ticks2 s in
476                    s
477            | JB addr1 addr2 ⇒ λinstr_refl.
478                  if get_arg_1 … s addr1 false then
479                   let s ≝ add_ticks1 s in
480                    set_program_counter … s (addr_of addr2 s)
481                  else
482                   let s ≝ add_ticks2 s in
483                    s
484            | JNB addr1 addr2 ⇒ λinstr_refl.
485                  if ¬(get_arg_1 … s addr1 false) then
486                   let s ≝ add_ticks1 s in
487                    set_program_counter … s (addr_of addr2 s)
488                  else
489                   let s ≝ add_ticks2 s in
490                    s
491            | JBC addr1 addr2 ⇒ λinstr_refl.
492                  let s ≝ set_arg_1 … s addr1 false in
493                    if get_arg_1 … s addr1 false then
494                     let s ≝ add_ticks1 s in
495                      set_program_counter … s (addr_of addr2 s)
496                    else
497                     let s ≝ add_ticks2 s in
498                      s
499            | JZ addr ⇒ λinstr_refl.
500                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
501                     let s ≝ add_ticks1 s in
502                      set_program_counter … s (addr_of addr s)
503                    else
504                     let s ≝ add_ticks2 s in
505                      s
506            | JNZ addr ⇒ λinstr_refl.
507                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
508                     let s ≝ add_ticks1 s in
509                      set_program_counter … s (addr_of addr s)
510                    else
511                     let s ≝ add_ticks2 s in
512                      s
513            | CJNE addr1 addr2 ⇒ λinstr_refl.
514                  match addr1 with
515                    [ inl l ⇒
516                        let 〈addr1, addr2'〉 ≝ l in
517                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
518                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
519                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
520                            let s ≝ add_ticks1 s in
521                            let s ≝ set_program_counter … s (addr_of addr2 s) in
522                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
523                          else
524                            let s ≝ add_ticks2 s in
525                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
526                    | inr r' ⇒
527                        let 〈addr1, addr2'〉 ≝ r' in
528                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
529                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
530                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
531                            let s ≝ add_ticks1 s in
532                            let s ≝ set_program_counter … s (addr_of addr2 s) in
533                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
534                          else
535                            let s ≝ add_ticks2 s in
536                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
537                    ]
538            | DJNZ addr1 addr2 ⇒ λinstr_refl.
539              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
540              let s ≝ set_arg_8 … s addr1 result in
541                if ¬(eq_bv ? result (zero 8)) then
542                 let s ≝ add_ticks1 s in
543                  set_program_counter … s (addr_of addr2 s)
544                else
545                 let s ≝ add_ticks2 s in
546                  s
547           ] (refl … instr))
548  try cases other
549  try assumption (*20s*)
550  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
551  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
552  whd in match execute_1_preinstruction; normalize nodelta
553  [1,2: (* ADD and ADDC *)
554    (* XXX: work on the right hand side *)
555    (* XXX: switch to the left hand side *)
556    >EQP -P normalize nodelta
557    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
558    whd in maps_assm:(??%%);
559    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
560    [2,4: normalize nodelta #absurd destruct(absurd) ]
561    inversion (assert_data ?????) #addressing_mode_ok_assm_2
562    [2,4: normalize nodelta #absurd destruct(absurd) ]
563    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
564    letin M' ≝ (〈low,high,accA〉)
565    whd in ⊢ (??%?);
566    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
567    whd in ⊢ (??%?);
568    normalize nodelta >EQs >EQticks <instr_refl
569    @let_pair_in_status_of_pseudo_status
570    [1,3:
571      @eq_f3
572      [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M')
573        [3,9:
574          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
575          @(subaddressing_mode_elim … addr1) %
576        |6,12:
577          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
578          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
579        |2,8:
580          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
581          @(subaddressing_mode_elim … addr1) %
582        |5,11:
583          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
584          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
585        |*: % ]
586      |3:
587        %
588      |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ]
589    |2,4:
590      #result #flags @set_flags_status_of_pseudo_status try %
591      @set_arg_8_status_of_pseudo_status try %
592      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)]
593  |(*3: (* SUBB *)
594    (* XXX: work on the right hand side *)
595    (* XXX: switch to the left hand side *)
596    >EQP -P normalize nodelta
597    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
598    whd in maps_assm:(??%%);
599    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
600    [2,4: normalize nodelta #absurd destruct(absurd) ]
601    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
602    [2,4: normalize nodelta #absurd destruct(absurd) ]
603    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
604    whd in ⊢ (??%?);
605    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
606    whd in ⊢ (??%?);
607    @(pair_replace ?????????? p)
608    [1:
609      @eq_f3
610      normalize nodelta >EQs >EQticks <instr_refl
611      [1:
612        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
613        @(get_arg_8_status_of_pseudo_status cm status … M')
614        [1:
615          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
616        |2:
617          >status_refl
618          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
619          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
620        |3:
621          >status_refl
622          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
623          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
624        ]
625      |2:
626        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
627        @(get_arg_8_status_of_pseudo_status cm status … M')
628        [1:
629          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
630        |2:
631          >status_refl
632          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
633          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
634        |3:
635          >status_refl
636          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
637          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
638        ]
639      |3:
640        @(get_cy_flag_status_of_pseudo_status … M')
641        @sym_eq @set_clock_status_of_pseudo_status
642        [1:
643          @sym_eq @set_program_counter_status_of_pseudo_status %
644        |2:
645          %
646        ]
647      ]
648    |2:
649      normalize nodelta
650      @(pair_replace ?????????? p)
651      [1:
652        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
653      |2:
654        @set_flags_status_of_pseudo_status try %
655        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
656        [1:
657          @sym_eq @set_clock_status_of_pseudo_status %
658        |2:
659          @I
660        |3:
661          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try %
662          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
663        ]
664      ]
665    ]
666  |4: (* INC *)
667    (* XXX: work on the right hand side *)
668    (* XXX: switch to the left hand side *)
669    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
670    @(subaddressing_mode_elim … addr) normalize nodelta
671    [1:
672      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
673      whd in maps_assm:(??%%);
674      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
675      [2: normalize nodelta #absurd destruct(absurd) ]
676      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
677      whd in ⊢ (??%?);
678      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
679      whd in ⊢ (??%?);
680      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
681      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
682      [1:
683        @eq_f2 try %
684        @(pose … (set_clock ????)) #status #status_refl
685        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
686        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
687      |2:
688        @set_arg_8_status_of_pseudo_status try %
689        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
690      ]
691    |2:
692      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
693      whd in maps_assm:(??%%);
694      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
695      [2: normalize nodelta #absurd destruct(absurd) ]
696      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
697      whd in ⊢ (??%?);
698      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
699      whd in ⊢ (??%?);
700      @let_pair_in_status_of_pseudo_status
701      [1:
702        @eq_f2 try %
703        @(pose … (set_clock ????)) #status #status_refl
704        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
705        >EQs >EQticks
706        [1:
707          @sym_eq @set_clock_status_of_pseudo_status %
708        |2:
709          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
710        |3:
711          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
712        ]
713      |2:
714        #carry #result
715        @sym_eq @set_arg_8_status_of_pseudo_status try %
716        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
717      ]
718    |3:
719      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
720      whd in maps_assm:(??%%);
721      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
722      [2: normalize nodelta #absurd destruct(absurd) ]
723      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
724      whd in ⊢ (??%?);
725      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
726      whd in ⊢ (??%?);
727      @let_pair_in_status_of_pseudo_status
728      [1:
729        @eq_f2 try %
730        @(pose … (set_clock ????)) #status #status_refl
731        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
732        >EQs >EQticks
733        [1:
734          @sym_eq @set_clock_status_of_pseudo_status %
735        |2:
736          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
737        |3:
738          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
739        ]
740      |2:
741        #carry #result
742        @sym_eq @set_arg_8_status_of_pseudo_status try %
743        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
744      ]
745    |4:
746      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
747      whd in maps_assm:(??%%);
748      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
749      [2: normalize nodelta #absurd destruct(absurd) ]
750      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
751      whd in ⊢ (??%?);
752      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
753      whd in ⊢ (??%?);
754      @let_pair_in_status_of_pseudo_status
755      [1:
756        @eq_f2 try %
757        @(pose … (set_clock ????)) #status #status_refl
758        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
759        >EQs >EQticks
760        [1:
761          @sym_eq @set_clock_status_of_pseudo_status %
762        |2:
763          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
764        |3:
765          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
766        ]
767      |2:
768        #carry #result
769        @sym_eq @set_arg_8_status_of_pseudo_status try %
770        [1:
771          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
772        |2:
773          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
774        ]
775      ]
776    |5:
777      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
778      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
779      whd in ⊢ (??%?);
780      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
781      whd in ⊢ (??%?);
782      @let_pair_in_status_of_pseudo_status
783      [1:
784        @eq_f2 try %
785        @(pose … (set_clock ????)) #status #status_refl
786        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
787        >EQs >EQticks %
788      |2:
789        #carry #bl
790        @sym_eq @let_pair_in_status_of_pseudo_status
791        [1:
792          @eq_f3 try %
793          @(pose … (set_clock ????)) #status #status_refl
794          @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
795          >EQs >EQticks %
796        |2:
797          #carry' #bu
798          @sym_eq @set_8051_sfr_status_of_pseudo_status %
799        ]
800      ]
801    ]
802  |5: (* DEC *)
803    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
804    @(subaddressing_mode_elim … addr) normalize nodelta
805    [1:
806      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
807      whd in maps_assm:(??%%);
808      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
809      [2: normalize nodelta #absurd destruct(absurd) ]
810      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
811      whd in ⊢ (??%?);
812      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
813      whd in ⊢ (??%?);
814      @let_pair_in_status_of_pseudo_status
815      [1:
816        @eq_f3 try %
817        @(pose … (set_clock ????)) #status #status_refl
818        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
819        >EQs >EQticks try %
820        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
821      |2:
822        #result #flags
823        @sym_eq @set_arg_8_status_of_pseudo_status try %
824        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
825      ]
826    |2:
827      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
828      whd in maps_assm:(??%%);
829      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
830      [2: normalize nodelta #absurd destruct(absurd) ]
831      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
832      whd in ⊢ (??%?);
833      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
834      whd in ⊢ (??%?);
835      @let_pair_in_status_of_pseudo_status
836      [1:
837        @eq_f3 try %
838        @(pose … (set_clock ????)) #status #status_refl
839        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
840        >EQs >EQticks try %
841        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
842      |2:
843        #result #flags
844        @sym_eq @set_arg_8_status_of_pseudo_status try %
845        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
846      ]
847    |3:
848      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
849      whd in maps_assm:(??%%);
850      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
851      [2: normalize nodelta #absurd destruct(absurd) ]
852      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
853      whd in ⊢ (??%?);
854      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
855      whd in ⊢ (??%?);
856      @let_pair_in_status_of_pseudo_status
857      [1:
858        @eq_f3 try %
859        @(pose … (set_clock ????)) #status #status_refl
860        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
861        >EQs >EQticks try %
862        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
863      |2:
864        #result #flags
865        @sym_eq @set_arg_8_status_of_pseudo_status try %
866        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
867      ]
868    |4:
869      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
870      whd in maps_assm:(??%%);
871      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
872      [2: normalize nodelta #absurd destruct(absurd) ]
873      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
874      whd in ⊢ (??%?);
875      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
876      whd in ⊢ (??%?);
877      @let_pair_in_status_of_pseudo_status
878      [1:
879        @eq_f3 try %
880        @(pose … (set_clock ????)) #status #status_refl
881        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
882        >EQs >EQticks try %
883        [1:
884          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
885        |2:
886          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
887        ]
888      |2:
889        #result #flags
890        @sym_eq @set_arg_8_status_of_pseudo_status try %
891        [1:
892          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
893        |2:
894          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
895        ]
896      ]
897    ]
898  |6: (* MUL *)
899    (* XXX: work on the right hand side *)
900    (* XXX: switch to the left hand side *)
901    >EQP -P normalize nodelta
902    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
903    whd in maps_assm:(??%%);
904    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
905    [2: normalize nodelta #absurd destruct(absurd) ]
906    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
907    [2: normalize nodelta #absurd destruct(absurd) ]
908    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
909    whd in ⊢ (??%?);
910    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
911    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
912    [2:
913      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
914      @sym_eq
915      [1:
916        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
917        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
918        %
919      |2:
920        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
921      ]
922    ]
923    @sym_eq @set_8051_sfr_status_of_pseudo_status
924    [2:
925      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
926      @eq_f @eq_f2 try % @eq_f2 @eq_f
927      @sym_eq
928      [1:
929        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
930        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
931      |2:
932        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
933      ]
934    ]
935    @sym_eq @set_clock_status_of_pseudo_status
936    [2:
937      @eq_f %
938    ]
939    @sym_eq @set_program_counter_status_of_pseudo_status %
940  |7,8: (* DIV *)
941    (* XXX: work on the right hand side *)
942    (* XXX: switch to the left hand side *)
943    >EQP -P normalize nodelta
944    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
945    whd in maps_assm:(??%%);
946    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
947    [2,4: normalize nodelta #absurd destruct(absurd) ]
948    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
949    [2,4: normalize nodelta #absurd destruct(absurd) ]
950    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
951    whd in ⊢ (??%?);
952    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
953    whd in ⊢ (??%?); normalize nodelta
954    @(match_nat_status_of_pseudo_status M' cm sigma policy)
955    [1,4:
956      @eq_f
957      @sym_eq @(pose … (set_clock ????)) #status #status_refl
958      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
959    |2,5:
960      @sym_eq @set_flags_status_of_pseudo_status %
961    |3,6:
962      #n @sym_eq @set_flags_status_of_pseudo_status try %
963      @sym_eq @set_8051_sfr_status_of_pseudo_status
964      [1,3:
965        @sym_eq @set_8051_sfr_status_of_pseudo_status try %
966        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
967        @eq_f @eq_f2 try % @eq_f
968        @(pose … (set_clock ????)) #status #status_refl
969        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
970        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
971      |2,4:
972        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
973        @(pose … (set_clock ????)) #status #status_refl
974        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
975        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
976      ]
977    ]
978  |9: (* DA *)
979    (* XXX: work on the right hand side *)
980    (* XXX: switch to the left hand side *)
981    >EQP -P normalize nodelta
982    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
983    whd in maps_assm:(??%%);
984    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
985    [2: normalize nodelta #absurd destruct(absurd) ]
986    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
987    whd in ⊢ (??%?);
988    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
989    whd in ⊢ (??%?); normalize nodelta
990    @(pair_replace ?????????? p)
991    [1:
992      @eq_f normalize nodelta >EQs >EQticks <instr_refl
993      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
994      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
995    |2:
996      @(pair_replace ?????????? p)
997      [1:
998        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
999      |2:
1000        @(if_then_else_replace ???????? p1) normalize nodelta
1001        [1:
1002          cases (gtb ? 9)
1003          [1:
1004            %
1005          |2:
1006            change with (get_ac_flag ??? = get_ac_flag ???)
1007            @(get_ac_flag_status_of_pseudo_status M')
1008            @sym_eq @set_clock_status_of_pseudo_status
1009            >EQs >EQticks <instr_refl %
1010          ]
1011        |2:
1012          @(if_then_else_replace ???????? p1) normalize nodelta try %
1013          @(pair_replace ?????????? p2)
1014          [1:
1015            @eq_f3 try % normalize nodelta
1016            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1017            whd in ⊢ (??%?);
1018            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1019          |2:
1020            @(pair_replace ?????????? p2) try %
1021            @(pair_replace ?????????? p3) try %
1022            @(pair_replace ?????????? p3) try %
1023            @(if_then_else_replace ???????? p4) try % normalize nodelta
1024            @(if_then_else_replace ???????? p4) try % normalize nodelta
1025            @(pair_replace ?????????? p5) try %
1026            @(pair_replace ?????????? p5) try %
1027            @set_flags_status_of_pseudo_status try %
1028            [1:
1029              @eq_f @(get_ac_flag_status_of_pseudo_status M')
1030              @sym_eq @set_8051_sfr_status_of_pseudo_status
1031              [1:
1032                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1033              |2:
1034                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1035              ]
1036            |2:
1037              @(get_ov_flag_status_of_pseudo_status M')
1038              @sym_eq @set_8051_sfr_status_of_pseudo_status
1039              [1:
1040                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1041              |2:
1042                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1043              ]
1044            |3:
1045              @sym_eq @set_8051_sfr_status_of_pseudo_status
1046              [1:
1047                @sym_eq @set_clock_status_of_pseudo_status
1048                [1:
1049                  >EQs
1050                  @sym_eq @set_program_counter_status_of_pseudo_status %
1051                |2:
1052                  >EQs >EQticks <instr_refl %
1053                ]
1054              |2:
1055                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1056              ]
1057            ]
1058          ]
1059        ]
1060      ]
1061    ]
1062  |10: (* DA *)
1063    (* XXX: work on the right hand side *)
1064    (* XXX: switch to the left hand side *)
1065    >EQP -P normalize nodelta
1066    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1067    whd in maps_assm:(??%%);
1068    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1069    [2: normalize nodelta #absurd destruct(absurd) ]
1070    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1071    whd in ⊢ (??%?);
1072    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1073    whd in ⊢ (??%?); normalize nodelta
1074    @(pair_replace ?????????? p)
1075    [1:
1076      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1077      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1078      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1079    |2:
1080      @(pair_replace ?????????? p)
1081      [1:
1082        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1083      |2:
1084        @(if_then_else_replace ???????? p1) normalize nodelta
1085        [1:
1086          cases (gtb ? 9)
1087          [1:
1088            %
1089          |2:
1090            change with (get_ac_flag ??? = get_ac_flag ???)
1091            @(get_ac_flag_status_of_pseudo_status M')
1092            @sym_eq @set_clock_status_of_pseudo_status
1093            >EQs >EQticks <instr_refl %
1094          ]
1095        |2:
1096          @(if_then_else_replace ???????? p1) normalize nodelta try %
1097          @(pair_replace ?????????? p2)
1098          [1:
1099            @eq_f3 try % normalize nodelta
1100            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1101            whd in ⊢ (??%?);
1102            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1103          |2:
1104            @(pair_replace ?????????? p2) try %
1105            @(pair_replace ?????????? p3) try %
1106            @(pair_replace ?????????? p3) try %
1107            @(if_then_else_replace ???????? p4) try % normalize nodelta
1108            @(if_then_else_replace ???????? p4) try % normalize nodelta
1109            @set_clock_status_of_pseudo_status
1110            [1:
1111              >EQs
1112              @sym_eq @set_program_counter_status_of_pseudo_status %
1113            |2:
1114              >EQs >EQticks <instr_refl %
1115            ]
1116          ]
1117        ]
1118      ]
1119    ]
1120  |11: (* DA *)
1121    (* XXX: work on the right hand side *)
1122    (* XXX: switch to the left hand side *)
1123    >EQP -P normalize nodelta
1124    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1125    whd in maps_assm:(??%%);
1126    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1127    [2: normalize nodelta #absurd destruct(absurd) ]
1128    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1129    whd in ⊢ (??%?);
1130    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1131    whd in ⊢ (??%?); normalize nodelta
1132    @(pair_replace ?????????? p)
1133    [1:
1134      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1135      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1136      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1137    |2:
1138      @(pair_replace ?????????? p)
1139      [1:
1140        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1141      |2:
1142        @(if_then_else_replace ???????? p1) normalize nodelta
1143        [1:
1144          cases (gtb ? 9)
1145          [1:
1146            %
1147          |2:
1148            change with (get_ac_flag ??? = get_ac_flag ???)
1149            @(get_ac_flag_status_of_pseudo_status M')
1150            @sym_eq @set_clock_status_of_pseudo_status
1151            >EQs >EQticks <instr_refl %
1152          ]
1153        |2:
1154          @(if_then_else_replace ???????? p1) normalize nodelta try %
1155          @set_clock_status_of_pseudo_status
1156          [1:
1157            >EQs
1158            @sym_eq @set_program_counter_status_of_pseudo_status %
1159          |2:
1160            >EQs >EQticks <instr_refl %
1161          ]
1162        ]
1163      ]
1164    ]
1165  |12: (* JC *)
1166    >EQP -P normalize nodelta
1167    whd in match assembly_1_pseudoinstruction; normalize nodelta
1168    whd in match expand_pseudo_instruction; normalize nodelta
1169    whd in match expand_relative_jump; normalize nodelta
1170    whd in match expand_relative_jump_internal; normalize nodelta
1171    >EQppc in ⊢ (% → ?);
1172    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1173    inversion sj_possible #sj_possible_refl normalize nodelta
1174    [1:
1175      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1176      whd in maps_assm:(??%%);
1177      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1178      whd in ⊢ (??%?); normalize nodelta
1179      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1180      whd in ⊢ (??%?);
1181      @if_then_else_status_of_pseudo_status
1182      >EQs >EQticks <instr_refl normalize nodelta
1183      [1:
1184        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
1185      |2:
1186        @set_program_counter_status_of_pseudo_status
1187        [1:
1188          >EQaddr_of normalize nodelta
1189          whd in match addr_of_relative; normalize nodelta
1190          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
1191          [1:
1192            @sym_eq whd in ⊢ (??%?); >EQppc %
1193          |2:
1194            >EQlookup_labels %
1195          |3:
1196            >sj_possible_refl @I
1197          ]
1198        |2:
1199          @set_clock_status_of_pseudo_status try %
1200          whd in match ticks_of0; normalize nodelta
1201          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1202          [1:
1203            >EQppc %
1204          |2:
1205            >sj_possible_refl %
1206          ]
1207        ]
1208      |3:
1209        @set_clock_status_of_pseudo_status try % @eq_f2 try %
1210        whd in match ticks_of0; normalize nodelta
1211        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1212        [1:
1213          >EQppc %
1214        |2:
1215          >sj_possible_refl %
1216        ]
1217      ]
1218    |2:
1219      #sigma_increment_commutation #maps_assm
1220      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1221      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
1222      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
1223      change with (execute 1 ?? = ?)
1224      whd in match execute_1; normalize nodelta
1225      whd in match execute_1'; normalize nodelta
1226      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
1227      whd in match execute_1_preinstruction; normalize nodelta
1228      @(if_then_else_replace ???????? p) normalize nodelta
1229      [1:
1230        >EQs
1231        whd in match get_cy_flag; normalize nodelta
1232        >special_function_registers_8051_set_program_counter
1233        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
1234        normalize #absurd destruct(absurd)
1235      |2:
1236        @(if_then_else_replace ???????? p) normalize nodelta try %
1237        change with (execute_1 ?? = ?)
1238        whd in match execute_1; normalize nodelta
1239        whd in match execute_1'; normalize nodelta
1240        >program_counter_set_program_counter
1241        whd in match addr_of_relative; normalize nodelta
1242        >set_clock_set_program_counter >program_counter_set_program_counter
1243        <ljmp_fetch_refl
1244        change with (set_program_counter ???? = ?)
1245        >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter
1246        >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter
1247        >EQs >EQticks <instr_refl
1248        >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%);
1249        @set_program_counter_status_of_pseudo_status
1250        [1:
1251          >program_counter_set_program_counter
1252          whd in match compute_target_of_unconditional_jump; normalize nodelta
1253          >EQaddr_of normalize nodelta >EQlookup_labels %
1254        |2:
1255          >set_clock_set_clock
1256          @set_clock_status_of_pseudo_status try %
1257          /demod nohyps/
1258          whd in match ticks_of0; normalize nodelta
1259          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1260          [1:
1261            >EQppc %
1262          |2:
1263            >sj_possible_refl %
1264          ]
1265        ]
1266      ]
1267    ]
1268  |13: (* JC *)
1269    >EQP -P normalize nodelta
1270    whd in match assembly_1_pseudoinstruction; normalize nodelta
1271    whd in match expand_pseudo_instruction; normalize nodelta
1272    whd in match expand_relative_jump; normalize nodelta
1273    whd in match expand_relative_jump_internal; normalize nodelta
1274    >EQppc in ⊢ (% → ?);
1275    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1276    inversion sj_possible #sj_possible_refl normalize nodelta
1277    [1:
1278      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1279      whd in maps_assm:(??%%);
1280      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1281      whd in ⊢ (??%?); normalize nodelta
1282      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1283      whd in ⊢ (??%?);
1284      @if_then_else_status_of_pseudo_status
1285      >EQs >EQticks <instr_refl normalize nodelta
1286      [1:
1287        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
1288      |2:
1289        @set_program_counter_status_of_pseudo_status
1290        [1:
1291          >EQaddr_of normalize nodelta
1292          whd in match addr_of_relative; normalize nodelta
1293          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
1294          [1:
1295            @sym_eq whd in ⊢ (??%?); >EQppc %
1296          |2:
1297            >EQlookup_labels %
1298          |3:
1299            >sj_possible_refl @I
1300          ]
1301        |2:
1302          @set_clock_status_of_pseudo_status try %
1303          whd in match ticks_of0; normalize nodelta
1304          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1305          [1:
1306            >EQppc %
1307          |2:
1308            >sj_possible_refl %
1309          ]
1310        ]
1311      |3:
1312        @set_clock_status_of_pseudo_status try % @eq_f2 try %
1313        whd in match ticks_of0; normalize nodelta
1314        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1315        [1:
1316          >EQppc %
1317        |2:
1318          >sj_possible_refl %
1319        ]
1320      ]
1321    |2:
1322      #sigma_increment_commutation #maps_assm
1323      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1324      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
1325      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
1326      change with (execute 1 ?? = ?)
1327      whd in match execute_1; normalize nodelta
1328      whd in match execute_1'; normalize nodelta
1329      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
1330      whd in match execute_1_preinstruction; normalize nodelta
1331      @(if_then_else_replace ???????? p) normalize nodelta
1332      [1:
1333        >EQs
1334        whd in match get_cy_flag; normalize nodelta
1335        >special_function_registers_8051_set_program_counter
1336        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
1337        normalize #absurd destruct(absurd)
1338      |2:
1339        @(if_then_else_replace ???????? p) normalize nodelta try %
1340        change with (execute_1 ?? = ?)
1341        whd in match execute_1; normalize nodelta
1342        whd in match execute_1'; normalize nodelta
1343       
1344        >set_clock_set_program_counter
1345        >program_counter_set_program_counter
1346        <sjmp_fetch_refl
1347        change with (set_program_counter ???? = ?)
1348        >set_clock_set_program_counter >set_clock_set_program_counter
1349        >set_program_counter_set_program_counter >set_program_counter_set_program_counter
1350        >EQs >EQticks <instr_refl
1351        >set_clock_set_program_counter >set_clock_set_clock
1352        @set_program_counter_status_of_pseudo_status
1353        [1:
1354          >program_counter_set_program_counter
1355          whd in match compute_target_of_unconditional_jump; normalize nodelta
1356          <(eq_bv_eq … ppc_eq_bv_refl) %
1357        |2:
1358          @set_clock_status_of_pseudo_status try % /demod nohyps/
1359          whd in match ticks_of0; normalize nodelta
1360          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1361          [1:
1362            >EQppc %
1363          |2:
1364            >sj_possible_refl %
1365          ]
1366        ]
1367      ]
1368    ]
1369  |14: (* JNC *)
1370    >EQP -P normalize nodelta
1371    whd in match assembly_1_pseudoinstruction; normalize nodelta
1372    whd in match expand_pseudo_instruction; normalize nodelta
1373    whd in match expand_relative_jump; normalize nodelta
1374    whd in match expand_relative_jump_internal; normalize nodelta
1375    >EQppc in ⊢ (% → ?);
1376    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1377    inversion sj_possible #sj_possible_refl normalize nodelta
1378    [1:
1379      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1380      whd in maps_assm:(??%%);
1381      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1382      whd in ⊢ (??%?); normalize nodelta
1383      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1384      whd in ⊢ (??%?);
1385      @if_then_else_status_of_pseudo_status
1386      >EQs >EQticks <instr_refl normalize nodelta
1387      [1:
1388        @eq_f @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
1389      |2:
1390        @set_program_counter_status_of_pseudo_status
1391        [1:
1392          >EQaddr_of normalize nodelta
1393          whd in match addr_of_relative; normalize nodelta
1394          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
1395          [1:
1396            @sym_eq whd in ⊢ (??%?); >EQppc %
1397          |2:
1398            >EQlookup_labels %
1399          |3:
1400            >sj_possible_refl @I
1401          ]
1402        |2:
1403          @set_clock_status_of_pseudo_status try %
1404          whd in match ticks_of0; normalize nodelta
1405          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1406          [1:
1407            >EQppc %
1408          |2:
1409            >sj_possible_refl %
1410          ]
1411        ]
1412      |3:
1413        @set_clock_status_of_pseudo_status try % @eq_f2 try %
1414        whd in match ticks_of0; normalize nodelta
1415        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1416        [1:
1417          >EQppc %
1418        |2:
1419          >sj_possible_refl %
1420        ]
1421      ]
1422    |2:
1423      #sigma_increment_commutation #maps_assm
1424      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1425      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
1426      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
1427      change with (execute 1 ?? = ?)
1428      whd in match execute_1; normalize nodelta
1429      whd in match execute_1'; normalize nodelta
1430      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
1431      whd in match execute_1_preinstruction; normalize nodelta
1432      @(if_then_else_replace ???????? p) normalize nodelta
1433      [1:
1434        @eq_f >EQs
1435        whd in match get_cy_flag; normalize nodelta
1436        >special_function_registers_8051_set_program_counter
1437        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
1438        normalize #absurd destruct(absurd)
1439      |2:
1440        @(if_then_else_replace ???????? p) normalize nodelta try %
1441        change with (execute_1 ?? = ?)
1442        whd in match execute_1; normalize nodelta
1443        whd in match execute_1'; normalize nodelta
1444        >program_counter_set_program_counter
1445        whd in match addr_of_relative; normalize nodelta
1446        >set_clock_set_program_counter >program_counter_set_program_counter
1447        <ljmp_fetch_refl
1448        change with (set_program_counter ???? = ?)
1449        >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter
1450        >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter
1451        >EQs >EQticks <instr_refl
1452        >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%);
1453        @set_program_counter_status_of_pseudo_status
1454        [1:
1455          >program_counter_set_program_counter
1456          whd in match compute_target_of_unconditional_jump; normalize nodelta
1457          >EQaddr_of normalize nodelta >EQlookup_labels %
1458        |2:
1459          >set_clock_set_clock
1460          @set_clock_status_of_pseudo_status try %
1461          /demod nohyps/
1462          whd in match ticks_of0; normalize nodelta
1463          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1464          [1:
1465            >EQppc %
1466          |2:
1467            >sj_possible_refl %
1468          ]
1469        ]
1470      ]
1471    ]
1472  |15: (* JNC *)
1473    >EQP -P normalize nodelta
1474    whd in match assembly_1_pseudoinstruction; normalize nodelta
1475    whd in match expand_pseudo_instruction; normalize nodelta
1476    whd in match expand_relative_jump; normalize nodelta
1477    whd in match expand_relative_jump_internal; normalize nodelta
1478    >EQppc in ⊢ (% → ?);
1479    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1480    inversion sj_possible #sj_possible_refl normalize nodelta
1481    [1:
1482      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1483      whd in maps_assm:(??%%);
1484      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1485      whd in ⊢ (??%?); normalize nodelta
1486      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1487      whd in ⊢ (??%?);
1488      @if_then_else_status_of_pseudo_status
1489      >EQs >EQticks <instr_refl normalize nodelta
1490      [1:
1491        @eq_f @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
1492      |2:
1493        @set_program_counter_status_of_pseudo_status
1494        [1:
1495          >EQaddr_of normalize nodelta
1496          whd in match addr_of_relative; normalize nodelta
1497          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
1498          [1:
1499            @sym_eq whd in ⊢ (??%?); >EQppc %
1500          |2:
1501            >EQlookup_labels %
1502          |3:
1503            >sj_possible_refl @I
1504          ]
1505        |2:
1506          @set_clock_status_of_pseudo_status try %
1507          whd in match ticks_of0; normalize nodelta
1508          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1509          [1:
1510            >EQppc %
1511          |2:
1512            >sj_possible_refl %
1513          ]
1514        ]
1515      |3:
1516        @set_clock_status_of_pseudo_status try % @eq_f2 try %
1517        whd in match ticks_of0; normalize nodelta
1518        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1519        [1:
1520          >EQppc %
1521        |2:
1522          >sj_possible_refl %
1523        ]
1524      ]
1525    |2:
1526      #sigma_increment_commutation #maps_assm
1527      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1528      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
1529      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
1530      change with (execute 1 ?? = ?)
1531      whd in match execute_1; normalize nodelta
1532      whd in match execute_1'; normalize nodelta
1533      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
1534      whd in match execute_1_preinstruction; normalize nodelta
1535      @(if_then_else_replace ???????? p) normalize nodelta
1536      [1:
1537        @eq_f >EQs
1538        whd in match get_cy_flag; normalize nodelta
1539        >special_function_registers_8051_set_program_counter
1540        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
1541        normalize #absurd destruct(absurd)
1542      |2:
1543        @(if_then_else_replace ???????? p) normalize nodelta try %
1544        change with (execute_1 ?? = ?)
1545        whd in match execute_1; normalize nodelta
1546        whd in match execute_1'; normalize nodelta
1547       
1548        >set_clock_set_program_counter
1549        >program_counter_set_program_counter
1550        <sjmp_fetch_refl
1551        change with (set_program_counter ???? = ?)
1552        >set_clock_set_program_counter >set_clock_set_program_counter
1553        >set_program_counter_set_program_counter >set_program_counter_set_program_counter
1554        >EQs >EQticks <instr_refl
1555        >set_clock_set_program_counter >set_clock_set_clock
1556        @set_program_counter_status_of_pseudo_status
1557        [1:
1558          >program_counter_set_program_counter
1559          whd in match compute_target_of_unconditional_jump; normalize nodelta
1560          <(eq_bv_eq … ppc_eq_bv_refl) %
1561        |2:
1562          @set_clock_status_of_pseudo_status try % /demod nohyps/
1563          whd in match ticks_of0; normalize nodelta
1564          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1565          [1:
1566            >EQppc %
1567          |2:
1568            >sj_possible_refl %
1569          ]
1570        ]
1571      ]
1572    ]
1573  |16: (* JB *)
1574    >EQP -P normalize nodelta
1575    whd in match assembly_1_pseudoinstruction; normalize nodelta
1576    whd in match expand_pseudo_instruction; normalize nodelta
1577    whd in match expand_relative_jump; normalize nodelta
1578    whd in match expand_relative_jump_internal; normalize nodelta
1579    >EQppc in ⊢ (% → ?);
1580    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1581    inversion sj_possible #sj_possible_refl normalize nodelta
1582    [1:
1583      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1584      whd in maps_assm:(??%%);
1585      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1586      whd in ⊢ (??%?); normalize nodelta
1587      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1588      whd in ⊢ (??%?);
1589      @if_then_else_status_of_pseudo_status
1590      >EQs >EQticks <instr_refl normalize nodelta
1591      [1:
1592        @(get_arg_1_status_of_pseudo_status … 〈low, high, accA〉) try %
1593        @(subaddressing_mode_elim … addr1) #w whd
1594      |2:
1595        @set_program_counter_status_of_pseudo_status
1596        [1:
1597          >EQaddr_of normalize nodelta
1598          whd in match addr_of_relative; normalize nodelta
1599          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
1600          [1:
1601            @sym_eq whd in ⊢ (??%?); >EQppc %
1602          |2:
1603            >EQlookup_labels %
1604          |3:
1605            >sj_possible_refl @I
1606          ]
1607        |2:
1608          @set_clock_status_of_pseudo_status try %
1609          whd in match ticks_of0; normalize nodelta
1610          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1611          [1:
1612            >EQppc %
1613          |2:
1614            >sj_possible_refl %
1615          ]
1616        ]
1617      |3:
1618        @set_clock_status_of_pseudo_status try % @eq_f2 try %
1619        whd in match ticks_of0; normalize nodelta
1620        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1621        [1:
1622          >EQppc %
1623        |2:
1624          >sj_possible_refl %
1625        ]
1626      ]
1627    |2:
1628      #sigma_increment_commutation #maps_assm
1629      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1630      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
1631      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
1632      change with (execute 1 ?? = ?)
1633      whd in match execute_1; normalize nodelta
1634      whd in match execute_1'; normalize nodelta
1635      <jc_fetch_refl whd in match execute_1_0; normalize nodelta
1636      whd in match execute_1_preinstruction; normalize nodelta
1637      @(if_then_else_replace ???????? p) normalize nodelta
1638      [1:
1639        @eq_f >EQs
1640        whd in match get_cy_flag; normalize nodelta
1641        >special_function_registers_8051_set_program_counter
1642        <(get_index_v_special_function_registers_8051_not_acc_a … 〈low, high, accA〉 … sigma policy) try %
1643        normalize #absurd destruct(absurd)
1644      |2:
1645        @(if_then_else_replace ???????? p) normalize nodelta try %
1646        change with (execute_1 ?? = ?)
1647        whd in match execute_1; normalize nodelta
1648        whd in match execute_1'; normalize nodelta
1649        >program_counter_set_program_counter
1650        whd in match addr_of_relative; normalize nodelta
1651        >set_clock_set_program_counter >program_counter_set_program_counter
1652        <ljmp_fetch_refl
1653        change with (set_program_counter ???? = ?)
1654        >set_clock_set_program_counter >set_clock_set_program_counter >set_clock_set_program_counter
1655        >set_program_counter_set_program_counter >set_program_counter_set_program_counter >set_program_counter_set_program_counter
1656        >EQs >EQticks <instr_refl
1657        >set_clock_set_program_counter >set_program_counter_set_program_counter in ⊢ (???%);
1658        @set_program_counter_status_of_pseudo_status
1659        [1:
1660          >program_counter_set_program_counter
1661          whd in match compute_target_of_unconditional_jump; normalize nodelta
1662          >EQaddr_of normalize nodelta >EQlookup_labels %
1663        |2:
1664          >set_clock_set_clock
1665          @set_clock_status_of_pseudo_status try %
1666          /demod nohyps/
1667          whd in match ticks_of0; normalize nodelta
1668          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1669          [1:
1670            >EQppc %
1671          |2:
1672            >sj_possible_refl %
1673          ]
1674        ]
1675      ]
1676    ]
1677  |16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
1678    cases daemon
1679  |(*29,30: (* ANL and ORL *)
1680    inversion addr
1681    [1,3:
1682      *
1683      [1,3:
1684        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1685        >EQP -P normalize nodelta
1686        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1687        whd in maps_assm:(??%%);
1688        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1689        [2,4: normalize nodelta #absurd destruct(absurd) ]
1690        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1691        [2,4: normalize nodelta #absurd destruct(absurd) ]
1692        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1693        whd in ⊢ (??%?);
1694        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1695        change with (set_arg_8 ????? = ?)
1696        @set_arg_8_status_of_pseudo_status try %
1697        >EQs >EQticks <instr_refl >addr_refl
1698        [1,4:
1699          @sym_eq @set_clock_status_of_pseudo_status
1700          [1,3:
1701            @sym_eq @set_program_counter_status_of_pseudo_status %
1702          |2,4:
1703            @eq_f2 %
1704          ]
1705        |2,5:
1706          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1707          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
1708        |3,6:
1709          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1710          [1,5:
1711            @(subaddressing_mode_elim … acc_a) %
1712          |4,8:
1713            @eq_f2
1714            @(pose … (set_clock ????)) #status #status_refl
1715            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1716            [1,5:
1717              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1718              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
1719            |3,7:
1720              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1721              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1722            |2,6:
1723              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1724              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
1725            |4,8:
1726              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1727              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1728            ]
1729          |*:
1730            %
1731          ]
1732        ]
1733      |2,4:
1734        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1735        >EQP -P normalize nodelta
1736        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1737        whd in maps_assm:(??%%);
1738        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1739        [2,4: normalize nodelta #absurd destruct(absurd) ]
1740        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1741        [2,4: normalize nodelta #absurd destruct(absurd) ]
1742        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1743        whd in ⊢ (??%?);
1744        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1745        change with (set_arg_8 ????? = ?)
1746        @set_arg_8_status_of_pseudo_status try %
1747        >EQs >EQticks <instr_refl >addr_refl
1748        [1,4:
1749          @sym_eq @set_clock_status_of_pseudo_status
1750          [1,3:
1751            @sym_eq @set_program_counter_status_of_pseudo_status %
1752          |2,4:
1753            @eq_f2 %
1754          ]
1755        |2,5:
1756          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1757          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
1758        |3,6:
1759          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1760          [1,5:
1761            @(subaddressing_mode_elim … direct) #w %
1762          |4,8:
1763            @eq_f2
1764            @(pose … (set_clock ????)) #status #status_refl
1765            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1766            [1,5:
1767              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1768              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
1769            |3,7:
1770              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1771              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1772            |2,6:
1773              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1774              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
1775            |4,8:
1776              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1777              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1778            ]
1779          |*:
1780            %
1781          ]
1782        ]
1783      ]
1784    |2,4:
1785      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
1786      >EQP -P normalize nodelta
1787      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1788      whd in maps_assm:(??%%);
1789      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1790      [2,4: normalize nodelta #absurd destruct(absurd) ]
1791      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1792      [2,4: normalize nodelta #absurd destruct(absurd) ]
1793      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1794      whd in ⊢ (??%?);
1795      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1796      change with (set_flags ?????? = ?)
1797      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
1798      >EQs >EQticks <instr_refl >addr_refl
1799      @sym_eq @set_clock_status_of_pseudo_status %
1800    ]
1801  |31: (* XRL *)
1802    inversion addr
1803    [1:
1804      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1805      >EQP -P normalize nodelta
1806      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1807      whd in maps_assm:(??%%);
1808      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1809      [2: normalize nodelta #absurd destruct(absurd) ]
1810      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1811      [2: normalize nodelta #absurd destruct(absurd) ]
1812      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1813      whd in ⊢ (??%?);
1814      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1815      change with (set_arg_8 ????? = ?)
1816      @set_arg_8_status_of_pseudo_status try %
1817      >EQs >EQticks <instr_refl >addr_refl
1818      [1:
1819        @sym_eq @set_clock_status_of_pseudo_status
1820        [1:
1821          @sym_eq @set_program_counter_status_of_pseudo_status %
1822        |2:
1823          @eq_f2 %
1824        ]
1825      |2:
1826        @(subaddressing_mode_elim … acc_a) @I
1827      |3:
1828        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1829        [1:
1830          @(subaddressing_mode_elim … acc_a) %
1831        |4:
1832          @eq_f2
1833          @(pose … (set_clock ????)) #status #status_refl
1834          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1835          [1:
1836            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1837            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
1838          |3:
1839            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1840            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1841          |2:
1842            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1843            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
1844          |4:
1845            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1846            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1847          ]
1848        |*:
1849          %
1850        ]
1851      ]
1852    |2:
1853      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1854      >EQP -P normalize nodelta
1855      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1856      whd in maps_assm:(??%%);
1857      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1858      [2: normalize nodelta #absurd destruct(absurd) ]
1859      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1860      [2: normalize nodelta #absurd destruct(absurd) ]
1861      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1862      whd in ⊢ (??%?);
1863      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1864      change with (set_arg_8 ????? = ?)
1865      @set_arg_8_status_of_pseudo_status try %
1866      >EQs >EQticks <instr_refl >addr_refl
1867      [1:
1868        @sym_eq @set_clock_status_of_pseudo_status
1869        [1:
1870          @sym_eq @set_program_counter_status_of_pseudo_status %
1871        |2:
1872          @eq_f2 %
1873        ]
1874      |2:
1875        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1876        [1: @(subaddressing_mode_elim … direct) #w % ] %
1877      |3:
1878        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1879        [1:
1880          @(subaddressing_mode_elim … direct) #w %
1881        |4:
1882          @eq_f2
1883          @(pose … (set_clock ????)) #status #status_refl
1884          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1885          [1:
1886            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1887            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
1888          |3:
1889            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1890            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1891          |2:
1892            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1893            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
1894          |4:
1895            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1896            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1897          ]
1898        |*:
1899          %
1900        ]
1901      ]
1902    ]
1903  |32: (* CLR *)
1904    >EQP -P normalize nodelta lapply instr_refl
1905    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1906    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1907    whd in maps_assm:(??%%);
1908    [1,2:
1909      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1910      [2,4: normalize nodelta #absurd destruct(absurd) ]
1911      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1912      whd in ⊢ (??%?);
1913      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1914      [1:
1915        >EQs >EQticks <instr_refl
1916        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1917        @set_arg_1_status_of_pseudo_status try %
1918        [1:
1919          @(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) %
1920        |2:
1921          @(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) %
1922        ]         
1923      |2:
1924        >EQs >EQticks <instr_refl
1925        change with (set_arg_8 ??? ACC_A ? = ?) try %
1926        @set_arg_8_status_of_pseudo_status try %
1927        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1928      ]
1929    |3:
1930      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1931      whd in ⊢ (??%?);
1932      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1933      >EQs >EQticks <instr_refl
1934      change with (set_arg_1 ??? CARRY ? = ?) try %
1935      @set_arg_1_status_of_pseudo_status %
1936    ]
1937  |33: (* CPL *)
1938    >EQP -P normalize nodelta lapply instr_refl
1939    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1940    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1941    whd in maps_assm:(??%%);
1942    [1,2:
1943      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1944      [2,4: normalize nodelta #absurd destruct(absurd) ]
1945      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1946      whd in ⊢ (??%?);
1947      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1948      [1:
1949        >EQs >EQticks <instr_refl
1950        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1951        @set_arg_1_status_of_pseudo_status
1952        [1:
1953          @eq_f
1954          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1955          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1956          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
1957        |2:
1958          %
1959        |3:
1960          @(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) %
1961        |4:
1962          @(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) %
1963        ]       
1964      |2:
1965        >EQs >EQticks <instr_refl
1966        change with (set_8051_sfr ????? = ?)
1967        @set_8051_sfr_status_of_pseudo_status try %
1968        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
1969        normalize nodelta @eq_f
1970        @(pose … (set_clock ????)) #status #status_refl
1971        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1972        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
1973      ]
1974    |3:
1975      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1976      whd in ⊢ (??%?);
1977      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1978      >EQs >EQticks <instr_refl
1979      change with (set_arg_1 ??? CARRY ? = ?) try %
1980      @set_arg_1_status_of_pseudo_status try %
1981      @eq_f
1982      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1983      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
1984    ]
1985  |34,36: (* RL and RR *)
1986    (* XXX: work on the right hand side *)
1987    (* XXX: switch to the left hand side *)
1988    >EQP -P normalize nodelta
1989    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1990    whd in maps_assm:(??%%);
1991    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1992    [2,4: normalize nodelta #absurd destruct(absurd) ]
1993    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1994    whd in ⊢ (??%?);
1995    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1996    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1997    [2,4:
1998      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1999      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
2000      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
2001      %
2002    ]
2003    @sym_eq @set_clock_status_of_pseudo_status
2004    [2,4:
2005      %
2006    ]
2007    @sym_eq @set_program_counter_status_of_pseudo_status %
2008  |35,37: (* RLC and RRC *)
2009    (* XXX: work on the right hand side *)
2010    (* XXX: switch to the left hand side *)
2011    >EQP -P normalize nodelta
2012    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2013    whd in maps_assm:(??%%);
2014    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
2015    [2,4: normalize nodelta #absurd destruct(absurd) ]
2016    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2017    whd in ⊢ (??%?);
2018    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2019    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
2020    [2,4:
2021      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
2022      @eq_f2
2023      [1,3:
2024        @sym_eq
2025        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
2026        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
2027      |2,4:
2028        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
2029        @sym_eq @set_clock_status_of_pseudo_status %
2030      ]
2031    |1,3:
2032      @sym_eq @set_arg_1_status_of_pseudo_status try %
2033      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
2034      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
2035    ]
2036  |38: (* SWAP *)
2037    >EQP -P normalize nodelta
2038    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2039    whd in maps_assm:(??%%);
2040    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2041    [2: normalize nodelta #absurd destruct(absurd) ]
2042    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2043    whd in ⊢ (??%?);
2044    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2045    whd in ⊢ (??%?);
2046    @(pair_replace ?????????? p)
2047    [1:
2048      @eq_f normalize nodelta
2049      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
2050      @(get_8051_sfr_status_of_pseudo_status … M' … status)
2051      [1:
2052        >status_refl -status_refl
2053        @sym_eq @set_clock_status_of_pseudo_status
2054        >EQs >EQticks <instr_refl %
2055      |2:
2056        whd in ⊢ (??%?);
2057        >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2058      ]
2059    |2:
2060      @(pair_replace ?????????? p) normalize nodelta
2061      [1:
2062        %
2063      |2:
2064        @set_8051_sfr_status_of_pseudo_status
2065        [1:
2066          @sym_eq @set_clock_status_of_pseudo_status
2067          >EQs >EQticks <instr_refl %
2068        |2:
2069          whd in ⊢ (??%?);
2070          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2071        ]
2072      ]     
2073    ]
2074  |39: (* MOV *)
2075    >EQP -P normalize nodelta
2076    inversion addr
2077    [1:
2078      #addr' normalize nodelta
2079      inversion addr'
2080      [1:
2081        #addr'' normalize nodelta
2082        inversion addr''
2083        [1:
2084          #addr''' normalize nodelta
2085          inversion addr'''
2086          [1:
2087            #addr'''' normalize nodelta
2088            inversion addr''''
2089            [1:
2090              normalize nodelta #acc_a_others
2091              cases acc_a_others #acc_a #others
2092              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2093              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2094              whd in maps_assm:(??%%);
2095              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2096              [2: normalize nodelta #absurd destruct(absurd) ]
2097              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2098              [2: normalize nodelta #absurd destruct(absurd) ]
2099              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2100              whd in ⊢ (??%?);
2101              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2102              change with (set_arg_8 ????? = ?)
2103              @set_arg_8_status_of_pseudo_status try %
2104              [1:
2105                @sym_eq @set_clock_status_of_pseudo_status
2106                >EQs >EQticks <instr_refl >addr_refl %
2107              |2:
2108                @(subaddressing_mode_elim … acc_a) @I
2109              |3:
2110                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
2111                [1: @(subaddressing_mode_elim … acc_a) % ]
2112                >EQs >EQticks <instr_refl >addr_refl
2113                [1,2:
2114                  %
2115                |3:
2116                  @(pose … (set_clock ????)) #status #status_refl
2117                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
2118                  [1:
2119                    @sym_eq @set_clock_status_of_pseudo_status %
2120                  |2:
2121                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2122                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2123                  |3:
2124                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2125                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2126                  ]
2127                ]
2128              ]
2129            |2:
2130              #others_others' cases others_others' #others #others' normalize nodelta
2131              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2132              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2133              whd in maps_assm:(??%%);
2134              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2135              [2: normalize nodelta #absurd destruct(absurd) ]
2136              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2137              [2: normalize nodelta #absurd destruct(absurd) ]
2138              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2139              whd in ⊢ (??%?);
2140              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2141              change with (set_arg_8 ????? = ?)
2142              @set_arg_8_status_of_pseudo_status try %
2143              >EQs >EQticks <instr_refl >addr_refl try %
2144              [1:
2145                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2146                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2147              |2:
2148                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2149                [1:
2150                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2151                |2,3:
2152                  %
2153                |4:
2154                  @(pose … (set_clock ????)) #status #status_refl
2155                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
2156                  [1:
2157                    @sym_eq @set_clock_status_of_pseudo_status %
2158                  |2:
2159                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
2160                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2161                  |3:
2162                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
2163                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2164                  ]
2165                ]
2166              ]
2167            ]
2168          |2:
2169            #direct_others cases direct_others #direct #others
2170            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2171            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2172            whd in maps_assm:(??%%);
2173            inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2174            [2: normalize nodelta #absurd destruct(absurd) ]
2175            inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2176            [2: normalize nodelta #absurd destruct(absurd) ]
2177            normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2178            whd in ⊢ (??%?);
2179            <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2180            change with (set_arg_8 ????? = ?)
2181            @set_arg_8_status_of_pseudo_status try %
2182            >EQs >EQticks <instr_refl >addr_refl
2183            [1:
2184              @sym_eq @set_clock_status_of_pseudo_status %
2185            |2:
2186              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
2187              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2188            |3:
2189              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
2190              [1:
2191                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2192              |2,3:
2193                %
2194              |4:
2195                @(pose … (set_clock ????)) #status #status_refl
2196                @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2197                [1:
2198                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2199                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2200                |2:
2201                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2202                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2203                ]
2204              ]
2205            ]
2206          ]
2207        |2:
2208          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
2209          #addr_refl'' #addr_refl' #addr_refl
2210          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2211          whd in maps_assm:(??%%);
2212          inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2213          [2: normalize nodelta #absurd destruct(absurd) ]
2214          inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2215          [2: normalize nodelta #absurd destruct(absurd) ]
2216          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2217          whd in ⊢ (??%?);
2218          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2219          change with (set_arg_16 ????? = ?)
2220          @set_arg_16_status_of_pseudo_status try %
2221          >EQs >EQticks <instr_refl >addr_refl
2222          @sym_eq @set_clock_status_of_pseudo_status %
2223        ]
2224      |2:
2225        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
2226        #addr_refl' #addr_refl
2227        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2228        whd in maps_assm:(??%%);
2229        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2230        [2: normalize nodelta #absurd destruct(absurd) ]
2231        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2232        [2: normalize nodelta #absurd destruct(absurd) ]
2233        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2234        whd in ⊢ (??%?);
2235        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2236        change with (set_arg_1 ????? = ?)
2237        @set_arg_1_status_of_pseudo_status
2238        >EQs >EQticks <instr_refl >addr_refl try %
2239        [1:
2240          @sym_eq @(pose … (set_clock ????)) #status #status_refl
2241          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2242          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
2243        |2,3:
2244          @(subaddressing_mode_elim … carry) @I
2245        ]
2246      ]
2247    |2:
2248      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
2249      #addr_refl
2250      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2251      whd in maps_assm:(??%%);
2252      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2253      [2: normalize nodelta #absurd destruct(absurd) ]
2254      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2255      [2: normalize nodelta #absurd destruct(absurd) ]
2256      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2257      whd in ⊢ (??%?);
2258      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2259      change with (set_arg_1 ????? = ?)
2260      @set_arg_1_status_of_pseudo_status
2261      [1:
2262        >EQs >EQticks <instr_refl >addr_refl
2263        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
2264        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2265        @(subaddressing_mode_elim … carry) @I
2266      |2:
2267        >EQs >EQticks <instr_refl >addr_refl %
2268      |3,4:
2269        @(pose … (set_clock ????)) #status #status_refl
2270        [1:
2271          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
2272        |2:
2273          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
2274        ]
2275        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
2276        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
2277        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
2278      ]
2279    ]
2280  |40: (* MOVX *)
2281    >EQP -P normalize nodelta
2282    inversion addr
2283    [1:
2284      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
2285      #addr_refl
2286      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2287      whd in maps_assm:(??%%);
2288      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2289      [2: normalize nodelta #absurd destruct(absurd) ]
2290      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2291      [2: normalize nodelta #absurd destruct(absurd) ]
2292      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2293      whd in ⊢ (??%?);
2294      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2295      change with (set_arg_8 ????? = ?)
2296      @set_arg_8_status_of_pseudo_status try %
2297      >EQs >EQticks <instr_refl >addr_refl
2298      [1:
2299        @sym_eq @set_clock_status_of_pseudo_status %
2300      |2:
2301        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
2302        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2303      |3:
2304        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
2305        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
2306        @(pose … (set_clock ????)) #status #status_refl
2307        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2308        [1:
2309          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2310          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2311        |2:
2312          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2313          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2314        ]
2315      ]
2316    |2:
2317      #others_acc_a cases others_acc_a #others #acc_a
2318      #addr_refl
2319      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2320      whd in maps_assm:(??%%);
2321      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2322      [2: normalize nodelta #absurd destruct(absurd) ]
2323      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2324      [2: normalize nodelta #absurd destruct(absurd) ]
2325      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2326      whd in ⊢ (??%?);
2327      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2328      change with (set_arg_8 ????? = ?)
2329      @set_arg_8_status_of_pseudo_status
2330      >EQs >EQticks <instr_refl >addr_refl try %
2331      [1:
2332        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2333        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2334      |2:
2335        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2336        [1:
2337          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2338        |2,3:
2339          %
2340        |4:
2341          @(pose … (set_clock ????)) #status #status_refl
2342          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2343          [1:
2344            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
2345            [1: @(subaddressing_mode_elim … acc_a) % ] %
2346          |2:
2347            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
2348            [1: @(subaddressing_mode_elim … acc_a) % ] %
2349          ]
2350        ]
2351      ]
2352    ]
2353  |41: (* SETB *)
2354    >EQs >EQticks <instr_refl
2355    >EQP -P normalize nodelta
2356    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2357    whd in maps_assm:(??%%);
2358    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2359    [2: normalize nodelta #absurd destruct(absurd) ]
2360    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2361    whd in ⊢ (??%?);
2362    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2363    change with (set_arg_1 ????? = ?)
2364    @set_arg_1_status_of_pseudo_status try %
2365    [1:
2366      @(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)
2367    |2:
2368      @(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)
2369    ]
2370  |*)*)42: (* PUSH *)
2371    >EQP -P normalize nodelta lapply instr_refl
2372    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
2373    #sigma_increment_commutation
2374    whd in ⊢ (??%? → ?);
2375    @vsplit_elim #bit_one #seven_bits
2376    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
2377    cases bitone #bit_one_seven_bits_refl normalize nodelta
2378    [ @eq_bv_elim #seven_bits_refl normalize nodelta ]
2379    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
2380    whd in ⊢ (??%?);
2381    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2382    whd in match execute_1_0; normalize nodelta
2383    whd in match execute_1_preinstruction; normalize nodelta
2384    >bit_one_seven_bits_refl
2385    [ >seven_bits_refl
2386      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
2387    | @write_at_stack_pointer_status_of_pseudo_status_sfr_not_accA [1:assumption]
2388    | @write_at_stack_pointer_status_of_pseudo_status_low ]
2389    [1,3,5: @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
2390      try %
2391      change with (add ??? = ?); @eq_f2 try %
2392      @(pose … (set_clock ????)) #status #status_refl
2393      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
2394    |*: >EQs /demod nohyps/ >add_commutative % ]
2395  |43: (* POP *)
2396    cases daemon
2397  |44:
2398    >EQP -P normalize nodelta
2399    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2400    whd in maps_assm:(??%%);
2401    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2402    [2: normalize nodelta #absurd destruct(absurd) ]
2403    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2404    [2: normalize nodelta #absurd destruct(absurd) ]
2405    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2406    whd in ⊢ (??%?);
2407    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2408    change with (set_arg_8 ????? = ?)
2409    >EQs >EQticks <instr_refl
2410    @set_arg_8_status_of_pseudo_status try %
2411    [1:
2412      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2413      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
2414      @(pose … (set_clock ????)) #status #status_refl
2415      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2416      [1:
2417        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2418        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2419      |2:
2420        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2421        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2422      ]
2423    |2:
2424      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2425      [1:
2426        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2427      |*:
2428        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2429        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2430        whd in match sfr_8051_index; normalize nodelta
2431        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2432      ]
2433    |3:
2434      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2435      [1:
2436        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2437      |2:
2438        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2439        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2440        whd in match sfr_8051_index; normalize nodelta
2441        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2442      |3:
2443        @(pose … (set_clock ????)) #status #status_refl
2444        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2445        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2446      ]
2447    ]
2448  |45: (* XCHD *)
2449    >EQP -P normalize nodelta
2450    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2451    whd in maps_assm:(??%%);
2452    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2453    [2: normalize nodelta #absurd destruct(absurd) ]
2454    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2455    [2: normalize nodelta #absurd destruct(absurd) ]
2456    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2457    whd in ⊢ (??%?);
2458    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2459    whd in ⊢ (??%?);
2460    @(pair_replace ?????????? p) normalize nodelta
2461    >EQs >EQticks <instr_refl
2462    [1:
2463      @eq_f
2464      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2465      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2466      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2467    |2:
2468      @(pair_replace ?????????? p1) normalize nodelta
2469      >EQs >EQticks <instr_refl
2470      [1:
2471        @eq_f
2472        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2473        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2474        [1:
2475          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2476          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2477        |2:
2478          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2479          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2480        ]
2481      |2:
2482        @(pair_replace ?????????? p) normalize nodelta
2483        >EQs >EQticks <instr_refl
2484        [1:
2485          %
2486        |2:
2487          @(pair_replace ?????????? p1) normalize nodelta
2488          >EQs >EQticks <instr_refl
2489          [1:
2490            %
2491          |2:
2492            @set_arg_8_status_of_pseudo_status try %
2493            [1:
2494              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2495              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2496            |2:
2497              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2498              [1:
2499                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2500              |2:
2501                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2502                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2503                whd in match sfr_8051_index; normalize nodelta
2504                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2505              ]
2506            |3:
2507              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2508              [1:
2509                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2510              |2:
2511                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2512                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2513                whd in match sfr_8051_index; normalize nodelta
2514                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2515              ]
2516            ]
2517          ]
2518        ]
2519      ]
2520    ]
2521  |46: (* RET *)
2522    >EQP -P normalize nodelta
2523    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2524    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2525    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2526    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2527    [2: normalize nodelta #absurd destruct(absurd) ]
2528    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2529    [2: normalize nodelta #absurd destruct(absurd) ]
2530    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2531    whd in ⊢ (??%?);
2532    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2533    whd in ⊢ (??%?);
2534    @(pair_replace ?????????? p) normalize nodelta
2535    >EQs >EQticks <instr_refl
2536    [1:
2537      @eq_f3 try %
2538      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2539      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2540    |2:
2541      @(pair_replace ?????????? p1) normalize nodelta
2542      >EQs >EQticks <instr_refl
2543      [1:
2544        @eq_f3 try %
2545        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2546        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2547        [1:
2548          cases daemon
2549          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2550        |2:
2551          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2552          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2553          whd in match sfr_8051_index; normalize nodelta
2554          >get_index_v_set_index_hit
2555          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2556          cases daemon
2557          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2558        ]
2559      |2:
2560        cases daemon (* XXX *)
2561      ]
2562    ]
2563  |47: (* RETI *)
2564    cases daemon
2565  |48: (* NOP *)
2566    >EQP -P normalize nodelta
2567    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2568    whd in maps_assm:(??%%);
2569    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
2570    whd in ⊢ (??%?);
2571    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2572    change with (set_clock ???? = ?)
2573    @set_clock_status_of_pseudo_status %
2574  ]
2575qed.
Note: See TracBrowser for help on using the repository browser.