source: src/ASM/AssemblyProofSplit.ma @ 2222

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

More work on the big lemma. Nearly there now.

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