source: src/ASM/AssemblyProofSplit.ma @ 2256

Last change on this file since 2256 was 2256, checked in by mulligan, 7 years ago

MOV and MOVX cases complete

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