source: src/ASM/AssemblyProofSplit.ma @ 2211

Last change on this file since 2211 was 2210, checked in by mulligan, 8 years ago

XOR case completely finished.

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