source: src/ASM/AssemblyProofSplit.ma @ 2260

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

Now we use the efficient lookup_address.

File size: 136.6 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      XXX
2251    ]
2252  |46: (* RET *)
2253    >EQP -P normalize nodelta
2254    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2255    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2256    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2257    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2258    [2: normalize nodelta #absurd destruct(absurd) ]
2259    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2260    [2: normalize nodelta #absurd destruct(absurd) ]
2261    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2262    whd in ⊢ (??%?);
2263    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2264    whd in ⊢ (??%?);
2265    @(pair_replace ?????????? p) normalize nodelta
2266    >EQs >EQticks <instr_refl
2267    [1:
2268      @eq_f3 try %
2269      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2270      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2271    |2:
2272      @(pair_replace ?????????? p1) normalize nodelta
2273      >EQs >EQticks <instr_refl
2274      [1:
2275        @eq_f3 try %
2276        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2277        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2278        [1:
2279          cases daemon
2280          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2281        |2:
2282          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2283          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2284          whd in match sfr_8051_index; normalize nodelta
2285          >get_index_v_set_index_hit
2286          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2287          cases daemon
2288          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2289        ]
2290      |2:
2291        cases daemon (* XXX *)
2292      ]
2293    ]
2294  |47: (* POP *)
2295  |48: (* XCH *)
2296    >EQP -P normalize nodelta
2297    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2298    whd in maps_assm:(??%%);
2299    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2300    [2: normalize nodelta #absurd destruct(absurd) ]
2301    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2302    [2: normalize nodelta #absurd destruct(absurd) ]
2303    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2304    whd in ⊢ (??%?);
2305    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2306    change with (set_arg_8 ????? = ?)
2307    >EQs >EQticks <instr_refl
2308    @set_arg_8_status_of_pseudo_status try %
2309    [1:
2310      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2311      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
2312      @(pose … (set_clock ????)) #status #status_refl
2313      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2314      [1:
2315        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2316        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2317      |2:
2318        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2319        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2320      ]
2321    |2:
2322      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2323      [1:
2324        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2325      |*:
2326        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2327        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2328        whd in match sfr_8051_index; normalize nodelta
2329        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2330      ]
2331    |3:
2332      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2333      [1:
2334        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2335      |2:
2336        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2337        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2338        whd in match sfr_8051_index; normalize nodelta
2339        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2340      |3:
2341        @(pose … (set_clock ????)) #status #status_refl
2342        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2343        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2344      ]
2345    ]
2346  |49: (* XCHD *)
2347    >EQP -P normalize nodelta
2348    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2349    whd in maps_assm:(??%%);
2350    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2351    [2: normalize nodelta #absurd destruct(absurd) ]
2352    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2353    [2: normalize nodelta #absurd destruct(absurd) ]
2354    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2355    whd in ⊢ (??%?);
2356    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2357    whd in ⊢ (??%?);
2358    @(pair_replace ?????????? p) normalize nodelta
2359    >EQs >EQticks <instr_refl
2360    [1:
2361      @eq_f
2362      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2363      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2364      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2365    |2:
2366      @(pair_replace ?????????? p1) normalize nodelta
2367      >EQs >EQticks <instr_refl
2368      [1:
2369        @eq_f
2370        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2371        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2372        [1:
2373          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2374          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2375        |2:
2376          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2377          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2378        ]
2379      |2:
2380        @(pair_replace ?????????? p) normalize nodelta
2381        >EQs >EQticks <instr_refl
2382        [1:
2383          %
2384        |2:
2385          @(pair_replace ?????????? p1) normalize nodelta
2386          >EQs >EQticks <instr_refl
2387          [1:
2388            %
2389          |2:
2390            @set_arg_8_status_of_pseudo_status try %
2391            [1:
2392              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2393              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2394            |2:
2395              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2396              [1:
2397                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2398              |2:
2399                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2400                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2401                whd in match sfr_8051_index; normalize nodelta
2402                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2403              ]
2404            |3:
2405              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2406              [1:
2407                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2408              |2:
2409                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2410                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2411                whd in match sfr_8051_index; normalize nodelta
2412                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2413              ]
2414            ]
2415          ]
2416        ]
2417      ]
2418    ]
2419  |50: (* RET *)
2420  |51: (* RETI *)
2421  |52: (* NOP *)
2422    >EQP -P normalize nodelta
2423    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2424    whd in maps_assm:(??%%);
2425    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
2426    whd in ⊢ (??%?);
2427    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2428    change with (set_clock ???? = ?)
2429    @set_clock_status_of_pseudo_status %
2430  ]
2431cases daemon
2432qed.
2433
2434(*
2435  (* XXX: work on the left hand side *)
2436  (* XXX: switch to the right hand side *)
2437  normalize nodelta >EQs -s >EQticks -ticks
2438  whd in ⊢ (??%%);
2439  (* XXX: finally, prove the equality using sigma commutation *)
2440  cases daemon
2441  |11,12: (* DIV *)
2442  (* XXX: work on the right hand side *)
2443  normalize nodelta in p;
2444  >p normalize nodelta
2445  (* XXX: switch to the left hand side *)
2446  -instr_refl >EQP -P normalize nodelta
2447  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2448  whd in ⊢ (??%?);
2449  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2450  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
2451  >(?: pose_assm = 0) normalize nodelta
2452  [2,4:
2453    <p >pose_refl
2454    cases daemon
2455  |1,3:
2456    (* XXX: switch to the right hand side *)
2457    >EQs -s >EQticks -ticks
2458    whd in ⊢ (??%%);
2459    (* XXX: finally, prove the equality using sigma commutation *)
2460    @split_eq_status try %
2461    cases daemon
2462  ]
2463  |13,14,15: (* DA *)
2464  (* XXX: work on the right hand side *)
2465  >p normalize nodelta
2466  >p1 normalize nodelta
2467  try (>p2 normalize nodelta
2468  try (>p3 normalize nodelta
2469  try (>p4 normalize nodelta
2470  try (>p5 normalize nodelta))))
2471  (* XXX: switch to the left hand side *)
2472  -instr_refl >EQP -P normalize nodelta
2473  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2474  whd in ⊢ (??%?);
2475  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2476  (* XXX: work on the left hand side *)
2477  @(pair_replace ?????????? p)
2478  [1,3,5:
2479    /demod/
2480    cases daemon
2481  |2,4,6:
2482    @(if_then_else_replace ???????? p1)
2483    [1,3,5:
2484      cases daemon
2485    |2,4:
2486      normalize nodelta
2487      @(pair_replace ?????????? p2)
2488      [1,3:
2489        cases daemon
2490      |2,4:
2491        normalize nodelta >p3 normalize nodelta
2492        >p4 normalize nodelta try >p5
2493      ]
2494    ]
2495  (* XXX: switch to the right hand side *)
2496  normalize nodelta >EQs -s >EQticks -ticks
2497  whd in ⊢ (??%%);
2498  (* XXX: finally, prove the equality using sigma commutation *)
2499  @split_eq_status try %
2500  cases daemon
2501  ]
2502  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
2503  (* XXX: work on the right hand side *)
2504  cases addr #addr' normalize nodelta
2505  [1,3:
2506    cases addr' #addr'' normalize nodelta
2507  ]
2508  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
2509  (* XXX: switch to the left hand side *)
2510  -instr_refl >EQP -P normalize nodelta
2511  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2512  whd in ⊢ (??%?);
2513  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2514  (* XXX: work on the left hand side *)
2515  (* XXX: switch to the right hand side *)
2516  normalize nodelta >EQs -s >EQticks -ticks
2517  whd in ⊢ (??%%);
2518  (* XXX: finally, prove the equality using sigma commutation *)
2519  cases daemon
2520  |47: (* MOV *)
2521  (* XXX: work on the right hand side *)
2522  cases addr -addr #addr normalize nodelta
2523  [1:
2524    cases addr #addr normalize nodelta
2525    [1:
2526      cases addr #addr normalize nodelta
2527      [1:
2528        cases addr #addr normalize nodelta
2529        [1:
2530          cases addr #addr normalize nodelta
2531        ]
2532      ]
2533    ]
2534  ]
2535  cases addr #lft #rgt normalize nodelta
2536  (* XXX: switch to the left hand side *)
2537  >EQP -P normalize nodelta
2538  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2539  whd in ⊢ (??%?);
2540  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2541  (* XXX: work on the left hand side *)
2542  (* XXX: switch to the right hand side *)
2543  normalize nodelta >EQs -s >EQticks -ticks
2544  whd in ⊢ (??%%);
2545  (* XXX: finally, prove the equality using sigma commutation *)
2546  cases daemon
2547  ]
2548*)
2549
2550
2551(*  [31,32: (* DJNZ *)
2552  (* XXX: work on the right hand side *)
2553  >p normalize nodelta >p1 normalize nodelta
2554  (* XXX: switch to the left hand side *)
2555  >EQP -P normalize nodelta
2556  #sigma_increment_commutation #maps_assm #fetch_many_assm
2557  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2558  <EQppc in fetch_many_assm;
2559  whd in match (short_jump_cond ??);
2560  @pair_elim #sj_possible #disp
2561  @pair_elim #result #flags #sub16_refl
2562  @pair_elim #upper #lower #vsplit_refl
2563  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2564  #sj_possible_pair destruct(sj_possible_pair)
2565  >p1 normalize nodelta
2566  [1,3:
2567    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2568    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2569    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2570    whd in ⊢ (??%?);
2571    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2572    lapply maps_assm whd in ⊢ (??%? → ?);
2573    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
2574    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
2575    (* XXX: work on the left hand side *)
2576    @(pair_replace ?????????? p) normalize nodelta
2577    [1,3:
2578      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
2579      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]
2580      >(get_arg_8_set_program_counter … true addr1)
2581      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]
2582      @get_arg_8_pseudo_addressing_mode_ok assumption
2583    |2,4:
2584      >p1 normalize nodelta >EQs
2585      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
2586      >set_program_counter_status_of_pseudo_status
2587       whd in ⊢ (??%%);
2588      @split_eq_status
2589      [1,10:
2590        whd in ⊢ (??%%); >set_arg_8_set_program_counter
2591        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2592        >low_internal_ram_set_program_counter
2593        [1:
2594          >low_internal_ram_set_program_counter
2595          (* XXX: ??? *)
2596        |2:
2597          >low_internal_ram_set_clock
2598          (* XXX: ??? *)
2599        ]
2600      |2,11:
2601        whd in ⊢ (??%%); >set_arg_8_set_program_counter
2602        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2603        >high_internal_ram_set_program_counter
2604        [1:
2605          >high_internal_ram_set_program_counter
2606          (* XXX: ??? *)
2607        |2:
2608          >high_internal_ram_set_clock
2609          (* XXX: ??? *)
2610        ]
2611      |3,12:
2612        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
2613        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2614        >(external_ram_set_arg_8 ??? addr1)
2615        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2616      |4,13:
2617        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
2618        [1:
2619          >program_counter_set_program_counter
2620          >set_arg_8_set_program_counter
2621          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2622          >set_clock_set_program_counter >program_counter_set_program_counter
2623          change with (add ??? = ?)
2624          (* XXX: ??? *)
2625        |2:
2626          >set_arg_8_set_program_counter
2627          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2628          >program_counter_set_program_counter
2629          >set_arg_8_set_program_counter
2630          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2631          >set_clock_set_program_counter >program_counter_set_program_counter
2632          >sigma_increment_commutation <EQppc
2633          whd in match (assembly_1_pseudoinstruction ??????);
2634          whd in match (expand_pseudo_instruction ??????);
2635          (* XXX: ??? *)
2636        ]
2637      |5,14:
2638        whd in match (special_function_registers_8051 ???);
2639        [1:
2640          >special_function_registers_8051_set_program_counter
2641          >special_function_registers_8051_set_clock
2642          >set_arg_8_set_program_counter in ⊢ (???%);
2643          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2644          >special_function_registers_8051_set_program_counter
2645          >set_arg_8_set_program_counter
2646          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2647          >special_function_registers_8051_set_program_counter
2648          @special_function_registers_8051_set_arg_8 assumption
2649        |2:
2650          >special_function_registers_8051_set_clock
2651          >set_arg_8_set_program_counter
2652          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2653          >set_arg_8_set_program_counter
2654          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2655          >special_function_registers_8051_set_program_counter
2656          >special_function_registers_8051_set_program_counter
2657          @special_function_registers_8051_set_arg_8 assumption
2658        ]
2659      |6,15:
2660        whd in match (special_function_registers_8052 ???);
2661        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
2662        [1:
2663          >set_arg_8_set_program_counter
2664          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2665          >set_arg_8_set_program_counter
2666          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2667          >special_function_registers_8052_set_program_counter
2668          >special_function_registers_8052_set_program_counter
2669          @special_function_registers_8052_set_arg_8 assumption
2670        |2:
2671          whd in ⊢ (??%%);
2672          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
2673        ]
2674        (* XXX: we need special_function_registers_8052_set_arg_8 *)
2675      |7,16:
2676        whd in match (p1_latch ???);
2677        whd in match (p1_latch ???) in ⊢ (???%);
2678        (* XXX: we need p1_latch_8052_set_arg_8 *)
2679      |8,17:
2680        whd in match (p3_latch ???);
2681        whd in match (p3_latch ???) in ⊢ (???%);
2682        (* XXX: we need p3_latch_8052_set_arg_8 *)
2683      |9:
2684        >clock_set_clock
2685        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
2686        >EQticks <instr_refl @eq_f2
2687        [1:
2688          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
2689        |2:
2690          (* XXX: we need clock_set_arg_8 *)
2691        ]
2692      |18:
2693      ]
2694    ]
2695    (* XXX: switch to the right hand side *)
2696    normalize nodelta >EQs -s >EQticks -ticks
2697    cases (¬ eq_bv ???) normalize nodelta
2698    whd in ⊢ (??%%);
2699    (* XXX: finally, prove the equality using sigma commutation *)
2700    @split_eq_status try %
2701    [1,2,3,19,20,21,28,29,30:
2702      cases daemon (* XXX: axioms as above *)
2703    |4,13,22,31:
2704    |5,14,23,32:
2705    |6,15,24,33:
2706    |7,16,25,34:
2707    |8,17,26,35:
2708      whd in ⊢ (??%%);maps_assm
2709     
2710    |9,18,27,36:
2711      whd in ⊢ (??%%);
2712      whd in match (ticks_of_instruction ?); <instr_refl
2713      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
2714    ]
2715  |2,4:
2716    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2717    [2, 4:
2718      cases daemon (* XXX: !!! *)
2719    ]
2720    normalize nodelta >EQppc
2721    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2722    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2723    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2724    #fetch_many_assm whd in fetch_many_assm; %{2}
2725    change with (execute_1 ?? = ?)
2726    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2727    #status_after_1 #EQstatus_after_1
2728    <(?: ? = status_after_1)
2729    [3,6:
2730      >EQstatus_after_1 in ⊢ (???%);
2731      whd in ⊢ (???%);
2732      [1:
2733        <fetch_refl in ⊢ (???%);
2734      |2:
2735        <fetch_refl in ⊢ (???%);
2736      ]
2737      whd in ⊢ (???%);
2738      @(pair_replace ?????????? p)
2739      [1,3:
2740        cases daemon
2741      |2,4:
2742        normalize nodelta
2743        whd in match (addr_of_relative ????);
2744        cases (¬ eq_bv ???) normalize nodelta
2745        >set_clock_mk_Status_commutation
2746        whd in ⊢ (???%);
2747        change with (add ???) in match (\snd (half_add ???));
2748        >set_arg_8_set_program_counter in ⊢ (???%);
2749        [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2750        >program_counter_set_program_counter in ⊢ (???%);
2751        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2752        [2,4,6,8:
2753          >bitvector_of_nat_sign_extension_equivalence
2754          [1,3,5,7:
2755            >EQintermediate_pc' %
2756          |*:
2757            repeat @le_S_S @le_O_n
2758          ]
2759        ]
2760        [1,3: % ]
2761      ]
2762    |1,4:
2763      skip
2764    ]
2765    [3,4:
2766      -status_after_1
2767      @(pose … (execute_1 ? (mk_PreStatus …)))
2768      #status_after_1 #EQstatus_after_1
2769      <(?: ? = status_after_1)
2770      [3,6:
2771        >EQstatus_after_1 in ⊢ (???%);
2772        whd in ⊢ (???%);
2773        (* XXX: matita bug with patterns across multiple goals *)
2774        [1:
2775          <fetch_refl'' in ⊢ (???%);
2776        |2:
2777          <fetch_refl'' in ⊢ (???%);
2778        ]
2779        [2: % |1: whd in ⊢ (???%); % ]
2780      |1,4:
2781        skip
2782      ]
2783      -status_after_1 whd in ⊢ (??%?);
2784      (* XXX: switch to the right hand side *)
2785      normalize nodelta >EQs -s >EQticks -ticks
2786      normalize nodelta whd in ⊢ (??%%);
2787    ]
2788    (* XXX: finally, prove the equality using sigma commutation *)
2789    @split_eq_status try %
2790    whd in ⊢ (??%%);
2791    cases daemon
2792  ]
2793  |30: (* CJNE *)
2794  (* XXX: work on the right hand side *)
2795  cases addr1 -addr1 #addr1 normalize nodelta
2796  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
2797  (* XXX: switch to the left hand side *)
2798  >EQP -P normalize nodelta
2799  #sigma_increment_commutation #maps_assm #fetch_many_assm
2800
2801  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2802  <EQppc in fetch_many_assm;
2803  whd in match (short_jump_cond ??);
2804  @pair_elim #sj_possible #disp
2805  @pair_elim #result #flags #sub16_refl
2806  @pair_elim #upper #lower #vsplit_refl
2807  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2808  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2809  [1,3:
2810    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2811    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2812    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2813    whd in ⊢ (??%?);
2814    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2815    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
2816    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
2817    @(if_then_else_replace ???????? eq_bv_refl)
2818    [1,3,5,7:
2819      cases daemon
2820    |2,4,6,8:
2821      (* XXX: switch to the right hand side *)
2822      normalize nodelta >EQs -s >EQticks -ticks
2823      whd in ⊢ (??%%);
2824      (* XXX: finally, prove the equality using sigma commutation *)
2825      @split_eq_status try %
2826      [3,7,11,15:
2827        whd in ⊢ (??%?);
2828        [1,3:
2829          cases daemon
2830        |2,4:
2831          cases daemon
2832        ]
2833      ]
2834      cases daemon (* XXX *)
2835    ]
2836  |2,4:
2837    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2838    [2, 4:
2839      cases daemon (* XXX: !!! *)
2840    ]
2841    normalize nodelta >EQppc
2842    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2843    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2844    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2845    #fetch_many_assm whd in fetch_many_assm; %{2}
2846    change with (execute_1 ?? = ?)
2847    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2848    #status_after_1 #EQstatus_after_1
2849    <(?: ? = status_after_1)
2850    [2,5:
2851      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
2852    |3,6:
2853      >EQstatus_after_1 in ⊢ (???%);
2854      whd in ⊢ (???%);
2855      [1: <fetch_refl in ⊢ (???%);
2856      |2: <fetch_refl in ⊢ (???%);
2857      ]
2858      whd in ⊢ (???%);
2859      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
2860      whd in ⊢ (???%);
2861      whd in match (addr_of_relative ????);
2862      change with (add ???) in match (\snd (half_add ???));
2863      >set_clock_set_program_counter in ⊢ (???%);
2864      >program_counter_set_program_counter in ⊢ (???%);
2865      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2866      [2,4,6,8:
2867        >bitvector_of_nat_sign_extension_equivalence
2868        [1,3,5,7:
2869          >EQintermediate_pc' %
2870        |*:
2871          repeat @le_S_S @le_O_n
2872        ]
2873      |1,5:
2874        %
2875      ]
2876    |1,4: skip
2877    ]
2878    [1,2,3,4:
2879      -status_after_1
2880      @(pose … (execute_1 ? (mk_PreStatus …)))
2881      #status_after_1 #EQstatus_after_1
2882      <(?: ? = status_after_1)
2883      [3,6,9,12:
2884        >EQstatus_after_1 in ⊢ (???%);
2885        whd in ⊢ (???%);
2886        (* XXX: matita bug with patterns across multiple goals *)
2887        [1: <fetch_refl'' in ⊢ (???%);
2888        |2: <fetch_refl'' in ⊢ (???%);
2889        |3: <fetch_refl'' in ⊢ (???%);
2890        |4: <fetch_refl'' in ⊢ (???%);
2891        ] %
2892      |1,4,7,10:
2893        skip
2894      ]
2895      -status_after_1 whd in ⊢ (??%?);
2896      (* XXX: switch to the right hand side *)
2897      normalize nodelta >EQs -s >EQticks -ticks
2898      whd in ⊢ (??%%);
2899    ]
2900    (* XXX: finally, prove the equality using sigma commutation *)
2901    @split_eq_status try %
2902    cases daemon
2903  ]
2904  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
2905  (* XXX: work on the right hand side *)
2906  >p normalize nodelta
2907  (* XXX: switch to the left hand side *)
2908  >EQP -P normalize nodelta
2909  #sigma_increment_commutation #maps_assm #fetch_many_assm
2910 
2911  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2912  <EQppc in fetch_many_assm;
2913  whd in match (short_jump_cond ??);
2914  @pair_elim #sj_possible #disp
2915  @pair_elim #result #flags #sub16_refl
2916  @pair_elim #upper #lower #vsplit_refl
2917  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2918  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2919  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2920    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2921    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2922    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2923    whd in ⊢ (??%?);
2924    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2925    (* XXX: work on the left hand side *)
2926    @(if_then_else_replace ???????? p) normalize nodelta
2927    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2928      cases daemon
2929    ]
2930    (* XXX: switch to the right hand side *)
2931    normalize nodelta >EQs -s >EQticks -ticks
2932    whd in ⊢ (??%%);
2933    (* XXX: finally, prove the equality using sigma commutation *)
2934    @split_eq_status try %
2935    cases daemon
2936  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2937    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2938    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2939      cases daemon (* XXX: !!! *)
2940    ]
2941    normalize nodelta >EQppc
2942    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2943    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2944    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2945    #fetch_many_assm whd in fetch_many_assm; %{2}
2946    change with (execute_1 ?? = ?)
2947    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2948    #status_after_1 #EQstatus_after_1
2949    <(?: ? = status_after_1)
2950    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
2951      >EQstatus_after_1 in ⊢ (???%);
2952      whd in ⊢ (???%);
2953      [1: <fetch_refl in ⊢ (???%);
2954      |2: <fetch_refl in ⊢ (???%);
2955      |3: <fetch_refl in ⊢ (???%);
2956      |4: <fetch_refl in ⊢ (???%);
2957      |5: <fetch_refl in ⊢ (???%);
2958      |6: <fetch_refl in ⊢ (???%);
2959      |7: <fetch_refl in ⊢ (???%);
2960      |8: <fetch_refl in ⊢ (???%);
2961      |9: <fetch_refl in ⊢ (???%);
2962      |10: <fetch_refl in ⊢ (???%);
2963      |11: <fetch_refl in ⊢ (???%);
2964      |12: <fetch_refl in ⊢ (???%);
2965      |13: <fetch_refl in ⊢ (???%);
2966      |14: <fetch_refl in ⊢ (???%);
2967      ]
2968      whd in ⊢ (???%);
2969      @(if_then_else_replace ???????? p)
2970      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2971        cases daemon
2972      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2973        normalize nodelta
2974        whd in match (addr_of_relative ????);
2975        >set_clock_mk_Status_commutation
2976        [9,10:
2977          (* XXX: demodulation not working in this case *)
2978          >program_counter_set_arg_1 in ⊢ (???%);
2979          >program_counter_set_program_counter in ⊢ (???%);
2980        |*:
2981          /demod/
2982        ]
2983        whd in ⊢ (???%);
2984        change with (add ???) in match (\snd (half_add ???));
2985        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2986        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2987          >bitvector_of_nat_sign_extension_equivalence
2988          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2989            >EQintermediate_pc' %
2990          |*:
2991            repeat @le_S_S @le_O_n
2992          ]
2993        ]
2994        %
2995      ]
2996    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
2997      skip
2998    ]
2999    -status_after_1
3000    @(pose … (execute_1 ? (mk_PreStatus …)))
3001    #status_after_1 #EQstatus_after_1
3002    <(?: ? = status_after_1)
3003    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
3004      >EQstatus_after_1 in ⊢ (???%);
3005      whd in ⊢ (???%);
3006      (* XXX: matita bug with patterns across multiple goals *)
3007      [1: <fetch_refl'' in ⊢ (???%);
3008      |2: <fetch_refl' in ⊢ (???%);
3009      |3: <fetch_refl'' in ⊢ (???%);
3010      |4: <fetch_refl' in ⊢ (???%);
3011      |5: <fetch_refl'' in ⊢ (???%);
3012      |6: <fetch_refl' in ⊢ (???%);
3013      |7: <fetch_refl'' in ⊢ (???%);
3014      |8: <fetch_refl' in ⊢ (???%);
3015      |9: <fetch_refl'' in ⊢ (???%);
3016      |10: <fetch_refl' in ⊢ (???%);
3017      |11: <fetch_refl'' in ⊢ (???%);
3018      |12: <fetch_refl' in ⊢ (???%);
3019      |13: <fetch_refl'' in ⊢ (???%);
3020      |14: <fetch_refl' in ⊢ (???%);
3021      ]
3022      whd in ⊢ (???%);
3023      [9,10:
3024      |*:
3025        /demod/
3026      ] %
3027    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
3028      skip
3029    ]
3030    -status_after_1 whd in ⊢ (??%?);
3031    (* XXX: switch to the right hand side *)
3032    normalize nodelta >EQs -s >EQticks -ticks
3033    whd in ⊢ (??%%);
3034    (* XXX: finally, prove the equality using sigma commutation *)
3035    @split_eq_status try %
3036    [3,11,19,27,36,53,61:
3037      >program_counter_set_program_counter >set_clock_mk_Status_commutation
3038      [5: >program_counter_set_program_counter ]
3039      >EQaddr_of normalize nodelta
3040      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
3041      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
3042      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
3043      >create_label_cost_refl normalize nodelta #relevant @relevant
3044      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
3045      try assumption whd in match instruction_has_label; normalize nodelta
3046      <instr_refl normalize nodelta %
3047    |7,15,23,31,45,57,65:
3048      >set_clock_mk_Status_commutation >program_counter_set_program_counter
3049      whd in ⊢ (??%?); normalize nodelta
3050      >EQppc in fetch_many_assm; #fetch_many_assm
3051      [5:
3052        >program_counter_set_arg_1 >program_counter_set_program_counter
3053      ]
3054      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
3055      <bitvector_of_nat_sign_extension_equivalence
3056      [1,3,5,7,9,11,13:
3057        whd in ⊢ (???%); cases (half_add ???) normalize //
3058      |2,4,6,8,10,12,14:
3059        @assembly1_lt_128
3060        @le_S_S @le_O_n
3061      ]
3062    |*:
3063      cases daemon
3064    ]
3065  ]
3066  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
3067  (* XXX: work on the right hand side *)
3068  lapply (subaddressing_modein ???)
3069  <EQaddr normalize nodelta #irrelevant
3070  try (>p normalize nodelta)
3071  try (>p1 normalize nodelta)
3072  (* XXX: switch to the left hand side *)
3073  >EQP -P normalize nodelta
3074  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
3075  whd in ⊢ (??%?);
3076  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
3077  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
3078  (* XXX: work on the left hand side *)
3079  [1,2,3,4,5:
3080    generalize in ⊢ (??(???(?%))?);
3081  |6,7,8,9,10,11:
3082    generalize in ⊢ (??(???(?%))?);
3083  |12:
3084    generalize in ⊢ (??(???(?%))?);
3085  ]
3086  <EQaddr normalize nodelta #irrelevant
3087  try @(jmpair_as_replace ?????????? p)
3088  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
3089  (* XXX: switch to the right hand side *)
3090  normalize nodelta >EQs -s >EQticks -ticks
3091  whd in ⊢ (??%%);
3092  (* XXX: finally, prove the equality using sigma commutation *)
3093  try @split_eq_status try % whd in ⊢ (??%%);
3094  cases daemon
3095  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
3096  (* XXX: work on the right hand side *)
3097  >p normalize nodelta
3098  try (>p1 normalize nodelta)
3099  (* XXX: switch to the left hand side *)
3100  -instr_refl >EQP -P normalize nodelta
3101  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
3102  whd in ⊢ (??%?);
3103  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
3104  (* XXX: work on the left hand side *)
3105  @(pair_replace ?????????? p)
3106  [1,3,5,7,9,11,13,15,17:
3107    >set_clock_set_program_counter >set_clock_mk_Status_commutation
3108    >set_program_counter_mk_Status_commutation >clock_set_program_counter
3109    cases daemon
3110  |14,16,18:
3111    normalize nodelta
3112    @(pair_replace ?????????? p1)
3113    [1,3,5:
3114      >set_clock_mk_Status_commutation
3115      cases daemon
3116    ]
3117  ]
3118  (* XXX: switch to the right hand side *)
3119  normalize nodelta >EQs -s >EQticks -ticks
3120  whd in ⊢ (??%%);
3121  (* XXX: finally, prove the equality using sigma commutation *)
3122  try @split_eq_status try %
3123  cases daemon *)
Note: See TracBrowser for help on using the repository browser.