source: src/ASM/AssemblyProofSplit.ma @ 2261

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

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