source: src/ASM/AssemblyProofSplit.ma @ 2279

Last change on this file since 2279 was 2279, checked in by sacerdot, 8 years ago
  1. Bug fixed in the semantics of PUSH (no indirection performed)
  2. Proved write_at_stack_pointer_status_of_pseudo_status
  3. PUSH case of main lemma almost done
File size: 100.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 start_pc.
13  #code_memory #final_pc #start_pc #i * #new_pc
14  #fetch_many_assm whd in fetch_many_assm;
15  cases (eq_bv_eq … fetch_many_assm) assumption
16qed.
17
18include alias "ASM/Vector.ma".
19include "ASM/Test.ma".
20include "ASM/Test2.ma".
21
22(*CSC: move elsewhere*)
23lemma not_b_c_to_b_not_c:
24  ∀b, c: bool.
25    (¬b) = c → b = (¬c).
26  //
27qed.
28 
29lemma match_nat_replace:
30  ∀l, o, p, r, o', p': nat.
31    l ≃ r →
32    o ≃ o' →
33    p ≃ p' →
34      match l with [ O ⇒ o | S n ⇒ p ] = match r with [ O ⇒ o' | S n' ⇒ p' ].
35  #l #o #o #r #o' #p' #lr_refl #o_refl #p_refl >lr_refl >o_refl >p_refl %
36qed.
37
38(*CSC: move elsewhere*)
39lemma conjunction_split:
40  ∀l, l', r, r': bool.
41    l = l' → r = r' → (l ∧ r) = (l' ∧ r').
42  #l #l' #r #r' #l_refl #r_refl <l_refl <r_refl %
43qed.
44
45lemma match_nat_status_of_pseudo_status:
46  ∀M, cm, sigma, policy, s, s', s'', s'''.
47  ∀n, n': nat.
48    n = n' →
49    status_of_pseudo_status M cm s' sigma policy = s →
50    (∀n. status_of_pseudo_status M cm (s''' n) sigma policy = s'' n) →
51      match n with [ O ⇒ s | S n' ⇒ s'' n' ] =
52        status_of_pseudo_status M cm (match n' with [ O ⇒ s' | S n'' ⇒ s''' n'']) sigma policy.
53  #M #cm #sigma #policy #s #s' #s'' #s''' #n #n'
54  #n_refl #s_refl #s_refl' <n_refl <s_refl
55  cases n normalize nodelta try % #n' <(s_refl' n') %
56qed.
57
58lemma get_arg_8_status_of_pseudo_status':
59  ∀cm,ps,l.
60  ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]].
61  ∀M. ∀sigma. ∀policy. ∀s.
62      s = status_of_pseudo_status M cm ps sigma policy →
63      map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr →
64      map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr)
65      = get_arg_8 … ps l addr →
66      get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy)
67      s l addr = get_arg_8 … ps l addr.
68 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status
69 try assumption %
70qed.
71
72lemma short_jump_cond_ok:
73  ∀v1, v1', v2, v2': Word.
74  ∀is_possible, offset.
75    v1 = v1' → v2 = v2' →
76    〈is_possible, offset〉 = short_jump_cond v1 v2 →
77      is_possible → v2' = add 16 v1' (sign_extension offset).
78  #v1 #v1' #v2 #v2' #is_possible #offset #v1_refl #v2_refl <v1_refl <v2_refl
79  whd in match short_jump_cond; normalize nodelta
80  @pair_elim #result #flags #sub16_refl
81  @pair_elim #upper #lower #vsplit_refl
82  inversion (get_index' bool ???) #get_index_refl normalize nodelta
83  #relevant destruct(relevant) #relevant
84  [1:
85    @(sub_16_to_add_16_8_1 … flags)
86  |2:
87    @(sub_16_to_add_16_8_0 … flags)
88  ]
89  try assumption >sub16_refl
90  <(eq_bv_eq … relevant)
91  >(vsplit_ok … (sym_eq … vsplit_refl)) %
92qed.
93
94lemma main_lemma_preinstruction:
95  ∀M, M': internal_pseudo_address_map.
96  ∀preamble: preamble.
97  ∀instr_list: list labelled_instruction.
98  ∀cm: pseudo_assembly_program.
99  ∀EQcm: cm = 〈preamble, instr_list〉.
100  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
101  ∀sigma: Word → Word.
102  ∀policy: Word → bool.
103  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
104  ∀ps: PseudoStatus cm.
105  ∀ppc: Word.
106  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
107  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
108  ∀labels: label_map.
109  ∀costs: BitVectorTrie costlabel 16.
110  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
111  ∀newppc: Word.
112  ∀lookup_labels: Identifier → Word.
113  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
114  ∀lookup_datalabels: Identifier → Word.
115  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
116  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
117  ∀instr: preinstruction Identifier.
118  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
119  ∀ticks: nat × nat.
120  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr).
121  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
122  ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)).
123  ∀s: PreStatus pseudo_assembly_program cm.
124  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
125  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
126  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
127              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
128                  lookup_datalabels (Instruction instr)))) →
129              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
130                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))
131                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
132                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
133                      status_of_pseudo_status M' cm s sigma policy).
134    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
135  (* XXX: takes about 45 minutes to type check! *)
136  ** #low #high #accA #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
137  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
138  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
139  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
140  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
141  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
142  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
143  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
144  [2: * // ]
145  @(
146  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
147  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
148  match instr in preinstruction return λx. x = instr → Σs'.? with
149        [ ADD addr1 addr2 ⇒ λinstr_refl.
150            let s ≝ add_ticks1 s in
151            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
152                                                   (get_arg_8 … s false addr2) false in
153            let cy_flag ≝ get_index' ? O ? flags in
154            let ac_flag ≝ get_index' ? 1 ? flags in
155            let ov_flag ≝ get_index' ? 2 ? flags in
156            let s ≝ set_arg_8 … s ACC_A result in
157              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
158        | ADDC addr1 addr2 ⇒ λinstr_refl.
159            let s ≝ add_ticks1 s in
160            let old_cy_flag ≝ get_cy_flag ?? s in
161            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
162                                                   (get_arg_8 … s false addr2) old_cy_flag in
163            let cy_flag ≝ get_index' ? O ? flags in
164            let ac_flag ≝ get_index' ? 1 ? flags in
165            let ov_flag ≝ get_index' ? 2 ? flags in
166            let s ≝ set_arg_8 … s ACC_A result in
167              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
168        | SUBB addr1 addr2 ⇒ λinstr_refl.
169            let s ≝ add_ticks1 s in
170            let old_cy_flag ≝ get_cy_flag ?? s in
171            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
172                                                   (get_arg_8 … s false addr2) old_cy_flag in
173            let cy_flag ≝ get_index' ? O ? flags in
174            let ac_flag ≝ get_index' ? 1 ? flags in
175            let ov_flag ≝ get_index' ? 2 ? flags in
176            let s ≝ set_arg_8 … s ACC_A result in
177              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
178        | ANL addr ⇒ λinstr_refl.
179          let s ≝ add_ticks1 s in
180          match addr with
181            [ inl l ⇒
182              match l with
183                [ inl l' ⇒
184                  let 〈addr1, addr2〉 ≝ l' in
185                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
186                    set_arg_8 … s addr1 and_val
187                | inr r ⇒
188                  let 〈addr1, addr2〉 ≝ r in
189                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
190                    set_arg_8 … s addr1 and_val
191                ]
192            | inr r ⇒
193              let 〈addr1, addr2〉 ≝ r in
194              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
195               set_flags … s and_val (None ?) (get_ov_flag ?? s)
196            ]
197        | ORL addr ⇒ λinstr_refl.
198          let s ≝ add_ticks1 s in
199          match addr with
200            [ inl l ⇒
201              match l with
202                [ inl l' ⇒
203                  let 〈addr1, addr2〉 ≝ l' in
204                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
205                    set_arg_8 … s addr1 or_val
206                | inr r ⇒
207                  let 〈addr1, addr2〉 ≝ r in
208                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
209                    set_arg_8 … s addr1 or_val
210                ]
211            | inr r ⇒
212              let 〈addr1, addr2〉 ≝ r in
213              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
214               set_flags … s or_val (None ?) (get_ov_flag … s)
215            ]
216        | XRL addr ⇒ λinstr_refl.
217          let s ≝ add_ticks1 s in
218          match addr with
219            [ inl l' ⇒
220              let 〈addr1, addr2〉 ≝ l' in
221              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
222                set_arg_8 … s addr1 xor_val
223            | inr r ⇒
224              let 〈addr1, addr2〉 ≝ r in
225              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
226                set_arg_8 … s addr1 xor_val
227            ]
228        | INC addr ⇒ λinstr_refl.
229            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → ? with
230              [ ACC_A ⇒ λacc_a: True. λEQaddr.
231                let s' ≝ add_ticks1 s in
232                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
233                 set_arg_8 … s' ACC_A result
234              | REGISTER r ⇒ λregister: True. λEQaddr.
235                let s' ≝ add_ticks1 s in
236                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
237                 set_arg_8 … s' (REGISTER r) result
238              | DIRECT d ⇒ λdirect: True. λEQaddr.
239                let s' ≝ add_ticks1 s in
240                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
241                 set_arg_8 … s' (DIRECT d) result
242              | INDIRECT i ⇒ λindirect: True. λEQaddr.
243                let s' ≝ add_ticks1 s in
244                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
245                 set_arg_8 … s' (INDIRECT i) result
246              | DPTR ⇒ λdptr: True. λEQaddr.
247                let s' ≝ add_ticks1 s in
248                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
249                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
250                let s ≝ set_8051_sfr … s' SFR_DPL bl in
251                 set_8051_sfr … s' SFR_DPH bu
252              | _ ⇒ λother: False. ⊥
253              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
254        | NOP ⇒ λinstr_refl.
255           let s ≝ add_ticks2 s in
256            s
257        | DEC addr ⇒ λinstr_refl.
258           let s ≝ add_ticks1 s in
259           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
260             set_arg_8 … s addr result
261        | MUL addr1 addr2 ⇒ λinstr_refl.
262           let s ≝ add_ticks1 s in
263           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
264           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
265           let product ≝ acc_a_nat * acc_b_nat in
266           let ov_flag ≝ product ≥ 256 in
267           let low ≝ bitvector_of_nat 8 (product mod 256) in
268           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
269           let s ≝ set_8051_sfr … s SFR_ACC_A low in
270             set_8051_sfr … s SFR_ACC_B high
271        | DIV addr1 addr2 ⇒ λinstr_refl.
272           let s ≝ add_ticks1 s in
273           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
274           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
275             match acc_b_nat with
276               [ O ⇒ set_flags … s false (None Bit) true
277               | S o ⇒
278                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
279                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
280                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
281                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
282                   set_flags … s false (None Bit) false
283               ]
284        | DA addr ⇒ λinstr_refl.
285            let s ≝ add_ticks1 s in
286            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
287              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
288                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
289                let cy_flag ≝ get_index' ? O ? flags in
290                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
291                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
292                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
293                    let new_acc ≝ nu @@ acc_nl' in
294                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
295                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
296                  else
297                    s
298              else
299                s
300        | CLR addr ⇒ λinstr_refl.
301          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
302            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
303              let s ≝ add_ticks1 s in
304               set_arg_8 … s ACC_A (zero 8)
305            | CARRY ⇒ λcarry: True.  λEQaddr.
306              let s ≝ add_ticks1 s in
307               set_arg_1 … s CARRY false
308            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
309              let s ≝ add_ticks1 s in
310               set_arg_1 … s (BIT_ADDR b) false
311            | _ ⇒ λother: False. ⊥
312            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
313        | CPL addr ⇒ λinstr_refl.
314          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → ? with
315            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
316                let s ≝ add_ticks1 s in
317                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
318                let new_acc ≝ negation_bv ? old_acc in
319                 set_8051_sfr … s SFR_ACC_A new_acc
320            | CARRY ⇒ λcarry: True. λEQaddr.
321                let s ≝ add_ticks1 s in
322                let old_cy_flag ≝ get_arg_1 … s CARRY true in
323                let new_cy_flag ≝ ¬old_cy_flag in
324                 set_arg_1 … s CARRY new_cy_flag
325            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
326                let s ≝ add_ticks1 s in
327                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
328                let new_bit ≝ ¬old_bit in
329                 set_arg_1 … s (BIT_ADDR b) new_bit
330            | _ ⇒ λother: False. ?
331            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
332        | SETB b ⇒ λinstr_refl.
333            let s ≝ add_ticks1 s in
334            set_arg_1 … s b false
335        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
336            let s ≝ add_ticks1 s in
337            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
338            let new_acc ≝ rotate_left … 1 old_acc in
339              set_8051_sfr … s SFR_ACC_A new_acc
340        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
341            let s ≝ add_ticks1 s in
342            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
343            let new_acc ≝ rotate_right … 1 old_acc in
344              set_8051_sfr … s SFR_ACC_A new_acc
345        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
346            let s ≝ add_ticks1 s in
347            let old_cy_flag ≝ get_cy_flag ?? s in
348            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
349            let new_cy_flag ≝ get_index' ? O ? old_acc in
350            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
351            let s ≝ set_arg_1 … s CARRY new_cy_flag in
352              set_8051_sfr … s SFR_ACC_A new_acc
353        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
354            let s ≝ add_ticks1 s in
355            let old_cy_flag ≝ get_cy_flag ?? s in
356            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
357            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
358            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
359            let s ≝ set_arg_1 … s CARRY new_cy_flag in
360              set_8051_sfr … s SFR_ACC_A new_acc
361        | SWAP addr ⇒ λinstr_refl. (* DPM: always ACC_A *)
362            let s ≝ add_ticks1 s in
363            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
364            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
365            let new_acc ≝ nl @@ nu in
366              set_8051_sfr … s SFR_ACC_A new_acc
367        | PUSH addr ⇒ λinstr_refl.
368            let s ≝ add_ticks1 s in
369            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
370            let s ≝ set_8051_sfr … s SFR_SP new_sp in
371             write_at_stack_pointer … s (get_arg_8 … s false addr)
372        | POP addr ⇒ λinstr_refl.
373            let s ≝ add_ticks1 s in
374            let contents ≝ read_at_stack_pointer ?? s in
375            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
376            let s ≝ set_8051_sfr … s SFR_SP new_sp in
377              set_arg_8 … s addr contents
378        | XCH addr1 addr2 ⇒ λinstr_refl.
379            let s ≝ add_ticks1 s in
380            let old_addr ≝ get_arg_8 … s false addr2 in
381            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
382            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
383              set_arg_8 … s addr2 old_acc
384        | XCHD addr1 addr2 ⇒ λinstr_refl.
385            let s ≝ add_ticks1 s in
386            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
387            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
388            let new_acc ≝ acc_nu @@ arg_nl in
389            let new_arg ≝ arg_nu @@ acc_nl in
390            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
391              set_arg_8 … s addr2 new_arg
392        | RET ⇒ λinstr_refl.
393            let s ≝ add_ticks1 s in
394            let high_bits ≝ read_at_stack_pointer ?? s in
395            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
396            let s ≝ set_8051_sfr … s SFR_SP new_sp in
397            let low_bits ≝ read_at_stack_pointer ?? s in
398            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
399            let s ≝ set_8051_sfr … s SFR_SP new_sp in
400            let new_pc ≝ high_bits @@ low_bits in
401              set_program_counter … s new_pc
402        | RETI ⇒ λinstr_refl.
403            let s ≝ add_ticks1 s in
404            let high_bits ≝ read_at_stack_pointer ?? s in
405            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
406            let s ≝ set_8051_sfr … s SFR_SP new_sp in
407            let low_bits ≝ read_at_stack_pointer ?? s in
408            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
409            let s ≝ set_8051_sfr … s SFR_SP new_sp in
410            let new_pc ≝ high_bits @@ low_bits in
411              set_program_counter … s new_pc
412        | MOVX addr ⇒ λinstr_refl.
413          let s ≝ add_ticks1 s in
414          (* DPM: only copies --- doesn't affect I/O *)
415          match addr with
416            [ inl l ⇒
417              let 〈addr1, addr2〉 ≝ l in
418                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
419            | inr r ⇒
420              let 〈addr1, addr2〉 ≝ r in
421                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
422            ]
423        | MOV addr ⇒ λinstr_refl.
424          let s ≝ add_ticks1 s in
425          match addr with
426            [ inl l ⇒
427              match l with
428                [ inl l' ⇒
429                  match l' with
430                    [ inl l'' ⇒
431                      match l'' with
432                        [ inl l''' ⇒
433                          match l''' with
434                            [ inl l'''' ⇒
435                              let 〈addr1, addr2〉 ≝ l'''' in
436                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
437                            | inr r'''' ⇒
438                              let 〈addr1, addr2〉 ≝ r'''' in
439                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
440                            ]
441                        | inr r''' ⇒
442                          let 〈addr1, addr2〉 ≝ r''' in
443                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
444                        ]
445                    | inr r'' ⇒
446                      let 〈addr1, addr2〉 ≝ r'' in
447                       set_arg_16 … s (get_arg_16 … s addr2) addr1
448                    ]
449                | inr r ⇒
450                  let 〈addr1, addr2〉 ≝ r in
451                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
452                ]
453            | inr r ⇒
454              let 〈addr1, addr2〉 ≝ r in
455               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
456            ]
457          | JC addr ⇒ λinstr_refl.
458                  if get_cy_flag ?? s then
459                    let s ≝ add_ticks1 s in
460                      set_program_counter … s (addr_of addr s)
461                  else
462                    let s ≝ add_ticks2 s in
463                      s
464            | JNC addr ⇒ λinstr_refl.
465                  if ¬(get_cy_flag ?? s) then
466                   let s ≝ add_ticks1 s in
467                     set_program_counter … s (addr_of addr s)
468                  else
469                   let s ≝ add_ticks2 s in
470                    s
471            | JB addr1 addr2 ⇒ λinstr_refl.
472                  if get_arg_1 … s addr1 false then
473                   let s ≝ add_ticks1 s in
474                    set_program_counter … s (addr_of addr2 s)
475                  else
476                   let s ≝ add_ticks2 s in
477                    s
478            | JNB addr1 addr2 ⇒ λinstr_refl.
479                  if ¬(get_arg_1 … s addr1 false) then
480                   let s ≝ add_ticks1 s in
481                    set_program_counter … s (addr_of addr2 s)
482                  else
483                   let s ≝ add_ticks2 s in
484                    s
485            | JBC addr1 addr2 ⇒ λinstr_refl.
486                  let s ≝ set_arg_1 … s addr1 false in
487                    if get_arg_1 … s addr1 false then
488                     let s ≝ add_ticks1 s in
489                      set_program_counter … s (addr_of addr2 s)
490                    else
491                     let s ≝ add_ticks2 s in
492                      s
493            | JZ addr ⇒ λinstr_refl.
494                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
495                     let s ≝ add_ticks1 s in
496                      set_program_counter … s (addr_of addr s)
497                    else
498                     let s ≝ add_ticks2 s in
499                      s
500            | JNZ addr ⇒ λinstr_refl.
501                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
502                     let s ≝ add_ticks1 s in
503                      set_program_counter … s (addr_of addr s)
504                    else
505                     let s ≝ add_ticks2 s in
506                      s
507            | CJNE addr1 addr2 ⇒ λinstr_refl.
508                  match addr1 with
509                    [ inl l ⇒
510                        let 〈addr1, addr2'〉 ≝ l in
511                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
512                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
513                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
514                            let s ≝ add_ticks1 s in
515                            let s ≝ set_program_counter … s (addr_of addr2 s) in
516                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
517                          else
518                            let s ≝ add_ticks2 s in
519                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
520                    | inr r' ⇒
521                        let 〈addr1, addr2'〉 ≝ r' in
522                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
523                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
524                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
525                            let s ≝ add_ticks1 s in
526                            let s ≝ set_program_counter … s (addr_of addr2 s) in
527                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
528                          else
529                            let s ≝ add_ticks2 s in
530                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
531                    ]
532            | DJNZ addr1 addr2 ⇒ λinstr_refl.
533              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
534              let s ≝ set_arg_8 … s addr1 result in
535                if ¬(eq_bv ? result (zero 8)) then
536                 let s ≝ add_ticks1 s in
537                  set_program_counter … s (addr_of addr2 s)
538                else
539                 let s ≝ add_ticks2 s in
540                  s
541           ] (refl … instr))
542  try cases other
543  try assumption (*20s*)
544  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
545  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
546  whd in match execute_1_preinstruction; normalize nodelta
547  [1,2: (* ADD and ADDC *)
548    (* XXX: work on the right hand side *)
549    (* XXX: switch to the left hand side *)
550    >EQP -P normalize nodelta
551    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
552    whd in maps_assm:(??%%);
553    inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1
554    [2,4: normalize nodelta #absurd destruct(absurd) ]
555    inversion (assert_data ?????) #addressing_mode_ok_assm_2
556    [2,4: normalize nodelta #absurd destruct(absurd) ]
557    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
558    letin M' ≝ (〈low,high,accA〉)
559    whd in ⊢ (??%?);
560    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
561    whd in ⊢ (??%?);
562    normalize nodelta >EQs >EQticks <instr_refl
563    @let_pair_in_status_of_pseudo_status
564    [1,3:
565      @eq_f3
566      [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M')
567        [3,9:
568          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try %
569          @(subaddressing_mode_elim … addr1) %
570        |6,12:
571          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
572          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
573        |2,8:
574          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try %
575          @(subaddressing_mode_elim … addr1) %
576        |5,11:
577          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try %
578          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
579        |*: % ]
580      |3:
581        %
582      |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ]
583    |2,4:
584      #result #flags @set_flags_status_of_pseudo_status try %
585      @set_arg_8_status_of_pseudo_status try %
586      @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)]
587  |(*3: (* SUBB *)
588    (* XXX: work on the right hand side *)
589    (* XXX: switch to the left hand side *)
590    >EQP -P normalize nodelta
591    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
592    whd in maps_assm:(??%%);
593    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
594    [2,4: normalize nodelta #absurd destruct(absurd) ]
595    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
596    [2,4: normalize nodelta #absurd destruct(absurd) ]
597    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
598    whd in ⊢ (??%?);
599    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
600    whd in ⊢ (??%?);
601    @(pair_replace ?????????? p)
602    [1:
603      @eq_f3
604      normalize nodelta >EQs >EQticks <instr_refl
605      [1:
606        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
607        @(get_arg_8_status_of_pseudo_status cm status … M')
608        [1:
609          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
610        |2:
611          >status_refl
612          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1)
613          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
614        |3:
615          >status_refl
616          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1)
617          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
618        ]
619      |2:
620        @(pose … (set_clock pseudo_assembly_program ???)) #status #status_refl
621        @(get_arg_8_status_of_pseudo_status cm status … M')
622        [1:
623          >status_refl @sym_eq @set_clock_status_of_pseudo_status %
624        |2:
625          >status_refl
626          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
627          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
628        |3:
629          >status_refl
630          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
631          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] %
632        ]
633      |3:
634        @(get_cy_flag_status_of_pseudo_status … M')
635        @sym_eq @set_clock_status_of_pseudo_status
636        [1:
637          @sym_eq @set_program_counter_status_of_pseudo_status %
638        |2:
639          %
640        ]
641      ]
642    |2:
643      normalize nodelta
644      @(pair_replace ?????????? p)
645      [1:
646        @eq_f3 normalize nodelta >EQs >EQticks <instr_refl %
647      |2:
648        @set_flags_status_of_pseudo_status try %
649        @sym_eq @(set_arg_8_status_of_pseudo_status … (refl …))
650        [1:
651          @sym_eq @set_clock_status_of_pseudo_status %
652        |2:
653          @I
654        |3:
655          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try %
656          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
657        ]
658      ]
659    ]
660  |4: (* INC *)
661    (* XXX: work on the right hand side *)
662    (* XXX: switch to the left hand side *)
663    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
664    @(subaddressing_mode_elim … addr) normalize nodelta
665    [1:
666      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
667      whd in maps_assm:(??%%);
668      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
669      [2: normalize nodelta #absurd destruct(absurd) ]
670      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
671      whd in ⊢ (??%?);
672      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
673      whd in ⊢ (??%?);
674      inversion (half_add ???) #carry #result #carry_result_refl normalize nodelta
675      @(pair_replace ?????????? (refl_to_jmrefl ??? carry_result_refl))
676      [1:
677        @eq_f2 try %
678        @(pose … (set_clock ????)) #status #status_refl
679        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
680        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
681      |2:
682        @set_arg_8_status_of_pseudo_status try %
683        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) try %
684      ]
685    |2:
686      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
687      whd in maps_assm:(??%%);
688      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
689      [2: normalize nodelta #absurd destruct(absurd) ]
690      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
691      whd in ⊢ (??%?);
692      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
693      whd in ⊢ (??%?);
694      @let_pair_in_status_of_pseudo_status
695      [1:
696        @eq_f2 try %
697        @(pose … (set_clock ????)) #status #status_refl
698        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
699        >EQs >EQticks
700        [1:
701          @sym_eq @set_clock_status_of_pseudo_status %
702        |2:
703          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
704        |3:
705          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (REGISTER w) … addressing_mode_ok_assm_1) %
706        ]
707      |2:
708        #carry #result
709        @sym_eq @set_arg_8_status_of_pseudo_status try %
710        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
711      ]
712    |3:
713      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
714      whd in maps_assm:(??%%);
715      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
716      [2: normalize nodelta #absurd destruct(absurd) ]
717      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
718      whd in ⊢ (??%?);
719      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
720      whd in ⊢ (??%?);
721      @let_pair_in_status_of_pseudo_status
722      [1:
723        @eq_f2 try %
724        @(pose … (set_clock ????)) #status #status_refl
725        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
726        >EQs >EQticks
727        [1:
728          @sym_eq @set_clock_status_of_pseudo_status %
729        |2:
730          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
731        |3:
732          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (DIRECT w) … addressing_mode_ok_assm_1) %
733        ]
734      |2:
735        #carry #result
736        @sym_eq @set_arg_8_status_of_pseudo_status try %
737        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %   
738      ]
739    |4:
740      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
741      whd in maps_assm:(??%%);
742      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
743      [2: normalize nodelta #absurd destruct(absurd) ]
744      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
745      whd in ⊢ (??%?);
746      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
747      whd in ⊢ (??%?);
748      @let_pair_in_status_of_pseudo_status
749      [1:
750        @eq_f2 try %
751        @(pose … (set_clock ????)) #status #status_refl
752        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
753        >EQs >EQticks
754        [1:
755          @sym_eq @set_clock_status_of_pseudo_status %
756        |2:
757          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
758        |3:
759          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
760        ]
761      |2:
762        #carry #result
763        @sym_eq @set_arg_8_status_of_pseudo_status try %
764        [1:
765          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
766        |2:
767          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %   
768        ]
769      ]
770    |5:
771      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
772      whd in maps_assm:(??%%); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
773      whd in ⊢ (??%?);
774      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
775      whd in ⊢ (??%?);
776      @let_pair_in_status_of_pseudo_status
777      [1:
778        @eq_f2 try %
779        @(pose … (set_clock ????)) #status #status_refl
780        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
781        >EQs >EQticks %
782      |2:
783        #carry #bl
784        @sym_eq @let_pair_in_status_of_pseudo_status
785        [1:
786          @eq_f3 try %
787          @(pose … (set_clock ????)) #status #status_refl
788          @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl
789          >EQs >EQticks %
790        |2:
791          #carry' #bu
792          @sym_eq @set_8051_sfr_status_of_pseudo_status %
793        ]
794      ]
795    ]
796  |5: (* DEC *)
797    >EQs >EQticks <instr_refl >EQP -P normalize nodelta
798    @(subaddressing_mode_elim … addr) normalize nodelta
799    [1:
800      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
801      whd in maps_assm:(??%%);
802      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
803      [2: normalize nodelta #absurd destruct(absurd) ]
804      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
805      whd in ⊢ (??%?);
806      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
807      whd in ⊢ (??%?);
808      @let_pair_in_status_of_pseudo_status
809      [1:
810        @eq_f3 try %
811        @(pose … (set_clock ????)) #status #status_refl
812        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
813        >EQs >EQticks try %
814        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
815      |2:
816        #result #flags
817        @sym_eq @set_arg_8_status_of_pseudo_status try %
818        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
819      ]
820    |2:
821      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
822      whd in maps_assm:(??%%);
823      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
824      [2: normalize nodelta #absurd destruct(absurd) ]
825      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
826      whd in ⊢ (??%?);
827      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
828      whd in ⊢ (??%?);
829      @let_pair_in_status_of_pseudo_status
830      [1:
831        @eq_f3 try %
832        @(pose … (set_clock ????)) #status #status_refl
833        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
834        >EQs >EQticks try %
835        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
836      |2:
837        #result #flags
838        @sym_eq @set_arg_8_status_of_pseudo_status try %
839        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (REGISTER w) … addressing_mode_ok_assm_1) %
840      ]
841    |3:
842      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
843      whd in maps_assm:(??%%);
844      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
845      [2: normalize nodelta #absurd destruct(absurd) ]
846      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
847      whd in ⊢ (??%?);
848      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
849      whd in ⊢ (??%?);
850      @let_pair_in_status_of_pseudo_status
851      [1:
852        @eq_f3 try %
853        @(pose … (set_clock ????)) #status #status_refl
854        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
855        >EQs >EQticks try %
856        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
857      |2:
858        #result #flags
859        @sym_eq @set_arg_8_status_of_pseudo_status try %
860        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (DIRECT w) … addressing_mode_ok_assm_1) %
861      ]
862    |4:
863      #w #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
864      whd in maps_assm:(??%%);
865      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
866      [2: normalize nodelta #absurd destruct(absurd) ]
867      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
868      whd in ⊢ (??%?);
869      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
870      whd in ⊢ (??%?);
871      @let_pair_in_status_of_pseudo_status
872      [1:
873        @eq_f3 try %
874        @(pose … (set_clock ????)) #status #status_refl
875        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
876        >EQs >EQticks try %
877        [1:
878          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
879        |2:
880          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
881        ]
882      |2:
883        #result #flags
884        @sym_eq @set_arg_8_status_of_pseudo_status try %
885        [1:
886          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … (INDIRECT w) … addressing_mode_ok_assm_1) %
887        |2:
888          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … (INDIRECT w) … addressing_mode_ok_assm_1) %
889        ]
890      ]
891    ]
892  |6: (* MUL *)
893    (* XXX: work on the right hand side *)
894    (* XXX: switch to the left hand side *)
895    >EQP -P normalize nodelta
896    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
897    whd in maps_assm:(??%%);
898    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
899    [2: normalize nodelta #absurd destruct(absurd) ]
900    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
901    [2: normalize nodelta #absurd destruct(absurd) ]
902    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
903    whd in ⊢ (??%?);
904    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
905    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
906    [2:
907      whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
908      @sym_eq
909      [1:
910        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
911        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1)
912        %
913      |2:
914        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …)) %
915      ]
916    ]
917    @sym_eq @set_8051_sfr_status_of_pseudo_status
918    [2:
919      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
920      @eq_f @eq_f2 try % @eq_f2 @eq_f
921      @sym_eq
922      [1:
923        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
924        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
925      |2:
926        @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …)) %
927      ]
928    ]
929    @sym_eq @set_clock_status_of_pseudo_status
930    [2:
931      @eq_f %
932    ]
933    @sym_eq @set_program_counter_status_of_pseudo_status %
934  |7,8: (* DIV *)
935    (* XXX: work on the right hand side *)
936    (* XXX: switch to the left hand side *)
937    >EQP -P normalize nodelta
938    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
939    whd in maps_assm:(??%%);
940    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
941    [2,4: normalize nodelta #absurd destruct(absurd) ]
942    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
943    [2,4: normalize nodelta #absurd destruct(absurd) ]
944    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
945    whd in ⊢ (??%?);
946    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
947    whd in ⊢ (??%?); normalize nodelta
948    @(match_nat_status_of_pseudo_status M' cm sigma policy)
949    [1,4:
950      @eq_f
951      @sym_eq @(pose … (set_clock ????)) #status #status_refl
952      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
953    |2,5:
954      @sym_eq @set_flags_status_of_pseudo_status %
955    |3,6:
956      #n @sym_eq @set_flags_status_of_pseudo_status try %
957      @sym_eq @set_8051_sfr_status_of_pseudo_status
958      [1,3:
959        @sym_eq @set_8051_sfr_status_of_pseudo_status try %
960        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
961        @eq_f @eq_f2 try % @eq_f
962        @(pose … (set_clock ????)) #status #status_refl
963        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
964        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
965      |2,4:
966        whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f
967        @(pose … (set_clock ????)) #status #status_refl
968        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
969        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
970      ]
971    ]
972  |9: (* DA *)
973    (* XXX: work on the right hand side *)
974    (* XXX: switch to the left hand side *)
975    >EQP -P normalize nodelta
976    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
977    whd in maps_assm:(??%%);
978    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
979    [2: normalize nodelta #absurd destruct(absurd) ]
980    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
981    whd in ⊢ (??%?);
982    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
983    whd in ⊢ (??%?); normalize nodelta
984    @(pair_replace ?????????? p)
985    [1:
986      @eq_f normalize nodelta >EQs >EQticks <instr_refl
987      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
988      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
989    |2:
990      @(pair_replace ?????????? p)
991      [1:
992        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
993      |2:
994        @(if_then_else_replace ???????? p1) normalize nodelta
995        [1:
996          cases (gtb ? 9)
997          [1:
998            %
999          |2:
1000            change with (get_ac_flag ??? = get_ac_flag ???)
1001            @(get_ac_flag_status_of_pseudo_status M')
1002            @sym_eq @set_clock_status_of_pseudo_status
1003            >EQs >EQticks <instr_refl %
1004          ]
1005        |2:
1006          @(if_then_else_replace ???????? p1) normalize nodelta try %
1007          @(pair_replace ?????????? p2)
1008          [1:
1009            @eq_f3 try % normalize nodelta
1010            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1011            whd in ⊢ (??%?);
1012            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1013          |2:
1014            @(pair_replace ?????????? p2) try %
1015            @(pair_replace ?????????? p3) try %
1016            @(pair_replace ?????????? p3) try %
1017            @(if_then_else_replace ???????? p4) try % normalize nodelta
1018            @(if_then_else_replace ???????? p4) try % normalize nodelta
1019            @(pair_replace ?????????? p5) try %
1020            @(pair_replace ?????????? p5) try %
1021            @set_flags_status_of_pseudo_status try %
1022            [1:
1023              @eq_f @(get_ac_flag_status_of_pseudo_status M')
1024              @sym_eq @set_8051_sfr_status_of_pseudo_status
1025              [1:
1026                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1027              |2:
1028                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1029              ]
1030            |2:
1031              @(get_ov_flag_status_of_pseudo_status M')
1032              @sym_eq @set_8051_sfr_status_of_pseudo_status
1033              [1:
1034                @sym_eq @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1035              |2:
1036                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1037              ]
1038            |3:
1039              @sym_eq @set_8051_sfr_status_of_pseudo_status
1040              [1:
1041                @sym_eq @set_clock_status_of_pseudo_status
1042                [1:
1043                  >EQs
1044                  @sym_eq @set_program_counter_status_of_pseudo_status %
1045                |2:
1046                  >EQs >EQticks <instr_refl %
1047                ]
1048              |2:
1049                whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1050              ]
1051            ]
1052          ]
1053        ]
1054      ]
1055    ]
1056  |10: (* DA *)
1057    (* XXX: work on the right hand side *)
1058    (* XXX: switch to the left hand side *)
1059    >EQP -P normalize nodelta
1060    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1061    whd in maps_assm:(??%%);
1062    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1063    [2: normalize nodelta #absurd destruct(absurd) ]
1064    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1065    whd in ⊢ (??%?);
1066    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1067    whd in ⊢ (??%?); normalize nodelta
1068    @(pair_replace ?????????? p)
1069    [1:
1070      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1071      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1072      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1073    |2:
1074      @(pair_replace ?????????? p)
1075      [1:
1076        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1077      |2:
1078        @(if_then_else_replace ???????? p1) normalize nodelta
1079        [1:
1080          cases (gtb ? 9)
1081          [1:
1082            %
1083          |2:
1084            change with (get_ac_flag ??? = get_ac_flag ???)
1085            @(get_ac_flag_status_of_pseudo_status M')
1086            @sym_eq @set_clock_status_of_pseudo_status
1087            >EQs >EQticks <instr_refl %
1088          ]
1089        |2:
1090          @(if_then_else_replace ???????? p1) normalize nodelta try %
1091          @(pair_replace ?????????? p2)
1092          [1:
1093            @eq_f3 try % normalize nodelta
1094            @(get_8051_sfr_status_of_pseudo_status M' … policy … (refl …))
1095            whd in ⊢ (??%?);
1096            >EQs >EQticks <instr_refl >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1097          |2:
1098            @(pair_replace ?????????? p2) try %
1099            @(pair_replace ?????????? p3) try %
1100            @(pair_replace ?????????? p3) try %
1101            @(if_then_else_replace ???????? p4) try % normalize nodelta
1102            @(if_then_else_replace ???????? p4) try % normalize nodelta
1103            @set_clock_status_of_pseudo_status
1104            [1:
1105              >EQs
1106              @sym_eq @set_program_counter_status_of_pseudo_status %
1107            |2:
1108              >EQs >EQticks <instr_refl %
1109            ]
1110          ]
1111        ]
1112      ]
1113    ]
1114  |11: (* DA *)
1115    (* XXX: work on the right hand side *)
1116    (* XXX: switch to the left hand side *)
1117    >EQP -P normalize nodelta
1118    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1119    whd in maps_assm:(??%%);
1120    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1121    [2: normalize nodelta #absurd destruct(absurd) ]
1122    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1123    whd in ⊢ (??%?);
1124    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1125    whd in ⊢ (??%?); normalize nodelta
1126    @(pair_replace ?????????? p)
1127    [1:
1128      @eq_f normalize nodelta >EQs >EQticks <instr_refl
1129      @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1130      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1131    |2:
1132      @(pair_replace ?????????? p)
1133      [1:
1134        @eq_f normalize nodelta >EQs >EQticks <instr_refl %
1135      |2:
1136        @(if_then_else_replace ???????? p1) normalize nodelta
1137        [1:
1138          cases (gtb ? 9)
1139          [1:
1140            %
1141          |2:
1142            change with (get_ac_flag ??? = get_ac_flag ???)
1143            @(get_ac_flag_status_of_pseudo_status M')
1144            @sym_eq @set_clock_status_of_pseudo_status
1145            >EQs >EQticks <instr_refl %
1146          ]
1147        |2:
1148          @(if_then_else_replace ???????? p1) normalize nodelta try %
1149          @set_clock_status_of_pseudo_status
1150          [1:
1151            >EQs
1152            @sym_eq @set_program_counter_status_of_pseudo_status %
1153          |2:
1154            >EQs >EQticks <instr_refl %
1155          ]
1156        ]
1157      ]
1158    ]
1159  |*)12: (* JC *)
1160    >EQP -P normalize nodelta
1161    whd in match assembly_1_pseudoinstruction; normalize nodelta
1162    whd in match expand_pseudo_instruction; normalize nodelta
1163    whd in match expand_relative_jump; normalize nodelta
1164    whd in match expand_relative_jump_internal; normalize nodelta
1165    >EQppc in ⊢ (% → ?);
1166    @pair_elim #sj_possible #disp #sj_possible_disp_refl
1167    inversion sj_possible #sj_possible_refl normalize nodelta
1168    [1:
1169      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1170      whd in maps_assm:(??%%);
1171      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1172      whd in ⊢ (??%?); normalize nodelta
1173      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1174      whd in ⊢ (??%?);
1175      @if_then_else_status_of_pseudo_status
1176      >EQs >EQticks <instr_refl normalize nodelta
1177      [1:
1178        @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) %
1179      |2:
1180        @set_program_counter_status_of_pseudo_status
1181        [1:
1182          >EQaddr_of normalize nodelta
1183          whd in match addr_of_relative; normalize nodelta
1184          @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl))
1185          [1:
1186            @sym_eq whd in ⊢ (??%?); >EQppc %
1187          |2:
1188            >EQlookup_labels %
1189          |3:
1190            >sj_possible_refl @I
1191          ]
1192        |2:
1193          @set_clock_status_of_pseudo_status try %
1194          whd in match ticks_of0; normalize nodelta
1195          @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1196          [1:
1197            >EQppc %
1198          |2:
1199            >sj_possible_refl %
1200          ]
1201        ]
1202      |3:
1203        @set_clock_status_of_pseudo_status try % @eq_f2 try %
1204        whd in match ticks_of0; normalize nodelta
1205        @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl))
1206        [1:
1207          >EQppc %
1208        |2:
1209          >sj_possible_refl %
1210        ]
1211      ]
1212    |2:
1213      #sigma_increment_commutation #maps_assm
1214      whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1215      whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl
1216      whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2}
1217      @(if_then_else_replace ???????? p) try % normalize nodelta
1218      change with (execute_1 ?? = ?) destruct
1219      whd in ⊢ (??%?); >EQs >EQticks <instr_refl
1220      change with (set_program_counter ???? = ?)
1221    ]
1222    cases daemon
1223  |13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28: (* XXX: conditional jumps *)
1224    cases daemon
1225  |(*29,30: (* ANL and ORL *)
1226    inversion addr
1227    [1,3:
1228      *
1229      [1,3:
1230        #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1231        >EQP -P normalize nodelta
1232        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1233        whd in maps_assm:(??%%);
1234        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1235        [2,4: normalize nodelta #absurd destruct(absurd) ]
1236        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1237        [2,4: normalize nodelta #absurd destruct(absurd) ]
1238        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1239        whd in ⊢ (??%?);
1240        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1241        change with (set_arg_8 ????? = ?)
1242        @set_arg_8_status_of_pseudo_status try %
1243        >EQs >EQticks <instr_refl >addr_refl
1244        [1,4:
1245          @sym_eq @set_clock_status_of_pseudo_status
1246          [1,3:
1247            @sym_eq @set_program_counter_status_of_pseudo_status %
1248          |2,4:
1249            @eq_f2 %
1250          ]
1251        |2,5:
1252          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1253          [1,3: @(subaddressing_mode_elim … acc_a) % ] %
1254        |3,6:
1255          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1256          [1,5:
1257            @(subaddressing_mode_elim … acc_a) %
1258          |4,8:
1259            @eq_f2
1260            @(pose … (set_clock ????)) #status #status_refl
1261            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1262            [1,5:
1263              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1264              [1,5: @(subaddressing_mode_elim … acc_a) % |*: % ]
1265            |3,7:
1266              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1267              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1268            |2,6:
1269              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1270              [1,3: @(subaddressing_mode_elim … acc_a) % |*: % ]
1271            |4,8:
1272              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1273              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1274            ]
1275          |*:
1276            %
1277          ]
1278        ]
1279      |2,4:
1280        #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1281        >EQP -P normalize nodelta
1282        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1283        whd in maps_assm:(??%%);
1284        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1285        [2,4: normalize nodelta #absurd destruct(absurd) ]
1286        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1287        [2,4: normalize nodelta #absurd destruct(absurd) ]
1288        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1289        whd in ⊢ (??%?);
1290        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1291        change with (set_arg_8 ????? = ?)
1292        @set_arg_8_status_of_pseudo_status try %
1293        >EQs >EQticks <instr_refl >addr_refl
1294        [1,4:
1295          @sym_eq @set_clock_status_of_pseudo_status
1296          [1,3:
1297            @sym_eq @set_program_counter_status_of_pseudo_status %
1298          |2,4:
1299            @eq_f2 %
1300          ]
1301        |2,5:
1302          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1303          [1,3: @(subaddressing_mode_elim … direct) #w % ] %
1304        |3,6:
1305          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1306          [1,5:
1307            @(subaddressing_mode_elim … direct) #w %
1308          |4,8:
1309            @eq_f2
1310            @(pose … (set_clock ????)) #status #status_refl
1311            @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1312            [1,5:
1313              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1314              [1,5: @(subaddressing_mode_elim … direct) #w % |*: % ]
1315            |3,7:
1316              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1317              [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1318            |2,6:
1319              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1320              [1,3: @(subaddressing_mode_elim … direct) #w % |*: % ]
1321            |4,8:
1322              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1323              [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1324            ]
1325          |*:
1326            %
1327          ]
1328        ]
1329      ]
1330    |2,4:
1331      #carry_others inversion carry_others #carry #others #carry_others_refl #addr_refl
1332      >EQP -P normalize nodelta
1333      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1334      whd in maps_assm:(??%%);
1335      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1336      [2,4: normalize nodelta #absurd destruct(absurd) ]
1337      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1338      [2,4: normalize nodelta #absurd destruct(absurd) ]
1339      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1340      whd in ⊢ (??%?);
1341      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1342      change with (set_flags ?????? = ?)
1343      [1,4: @set_flags_status_of_pseudo_status try % |*: skip ]
1344      >EQs >EQticks <instr_refl >addr_refl
1345      @sym_eq @set_clock_status_of_pseudo_status %
1346    ]
1347  |31: (* XRL *)
1348    inversion addr
1349    [1:
1350      #acc_a_others inversion acc_a_others #acc_a #others #acc_a_others_refl #addr_refl
1351      >EQP -P normalize nodelta
1352      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1353      whd in maps_assm:(??%%);
1354      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1355      [2: normalize nodelta #absurd destruct(absurd) ]
1356      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
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      change with (set_arg_8 ????? = ?)
1362      @set_arg_8_status_of_pseudo_status try %
1363      >EQs >EQticks <instr_refl >addr_refl
1364      [1:
1365        @sym_eq @set_clock_status_of_pseudo_status
1366        [1:
1367          @sym_eq @set_program_counter_status_of_pseudo_status %
1368        |2:
1369          @eq_f2 %
1370        ]
1371      |2:
1372        @(subaddressing_mode_elim … acc_a) @I
1373      |3:
1374        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1375        [1:
1376          @(subaddressing_mode_elim … acc_a) %
1377        |4:
1378          @eq_f2
1379          @(pose … (set_clock ????)) #status #status_refl
1380          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1381          [1:
1382            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1383            [1: @(subaddressing_mode_elim … acc_a) % |*: % ]
1384          |3:
1385            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1386            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1387          |2:
1388            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1389            [1: @(subaddressing_mode_elim … acc_a) % |2: % ]
1390          |4:
1391            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1392            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1393          ]
1394        |*:
1395          %
1396        ]
1397      ]
1398    |2:
1399      #direct_others inversion direct_others #direct #others #direct_others_refl #addr_refl
1400      >EQP -P normalize nodelta
1401      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1402      whd in maps_assm:(??%%);
1403      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1404      [2: normalize nodelta #absurd destruct(absurd) ]
1405      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1406      [2: normalize nodelta #absurd destruct(absurd) ]
1407      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1408      whd in ⊢ (??%?);
1409      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1410      change with (set_arg_8 ????? = ?)
1411      @set_arg_8_status_of_pseudo_status try %
1412      >EQs >EQticks <instr_refl >addr_refl
1413      [1:
1414        @sym_eq @set_clock_status_of_pseudo_status
1415        [1:
1416          @sym_eq @set_program_counter_status_of_pseudo_status %
1417        |2:
1418          @eq_f2 %
1419        ]
1420      |2:
1421        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1422        [1: @(subaddressing_mode_elim … direct) #w % ] %
1423      |3:
1424        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1425        [1:
1426          @(subaddressing_mode_elim … direct) #w %
1427        |4:
1428          @eq_f2
1429          @(pose … (set_clock ????)) #status #status_refl
1430          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1431          [1:
1432            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1433            [1: @(subaddressing_mode_elim … direct) #w % |*: % ]
1434          |3:
1435            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1436            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1437          |2:
1438            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1439            [1: @(subaddressing_mode_elim … direct) #w % |2: % ]
1440          |4:
1441            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1442            [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1443          ]
1444        |*:
1445          %
1446        ]
1447      ]
1448    ]
1449  |32: (* CLR *)
1450    >EQP -P normalize nodelta lapply instr_refl
1451    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1452    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1453    whd in maps_assm:(??%%);
1454    [1,2:
1455      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1456      [2,4: normalize nodelta #absurd destruct(absurd) ]
1457      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1458      whd in ⊢ (??%?);
1459      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1460      [1:
1461        >EQs >EQticks <instr_refl
1462        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1463        @set_arg_1_status_of_pseudo_status try %
1464        [1:
1465          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
1466        |2:
1467          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … false (refl …) addressing_mode_ok_assm_1) %
1468        ]         
1469      |2:
1470        >EQs >EQticks <instr_refl
1471        change with (set_arg_8 ??? ACC_A ? = ?) try %
1472        @set_arg_8_status_of_pseudo_status try %
1473        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ACC_A … addressing_mode_ok_assm_1) %
1474      ]
1475    |3:
1476      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1477      whd in ⊢ (??%?);
1478      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1479      >EQs >EQticks <instr_refl
1480      change with (set_arg_1 ??? CARRY ? = ?) try %
1481      @set_arg_1_status_of_pseudo_status %
1482    ]
1483  |33: (* CPL *)
1484    >EQP -P normalize nodelta lapply instr_refl
1485    @(subaddressing_mode_elim … addr) [3: #w ] -instr_refl #instr_refl normalize nodelta
1486    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1487    whd in maps_assm:(??%%);
1488    [1,2:
1489      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1490      [2,4: normalize nodelta #absurd destruct(absurd) ]
1491      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1492      whd in ⊢ (??%?);
1493      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1494      [1:
1495        >EQs >EQticks <instr_refl
1496        change with (set_arg_1 ??? (BIT_ADDR w) ? = ?)
1497        @set_arg_1_status_of_pseudo_status
1498        [1:
1499          @eq_f
1500          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1501          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1502          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … (BIT_ADDR w) … addressing_mode_ok_assm_1) %
1503        |2:
1504          %
1505        |3:
1506          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … (BIT_ADDR w) … true (refl …) addressing_mode_ok_assm_1) %
1507        |4:
1508          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … (BIT_ADDR w) … (refl …) addressing_mode_ok_assm_1) %
1509        ]       
1510      |2:
1511        >EQs >EQticks <instr_refl
1512        change with (set_8051_sfr ????? = ?)
1513        @set_8051_sfr_status_of_pseudo_status try %
1514        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) try %
1515        normalize nodelta @eq_f
1516        @(pose … (set_clock ????)) #status #status_refl
1517        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
1518        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … ACC_A addressing_mode_ok_assm_1) %
1519      ]
1520    |3:
1521      lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl)
1522      whd in ⊢ (??%?);
1523      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1524      >EQs >EQticks <instr_refl
1525      change with (set_arg_1 ??? CARRY ? = ?) try %
1526      @set_arg_1_status_of_pseudo_status try %
1527      @eq_f
1528      @sym_eq @(pose … (set_clock ????)) #status #status_refl
1529      @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl %
1530    ]
1531  |34,36: (* RL and RR *)
1532    (* XXX: work on the right hand side *)
1533    (* XXX: switch to the left hand side *)
1534    >EQP -P normalize nodelta
1535    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1536    whd in maps_assm:(??%%);
1537    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1538    [2,4: normalize nodelta #absurd destruct(absurd) ]
1539    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1540    whd in ⊢ (??%?);
1541    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1542    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1543    [2,4:
1544      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1545      @eq_f @sym_eq @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1546      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1547      %
1548    ]
1549    @sym_eq @set_clock_status_of_pseudo_status
1550    [2,4:
1551      %
1552    ]
1553    @sym_eq @set_program_counter_status_of_pseudo_status %
1554  |35,37: (* RLC and RRC *)
1555    (* XXX: work on the right hand side *)
1556    (* XXX: switch to the left hand side *)
1557    >EQP -P normalize nodelta
1558    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1559    whd in maps_assm:(??%%);
1560    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm
1561    [2,4: normalize nodelta #absurd destruct(absurd) ]
1562    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1563    whd in ⊢ (??%?);
1564    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1565    change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1566    [2,4:
1567      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm)
1568      @eq_f2
1569      [1,3:
1570        @sym_eq
1571        @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1572        >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1573      |2,4:
1574        @sym_eq @(get_cy_flag_status_of_pseudo_status … M')
1575        @sym_eq @set_clock_status_of_pseudo_status %
1576      ]
1577    |1,3:
1578      @sym_eq @set_arg_1_status_of_pseudo_status try %
1579      @eq_f @(get_8051_sfr_status_of_pseudo_status … policy … (refl …))
1580      >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm) %
1581    ]
1582  |38: (* SWAP *)
1583    >EQP -P normalize nodelta
1584    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1585    whd in maps_assm:(??%%);
1586    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1587    [2: normalize nodelta #absurd destruct(absurd) ]
1588    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1589    whd in ⊢ (??%?);
1590    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1591    whd in ⊢ (??%?);
1592    @(pair_replace ?????????? p)
1593    [1:
1594      @eq_f normalize nodelta
1595      @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
1596      @(get_8051_sfr_status_of_pseudo_status … M' … status)
1597      [1:
1598        >status_refl -status_refl
1599        @sym_eq @set_clock_status_of_pseudo_status
1600        >EQs >EQticks <instr_refl %
1601      |2:
1602        whd in ⊢ (??%?);
1603        >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1604      ]
1605    |2:
1606      @(pair_replace ?????????? p) normalize nodelta
1607      [1:
1608        %
1609      |2:
1610        @set_8051_sfr_status_of_pseudo_status
1611        [1:
1612          @sym_eq @set_clock_status_of_pseudo_status
1613          >EQs >EQticks <instr_refl %
1614        |2:
1615          whd in ⊢ (??%?);
1616          >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
1617        ]
1618      ]     
1619    ]
1620  |39: (* MOV *)
1621    >EQP -P normalize nodelta
1622    inversion addr
1623    [1:
1624      #addr' normalize nodelta
1625      inversion addr'
1626      [1:
1627        #addr'' normalize nodelta
1628        inversion addr''
1629        [1:
1630          #addr''' normalize nodelta
1631          inversion addr'''
1632          [1:
1633            #addr'''' normalize nodelta
1634            inversion addr''''
1635            [1:
1636              normalize nodelta #acc_a_others
1637              cases acc_a_others #acc_a #others
1638              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1639              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1640              whd in maps_assm:(??%%);
1641              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1642              [2: normalize nodelta #absurd destruct(absurd) ]
1643              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1644              [2: normalize nodelta #absurd destruct(absurd) ]
1645              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1646              whd in ⊢ (??%?);
1647              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1648              change with (set_arg_8 ????? = ?)
1649              @set_arg_8_status_of_pseudo_status try %
1650              [1:
1651                @sym_eq @set_clock_status_of_pseudo_status
1652                >EQs >EQticks <instr_refl >addr_refl %
1653              |2:
1654                @(subaddressing_mode_elim … acc_a) @I
1655              |3:
1656                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1657                [1: @(subaddressing_mode_elim … acc_a) % ]
1658                >EQs >EQticks <instr_refl >addr_refl
1659                [1,2:
1660                  %
1661                |3:
1662                  @(pose … (set_clock ????)) #status #status_refl
1663                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1664                  [1:
1665                    @sym_eq @set_clock_status_of_pseudo_status %
1666                  |2:
1667                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1668                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1669                  |3:
1670                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1671                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1672                  ]
1673                ]
1674              ]
1675            |2:
1676              #others_others' cases others_others' #others #others' normalize nodelta
1677              #addr_refl'''' #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1678              #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1679              whd in maps_assm:(??%%);
1680              inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1681              [2: normalize nodelta #absurd destruct(absurd) ]
1682              inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1683              [2: normalize nodelta #absurd destruct(absurd) ]
1684              normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1685              whd in ⊢ (??%?);
1686              <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1687              change with (set_arg_8 ????? = ?)
1688              @set_arg_8_status_of_pseudo_status try %
1689              >EQs >EQticks <instr_refl >addr_refl try %
1690              [1:
1691                @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
1692                [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1693              |2:
1694                @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
1695                [1:
1696                  @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1697                |2,3:
1698                  %
1699                |4:
1700                  @(pose … (set_clock ????)) #status #status_refl
1701                  @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl
1702                  [1:
1703                    @sym_eq @set_clock_status_of_pseudo_status %
1704                  |2:
1705                    @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2)
1706                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1707                  |3:
1708                    @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2)
1709                    [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1710                  ]
1711                ]
1712              ]
1713            ]
1714          |2:
1715            #direct_others cases direct_others #direct #others
1716            #addr_refl''' #addr_refl'' #addr_refl' #addr_refl
1717            #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1718            whd in maps_assm:(??%%);
1719            inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1720            [2: normalize nodelta #absurd destruct(absurd) ]
1721            inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1722            [2: normalize nodelta #absurd destruct(absurd) ]
1723            normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1724            whd in ⊢ (??%?);
1725            <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1726            change with (set_arg_8 ????? = ?)
1727            @set_arg_8_status_of_pseudo_status try %
1728            >EQs >EQticks <instr_refl >addr_refl
1729            [1:
1730              @sym_eq @set_clock_status_of_pseudo_status %
1731            |2:
1732              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1)
1733              [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1734            |3:
1735              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1)
1736              [1:
1737                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1738              |2,3:
1739                %
1740              |4:
1741                @(pose … (set_clock ????)) #status #status_refl
1742                @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1743                [1:
1744                  @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1745                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1746                |2:
1747                  @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1748                  [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1749                ]
1750              ]
1751            ]
1752          ]
1753        |2:
1754          #dptr_data16 cases dptr_data16 #dptr #data16 normalize nodelta
1755          #addr_refl'' #addr_refl' #addr_refl
1756          #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1757          whd in maps_assm:(??%%);
1758          inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1759          [2: normalize nodelta #absurd destruct(absurd) ]
1760          inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1761          [2: normalize nodelta #absurd destruct(absurd) ]
1762          normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1763          whd in ⊢ (??%?);
1764          <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1765          change with (set_arg_16 ????? = ?)
1766          @set_arg_16_status_of_pseudo_status try %
1767          >EQs >EQticks <instr_refl >addr_refl
1768          @sym_eq @set_clock_status_of_pseudo_status %
1769        ]
1770      |2:
1771        #carry_bit_addr cases carry_bit_addr #carry #bit_addr normalize nodelta
1772        #addr_refl' #addr_refl
1773        #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1774        whd in maps_assm:(??%%);
1775        inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1776        [2: normalize nodelta #absurd destruct(absurd) ]
1777        inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1778        [2: normalize nodelta #absurd destruct(absurd) ]
1779        normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1780        whd in ⊢ (??%?);
1781        <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1782        change with (set_arg_1 ????? = ?)
1783        @set_arg_1_status_of_pseudo_status
1784        >EQs >EQticks <instr_refl >addr_refl try %
1785        [1:
1786          @sym_eq @(pose … (set_clock ????)) #status #status_refl
1787          @sym_eq @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1788          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get … addressing_mode_ok_assm_2)
1789        |2,3:
1790          @(subaddressing_mode_elim … carry) @I
1791        ]
1792      ]
1793    |2:
1794      #bit_addr_carry cases bit_addr_carry #bit_addr #carry normalize nodelta
1795      #addr_refl
1796      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1797      whd in maps_assm:(??%%);
1798      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1799      [2: normalize nodelta #absurd destruct(absurd) ]
1800      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1801      [2: normalize nodelta #absurd destruct(absurd) ]
1802      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1803      whd in ⊢ (??%?);
1804      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1805      change with (set_arg_1 ????? = ?)
1806      @set_arg_1_status_of_pseudo_status
1807      [1:
1808        >EQs >EQticks <instr_refl >addr_refl
1809        @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
1810        @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1811        @(subaddressing_mode_elim … carry) @I
1812      |2:
1813        >EQs >EQticks <instr_refl >addr_refl %
1814      |3,4:
1815        @(pose … (set_clock ????)) #status #status_refl
1816        [1:
1817          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try %
1818        |2:
1819          @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try %
1820        ]
1821        >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl
1822        lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?);
1823        @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption
1824      ]
1825    ]
1826  |40: (* MOVX *)
1827    >EQP -P normalize nodelta
1828    inversion addr
1829    [1:
1830      #acc_a_others cases acc_a_others #acc_a #others normalize nodelta
1831      #addr_refl
1832      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1833      whd in maps_assm:(??%%);
1834      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1835      [2: normalize nodelta #absurd destruct(absurd) ]
1836      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1837      [2: normalize nodelta #absurd destruct(absurd) ]
1838      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1839      whd in ⊢ (??%?);
1840      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1841      change with (set_arg_8 ????? = ?)
1842      @set_arg_8_status_of_pseudo_status try %
1843      >EQs >EQticks <instr_refl >addr_refl
1844      [1:
1845        @sym_eq @set_clock_status_of_pseudo_status %
1846      |2:
1847        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1)
1848        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1849      |3:
1850        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1)
1851        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try %
1852        @(pose … (set_clock ????)) #status #status_refl
1853        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1854        [1:
1855          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2)
1856          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1857        |2:
1858          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2)
1859          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1860        ]
1861      ]
1862    |2:
1863      #others_acc_a cases others_acc_a #others #acc_a
1864      #addr_refl
1865      #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1866      whd in maps_assm:(??%%);
1867      inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1868      [2: normalize nodelta #absurd destruct(absurd) ]
1869      inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1870      [2: normalize nodelta #absurd destruct(absurd) ]
1871      normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1872      whd in ⊢ (??%?);
1873      <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1874      change with (set_arg_8 ????? = ?)
1875      @set_arg_8_status_of_pseudo_status
1876      >EQs >EQticks <instr_refl >addr_refl try %
1877      [1:
1878        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1)
1879        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %
1880      |2:
1881        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1)
1882        [1:
1883          @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1884        |2,3:
1885          %
1886        |4:
1887          @(pose … (set_clock ????)) #status #status_refl
1888          @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1889          [1:
1890            @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2)
1891            [1: @(subaddressing_mode_elim … acc_a) % ] %
1892          |2:
1893            @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2)
1894            [1: @(subaddressing_mode_elim … acc_a) % ] %
1895          ]
1896        ]
1897      ]
1898    ]
1899  |41: (* SETB *)
1900    >EQs >EQticks <instr_refl
1901    >EQP -P normalize nodelta
1902    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1903    whd in maps_assm:(??%%);
1904    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1905    [2: normalize nodelta #absurd destruct(absurd) ]
1906    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1907    whd in ⊢ (??%?);
1908    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1909    change with (set_arg_1 ????? = ?)
1910    @set_arg_1_status_of_pseudo_status try %
1911    [1:
1912      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
1913    |2:
1914      @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1)
1915    ]
1916  |*)*)42: (* PUSH *)
1917    >EQP -P normalize nodelta lapply instr_refl
1918    @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta
1919    #sigma_increment_commutation
1920    whd in ⊢ (??%? → ?);
1921    @vsplit_elim #bit_one #seven_bits
1922    cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one
1923    cases bitone #bit_one_seven_bits_refl normalize nodelta
1924    [ @eq_bv_elim #seven_bits_refl normalize nodelta
1925    | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
1926      #lookup_from_internal_ram_refl ]
1927    @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
1928    whd in ⊢ (??%?);
1929    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1930    whd in ⊢ (??%?);
1931    @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
1932    @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
1933    [1,3,5,7:
1934      @eq_f2 try %
1935      @(pose … (set_clock ????)) #status #status_refl
1936      @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try %
1937      @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
1938    |*:
1939      >EQs >EQticks <instr_refl
1940      @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉)
1941      [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try %
1942      | >get_8051_sfr_set_8051_sfr
1943        cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1)))
1944        [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl))
1945          change with (add ??? = ?); @eq_f2 try %
1946          cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp
1947        >EQnew_sp
1948        @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
1949       
1950     
1951         XXX
1952        (*CSC: lemma here*)
1953        cases accA
1954        whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
1955        [ whd whd in match delete_from_internal_ram; normalize nodelta
1956          @pair_elim #bit_one
1957        |
1958        ]
1959      |
1960      |
1961      ]
1962    ]
1963  |43: (* POP *)
1964    cases daemon
1965  |44:
1966    >EQP -P normalize nodelta
1967    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1968    whd in maps_assm:(??%%);
1969    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1970    [2: normalize nodelta #absurd destruct(absurd) ]
1971    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1972    [2: normalize nodelta #absurd destruct(absurd) ]
1973    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1974    whd in ⊢ (??%?);
1975    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
1976    change with (set_arg_8 ????? = ?)
1977    >EQs >EQticks <instr_refl
1978    @set_arg_8_status_of_pseudo_status try %
1979    [1:
1980      @sym_eq @set_8051_sfr_status_of_pseudo_status try %
1981      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) normalize nodelta
1982      @(pose … (set_clock ????)) #status #status_refl
1983      @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
1984      [1:
1985        @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
1986        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
1987      |2:
1988        @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1989        [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
1990      ]
1991    |2:
1992      @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
1993      [1:
1994        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
1995      |*:
1996        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
1997        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
1998        whd in match sfr_8051_index; normalize nodelta
1999        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2000      ]
2001    |3:
2002      @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2003      [1:
2004        @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2005      |2:
2006        whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2007        whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2008        whd in match sfr_8051_index; normalize nodelta
2009        >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2010      |3:
2011        @(pose … (set_clock ????)) #status #status_refl
2012        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2013        whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2014      ]
2015    ]
2016  |45: (* XCHD *)
2017    >EQP -P normalize nodelta
2018    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2019    whd in maps_assm:(??%%);
2020    inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
2021    [2: normalize nodelta #absurd destruct(absurd) ]
2022    inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
2023    [2: normalize nodelta #absurd destruct(absurd) ]
2024    normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
2025    whd in ⊢ (??%?);
2026    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2027    whd in ⊢ (??%?);
2028    @(pair_replace ?????????? p) normalize nodelta
2029    >EQs >EQticks <instr_refl
2030    [1:
2031      @eq_f
2032      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2033      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M' … status) >status_refl -status_refl try %
2034      whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2035    |2:
2036      @(pair_replace ?????????? p1) normalize nodelta
2037      >EQs >EQticks <instr_refl
2038      [1:
2039        @eq_f
2040        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2041        @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try %
2042        [1:
2043          @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2)
2044          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2045        |2:
2046          @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2047          [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % |*: % ]
2048        ]
2049      |2:
2050        @(pair_replace ?????????? p) normalize nodelta
2051        >EQs >EQticks <instr_refl
2052        [1:
2053          %
2054        |2:
2055          @(pair_replace ?????????? p1) normalize nodelta
2056          >EQs >EQticks <instr_refl
2057          [1:
2058            %
2059          |2:
2060            @set_arg_8_status_of_pseudo_status try %
2061            [1:
2062              @sym_eq @set_8051_sfr_status_of_pseudo_status try %
2063              whd in ⊢ (??%?); >(addressing_mode_ok_to_snd_M_data … addressing_mode_ok_assm_1) %
2064            |2:
2065              @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2)
2066              [1:
2067                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2068              |2:
2069                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2070                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2071                whd in match sfr_8051_index; normalize nodelta
2072                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2073              ]
2074            |3:
2075              @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try %
2076              [1:
2077                @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %
2078              |2:
2079                whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2080                whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2081                whd in match sfr_8051_index; normalize nodelta
2082                >get_index_v_set_index_miss [2: % #absurd destruct(absurd) ] %
2083              ]
2084            ]
2085          ]
2086        ]
2087      ]
2088    ]
2089  |46: (* RET *)
2090    >EQP -P normalize nodelta
2091    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2092    whd in maps_assm:(??%%); normalize nodelta in maps_assm;
2093    lapply maps_assm inversion M #callM #accM #callM_accM_refl normalize nodelta
2094    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_1
2095    [2: normalize nodelta #absurd destruct(absurd) ]
2096    inversion (assoc_list_exists ?????) #addressing_mode_ok_assm_2
2097    [2: normalize nodelta #absurd destruct(absurd) ]
2098    normalize nodelta @Some_Some_elim #Mrefl <callM_accM_refl destruct(Mrefl)
2099    whd in ⊢ (??%?);
2100    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
2101    whd in ⊢ (??%?);
2102    @(pair_replace ?????????? p) normalize nodelta
2103    >EQs >EQticks <instr_refl
2104    [1:
2105      @eq_f3 try %
2106      @sym_eq @(pose … (set_clock ????)) #status #status_refl
2107      @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl %
2108    |2:
2109      @(pair_replace ?????????? p1) normalize nodelta
2110      >EQs >EQticks <instr_refl
2111      [1:
2112        @eq_f3 try %
2113        @sym_eq @(pose … (set_clock ????)) #status #status_refl
2114        @sym_eq @(get_8051_sfr_status_of_pseudo_status … M … status) >status_refl -status_refl
2115        [1:
2116          cases daemon
2117          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2118        |2:
2119          whd in match get_8051_sfr in ⊢ (???%); normalize nodelta
2120          whd in match set_8051_sfr in ⊢ (???%); normalize nodelta
2121          whd in match sfr_8051_index; normalize nodelta
2122          >get_index_v_set_index_hit
2123          change with (get_8051_sfr pseudo_assembly_program cm ? SFR_SP = new_sp)
2124          cases daemon
2125          (* XXX: bug in the return code for addressing_mode_ok --- should not add to the SP when returning *)
2126        ]
2127      |2:
2128        cases daemon (* XXX *)
2129      ]
2130    ]
2131  |47: (* RETI *)
2132    cases daemon
2133  |48: (* NOP *)
2134    >EQP -P normalize nodelta
2135    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
2136    whd in maps_assm:(??%%);
2137    lapply maps_assm; @Some_Some_elim #Mrefl destruct(Mrefl)
2138    whd in ⊢ (??%?);
2139    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
2140    change with (set_clock ???? = ?)
2141    @set_clock_status_of_pseudo_status %
2142  ]
2143qed.
Note: See TracBrowser for help on using the repository browser.