source: src/ASM/AssemblyProofSplit.ma @ 2262

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

Changes from today.

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) try %
1034          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
1035        ]
1036      ]
1037    ]
1038  |4: (* INC *)
1039    (* XXX: work on the right hand side *)
1040    (* XXX: switch to the left hand side *)
1041    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
1042    @(subaddressing_mode_elim … addr) normalize nodelta
1043    [1:
1044      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1045      whd in maps_assm:(??%%);
1046      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1047      [2: normalize nodelta #absurd destruct(absurd) ]
1048      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1049      whd in ⊢ (??%?);
1050      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1051      whd in ⊢ (??%?);
1052      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
1053      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
1054      [1:
1055        @eq_f2 try %
1056        @(pose … (set_clock ????)) #status #status_refl
1057        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1058        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
1059      |2:
1060        @set_arg_8_status_of_pseudo_status try %
1061        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
1062      ]
1063    |2:
1064      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1065      whd in maps_assm:(??%%);
1066      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1067      [2: normalize nodelta #absurd destruct(absurd) ]
1068      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1069      whd in ⊢ (??%?);
1070      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1071      whd in ⊢ (??%?);
1072      @let_pair_in_status_of_pseudo_status
1073      [1:
1074        @eq_f2 try %
1075        @(pose … (set_clock ????)) #status #status_refl
1076        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1077        >EQs >EQticks
1078        [1:
1079          @sym_eq @set_clock_status_of_pseudo_status %
1080        |2:
1081          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1082        |3:
1083          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
1084        ]
1085      |2:
1086        #carry #result
1087        @sym_eq @set_arg_8_status_of_pseudo_status try %
1088        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1089      ]
1090    |3:
1091      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1092      whd in maps_assm:(??%%);
1093      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1094      [2: normalize nodelta #absurd destruct(absurd) ]
1095      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1096      whd in ⊢ (??%?);
1097      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1098      whd in ⊢ (??%?);
1099      @let_pair_in_status_of_pseudo_status
1100      [1:
1101        @eq_f2 try %
1102        @(pose … (set_clock ????)) #status #status_refl
1103        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1104        >EQs >EQticks
1105        [1:
1106          @sym_eq @set_clock_status_of_pseudo_status %
1107        |2:
1108          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
1109        |3:
1110          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
1111        ]
1112      |2:
1113        #carry #result
1114        @sym_eq @set_arg_8_status_of_pseudo_status try %
1115        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
1116      ]
1117    |4:
1118      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1119      whd in maps_assm:(??%%);
1120      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1121      [2: normalize nodelta #absurd destruct(absurd) ]
1122      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1123      whd in ⊢ (??%?);
1124      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1125      whd in ⊢ (??%?);
1126      @let_pair_in_status_of_pseudo_status
1127      [1:
1128        @eq_f2 try %
1129        @(pose … (set_clock ????)) #status #status_refl
1130        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1131        >EQs >EQticks
1132        [1:
1133          @sym_eq @set_clock_status_of_pseudo_status %
1134        |2:
1135          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
1136        |3:
1137          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1138        ]
1139      |2:
1140        #carry #result
1141        @sym_eq @set_arg_8_status_of_pseudo_status try %
1142        [1:
1143          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1144        |2:
1145          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
1146        ]
1147      ]
1148    |5:
1149      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1150      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1151      whd in ⊢ (??%?);
1152      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1153      whd in ⊢ (??%?);
1154      @let_pair_in_status_of_pseudo_status
1155      [1:
1156        @eq_f2 try %
1157        @(pose … (set_clock ????)) #status #status_refl
1158        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
1159        >EQs >EQticks %
1160      |2:
1161        #carry #bl
1162        @sym_eq @let_pair_in_status_of_pseudo_status
1163        [1:
1164          @eq_f3 try %
1165          @(pose … (set_clock ????)) #status #status_refl
1166          @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
1167          >EQs >EQticks %
1168        |2:
1169          #carry' #bu
1170          @sym_eq @set_8051_sfr_status_of_pseudo_status %
1171        ]
1172      ]
1173    ]
1174  |5: (* DEC *)
1175    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
1176    @(subaddressing_mode_elim … addr) normalize nodelta
1177    [1:
1178      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1179      whd in maps_assm:(??%%);
1180      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1181      [2: normalize nodelta #absurd destruct(absurd) ]
1182      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1183      whd in ⊢ (??%?);
1184      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1185      whd in ⊢ (??%?);
1186      @let_pair_in_status_of_pseudo_status
1187      [1:
1188        @eq_f3 try %
1189        @(pose … (set_clock ????)) #status #status_refl
1190        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1191        >EQs >EQticks try %
1192        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1193      |2:
1194        #result #flags
1195        @sym_eq @set_arg_8_status_of_pseudo_status try %
1196        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1197      ]
1198    |2:
1199      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1200      whd in maps_assm:(??%%);
1201      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1202      [2: normalize nodelta #absurd destruct(absurd) ]
1203      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1204      whd in ⊢ (??%?);
1205      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1206      whd in ⊢ (??%?);
1207      @let_pair_in_status_of_pseudo_status
1208      [1:
1209        @eq_f3 try %
1210        @(pose … (set_clock ????)) #status #status_refl
1211        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1212        >EQs >EQticks try %
1213        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1214      |2:
1215        #result #flags
1216        @sym_eq @set_arg_8_status_of_pseudo_status try %
1217        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
1218      ]
1219    |3:
1220      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1221      whd in maps_assm:(??%%);
1222      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1223      [2: normalize nodelta #absurd destruct(absurd) ]
1224      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1225      whd in ⊢ (??%?);
1226      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1227      whd in ⊢ (??%?);
1228      @let_pair_in_status_of_pseudo_status
1229      [1:
1230        @eq_f3 try %
1231        @(pose … (set_clock ????)) #status #status_refl
1232        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1233        >EQs >EQticks try %
1234        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
1235      |2:
1236        #result #flags
1237        @sym_eq @set_arg_8_status_of_pseudo_status try %
1238        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
1239      ]
1240    |4:
1241      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1242      whd in maps_assm:(??%%);
1243      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1244      [2: normalize nodelta #absurd destruct(absurd) ]
1245      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1246      whd in ⊢ (??%?);
1247      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1248      whd in ⊢ (??%?);
1249      @let_pair_in_status_of_pseudo_status
1250      [1:
1251        @eq_f3 try %
1252        @(pose … (set_clock ????)) #status #status_refl
1253        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1254        >EQs >EQticks try %
1255        [1:
1256          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
1257        |2:
1258          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1259        ]
1260      |2:
1261        #result #flags
1262        @sym_eq @set_arg_8_status_of_pseudo_status try %
1263        [1:
1264          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
1265        |2:
1266          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
1267        ]
1268      ]
1269    ]
1270  |6: (* MUL *)
1271    (* XXX: work on the right hand side *)
1272    (* XXX: switch to the left hand side *)
1273    >EQP -P normalize nodelta
1274    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1275    whd in maps_assm:(??%%);
1276    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1277    [2: normalize nodelta #absurd destruct(absurd) ]
1278    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1279    [2: normalize nodelta #absurd destruct(absurd) ]
1280    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1281    whd in ⊢ (??%?);
1282    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1283    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1284    [2:
1285      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
1286      @sym_eq
1287      [1:
1288        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1289        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
1290        %
1291      |2:
1292        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
1293      ]
1294    ]
1295    @sym_eq @set_8051_sfr_status_of_pseudo_status
1296    [2:
1297      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
1298      @eq_f @eq_f2 try % @eq_f2 @eq_f
1299      @sym_eq
1300      [1:
1301        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1302        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1303      |2:
1304        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
1305      ]
1306    ]
1307    @sym_eq @set_clock_status_of_pseudo_status
1308    [2:
1309      @eq_f %
1310    ]
1311    @sym_eq @set_program_counter_status_of_pseudo_status %
1312  |7,8: (* DIV *)
1313    (* XXX: work on the right hand side *)
1314    (* XXX: switch to the left hand side *)
1315    >EQP -P normalize nodelta
1316    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1317    whd in maps_assm:(??%%);
1318    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1319    [2,4: normalize nodelta #absurd destruct(absurd) ]
1320    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1321    [2,4: normalize nodelta #absurd destruct(absurd) ]
1322    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1323    whd in ⊢ (??%?);
1324    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1325    whd in ⊢ (??%?); normalize nodelta
1326    @(match_nat_status_of_pseudo_status M' cm sigma policy)
1327    [1,4:
1328      @eq_f
1329      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1330      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1331    |2,5:
1332      @sym_eq @set_flags_status_of_pseudo_status %
1333    |3,6:
1334      #n @sym_eq @set_flags_status_of_pseudo_status try %
1335      @sym_eq @set_8051_sfr_status_of_pseudo_status
1336      [1,3:
1337        @sym_eq @set_8051_sfr_status_of_pseudo_status try %
1338        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
1339        @eq_f @eq_f2 try % @eq_f
1340        @(pose … (set_clock ????)) #status #status_refl
1341        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1342        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1343      |2,4:
1344        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
1345        @(pose … (set_clock ????)) #status #status_refl
1346        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1347        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1348      ]
1349    ]
1350  |9: (* DA *)
1351    (* XXX: work on the right hand side *)
1352    (* XXX: switch to the left hand side *)
1353    >EQP -P normalize nodelta
1354    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1355    whd in maps_assm:(??%%);
1356    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1357    [2: normalize nodelta #absurd destruct(absurd) ]
1358    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1359    whd in ⊢ (??%?);
1360    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1361    whd in ⊢ (??%?); normalize nodelta
1362    @(pair_replace ?????????? p)
1363    [1:
1364      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1365      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1366      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1367    |2:
1368      @(pair_replace ?????????? p)
1369      [1:
1370        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1371      |2:
1372        @(if_then_else_replace ???????? p1) normalize nodelta
1373        [1:
1374          cases (gtb ? 9)
1375          [1:
1376            %
1377          |2:
1378            change with (get_ac_flag ??? = get_ac_flag ???)
1379            @(get_ac_flag_status_of_pseudo_status M')
1380            @sym_eq @set_clock_status_of_pseudo_status
1381            >EQs >EQticks <instr_refl %
1382          ]
1383        |2:
1384          @(if_then_else_replace ???????? p1) normalize nodelta try %
1385          @(pair_replace ?????????? p2)
1386          [1:
1387            @eq_f3 try % normalize nodelta
1388            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1389            whd in ⊢ (??%?);
1390            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1391          |2:
1392            @(pair_replace ?????????? p2) try %
1393            @(pair_replace ?????????? p3) try %
1394            @(pair_replace ?????????? p3) try %
1395            @(if_then_else_replace ???????? p4) try % normalize nodelta
1396            @(if_then_else_replace ???????? p4) try % normalize nodelta
1397            @(pair_replace ?????????? p5) try %
1398            @(pair_replace ?????????? p5) try %
1399            @set_flags_status_of_pseudo_status try %
1400            [1:
1401              @eq_f @(get_ac_flag_status_of_pseudo_status M')
1402              @sym_eq @set_8051_sfr_status_of_pseudo_status
1403              [1:
1404                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1405              |2:
1406                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1407              ]
1408            |2:
1409              @(get_ov_flag_status_of_pseudo_status M')
1410              @sym_eq @set_8051_sfr_status_of_pseudo_status
1411              [1:
1412                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1413              |2:
1414                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1415              ]
1416            |3:
1417              @sym_eq @set_8051_sfr_status_of_pseudo_status
1418              [1:
1419                @sym_eq @set_clock_status_of_pseudo_status
1420                [1:
1421                  >EQs
1422                  @sym_eq @set_program_counter_status_of_pseudo_status %
1423                |2:
1424                  >EQs >EQticks <instr_refl %
1425                ]
1426              |2:
1427                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1428              ]
1429            ]
1430          ]
1431        ]
1432      ]
1433    ]
1434  |10: (* DA *)
1435    (* XXX: work on the right hand side *)
1436    (* XXX: switch to the left hand side *)
1437    >EQP -P normalize nodelta
1438    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1439    whd in maps_assm:(??%%);
1440    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1441    [2: normalize nodelta #absurd destruct(absurd) ]
1442    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1443    whd in ⊢ (??%?);
1444    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1445    whd in ⊢ (??%?); normalize nodelta
1446    @(pair_replace ?????????? p)
1447    [1:
1448      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1449      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1450      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1451    |2:
1452      @(pair_replace ?????????? p)
1453      [1:
1454        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1455      |2:
1456        @(if_then_else_replace ???????? p1) normalize nodelta
1457        [1:
1458          cases (gtb ? 9)
1459          [1:
1460            %
1461          |2:
1462            change with (get_ac_flag ??? = get_ac_flag ???)
1463            @(get_ac_flag_status_of_pseudo_status M')
1464            @sym_eq @set_clock_status_of_pseudo_status
1465            >EQs >EQticks <instr_refl %
1466          ]
1467        |2:
1468          @(if_then_else_replace ???????? p1) normalize nodelta try %
1469          @(pair_replace ?????????? p2)
1470          [1:
1471            @eq_f3 try % normalize nodelta
1472            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1473            whd in ⊢ (??%?);
1474            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1475          |2:
1476            @(pair_replace ?????????? p2) try %
1477            @(pair_replace ?????????? p3) try %
1478            @(pair_replace ?????????? p3) try %
1479            @(if_then_else_replace ???????? p4) try % normalize nodelta
1480            @(if_then_else_replace ???????? p4) try % normalize nodelta
1481            @set_clock_status_of_pseudo_status
1482            [1:
1483              >EQs
1484              @sym_eq @set_program_counter_status_of_pseudo_status %
1485            |2:
1486              >EQs >EQticks <instr_refl %
1487            ]
1488          ]
1489        ]
1490      ]
1491    ]
1492  |11: (* DA *)
1493    (* XXX: work on the right hand side *)
1494    (* XXX: switch to the left hand side *)
1495    >EQP -P normalize nodelta
1496    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1497    whd in maps_assm:(??%%);
1498    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1499    [2: normalize nodelta #absurd destruct(absurd) ]
1500    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1501    whd in ⊢ (??%?);
1502    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1503    whd in ⊢ (??%?); normalize nodelta
1504    @(pair_replace ?????????? p)
1505    [1:
1506      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1507      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1508      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1509    |2:
1510      @(pair_replace ?????????? p)
1511      [1:
1512        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1513      |2:
1514        @(if_then_else_replace ???????? p1) normalize nodelta
1515        [1:
1516          cases (gtb ? 9)
1517          [1:
1518            %
1519          |2:
1520            change with (get_ac_flag ??? = get_ac_flag ???)
1521            @(get_ac_flag_status_of_pseudo_status M')
1522            @sym_eq @set_clock_status_of_pseudo_status
1523            >EQs >EQticks <instr_refl %
1524          ]
1525        |2:
1526          @(if_then_else_replace ???????? p1) normalize nodelta try %
1527          @set_clock_status_of_pseudo_status
1528          [1:
1529            >EQs
1530            @sym_eq @set_program_counter_status_of_pseudo_status %
1531          |2:
1532            >EQs >EQticks <instr_refl %
1533          ]
1534        ]
1535      ]
1536    ]
1537  |12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
1538    cases daemon
1539  |29,30: (* ANL and ORL *)
1540    inversion addr
1541    [1,3:
1542      *
1543      [1,3:
1544        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1545        >EQP -P normalize nodelta
1546        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1547        whd in maps_assm:(??%%);
1548        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1549        [2,4: normalize nodelta #absurd destruct(absurd) ]
1550        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1551        [2,4: normalize nodelta #absurd destruct(absurd) ]
1552        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1553        whd in ⊢ (??%?);
1554        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1555        change with (set_arg_8 ????? = ?)
1556        @set_arg_8_status_of_pseudo_status try %
1557        >EQs >EQticks <instr_refl >addr_refl
1558        [1,4:
1559          @sym_eq @set_clock_status_of_pseudo_status
1560          [1,3:
1561            @sym_eq @set_program_counter_status_of_pseudo_status %
1562          |2,4:
1563            @eq_f2 %
1564          ]
1565        |2,5:
1566          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1567          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
1568        |3,6:
1569          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1570          [1,5:
1571            @(subaddressing_mode_elim … acc_a) %
1572          |4,8:
1573            @eq_f2
1574            @(pose … (set_clock ????)) #status #status_refl
1575            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1576            [1,5:
1577              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1578              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
1579            |3,7:
1580              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1581              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1582            |2,6:
1583              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1584              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
1585            |4,8:
1586              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1587              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1588            ]
1589          |*:
1590            %
1591          ]
1592        ]
1593      |2,4:
1594        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1595        >EQP -P normalize nodelta
1596        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1597        whd in maps_assm:(??%%);
1598        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1599        [2,4: normalize nodelta #absurd destruct(absurd) ]
1600        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1601        [2,4: normalize nodelta #absurd destruct(absurd) ]
1602        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1603        whd in ⊢ (??%?);
1604        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1605        change with (set_arg_8 ????? = ?)
1606        @set_arg_8_status_of_pseudo_status try %
1607        >EQs >EQticks <instr_refl >addr_refl
1608        [1,4:
1609          @sym_eq @set_clock_status_of_pseudo_status
1610          [1,3:
1611            @sym_eq @set_program_counter_status_of_pseudo_status %
1612          |2,4:
1613            @eq_f2 %
1614          ]
1615        |2,5:
1616          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1617          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
1618        |3,6:
1619          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1620          [1,5:
1621            @(subaddressing_mode_elim … direct) #w %
1622          |4,8:
1623            @eq_f2
1624            @(pose … (set_clock ????)) #status #status_refl
1625            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1626            [1,5:
1627              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1628              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
1629            |3,7:
1630              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1631              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1632            |2,6:
1633              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1634              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
1635            |4,8:
1636              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1637              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1638            ]
1639          |*:
1640            %
1641          ]
1642        ]
1643      ]
1644    |2,4:
1645      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
1646      >EQP -P normalize nodelta
1647      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1648      whd in maps_assm:(??%%);
1649      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1650      [2,4: normalize nodelta #absurd destruct(absurd) ]
1651      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1652      [2,4: normalize nodelta #absurd destruct(absurd) ]
1653      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1654      whd in ⊢ (??%?);
1655      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1656      change with (set_flags ?????? = ?)
1657      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
1658      >EQs >EQticks <instr_refl >addr_refl
1659      @sym_eq @set_clock_status_of_pseudo_status %
1660    ]
1661  |31: (* XRL *)
1662    inversion addr
1663    [1:
1664      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1665      >EQP -P normalize nodelta
1666      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1667      whd in maps_assm:(??%%);
1668      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1669      [2: normalize nodelta #absurd destruct(absurd) ]
1670      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1671      [2: normalize nodelta #absurd destruct(absurd) ]
1672      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1673      whd in ⊢ (??%?);
1674      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1675      change with (set_arg_8 ????? = ?)
1676      @set_arg_8_status_of_pseudo_status try %
1677      >EQs >EQticks <instr_refl >addr_refl
1678      [1:
1679        @sym_eq @set_clock_status_of_pseudo_status
1680        [1:
1681          @sym_eq @set_program_counter_status_of_pseudo_status %
1682        |2:
1683          @eq_f2 %
1684        ]
1685      |2:
1686        @(subaddressing_mode_elim … acc_a) @I
1687      |3:
1688        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1689        [1:
1690          @(subaddressing_mode_elim … acc_a) %
1691        |4:
1692          @eq_f2
1693          @(pose … (set_clock ????)) #status #status_refl
1694          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1695          [1:
1696            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1697            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
1698          |3:
1699            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1700            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1701          |2:
1702            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1703            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
1704          |4:
1705            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1706            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1707          ]
1708        |*:
1709          %
1710        ]
1711      ]
1712    |2:
1713      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1714      >EQP -P normalize nodelta
1715      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1716      whd in maps_assm:(??%%);
1717      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1718      [2: normalize nodelta #absurd destruct(absurd) ]
1719      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1720      [2: normalize nodelta #absurd destruct(absurd) ]
1721      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1722      whd in ⊢ (??%?);
1723      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1724      change with (set_arg_8 ????? = ?)
1725      @set_arg_8_status_of_pseudo_status try %
1726      >EQs >EQticks <instr_refl >addr_refl
1727      [1:
1728        @sym_eq @set_clock_status_of_pseudo_status
1729        [1:
1730          @sym_eq @set_program_counter_status_of_pseudo_status %
1731        |2:
1732          @eq_f2 %
1733        ]
1734      |2:
1735        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1736        [1: @(subaddressing_mode_elim … direct) #w % ] %
1737      |3:
1738        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1739        [1:
1740          @(subaddressing_mode_elim … direct) #w %
1741        |4:
1742          @eq_f2
1743          @(pose … (set_clock ????)) #status #status_refl
1744          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1745          [1:
1746            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1747            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
1748          |3:
1749            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1750            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1751          |2:
1752            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1753            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
1754          |4:
1755            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1756            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1757          ]
1758        |*:
1759          %
1760        ]
1761      ]
1762    ]
1763  |32: (* CLR *)
1764    >EQP -P normalize nodelta lapply instr_refl
1765    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1766    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1767    whd in maps_assm:(??%%);
1768    [1,2:
1769      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1770      [2,4: normalize nodelta #absurd destruct(absurd) ]
1771      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1772      whd in ⊢ (??%?);
1773      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1774      [1:
1775        >EQs >EQticks <instr_refl
1776        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1777        @set_arg_1_status_of_pseudo_status try %
1778        [1:
1779          @(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) %
1780        |2:
1781          @(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) %
1782        ]         
1783      |2:
1784        >EQs >EQticks <instr_refl
1785        change with (set_arg_8 ??? ACC_A ? = ?) try %
1786        @set_arg_8_status_of_pseudo_status try %
1787        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1788      ]
1789    |3:
1790      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1791      whd in ⊢ (??%?);
1792      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1793      >EQs >EQticks <instr_refl
1794      change with (set_arg_1 ??? CARRY ? = ?) try %
1795      @set_arg_1_status_of_pseudo_status %
1796    ]
1797  |33: (* CPL *)
1798    >EQP -P normalize nodelta lapply instr_refl
1799    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1800    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1801    whd in maps_assm:(??%%);
1802    [1,2:
1803      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1804      [2,4: normalize nodelta #absurd destruct(absurd) ]
1805      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1806      whd in ⊢ (??%?);
1807      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1808      [1:
1809        >EQs >EQticks <instr_refl
1810        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1811        @set_arg_1_status_of_pseudo_status
1812        [1:
1813          @eq_f
1814          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1815          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1816          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
1817        |2:
1818          %
1819        |3:
1820          @(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) %
1821        |4:
1822          @(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) %
1823        ]       
1824      |2:
1825        >EQs >EQticks <instr_refl
1826        change with (set_8051_sfr ????? = ?)
1827        @set_8051_sfr_status_of_pseudo_status try %
1828        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
1829        normalize nodelta @eq_f
1830        @(pose … (set_clock ????)) #status #status_refl
1831        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1832        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
1833      ]
1834    |3:
1835      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1836      whd in ⊢ (??%?);
1837      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1838      >EQs >EQticks <instr_refl
1839      change with (set_arg_1 ??? CARRY ? = ?) try %
1840      @set_arg_1_status_of_pseudo_status try %
1841      @eq_f
1842      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1843      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
1844    ]
1845  |34,36: (* RL and RR *)
1846    (* XXX: work on the right hand side *)
1847    (* XXX: switch to the left hand side *)
1848    >EQP -P normalize nodelta
1849    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1850    whd in maps_assm:(??%%);
1851    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1852    [2,4: normalize nodelta #absurd destruct(absurd) ]
1853    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1854    whd in ⊢ (??%?);
1855    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1856    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1857    [2,4:
1858      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1859      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1860      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1861      %
1862    ]
1863    @sym_eq @set_clock_status_of_pseudo_status
1864    [2,4:
1865      %
1866    ]
1867    @sym_eq @set_program_counter_status_of_pseudo_status %
1868  |35,37: (* RLC and RRC *)
1869    (* XXX: work on the right hand side *)
1870    (* XXX: switch to the left hand side *)
1871    >EQP -P normalize nodelta
1872    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1873    whd in maps_assm:(??%%);
1874    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1875    [2,4: normalize nodelta #absurd destruct(absurd) ]
1876    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1877    whd in ⊢ (??%?);
1878    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1879    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1880    [2,4:
1881      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1882      @eq_f2
1883      [1,3:
1884        @sym_eq
1885        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1886        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1887      |2,4:
1888        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
1889        @sym_eq @set_clock_status_of_pseudo_status %
1890      ]
1891    |1,3:
1892      @sym_eq @set_arg_1_status_of_pseudo_status try %
1893      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1894      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1895    ]
1896  |38: (* SWAP *)
1897    >EQP -P normalize nodelta
1898    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1899    whd in maps_assm:(??%%);
1900    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1901    [2: normalize nodelta #absurd destruct(absurd) ]
1902    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1903    whd in ⊢ (??%?);
1904    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1905    whd in ⊢ (??%?);
1906    @(pair_replace ?????????? p)
1907    [1:
1908      @eq_f normalize nodelta
1909      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
1910      @(get_8051_sfr_status_of_pseudo_status … M' … status)
1911      [1:
1912        >status_refl -status_refl
1913        @sym_eq @set_clock_status_of_pseudo_status
1914        >EQs >EQticks <instr_refl %
1915      |2:
1916        whd in ⊢ (??%?);
1917        >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1918      ]
1919    |2:
1920      @(pair_replace ?????????? p) normalize nodelta
1921      [1:
1922        %
1923      |2:
1924        @set_8051_sfr_status_of_pseudo_status
1925        [1:
1926          @sym_eq @set_clock_status_of_pseudo_status
1927          >EQs >EQticks <instr_refl %
1928        |2:
1929          whd in ⊢ (??%?);
1930          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1931        ]
1932      ]     
1933    ]
1934  |39: (* MOV *)
1935    >EQP -P normalize nodelta
1936    inversion addr
1937    [1:
1938      #addr' normalize nodelta
1939      inversion addr'
1940      [1:
1941        #addr'' normalize nodelta
1942        inversion addr''
1943        [1:
1944          #addr''' normalize nodelta
1945          inversion addr'''
1946          [1:
1947            #addr'''' normalize nodelta
1948            inversion addr''''
1949            [1:
1950              normalize nodelta #acc_a_others
1951              cases acc_a_others #acc_a #others
1952              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1953              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1954              whd in maps_assm:(??%%);
1955              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1956              [2: normalize nodelta #absurd destruct(absurd) ]
1957              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1958              [2: normalize nodelta #absurd destruct(absurd) ]
1959              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1960              whd in ⊢ (??%?);
1961              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1962              change with (set_arg_8 ????? = ?)
1963              @set_arg_8_status_of_pseudo_status try %
1964              [1:
1965                @sym_eq @set_clock_status_of_pseudo_status
1966                >EQs >EQticks <instr_refl >addr_refl %
1967              |2:
1968                @(subaddressing_mode_elim … acc_a) @I
1969              |3:
1970                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1971                [1: @(subaddressing_mode_elim … acc_a) % ]
1972                >EQs >EQticks <instr_refl >addr_refl
1973                [1,2:
1974                  %
1975                |3:
1976                  @(pose … (set_clock ????)) #status #status_refl
1977                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1978                  [1:
1979                    @sym_eq @set_clock_status_of_pseudo_status %
1980                  |2:
1981                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1982                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1983                  |3:
1984                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1985                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1986                  ]
1987                ]
1988              ]
1989            |2:
1990              #others_others' cases others_others' #others #others' normalize nodelta
1991              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1992              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1993              whd in maps_assm:(??%%);
1994              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1995              [2: normalize nodelta #absurd destruct(absurd) ]
1996              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1997              [2: normalize nodelta #absurd destruct(absurd) ]
1998              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1999              whd in ⊢ (??%?);
2000              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2001              change with (set_arg_8 ????? = ?)
2002              @set_arg_8_status_of_pseudo_status try %
2003              >EQs >EQticks <instr_refl >addr_refl try %
2004              [1:
2005                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2006                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2007              |2:
2008                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2009                [1:
2010                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2011                |2,3:
2012                  %
2013                |4:
2014                  @(pose … (set_clock ????)) #status #status_refl
2015                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
2016                  [1:
2017                    @sym_eq @set_clock_status_of_pseudo_status %
2018                  |2:
2019                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
2020                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2021                  |3:
2022                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
2023                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2024                  ]
2025                ]
2026              ]
2027            ]
2028          |2:
2029            #direct_others cases direct_others #direct #others
2030            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
2031            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2032            whd in maps_assm:(??%%);
2033            inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2034            [2: normalize nodelta #absurd destruct(absurd) ]
2035            inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2036            [2: normalize nodelta #absurd destruct(absurd) ]
2037            normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2038            whd in ⊢ (??%?);
2039            <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2040            change with (set_arg_8 ????? = ?)
2041            @set_arg_8_status_of_pseudo_status try %
2042            >EQs >EQticks <instr_refl >addr_refl
2043            [1:
2044              @sym_eq @set_clock_status_of_pseudo_status %
2045            |2:
2046              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
2047              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2048            |3:
2049              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
2050              [1:
2051                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2052              |2,3:
2053                %
2054              |4:
2055                @(pose … (set_clock ????)) #status #status_refl
2056                @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2057                [1:
2058                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2059                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2060                |2:
2061                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2062                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2063                ]
2064              ]
2065            ]
2066          ]
2067        |2:
2068          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
2069          #addr_refl'' #addr_refl' #addr_refl
2070          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2071          whd in maps_assm:(??%%);
2072          inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2073          [2: normalize nodelta #absurd destruct(absurd) ]
2074          inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2075          [2: normalize nodelta #absurd destruct(absurd) ]
2076          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2077          whd in ⊢ (??%?);
2078          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2079          change with (set_arg_16 ????? = ?)
2080          @set_arg_16_status_of_pseudo_status try %
2081          >EQs >EQticks <instr_refl >addr_refl
2082          @sym_eq @set_clock_status_of_pseudo_status %
2083        ]
2084      |2:
2085        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
2086        #addr_refl' #addr_refl
2087        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2088        whd in maps_assm:(??%%);
2089        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2090        [2: normalize nodelta #absurd destruct(absurd) ]
2091        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2092        [2: normalize nodelta #absurd destruct(absurd) ]
2093        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2094        whd in ⊢ (??%?);
2095        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2096        change with (set_arg_1 ????? = ?)
2097        @set_arg_1_status_of_pseudo_status
2098        >EQs >EQticks <instr_refl >addr_refl try %
2099        [1:
2100          @sym_eq @(pose … (set_clock ????)) #status #status_refl
2101          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2102          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
2103        |2,3:
2104          @(subaddressing_mode_elim … carry) @I
2105        ]
2106      ]
2107    |2:
2108      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
2109      #addr_refl
2110      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2111      whd in maps_assm:(??%%);
2112      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2113      [2: normalize nodelta #absurd destruct(absurd) ]
2114      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2115      [2: normalize nodelta #absurd destruct(absurd) ]
2116      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2117      whd in ⊢ (??%?);
2118      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2119      change with (set_arg_1 ????? = ?)
2120      @set_arg_1_status_of_pseudo_status
2121      [1:
2122        >EQs >EQticks <instr_refl >addr_refl
2123        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
2124        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2125        @(subaddressing_mode_elim … carry) @I
2126      |2:
2127        >EQs >EQticks <instr_refl >addr_refl %
2128      |3,4:
2129        @(pose … (set_clock ????)) #status #status_refl
2130        [1:
2131          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
2132        |2:
2133          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
2134        ]
2135        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
2136        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
2137        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
2138      ]
2139    ]
2140  |40: (* MOVX *)
2141    >EQP -P normalize nodelta
2142    inversion addr
2143    [1:
2144      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
2145      #addr_refl
2146      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2147      whd in maps_assm:(??%%);
2148      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2149      [2: normalize nodelta #absurd destruct(absurd) ]
2150      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2151      [2: normalize nodelta #absurd destruct(absurd) ]
2152      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2153      whd in ⊢ (??%?);
2154      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2155      change with (set_arg_8 ????? = ?)
2156      @set_arg_8_status_of_pseudo_status try %
2157      >EQs >EQticks <instr_refl >addr_refl
2158      [1:
2159        @sym_eq @set_clock_status_of_pseudo_status %
2160      |2:
2161        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
2162        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2163      |3:
2164        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
2165        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
2166        @(pose … (set_clock ????)) #status #status_refl
2167        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2168        [1:
2169          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
2170          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2171        |2:
2172          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
2173          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2174        ]
2175      ]
2176    |2:
2177      #others_acc_a cases others_acc_a #others #acc_a
2178      #addr_refl
2179      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2180      whd in maps_assm:(??%%);
2181      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2182      [2: normalize nodelta #absurd destruct(absurd) ]
2183      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2184      [2: normalize nodelta #absurd destruct(absurd) ]
2185      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2186      whd in ⊢ (??%?);
2187      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2188      change with (set_arg_8 ????? = ?)
2189      @set_arg_8_status_of_pseudo_status
2190      >EQs >EQticks <instr_refl >addr_refl try %
2191      [1:
2192        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
2193        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2194      |2:
2195        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
2196        [1:
2197          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2198        |2,3:
2199          %
2200        |4:
2201          @(pose … (set_clock ????)) #status #status_refl
2202          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2203          [1:
2204            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
2205            [1: @(subaddressing_mode_elim … acc_a) % ] %
2206          |2:
2207            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
2208            [1: @(subaddressing_mode_elim … acc_a) % ] %
2209          ]
2210        ]
2211      ]
2212    ]
2213  |41: (* SETB *)
2214    >EQs >EQticks <instr_refl
2215    >EQP -P normalize nodelta
2216    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2217    whd in maps_assm:(??%%);
2218    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2219    [2: normalize nodelta #absurd destruct(absurd) ]
2220    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2221    whd in ⊢ (??%?);
2222    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2223    change with (set_arg_1 ????? = ?)
2224    @set_arg_1_status_of_pseudo_status try %
2225    [1:
2226      @(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)
2227    |2:
2228      @(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)
2229    ]
2230  |42: (* PUSH *)
2231    >EQP -P normalize nodelta lapply instr_refl
2232    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
2233    #sigma_increment_commutation
2234    whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta
2235    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
2236    whd in ⊢ (??%?);
2237    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2238    whd in ⊢ (??%?);
2239    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
2240    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
2241    [1:
2242      @eq_f2 try %
2243      @(pose … (set_clock ????)) #status #status_refl
2244      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try %
2245      @sym_eq @set_clock_status_of_pseudo_status
2246      >EQs >EQticks <instr_refl %
2247    |2:
2248      >EQs >EQticks <instr_refl
2249      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
2250    ]
2251  |*)43: (* POP *)
2252    cases daemon
2253  |44:
2254    >EQP -P normalize nodelta
2255    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2256    whd in maps_assm:(??%%);
2257    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2258    [2: normalize nodelta #absurd destruct(absurd) ]
2259    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2260    [2: normalize nodelta #absurd destruct(absurd) ]
2261    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2262    whd in ⊢ (??%?);
2263    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2264    change with (set_arg_8 ????? = ?)
2265    >EQs >EQticks <instr_refl
2266    @set_arg_8_status_of_pseudo_status try %
2267    [1:
2268      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2269      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
2270      @(pose … (set_clock ????)) #status #status_refl
2271      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2272      [1:
2273        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2274        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2275      |2:
2276        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2277        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2278      ]
2279    |2:
2280      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2281      [1:
2282        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2283      |*:
2284        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2285        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2286        whd in match sfr_8051_index; normalize nodelta
2287        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2288      ]
2289    |3:
2290      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2291      [1:
2292        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2293      |2:
2294        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2295        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2296        whd in match sfr_8051_index; normalize nodelta
2297        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2298      |3:
2299        @(pose … (set_clock ????)) #status #status_refl
2300        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2301        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2302      ]
2303    ]
2304  |45: (* XCHD *)
2305    >EQP -P normalize nodelta
2306    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2307    whd in maps_assm:(??%%);
2308    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2309    [2: normalize nodelta #absurd destruct(absurd) ]
2310    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2311    [2: normalize nodelta #absurd destruct(absurd) ]
2312    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2313    whd in ⊢ (??%?);
2314    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2315    whd in ⊢ (??%?);
2316    @(pair_replace ?????????? p) normalize nodelta
2317    >EQs >EQticks <instr_refl
2318    [1:
2319      @eq_f
2320      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2321      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2322      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2323    |2:
2324      @(pair_replace ?????????? p1) normalize nodelta
2325      >EQs >EQticks <instr_refl
2326      [1:
2327        @eq_f
2328        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2329        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2330        [1:
2331          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2332          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2333        |2:
2334          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2335          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2336        ]
2337      |2:
2338        @(pair_replace ?????????? p) normalize nodelta
2339        >EQs >EQticks <instr_refl
2340        [1:
2341          %
2342        |2:
2343          @(pair_replace ?????????? p1) normalize nodelta
2344          >EQs >EQticks <instr_refl
2345          [1:
2346            %
2347          |2:
2348            @set_arg_8_status_of_pseudo_status try %
2349            [1:
2350              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2351              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2352            |2:
2353              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2354              [1:
2355                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2356              |2:
2357                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2358                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2359                whd in match sfr_8051_index; normalize nodelta
2360                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2361              ]
2362            |3:
2363              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2364              [1:
2365                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2366              |2:
2367                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2368                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2369                whd in match sfr_8051_index; normalize nodelta
2370                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2371              ]
2372            ]
2373          ]
2374        ]
2375      ]
2376    ]
2377  |46: (* RET *)
2378    >EQP -P normalize nodelta
2379    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2380    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2381    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2382    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2383    [2: normalize nodelta #absurd destruct(absurd) ]
2384    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2385    [2: normalize nodelta #absurd destruct(absurd) ]
2386    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2387    whd in ⊢ (??%?);
2388    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2389    whd in ⊢ (??%?);
2390    @(pair_replace ?????????? p) normalize nodelta
2391    >EQs >EQticks <instr_refl
2392    [1:
2393      @eq_f3 try %
2394      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2395      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2396    |2:
2397      @(pair_replace ?????????? p1) normalize nodelta
2398      >EQs >EQticks <instr_refl
2399      [1:
2400        @eq_f3 try %
2401        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2402        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2403        [1:
2404          cases daemon
2405          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2406        |2:
2407          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2408          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2409          whd in match sfr_8051_index; normalize nodelta
2410          >get_index_v_set_index_hit
2411          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2412          cases daemon
2413          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2414        ]
2415      |2:
2416        cases daemon (* XXX *)
2417      ]
2418    ]
2419  |47: (* RETI *)
2420    cases daemon
2421  |48: (* 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  ]
2431qed.
2432
2433(*
2434  (* XXX: work on the left hand side *)
2435  (* XXX: switch to the right hand side *)
2436  normalize nodelta >EQs -s >EQticks -ticks
2437  whd in ⊢ (??%%);
2438  (* XXX: finally, prove the equality using sigma commutation *)
2439  cases daemon
2440  |11,12: (* DIV *)
2441  (* XXX: work on the right hand side *)
2442  normalize nodelta in p;
2443  >p normalize nodelta
2444  (* XXX: switch to the left hand side *)
2445  -instr_refl >EQP -P normalize nodelta
2446  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2447  whd in ⊢ (??%?);
2448  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2449  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
2450  >(?: pose_assm = 0) normalize nodelta
2451  [2,4:
2452    <p >pose_refl
2453    cases daemon
2454  |1,3:
2455    (* XXX: switch to the right hand side *)
2456    >EQs -s >EQticks -ticks
2457    whd in ⊢ (??%%);
2458    (* XXX: finally, prove the equality using sigma commutation *)
2459    @split_eq_status try %
2460    cases daemon
2461  ]
2462  |13,14,15: (* DA *)
2463  (* XXX: work on the right hand side *)
2464  >p normalize nodelta
2465  >p1 normalize nodelta
2466  try (>p2 normalize nodelta
2467  try (>p3 normalize nodelta
2468  try (>p4 normalize nodelta
2469  try (>p5 normalize nodelta))))
2470  (* XXX: switch to the left hand side *)
2471  -instr_refl >EQP -P normalize nodelta
2472  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2473  whd in ⊢ (??%?);
2474  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2475  (* XXX: work on the left hand side *)
2476  @(pair_replace ?????????? p)
2477  [1,3,5:
2478    /demod/
2479    cases daemon
2480  |2,4,6:
2481    @(if_then_else_replace ???????? p1)
2482    [1,3,5:
2483      cases daemon
2484    |2,4:
2485      normalize nodelta
2486      @(pair_replace ?????????? p2)
2487      [1,3:
2488        cases daemon
2489      |2,4:
2490        normalize nodelta >p3 normalize nodelta
2491        >p4 normalize nodelta try >p5
2492      ]
2493    ]
2494  (* XXX: switch to the right hand side *)
2495  normalize nodelta >EQs -s >EQticks -ticks
2496  whd in ⊢ (??%%);
2497  (* XXX: finally, prove the equality using sigma commutation *)
2498  @split_eq_status try %
2499  cases daemon
2500  ]
2501  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
2502  (* XXX: work on the right hand side *)
2503  cases addr #addr' normalize nodelta
2504  [1,3:
2505    cases addr' #addr'' normalize nodelta
2506  ]
2507  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
2508  (* XXX: switch to the left hand side *)
2509  -instr_refl >EQP -P normalize nodelta
2510  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2511  whd in ⊢ (??%?);
2512  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2513  (* XXX: work on the left hand side *)
2514  (* XXX: switch to the right hand side *)
2515  normalize nodelta >EQs -s >EQticks -ticks
2516  whd in ⊢ (??%%);
2517  (* XXX: finally, prove the equality using sigma commutation *)
2518  cases daemon
2519  |47: (* MOV *)
2520  (* XXX: work on the right hand side *)
2521  cases addr -addr #addr normalize nodelta
2522  [1:
2523    cases addr #addr normalize nodelta
2524    [1:
2525      cases addr #addr normalize nodelta
2526      [1:
2527        cases addr #addr normalize nodelta
2528        [1:
2529          cases addr #addr normalize nodelta
2530        ]
2531      ]
2532    ]
2533  ]
2534  cases addr #lft #rgt normalize nodelta
2535  (* XXX: switch to the left hand side *)
2536  >EQP -P normalize nodelta
2537  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2538  whd in ⊢ (??%?);
2539  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2540  (* XXX: work on the left hand side *)
2541  (* XXX: switch to the right hand side *)
2542  normalize nodelta >EQs -s >EQticks -ticks
2543  whd in ⊢ (??%%);
2544  (* XXX: finally, prove the equality using sigma commutation *)
2545  cases daemon
2546  ]
2547*)
2548
2549
2550(*  [31,32: (* DJNZ *)
2551  (* XXX: work on the right hand side *)
2552  >p normalize nodelta >p1 normalize nodelta
2553  (* XXX: switch to the left hand side *)
2554  >EQP -P normalize nodelta
2555  #sigma_increment_commutation #maps_assm #fetch_many_assm
2556  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2557  <EQppc in fetch_many_assm;
2558  whd in match (short_jump_cond ??);
2559  @pair_elim #sj_possible #disp
2560  @pair_elim #result #flags #sub16_refl
2561  @pair_elim #upper #lower #vsplit_refl
2562  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2563  #sj_possible_pair destruct(sj_possible_pair)
2564  >p1 normalize nodelta
2565  [1,3:
2566    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2567    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2568    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2569    whd in ⊢ (??%?);
2570    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2571    lapply maps_assm whd in ⊢ (??%? → ?);
2572    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
2573    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
2574    (* XXX: work on the left hand side *)
2575    @(pair_replace ?????????? p) normalize nodelta
2576    [1,3:
2577      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
2578      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]
2579      >(get_arg_8_set_program_counter … true addr1)
2580      [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]
2581      @get_arg_8_pseudo_addressing_mode_ok assumption
2582    |2,4:
2583      >p1 normalize nodelta >EQs
2584      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
2585      >set_program_counter_status_of_pseudo_status
2586       whd in ⊢ (??%%);
2587      @split_eq_status
2588      [1,10:
2589        whd in ⊢ (??%%); >set_arg_8_set_program_counter
2590        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2591        >low_internal_ram_set_program_counter
2592        [1:
2593          >low_internal_ram_set_program_counter
2594          (* XXX: ??? *)
2595        |2:
2596          >low_internal_ram_set_clock
2597          (* XXX: ??? *)
2598        ]
2599      |2,11:
2600        whd in ⊢ (??%%); >set_arg_8_set_program_counter
2601        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2602        >high_internal_ram_set_program_counter
2603        [1:
2604          >high_internal_ram_set_program_counter
2605          (* XXX: ??? *)
2606        |2:
2607          >high_internal_ram_set_clock
2608          (* XXX: ??? *)
2609        ]
2610      |3,12:
2611        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
2612        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2613        >(external_ram_set_arg_8 ??? addr1)
2614        [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
2615      |4,13:
2616        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
2617        [1:
2618          >program_counter_set_program_counter
2619          >set_arg_8_set_program_counter
2620          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2621          >set_clock_set_program_counter >program_counter_set_program_counter
2622          change with (add ??? = ?)
2623          (* XXX: ??? *)
2624        |2:
2625          >set_arg_8_set_program_counter
2626          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
2627          >program_counter_set_program_counter
2628          >set_arg_8_set_program_counter
2629          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2630          >set_clock_set_program_counter >program_counter_set_program_counter
2631          >sigma_increment_commutation <EQppc
2632          whd in match (assembly_1_pseudoinstruction ??????);
2633          whd in match (expand_pseudo_instruction ??????);
2634          (* XXX: ??? *)
2635        ]
2636      |5,14:
2637        whd in match (special_function_registers_8051 ???);
2638        [1:
2639          >special_function_registers_8051_set_program_counter
2640          >special_function_registers_8051_set_clock
2641          >set_arg_8_set_program_counter in ⊢ (???%);
2642          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2643          >special_function_registers_8051_set_program_counter
2644          >set_arg_8_set_program_counter
2645          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2646          >special_function_registers_8051_set_program_counter
2647          @special_function_registers_8051_set_arg_8 assumption
2648        |2:
2649          >special_function_registers_8051_set_clock
2650          >set_arg_8_set_program_counter
2651          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2652          >set_arg_8_set_program_counter
2653          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2654          >special_function_registers_8051_set_program_counter
2655          >special_function_registers_8051_set_program_counter
2656          @special_function_registers_8051_set_arg_8 assumption
2657        ]
2658      |6,15:
2659        whd in match (special_function_registers_8052 ???);
2660        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
2661        [1:
2662          >set_arg_8_set_program_counter
2663          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2664          >set_arg_8_set_program_counter
2665          [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2666          >special_function_registers_8052_set_program_counter
2667          >special_function_registers_8052_set_program_counter
2668          @special_function_registers_8052_set_arg_8 assumption
2669        |2:
2670          whd in ⊢ (??%%);
2671          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
2672        ]
2673        (* XXX: we need special_function_registers_8052_set_arg_8 *)
2674      |7,16:
2675        whd in match (p1_latch ???);
2676        whd in match (p1_latch ???) in ⊢ (???%);
2677        (* XXX: we need p1_latch_8052_set_arg_8 *)
2678      |8,17:
2679        whd in match (p3_latch ???);
2680        whd in match (p3_latch ???) in ⊢ (???%);
2681        (* XXX: we need p3_latch_8052_set_arg_8 *)
2682      |9:
2683        >clock_set_clock
2684        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
2685        >EQticks <instr_refl @eq_f2
2686        [1:
2687          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
2688        |2:
2689          (* XXX: we need clock_set_arg_8 *)
2690        ]
2691      |18:
2692      ]
2693    ]
2694    (* XXX: switch to the right hand side *)
2695    normalize nodelta >EQs -s >EQticks -ticks
2696    cases (¬ eq_bv ???) normalize nodelta
2697    whd in ⊢ (??%%);
2698    (* XXX: finally, prove the equality using sigma commutation *)
2699    @split_eq_status try %
2700    [1,2,3,19,20,21,28,29,30:
2701      cases daemon (* XXX: axioms as above *)
2702    |4,13,22,31:
2703    |5,14,23,32:
2704    |6,15,24,33:
2705    |7,16,25,34:
2706    |8,17,26,35:
2707      whd in ⊢ (??%%);maps_assm
2708     
2709    |9,18,27,36:
2710      whd in ⊢ (??%%);
2711      whd in match (ticks_of_instruction ?); <instr_refl
2712      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
2713    ]
2714  |2,4:
2715    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2716    [2, 4:
2717      cases daemon (* XXX: !!! *)
2718    ]
2719    normalize nodelta >EQppc
2720    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2721    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2722    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2723    #fetch_many_assm whd in fetch_many_assm; %{2}
2724    change with (execute_1 ?? = ?)
2725    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2726    #status_after_1 #EQstatus_after_1
2727    <(?: ? = status_after_1)
2728    [3,6:
2729      >EQstatus_after_1 in ⊢ (???%);
2730      whd in ⊢ (???%);
2731      [1:
2732        <fetch_refl in ⊢ (???%);
2733      |2:
2734        <fetch_refl in ⊢ (???%);
2735      ]
2736      whd in ⊢ (???%);
2737      @(pair_replace ?????????? p)
2738      [1,3:
2739        cases daemon
2740      |2,4:
2741        normalize nodelta
2742        whd in match (addr_of_relative ????);
2743        cases (¬ eq_bv ???) normalize nodelta
2744        >set_clock_mk_Status_commutation
2745        whd in ⊢ (???%);
2746        change with (add ???) in match (\snd (half_add ???));
2747        >set_arg_8_set_program_counter in ⊢ (???%);
2748        [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
2749        >program_counter_set_program_counter in ⊢ (???%);
2750        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2751        [2,4,6,8:
2752          >bitvector_of_nat_sign_extension_equivalence
2753          [1,3,5,7:
2754            >EQintermediate_pc' %
2755          |*:
2756            repeat @le_S_S @le_O_n
2757          ]
2758        ]
2759        [1,3: % ]
2760      ]
2761    |1,4:
2762      skip
2763    ]
2764    [3,4:
2765      -status_after_1
2766      @(pose … (execute_1 ? (mk_PreStatus …)))
2767      #status_after_1 #EQstatus_after_1
2768      <(?: ? = status_after_1)
2769      [3,6:
2770        >EQstatus_after_1 in ⊢ (???%);
2771        whd in ⊢ (???%);
2772        (* XXX: matita bug with patterns across multiple goals *)
2773        [1:
2774          <fetch_refl'' in ⊢ (???%);
2775        |2:
2776          <fetch_refl'' in ⊢ (???%);
2777        ]
2778        [2: % |1: whd in ⊢ (???%); % ]
2779      |1,4:
2780        skip
2781      ]
2782      -status_after_1 whd in ⊢ (??%?);
2783      (* XXX: switch to the right hand side *)
2784      normalize nodelta >EQs -s >EQticks -ticks
2785      normalize nodelta whd in ⊢ (??%%);
2786    ]
2787    (* XXX: finally, prove the equality using sigma commutation *)
2788    @split_eq_status try %
2789    whd in ⊢ (??%%);
2790    cases daemon
2791  ]
2792  |30: (* CJNE *)
2793  (* XXX: work on the right hand side *)
2794  cases addr1 -addr1 #addr1 normalize nodelta
2795  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
2796  (* XXX: switch to the left hand side *)
2797  >EQP -P normalize nodelta
2798  #sigma_increment_commutation #maps_assm #fetch_many_assm
2799
2800  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2801  <EQppc in fetch_many_assm;
2802  whd in match (short_jump_cond ??);
2803  @pair_elim #sj_possible #disp
2804  @pair_elim #result #flags #sub16_refl
2805  @pair_elim #upper #lower #vsplit_refl
2806  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2807  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2808  [1,3:
2809    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2810    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2811    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2812    whd in ⊢ (??%?);
2813    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2814    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
2815    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
2816    @(if_then_else_replace ???????? eq_bv_refl)
2817    [1,3,5,7:
2818      cases daemon
2819    |2,4,6,8:
2820      (* XXX: switch to the right hand side *)
2821      normalize nodelta >EQs -s >EQticks -ticks
2822      whd in ⊢ (??%%);
2823      (* XXX: finally, prove the equality using sigma commutation *)
2824      @split_eq_status try %
2825      [3,7,11,15:
2826        whd in ⊢ (??%?);
2827        [1,3:
2828          cases daemon
2829        |2,4:
2830          cases daemon
2831        ]
2832      ]
2833      cases daemon (* XXX *)
2834    ]
2835  |2,4:
2836    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2837    [2, 4:
2838      cases daemon (* XXX: !!! *)
2839    ]
2840    normalize nodelta >EQppc
2841    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2842    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2843    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2844    #fetch_many_assm whd in fetch_many_assm; %{2}
2845    change with (execute_1 ?? = ?)
2846    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2847    #status_after_1 #EQstatus_after_1
2848    <(?: ? = status_after_1)
2849    [2,5:
2850      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
2851    |3,6:
2852      >EQstatus_after_1 in ⊢ (???%);
2853      whd in ⊢ (???%);
2854      [1: <fetch_refl in ⊢ (???%);
2855      |2: <fetch_refl in ⊢ (???%);
2856      ]
2857      whd in ⊢ (???%);
2858      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
2859      whd in ⊢ (???%);
2860      whd in match (addr_of_relative ????);
2861      change with (add ???) in match (\snd (half_add ???));
2862      >set_clock_set_program_counter in ⊢ (???%);
2863      >program_counter_set_program_counter in ⊢ (???%);
2864      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2865      [2,4,6,8:
2866        >bitvector_of_nat_sign_extension_equivalence
2867        [1,3,5,7:
2868          >EQintermediate_pc' %
2869        |*:
2870          repeat @le_S_S @le_O_n
2871        ]
2872      |1,5:
2873        %
2874      ]
2875    |1,4: skip
2876    ]
2877    [1,2,3,4:
2878      -status_after_1
2879      @(pose … (execute_1 ? (mk_PreStatus …)))
2880      #status_after_1 #EQstatus_after_1
2881      <(?: ? = status_after_1)
2882      [3,6,9,12:
2883        >EQstatus_after_1 in ⊢ (???%);
2884        whd in ⊢ (???%);
2885        (* XXX: matita bug with patterns across multiple goals *)
2886        [1: <fetch_refl'' in ⊢ (???%);
2887        |2: <fetch_refl'' in ⊢ (???%);
2888        |3: <fetch_refl'' in ⊢ (???%);
2889        |4: <fetch_refl'' in ⊢ (???%);
2890        ] %
2891      |1,4,7,10:
2892        skip
2893      ]
2894      -status_after_1 whd in ⊢ (??%?);
2895      (* XXX: switch to the right hand side *)
2896      normalize nodelta >EQs -s >EQticks -ticks
2897      whd in ⊢ (??%%);
2898    ]
2899    (* XXX: finally, prove the equality using sigma commutation *)
2900    @split_eq_status try %
2901    cases daemon
2902  ]
2903  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
2904  (* XXX: work on the right hand side *)
2905  >p normalize nodelta
2906  (* XXX: switch to the left hand side *)
2907  >EQP -P normalize nodelta
2908  #sigma_increment_commutation #maps_assm #fetch_many_assm
2909 
2910  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
2911  <EQppc in fetch_many_assm;
2912  whd in match (short_jump_cond ??);
2913  @pair_elim #sj_possible #disp
2914  @pair_elim #result #flags #sub16_refl
2915  @pair_elim #upper #lower #vsplit_refl
2916  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
2917  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
2918  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2919    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
2920    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
2921    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
2922    whd in ⊢ (??%?);
2923    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
2924    (* XXX: work on the left hand side *)
2925    @(if_then_else_replace ???????? p) normalize nodelta
2926    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2927      cases daemon
2928    ]
2929    (* XXX: switch to the right hand side *)
2930    normalize nodelta >EQs -s >EQticks -ticks
2931    whd in ⊢ (??%%);
2932    (* XXX: finally, prove the equality using sigma commutation *)
2933    @split_eq_status try %
2934    cases daemon
2935  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2936    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
2937    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2938      cases daemon (* XXX: !!! *)
2939    ]
2940    normalize nodelta >EQppc
2941    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
2942    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
2943    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
2944    #fetch_many_assm whd in fetch_many_assm; %{2}
2945    change with (execute_1 ?? = ?)
2946    @(pose … (execute_1 ? (status_of_pseudo_status …)))
2947    #status_after_1 #EQstatus_after_1
2948    <(?: ? = status_after_1)
2949    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
2950      >EQstatus_after_1 in ⊢ (???%);
2951      whd in ⊢ (???%);
2952      [1: <fetch_refl in ⊢ (???%);
2953      |2: <fetch_refl in ⊢ (???%);
2954      |3: <fetch_refl in ⊢ (???%);
2955      |4: <fetch_refl in ⊢ (???%);
2956      |5: <fetch_refl in ⊢ (???%);
2957      |6: <fetch_refl in ⊢ (???%);
2958      |7: <fetch_refl in ⊢ (???%);
2959      |8: <fetch_refl in ⊢ (???%);
2960      |9: <fetch_refl in ⊢ (???%);
2961      |10: <fetch_refl in ⊢ (???%);
2962      |11: <fetch_refl in ⊢ (???%);
2963      |12: <fetch_refl in ⊢ (???%);
2964      |13: <fetch_refl in ⊢ (???%);
2965      |14: <fetch_refl in ⊢ (???%);
2966      ]
2967      whd in ⊢ (???%);
2968      @(if_then_else_replace ???????? p)
2969      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2970        cases daemon
2971      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2972        normalize nodelta
2973        whd in match (addr_of_relative ????);
2974        >set_clock_mk_Status_commutation
2975        [9,10:
2976          (* XXX: demodulation not working in this case *)
2977          >program_counter_set_arg_1 in ⊢ (???%);
2978          >program_counter_set_program_counter in ⊢ (???%);
2979        |*:
2980          /demod/
2981        ]
2982        whd in ⊢ (???%);
2983        change with (add ???) in match (\snd (half_add ???));
2984        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
2985        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
2986          >bitvector_of_nat_sign_extension_equivalence
2987          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
2988            >EQintermediate_pc' %
2989          |*:
2990            repeat @le_S_S @le_O_n
2991          ]
2992        ]
2993        %
2994      ]
2995    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
2996      skip
2997    ]
2998    -status_after_1
2999    @(pose … (execute_1 ? (mk_PreStatus …)))
3000    #status_after_1 #EQstatus_after_1
3001    <(?: ? = status_after_1)
3002    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
3003      >EQstatus_after_1 in ⊢ (???%);
3004      whd in ⊢ (???%);
3005      (* XXX: matita bug with patterns across multiple goals *)
3006      [1: <fetch_refl'' in ⊢ (???%);
3007      |2: <fetch_refl' in ⊢ (???%);
3008      |3: <fetch_refl'' in ⊢ (???%);
3009      |4: <fetch_refl' in ⊢ (???%);
3010      |5: <fetch_refl'' in ⊢ (???%);
3011      |6: <fetch_refl' in ⊢ (???%);
3012      |7: <fetch_refl'' in ⊢ (???%);
3013      |8: <fetch_refl' in ⊢ (???%);
3014      |9: <fetch_refl'' in ⊢ (???%);
3015      |10: <fetch_refl' in ⊢ (???%);
3016      |11: <fetch_refl'' in ⊢ (???%);
3017      |12: <fetch_refl' in ⊢ (???%);
3018      |13: <fetch_refl'' in ⊢ (???%);
3019      |14: <fetch_refl' in ⊢ (???%);
3020      ]
3021      whd in ⊢ (???%);
3022      [9,10:
3023      |*:
3024        /demod/
3025      ] %
3026    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
3027      skip
3028    ]
3029    -status_after_1 whd in ⊢ (??%?);
3030    (* XXX: switch to the right hand side *)
3031    normalize nodelta >EQs -s >EQticks -ticks
3032    whd in ⊢ (??%%);
3033    (* XXX: finally, prove the equality using sigma commutation *)
3034    @split_eq_status try %
3035    [3,11,19,27,36,53,61:
3036      >program_counter_set_program_counter >set_clock_mk_Status_commutation
3037      [5: >program_counter_set_program_counter ]
3038      >EQaddr_of normalize nodelta
3039      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
3040      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
3041      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
3042      >create_label_cost_refl normalize nodelta #relevant @relevant
3043      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
3044      try assumption whd in match instruction_has_label; normalize nodelta
3045      <instr_refl normalize nodelta %
3046    |7,15,23,31,45,57,65:
3047      >set_clock_mk_Status_commutation >program_counter_set_program_counter
3048      whd in ⊢ (??%?); normalize nodelta
3049      >EQppc in fetch_many_assm; #fetch_many_assm
3050      [5:
3051        >program_counter_set_arg_1 >program_counter_set_program_counter
3052      ]
3053      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
3054      <bitvector_of_nat_sign_extension_equivalence
3055      [1,3,5,7,9,11,13:
3056        whd in ⊢ (???%); cases (half_add ???) normalize //
3057      |2,4,6,8,10,12,14:
3058        @assembly1_lt_128
3059        @le_S_S @le_O_n
3060      ]
3061    |*:
3062      cases daemon
3063    ]
3064  ]
3065  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
3066  (* XXX: work on the right hand side *)
3067  lapply (subaddressing_modein ???)
3068  <EQaddr normalize nodelta #irrelevant
3069  try (>p normalize nodelta)
3070  try (>p1 normalize nodelta)
3071  (* XXX: switch to the left hand side *)
3072  >EQP -P normalize nodelta
3073  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
3074  whd in ⊢ (??%?);
3075  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
3076  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
3077  (* XXX: work on the left hand side *)
3078  [1,2,3,4,5:
3079    generalize in ⊢ (??(???(?%))?);
3080  |6,7,8,9,10,11:
3081    generalize in ⊢ (??(???(?%))?);
3082  |12:
3083    generalize in ⊢ (??(???(?%))?);
3084  ]
3085  <EQaddr normalize nodelta #irrelevant
3086  try @(jmpair_as_replace ?????????? p)
3087  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
3088  (* XXX: switch to the right hand side *)
3089  normalize nodelta >EQs -s >EQticks -ticks
3090  whd in ⊢ (??%%);
3091  (* XXX: finally, prove the equality using sigma commutation *)
3092  try @split_eq_status try % whd in ⊢ (??%%);
3093  cases daemon
3094  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
3095  (* XXX: work on the right hand side *)
3096  >p normalize nodelta
3097  try (>p1 normalize nodelta)
3098  (* XXX: switch to the left hand side *)
3099  -instr_refl >EQP -P normalize nodelta
3100  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
3101  whd in ⊢ (??%?);
3102  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
3103  (* XXX: work on the left hand side *)
3104  @(pair_replace ?????????? p)
3105  [1,3,5,7,9,11,13,15,17:
3106    >set_clock_set_program_counter >set_clock_mk_Status_commutation
3107    >set_program_counter_mk_Status_commutation >clock_set_program_counter
3108    cases daemon
3109  |14,16,18:
3110    normalize nodelta
3111    @(pair_replace ?????????? p1)
3112    [1,3,5:
3113      >set_clock_mk_Status_commutation
3114      cases daemon
3115    ]
3116  ]
3117  (* XXX: switch to the right hand side *)
3118  normalize nodelta >EQs -s >EQticks -ticks
3119  whd in ⊢ (??%%);
3120  (* XXX: finally, prove the equality using sigma commutation *)
3121  try @split_eq_status try %
3122  cases daemon *)
Note: See TracBrowser for help on using the repository browser.