1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "freescale/opcode_base_lemmas_instrmode1.ma".
25 (* ********************************************** *)
26 (* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
27 (* ********************************************** *)
29 nlemma decidable_im1 : ∀x:instr_mode.decidable (MODE_INH = x).
30 #x; nnormalize; nelim x;
31 ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
32 ##| ##31,32,33,34: #n; ##]
33 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
36 nlemma decidable_im2 : ∀x:instr_mode.decidable (MODE_INHA = x).
37 #x; nnormalize; nelim x;
38 ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
39 ##| ##31,32,33,34: #n; ##]
40 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
43 nlemma decidable_im3 : ∀x:instr_mode.decidable (MODE_INHX = x).
44 #x; nnormalize; nelim x;
45 ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
46 ##| ##31,32,33,34: #n; ##]
47 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
50 nlemma decidable_im4 : ∀x:instr_mode.decidable (MODE_INHH = x).
51 #x; nnormalize; nelim x;
52 ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
53 ##| ##31,32,33,34: #n; ##]
54 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
57 nlemma decidable_im5 : ∀x:instr_mode.decidable (MODE_INHX0ADD = x).
58 #x; nnormalize; nelim x;
59 ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
60 ##| ##31,32,33,34: #n; ##]
61 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
64 nlemma decidable_im6 : ∀x:instr_mode.decidable (MODE_INHX1ADD = x).
65 #x; nnormalize; nelim x;
66 ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
67 ##| ##31,32,33,34: #n; ##]
68 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
71 nlemma decidable_im7 : ∀x:instr_mode.decidable (MODE_INHX2ADD = x).
72 #x; nnormalize; nelim x;
73 ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
74 ##| ##31,32,33,34: #n; ##]
75 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
78 nlemma decidable_im8 : ∀x:instr_mode.decidable (MODE_IMM1 = x).
79 #x; nnormalize; nelim x;
80 ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
81 ##| ##31,32,33,34: #n; ##]
82 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
85 nlemma decidable_im9 : ∀x:instr_mode.decidable (MODE_IMM1EXT = x).
86 #x; nnormalize; nelim x;
87 ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
88 ##| ##31,32,33,34: #n; ##]
89 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
92 nlemma decidable_im10 : ∀x:instr_mode.decidable (MODE_IMM2 = x).
93 #x; nnormalize; nelim x;
94 ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
95 ##| ##31,32,33,34: #n; ##]
96 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
99 nlemma decidable_im11 : ∀x:instr_mode.decidable (MODE_DIR1 = x).
100 #x; nnormalize; nelim x;
101 ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
102 ##| ##31,32,33,34: #n; ##]
103 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
106 nlemma decidable_im12 : ∀x:instr_mode.decidable (MODE_DIR2 = x).
107 #x; nnormalize; nelim x;
108 ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
109 ##| ##31,32,33,34: #n; ##]
110 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
113 nlemma decidable_im13 : ∀x:instr_mode.decidable (MODE_IX0 = x).
114 #x; nnormalize; nelim x;
115 ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
116 ##| ##31,32,33,34: #n; ##]
117 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
120 nlemma decidable_im14 : ∀x:instr_mode.decidable (MODE_IX1 = x).
121 #x; nnormalize; nelim x;
122 ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
123 ##| ##31,32,33,34: #n; ##]
124 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
127 nlemma decidable_im15 : ∀x:instr_mode.decidable (MODE_IX2 = x).
128 #x; nnormalize; nelim x;
129 ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
130 ##| ##31,32,33,34: #n; ##]
131 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
134 nlemma decidable_im16 : ∀x:instr_mode.decidable (MODE_SP1 = x).
135 #x; nnormalize; nelim x;
136 ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
137 ##| ##31,32,33,34: #n; ##]
138 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
141 nlemma decidable_im17 : ∀x:instr_mode.decidable (MODE_SP2 = x).
142 #x; nnormalize; nelim x;
143 ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
144 ##| ##31,32,33,34: #n; ##]
145 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
148 nlemma decidable_im18 : ∀x:instr_mode.decidable (MODE_DIR1_to_DIR1 = x).
149 #x; nnormalize; nelim x;
150 ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
151 ##| ##31,32,33,34: #n; ##]
152 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
155 nlemma decidable_im19 : ∀x:instr_mode.decidable (MODE_IMM1_to_DIR1 = x).
156 #x; nnormalize; nelim x;
157 ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
158 ##| ##31,32,33,34: #n; ##]
159 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
162 nlemma decidable_im20 : ∀x:instr_mode.decidable (MODE_IX0p_to_DIR1 = x).
163 #x; nnormalize; nelim x;
164 ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
165 ##| ##31,32,33,34: #n; ##]
166 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
169 nlemma decidable_im21 : ∀x:instr_mode.decidable (MODE_DIR1_to_IX0p = x).
170 #x; nnormalize; nelim x;
171 ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
172 ##| ##31,32,33,34: #n; ##]
173 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
176 nlemma decidable_im22 : ∀x:instr_mode.decidable (MODE_INHA_and_IMM1 = x).
177 #x; nnormalize; nelim x;
178 ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
179 ##| ##31,32,33,34: #n; ##]
180 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
183 nlemma decidable_im23 : ∀x:instr_mode.decidable (MODE_INHX_and_IMM1 = x).
184 #x; nnormalize; nelim x;
185 ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
186 ##| ##31,32,33,34: #n; ##]
187 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
190 nlemma decidable_im24 : ∀x:instr_mode.decidable (MODE_IMM1_and_IMM1 = x).
191 #x; nnormalize; nelim x;
192 ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
193 ##| ##31,32,33,34: #n; ##]
194 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
197 nlemma decidable_im25 : ∀x:instr_mode.decidable (MODE_DIR1_and_IMM1 = x).
198 #x; nnormalize; nelim x;
199 ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
200 ##| ##31,32,33,34: #n; ##]
201 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
204 nlemma decidable_im26 : ∀x:instr_mode.decidable (MODE_IX0_and_IMM1 = x).
205 #x; nnormalize; nelim x;
206 ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
207 ##| ##31,32,33,34: #n; ##]
208 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
211 nlemma decidable_im27 : ∀x:instr_mode.decidable (MODE_IX0p_and_IMM1 = x).
212 #x; nnormalize; nelim x;
213 ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
214 ##| ##31,32,33,34: #n; ##]
215 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
218 nlemma decidable_im28 : ∀x:instr_mode.decidable (MODE_IX1_and_IMM1 = x).
219 #x; nnormalize; nelim x;
220 ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
221 ##| ##31,32,33,34: #n; ##]
222 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
225 nlemma decidable_im29 : ∀x:instr_mode.decidable (MODE_IX1p_and_IMM1 = x).
226 #x; nnormalize; nelim x;
227 ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
228 ##| ##31,32,33,34: #n; ##]
229 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
232 nlemma decidable_im30 : ∀x:instr_mode.decidable (MODE_SP1_and_IMM1 = x).
233 #x; nnormalize; nelim x;
234 ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
235 ##| ##31,32,33,34: #n; ##]
236 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
239 nlemma decidable_im31 : ∀n.∀x:instr_mode.decidable ((MODE_DIRn n) = x).
240 #n1; #x; nnormalize; nelim x;
241 ##[ ##31: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct n1 n2) …);
242 ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
243 ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_DIRn … H1))
245 ##| ##32,33,34: #n; ##]
246 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
249 nlemma decidable_im32 : ∀n.∀x:instr_mode.decidable ((MODE_DIRn_and_IMM1 n) = x).
250 #n1; #x; nnormalize; nelim x;
251 ##[ ##32: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct n1 n2) …);
252 ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
253 ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_DIRn_and_IMM1 … H1))
255 ##| ##31,33,34: #n; ##]
256 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
259 nlemma decidable_im33 : ∀n.∀x:instr_mode.decidable ((MODE_TNY n) = x).
260 #n1; #x; nnormalize; nelim x;
261 ##[ ##33: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ex n1 n2) …);
262 ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
263 ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_TNY … H1))
265 ##| ##31,32,34: #n; ##]
266 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
269 nlemma decidable_im34 : ∀n.∀x:instr_mode.decidable ((MODE_SRT n) = x).
270 #n1; #x; nnormalize; nelim x;
271 ##[ ##34: #n2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bit n1 n2) …);
272 ##[ ##1: #H; nrewrite > H; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
273 ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) ?); #H1; napply (H (instrmode_destruct_MODE_SRT … H1))
275 ##| ##31,32,33: #n; ##]
276 ##[ ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (instrmode_destruct … H) ##]
279 nlemma decidable_im : ∀x,y:instr_mode.decidable (x = y).
281 ##[ ##1: napply decidable_im1 ##| ##2: napply decidable_im2
282 ##| ##3: napply decidable_im3 ##| ##4: napply decidable_im4
283 ##| ##5: napply decidable_im5 ##| ##6: napply decidable_im6
284 ##| ##7: napply decidable_im7 ##| ##8: napply decidable_im8
285 ##| ##9: napply decidable_im9 ##| ##10: napply decidable_im10
286 ##| ##11: napply decidable_im11 ##| ##12: napply decidable_im12
287 ##| ##13: napply decidable_im13 ##| ##14: napply decidable_im14
288 ##| ##15: napply decidable_im15 ##| ##16: napply decidable_im16
289 ##| ##17: napply decidable_im17 ##| ##18: napply decidable_im18
290 ##| ##19: napply decidable_im19 ##| ##20: napply decidable_im20
291 ##| ##21: napply decidable_im21 ##| ##22: napply decidable_im22
292 ##| ##23: napply decidable_im23 ##| ##24: napply decidable_im24
293 ##| ##25: napply decidable_im25 ##| ##26: napply decidable_im26
294 ##| ##27: napply decidable_im27 ##| ##28: napply decidable_im28
295 ##| ##29: napply decidable_im29 ##| ##30: napply decidable_im30
296 ##| ##31: napply decidable_im31 ##| ##32: napply decidable_im32
297 ##| ##33: napply decidable_im33 ##| ##34: napply decidable_im34
301 nlemma neqim_to_neq1 : ∀i2.(eq_im MODE_INH i2 = false) → (MODE_INH ≠ i2).
302 #i2; nelim i2; nnormalize;
303 ##[ ##1: #H; napply (bool_destruct … H)
304 ##| ##31,32,33,34: #n ##]
305 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
309 nlemma neqim_to_neq2 : ∀i2.(eq_im MODE_INHA i2 = false) → (MODE_INHA ≠ i2).
310 #i2; nelim i2; nnormalize;
311 ##[ ##2: #H; napply (bool_destruct … H)
312 ##| ##31,32,33,34: #n ##]
313 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
317 nlemma neqim_to_neq3 : ∀i2.(eq_im MODE_INHX i2 = false) → (MODE_INHX ≠ i2).
318 #i2; nelim i2; nnormalize;
319 ##[ ##3: #H; napply (bool_destruct … H)
320 ##| ##31,32,33,34: #n ##]
321 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
325 nlemma neqim_to_neq4 : ∀i2.(eq_im MODE_INHH i2 = false) → (MODE_INHH ≠ i2).
326 #i2; nelim i2; nnormalize;
327 ##[ ##4: #H; napply (bool_destruct … H)
328 ##| ##31,32,33,34: #n ##]
329 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
333 nlemma neqim_to_neq5 : ∀i2.(eq_im MODE_INHX0ADD i2 = false) → (MODE_INHX0ADD ≠ i2).
334 #i2; nelim i2; nnormalize;
335 ##[ ##5: #H; napply (bool_destruct … H)
336 ##| ##31,32,33,34: #n ##]
337 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
341 nlemma neqim_to_neq6 : ∀i2.(eq_im MODE_INHX1ADD i2 = false) → (MODE_INHX1ADD ≠ i2).
342 #i2; nelim i2; nnormalize;
343 ##[ ##6: #H; napply (bool_destruct … H)
344 ##| ##31,32,33,34: #n ##]
345 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
349 nlemma neqim_to_neq7 : ∀i2.(eq_im MODE_INHX2ADD i2 = false) → (MODE_INHX2ADD ≠ i2).
350 #i2; nelim i2; nnormalize;
351 ##[ ##7: #H; napply (bool_destruct … H)
352 ##| ##31,32,33,34: #n ##]
353 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
357 nlemma neqim_to_neq8 : ∀i2.(eq_im MODE_IMM1 i2 = false) → (MODE_IMM1 ≠ i2).
358 #i2; nelim i2; nnormalize;
359 ##[ ##8: #H; napply (bool_destruct … H)
360 ##| ##31,32,33,34: #n ##]
361 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
365 nlemma neqim_to_neq9 : ∀i2.(eq_im MODE_IMM1EXT i2 = false) → (MODE_IMM1EXT ≠ i2).
366 #i2; nelim i2; nnormalize;
367 ##[ ##9: #H; napply (bool_destruct … H)
368 ##| ##31,32,33,34: #n ##]
369 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
373 nlemma neqim_to_neq10 : ∀i2.(eq_im MODE_IMM2 i2 = false) → (MODE_IMM2 ≠ i2).
374 #i2; nelim i2; nnormalize;
375 ##[ ##10: #H; napply (bool_destruct … H)
376 ##| ##31,32,33,34: #n ##]
377 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
381 nlemma neqim_to_neq11 : ∀i2.(eq_im MODE_DIR1 i2 = false) → (MODE_DIR1 ≠ i2).
382 #i2; nelim i2; nnormalize;
383 ##[ ##11: #H; napply (bool_destruct … H)
384 ##| ##31,32,33,34: #n ##]
385 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
389 nlemma neqim_to_neq12 : ∀i2.(eq_im MODE_DIR2 i2 = false) → (MODE_DIR2 ≠ i2).
390 #i2; nelim i2; nnormalize;
391 ##[ ##12: #H; napply (bool_destruct … H)
392 ##| ##31,32,33,34: #n ##]
393 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
397 nlemma neqim_to_neq13 : ∀i2.(eq_im MODE_IX0 i2 = false) → (MODE_IX0 ≠ i2).
398 #i2; nelim i2; nnormalize;
399 ##[ ##13: #H; napply (bool_destruct … H)
400 ##| ##31,32,33,34: #n ##]
401 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
405 nlemma neqim_to_neq14 : ∀i2.(eq_im MODE_IX1 i2 = false) → (MODE_IX1 ≠ i2).
406 #i2; nelim i2; nnormalize;
407 ##[ ##14: #H; napply (bool_destruct … H)
408 ##| ##31,32,33,34: #n ##]
409 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
413 nlemma neqim_to_neq15 : ∀i2.(eq_im MODE_IX2 i2 = false) → (MODE_IX2 ≠ i2).
414 #i2; nelim i2; nnormalize;
415 ##[ ##15: #H; napply (bool_destruct … H)
416 ##| ##31,32,33,34: #n ##]
417 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
421 nlemma neqim_to_neq16 : ∀i2.(eq_im MODE_SP1 i2 = false) → (MODE_SP1 ≠ i2).
422 #i2; nelim i2; nnormalize;
423 ##[ ##16: #H; napply (bool_destruct … H)
424 ##| ##31,32,33,34: #n ##]
425 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
429 nlemma neqim_to_neq17 : ∀i2.(eq_im MODE_SP2 i2 = false) → (MODE_SP2 ≠ i2).
430 #i2; nelim i2; nnormalize;
431 ##[ ##17: #H; napply (bool_destruct … H)
432 ##| ##31,32,33,34: #n ##]
433 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
437 nlemma neqim_to_neq18 : ∀i2.(eq_im MODE_DIR1_to_DIR1 i2 = false) → (MODE_DIR1_to_DIR1 ≠ i2).
438 #i2; nelim i2; nnormalize;
439 ##[ ##18: #H; napply (bool_destruct … H)
440 ##| ##31,32,33,34: #n ##]
441 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
445 nlemma neqim_to_neq19 : ∀i2.(eq_im MODE_IMM1_to_DIR1 i2 = false) → (MODE_IMM1_to_DIR1 ≠ i2).
446 #i2; nelim i2; nnormalize;
447 ##[ ##19: #H; napply (bool_destruct … H)
448 ##| ##31,32,33,34: #n ##]
449 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
453 nlemma neqim_to_neq20 : ∀i2.(eq_im MODE_IX0p_to_DIR1 i2 = false) → (MODE_IX0p_to_DIR1 ≠ i2).
454 #i2; nelim i2; nnormalize;
455 ##[ ##20: #H; napply (bool_destruct … H)
456 ##| ##31,32,33,34: #n ##]
457 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
461 nlemma neqim_to_neq21 : ∀i2.(eq_im MODE_DIR1_to_IX0p i2 = false) → (MODE_DIR1_to_IX0p ≠ i2).
462 #i2; nelim i2; nnormalize;
463 ##[ ##21: #H; napply (bool_destruct … H)
464 ##| ##31,32,33,34: #n ##]
465 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
469 nlemma neqim_to_neq22 : ∀i2.(eq_im MODE_INHA_and_IMM1 i2 = false) → (MODE_INHA_and_IMM1 ≠ i2).
470 #i2; nelim i2; nnormalize;
471 ##[ ##22: #H; napply (bool_destruct … H)
472 ##| ##31,32,33,34: #n ##]
473 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
477 nlemma neqim_to_neq23 : ∀i2.(eq_im MODE_INHX_and_IMM1 i2 = false) → (MODE_INHX_and_IMM1 ≠ i2).
478 #i2; nelim i2; nnormalize;
479 ##[ ##23: #H; napply (bool_destruct … H)
480 ##| ##31,32,33,34: #n ##]
481 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
485 nlemma neqim_to_neq24 : ∀i2.(eq_im MODE_IMM1_and_IMM1 i2 = false) → (MODE_IMM1_and_IMM1 ≠ i2).
486 #i2; nelim i2; nnormalize;
487 ##[ ##24: #H; napply (bool_destruct … H)
488 ##| ##31,32,33,34: #n ##]
489 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
493 nlemma neqim_to_neq25 : ∀i2.(eq_im MODE_DIR1_and_IMM1 i2 = false) → (MODE_DIR1_and_IMM1 ≠ i2).
494 #i2; nelim i2; nnormalize;
495 ##[ ##25: #H; napply (bool_destruct … H)
496 ##| ##31,32,33,34: #n ##]
497 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
501 nlemma neqim_to_neq26 : ∀i2.(eq_im MODE_IX0_and_IMM1 i2 = false) → (MODE_IX0_and_IMM1 ≠ i2).
502 #i2; nelim i2; nnormalize;
503 ##[ ##26: #H; napply (bool_destruct … H)
504 ##| ##31,32,33,34: #n ##]
505 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
509 nlemma neqim_to_neq27 : ∀i2.(eq_im MODE_IX0p_and_IMM1 i2 = false) → (MODE_IX0p_and_IMM1 ≠ i2).
510 #i2; nelim i2; nnormalize;
511 ##[ ##27: #H; napply (bool_destruct … H)
512 ##| ##31,32,33,34: #n ##]
513 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
517 nlemma neqim_to_neq28 : ∀i2.(eq_im MODE_IX1_and_IMM1 i2 = false) → (MODE_IX1_and_IMM1 ≠ i2).
518 #i2; nelim i2; nnormalize;
519 ##[ ##28: #H; napply (bool_destruct … H)
520 ##| ##31,32,33,34: #n ##]
521 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
525 nlemma neqim_to_neq29 : ∀i2.(eq_im MODE_IX1p_and_IMM1 i2 = false) → (MODE_IX1p_and_IMM1 ≠ i2).
526 #i2; nelim i2; nnormalize;
527 ##[ ##29: #H; napply (bool_destruct … H)
528 ##| ##31,32,33,34: #n ##]
529 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
533 nlemma neqim_to_neq30 : ∀i2.(eq_im MODE_SP1_and_IMM1 i2 = false) → (MODE_SP1_and_IMM1 ≠ i2).
534 #i2; nelim i2; nnormalize;
535 ##[ ##30: #H; napply (bool_destruct … H)
536 ##| ##31,32,33,34: #n ##]
537 ##[ ##*: #H; #H1; napply (instrmode_destruct … H1)
541 nlemma neqim_to_neq31 : ∀n.∀i2.(eq_im (MODE_DIRn n) i2 = false) → ((MODE_DIRn n) ≠ i2).
543 ##[ ##31: #n2; #H; nchange in H:(%) with (eq_oct n1 n2 = false);
544 nnormalize; #H1; napply (neqoct_to_neq … H); napply (instrmode_destruct_MODE_DIRn … H1)
545 ##| ##32,33,34: #n ##]
546 ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
550 nlemma neqim_to_neq32 : ∀n.∀i2.(eq_im (MODE_DIRn_and_IMM1 n) i2 = false) → ((MODE_DIRn_and_IMM1 n) ≠ i2).
552 ##[ ##32: #n2; #H; nchange in H:(%) with (eq_oct n1 n2 = false);
553 nnormalize; #H1; napply (neqoct_to_neq … H); napply (instrmode_destruct_MODE_DIRn_and_IMM1 … H1)
554 ##| ##31,33,34: #n ##]
555 ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
559 nlemma neqim_to_neq33 : ∀n.∀i2.(eq_im (MODE_TNY n) i2 = false) → ((MODE_TNY n) ≠ i2).
561 ##[ ##33: #n2; #H; nchange in H:(%) with (eq_ex n1 n2 = false);
562 nnormalize; #H1; napply (neqex_to_neq … H); napply (instrmode_destruct_MODE_TNY … H1)
563 ##| ##31,32,34: #n ##]
564 ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
568 nlemma neqim_to_neq34 : ∀n.∀i2.(eq_im (MODE_SRT n) i2 = false) → ((MODE_SRT n) ≠ i2).
570 ##[ ##34: #n2; #H; nchange in H:(%) with (eq_bit n1 n2 = false);
571 nnormalize; #H1; napply (neqbit_to_neq … H); napply (instrmode_destruct_MODE_SRT … H1)
572 ##| ##31,32,33: #n ##]
573 ##[ ##*: nnormalize; #H; #H1; napply (instrmode_destruct … H1)
577 nlemma neqim_to_neq : ∀i1,i2.(eq_im i1 i2 = false) → (i1 ≠ i2).
579 ##[ ##1: napply neqim_to_neq1 ##| ##2: napply neqim_to_neq2
580 ##| ##3: napply neqim_to_neq3 ##| ##4: napply neqim_to_neq4
581 ##| ##5: napply neqim_to_neq5 ##| ##6: napply neqim_to_neq6
582 ##| ##7: napply neqim_to_neq7 ##| ##8: napply neqim_to_neq8
583 ##| ##9: napply neqim_to_neq9 ##| ##10: napply neqim_to_neq10
584 ##| ##11: napply neqim_to_neq11 ##| ##12: napply neqim_to_neq12
585 ##| ##13: napply neqim_to_neq13 ##| ##14: napply neqim_to_neq14
586 ##| ##15: napply neqim_to_neq15 ##| ##16: napply neqim_to_neq16
587 ##| ##17: napply neqim_to_neq17 ##| ##18: napply neqim_to_neq18
588 ##| ##19: napply neqim_to_neq19 ##| ##20: napply neqim_to_neq20
589 ##| ##21: napply neqim_to_neq21 ##| ##22: napply neqim_to_neq22
590 ##| ##23: napply neqim_to_neq23 ##| ##24: napply neqim_to_neq24
591 ##| ##25: napply neqim_to_neq25 ##| ##26: napply neqim_to_neq26
592 ##| ##27: napply neqim_to_neq27 ##| ##28: napply neqim_to_neq28
593 ##| ##29: napply neqim_to_neq29 ##| ##30: napply neqim_to_neq30
594 ##| ##31: napply neqim_to_neq31 ##| ##32: napply neqim_to_neq32
595 ##| ##33: napply neqim_to_neq33 ##| ##34: napply neqim_to_neq34
599 nlemma neq_to_neqim1 : ∀i2.MODE_INH ≠ i2 → eq_im MODE_INH i2 = false.
600 #i2; nelim i2; nnormalize;
601 ##[ ##1: #H; nelim (H (refl_eq …))
602 ##| ##31,32,33,34: #n; ##]
603 ##[ ##*: #H; napply refl_eq
607 nlemma neq_to_neqim2 : ∀i2.MODE_INHA ≠ i2 → eq_im MODE_INHA i2 = false.
608 #i2; nelim i2; nnormalize;
609 ##[ ##2: #H; nelim (H (refl_eq …))
610 ##| ##31,32,33,34: #n; ##]
611 ##[ ##*: #H; napply refl_eq
615 nlemma neq_to_neqim3 : ∀i2.MODE_INHX ≠ i2 → eq_im MODE_INHX i2 = false.
616 #i2; nelim i2; nnormalize;
617 ##[ ##3: #H; nelim (H (refl_eq …))
618 ##| ##31,32,33,34: #n; ##]
619 ##[ ##*: #H; napply refl_eq
623 nlemma neq_to_neqim4 : ∀i2.MODE_INHH ≠ i2 → eq_im MODE_INHH i2 = false.
624 #i2; nelim i2; nnormalize;
625 ##[ ##4: #H; nelim (H (refl_eq …))
626 ##| ##31,32,33,34: #n; ##]
627 ##[ ##*: #H; napply refl_eq
631 nlemma neq_to_neqim5 : ∀i2.MODE_INHX0ADD ≠ i2 → eq_im MODE_INHX0ADD i2 = false.
632 #i2; nelim i2; nnormalize;
633 ##[ ##5: #H; nelim (H (refl_eq …))
634 ##| ##31,32,33,34: #n; ##]
635 ##[ ##*: #H; napply refl_eq
639 nlemma neq_to_neqim6 : ∀i2.MODE_INHX1ADD ≠ i2 → eq_im MODE_INHX1ADD i2 = false.
640 #i2; nelim i2; nnormalize;
641 ##[ ##6: #H; nelim (H (refl_eq …))
642 ##| ##31,32,33,34: #n; ##]
643 ##[ ##*: #H; napply refl_eq
647 nlemma neq_to_neqim7 : ∀i2.MODE_INHX2ADD ≠ i2 → eq_im MODE_INHX2ADD i2 = false.
648 #i2; nelim i2; nnormalize;
649 ##[ ##7: #H; nelim (H (refl_eq …))
650 ##| ##31,32,33,34: #n; ##]
651 ##[ ##*: #H; napply refl_eq
655 nlemma neq_to_neqim8 : ∀i2.MODE_IMM1 ≠ i2 → eq_im MODE_IMM1 i2 = false.
656 #i2; nelim i2; nnormalize;
657 ##[ ##8: #H; nelim (H (refl_eq …))
658 ##| ##31,32,33,34: #n; ##]
659 ##[ ##*: #H; napply refl_eq
663 nlemma neq_to_neqim9 : ∀i2.MODE_IMM1EXT ≠ i2 → eq_im MODE_IMM1EXT i2 = false.
664 #i2; nelim i2; nnormalize;
665 ##[ ##9: #H; nelim (H (refl_eq …))
666 ##| ##31,32,33,34: #n; ##]
667 ##[ ##*: #H; napply refl_eq
671 nlemma neq_to_neqim10 : ∀i2.MODE_IMM2 ≠ i2 → eq_im MODE_IMM2 i2 = false.
672 #i2; nelim i2; nnormalize;
673 ##[ ##10: #H; nelim (H (refl_eq …))
674 ##| ##31,32,33,34: #n; ##]
675 ##[ ##*: #H; napply refl_eq
679 nlemma neq_to_neqim11 : ∀i2.MODE_DIR1 ≠ i2 → eq_im MODE_DIR1 i2 = false.
680 #i2; nelim i2; nnormalize;
681 ##[ ##11: #H; nelim (H (refl_eq …))
682 ##| ##31,32,33,34: #n; ##]
683 ##[ ##*: #H; napply refl_eq
687 nlemma neq_to_neqim12 : ∀i2.MODE_DIR2 ≠ i2 → eq_im MODE_DIR2 i2 = false.
688 #i2; nelim i2; nnormalize;
689 ##[ ##12: #H; nelim (H (refl_eq …))
690 ##| ##31,32,33,34: #n; ##]
691 ##[ ##*: #H; napply refl_eq
695 nlemma neq_to_neqim13 : ∀i2.MODE_IX0 ≠ i2 → eq_im MODE_IX0 i2 = false.
696 #i2; nelim i2; nnormalize;
697 ##[ ##13: #H; nelim (H (refl_eq …))
698 ##| ##31,32,33,34: #n; ##]
699 ##[ ##*: #H; napply refl_eq
703 nlemma neq_to_neqim14 : ∀i2.MODE_IX1 ≠ i2 → eq_im MODE_IX1 i2 = false.
704 #i2; nelim i2; nnormalize;
705 ##[ ##14: #H; nelim (H (refl_eq …))
706 ##| ##31,32,33,34: #n; ##]
707 ##[ ##*: #H; napply refl_eq
711 nlemma neq_to_neqim15 : ∀i2.MODE_IX2 ≠ i2 → eq_im MODE_IX2 i2 = false.
712 #i2; nelim i2; nnormalize;
713 ##[ ##15: #H; nelim (H (refl_eq …))
714 ##| ##31,32,33,34: #n; ##]
715 ##[ ##*: #H; napply refl_eq
719 nlemma neq_to_neqim16 : ∀i2.MODE_SP1 ≠ i2 → eq_im MODE_SP1 i2 = false.
720 #i2; nelim i2; nnormalize;
721 ##[ ##16: #H; nelim (H (refl_eq …))
722 ##| ##31,32,33,34: #n; ##]
723 ##[ ##*: #H; napply refl_eq
727 nlemma neq_to_neqim17 : ∀i2.MODE_SP2 ≠ i2 → eq_im MODE_SP2 i2 = false.
728 #i2; nelim i2; nnormalize;
729 ##[ ##17: #H; nelim (H (refl_eq …))
730 ##| ##31,32,33,34: #n; ##]
731 ##[ ##*: #H; napply refl_eq
735 nlemma neq_to_neqim18 : ∀i2.MODE_DIR1_to_DIR1 ≠ i2 → eq_im MODE_DIR1_to_DIR1 i2 = false.
736 #i2; nelim i2; nnormalize;
737 ##[ ##18: #H; nelim (H (refl_eq …))
738 ##| ##31,32,33,34: #n; ##]
739 ##[ ##*: #H; napply refl_eq
743 nlemma neq_to_neqim19 : ∀i2.MODE_IMM1_to_DIR1 ≠ i2 → eq_im MODE_IMM1_to_DIR1 i2 = false.
744 #i2; nelim i2; nnormalize;
745 ##[ ##19: #H; nelim (H (refl_eq …))
746 ##| ##31,32,33,34: #n; ##]
747 ##[ ##*: #H; napply refl_eq
751 nlemma neq_to_neqim20 : ∀i2.MODE_IX0p_to_DIR1 ≠ i2 → eq_im MODE_IX0p_to_DIR1 i2 = false.
752 #i2; nelim i2; nnormalize;
753 ##[ ##20: #H; nelim (H (refl_eq …))
754 ##| ##31,32,33,34: #n; ##]
755 ##[ ##*: #H; napply refl_eq
759 nlemma neq_to_neqim21 : ∀i2.MODE_DIR1_to_IX0p ≠ i2 → eq_im MODE_DIR1_to_IX0p i2 = false.
760 #i2; nelim i2; nnormalize;
761 ##[ ##21: #H; nelim (H (refl_eq …))
762 ##| ##31,32,33,34: #n; ##]
763 ##[ ##*: #H; napply refl_eq
767 nlemma neq_to_neqim22 : ∀i2.MODE_INHA_and_IMM1≠ i2 → eq_im MODE_INHA_and_IMM1 i2 = false.
768 #i2; nelim i2; nnormalize;
769 ##[ ##22: #H; nelim (H (refl_eq …))
770 ##| ##31,32,33,34: #n; ##]
771 ##[ ##*: #H; napply refl_eq
775 nlemma neq_to_neqim23 : ∀i2.MODE_INHX_and_IMM1 ≠ i2 → eq_im MODE_INHX_and_IMM1 i2 = false.
776 #i2; nelim i2; nnormalize;
777 ##[ ##23: #H; nelim (H (refl_eq …))
778 ##| ##31,32,33,34: #n; ##]
779 ##[ ##*: #H; napply refl_eq
783 nlemma neq_to_neqim24 : ∀i2.MODE_IMM1_and_IMM1 ≠ i2 → eq_im MODE_IMM1_and_IMM1 i2 = false.
784 #i2; nelim i2; nnormalize;
785 ##[ ##24: #H; nelim (H (refl_eq …))
786 ##| ##31,32,33,34: #n; ##]
787 ##[ ##*: #H; napply refl_eq
791 nlemma neq_to_neqim25 : ∀i2.MODE_DIR1_and_IMM1 ≠ i2 → eq_im MODE_DIR1_and_IMM1 i2 = false.
792 #i2; nelim i2; nnormalize;
793 ##[ ##25: #H; nelim (H (refl_eq …))
794 ##| ##31,32,33,34: #n; ##]
795 ##[ ##*: #H; napply refl_eq
799 nlemma neq_to_neqim26 : ∀i2.MODE_IX0_and_IMM1 ≠ i2 → eq_im MODE_IX0_and_IMM1 i2 = false.
800 #i2; nelim i2; nnormalize;
801 ##[ ##26: #H; nelim (H (refl_eq …))
802 ##| ##31,32,33,34: #n; ##]
803 ##[ ##*: #H; napply refl_eq
807 nlemma neq_to_neqim27 : ∀i2.MODE_IX0p_and_IMM1 ≠ i2 → eq_im MODE_IX0p_and_IMM1 i2 = false.
808 #i2; nelim i2; nnormalize;
809 ##[ ##27: #H; nelim (H (refl_eq …))
810 ##| ##31,32,33,34: #n; ##]
811 ##[ ##*: #H; napply refl_eq
815 nlemma neq_to_neqim28 : ∀i2.MODE_IX1_and_IMM1 ≠ i2 → eq_im MODE_IX1_and_IMM1 i2 = false.
816 #i2; nelim i2; nnormalize;
817 ##[ ##28: #H; nelim (H (refl_eq …))
818 ##| ##31,32,33,34: #n; ##]
819 ##[ ##*: #H; napply refl_eq
823 nlemma neq_to_neqim29 : ∀i2.MODE_IX1p_and_IMM1 ≠ i2 → eq_im MODE_IX1p_and_IMM1 i2 = false.
824 #i2; nelim i2; nnormalize;
825 ##[ ##29: #H; nelim (H (refl_eq …))
826 ##| ##31,32,33,34: #n; ##]
827 ##[ ##*: #H; napply refl_eq
831 nlemma neq_to_neqim30 : ∀i2.MODE_SP1_and_IMM1 ≠ i2 → eq_im MODE_SP1_and_IMM1 i2 = false.
832 #i2; nelim i2; nnormalize;
833 ##[ ##30: #H; nelim (H (refl_eq …))
834 ##| ##31,32,33,34: #n; ##]
835 ##[ ##*: #H; napply refl_eq
839 nlemma neq_to_neqim31 : ∀n.∀i2.(MODE_DIRn n) ≠ i2 → eq_im (MODE_DIRn n) i2 = false.
841 ##[ ##31: #n2; #H; nchange with (eq_oct n1 n2 = false); napply (neq_to_neqoct n1 n2 ?);
842 nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
843 ##| ##32,33,34: #n; ##]
844 ##[ ##*: #H; nnormalize; napply refl_eq
848 nlemma neq_to_neqim32 : ∀n.∀i2.(MODE_DIRn_and_IMM1 n) ≠ i2 → eq_im (MODE_DIRn_and_IMM1 n) i2 = false.
850 ##[ ##32: #n2; #H; nchange with (eq_oct n1 n2 = false); napply (neq_to_neqoct n1 n2 ?);
851 nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
852 ##| ##31,33,34: #n; ##]
853 ##[ ##*: #H; nnormalize; napply refl_eq
857 nlemma neq_to_neqim33 : ∀n.∀i2.(MODE_TNY n) ≠ i2 → eq_im (MODE_TNY n) i2 = false.
859 ##[ ##33: #n2; #H; nchange with (eq_ex n1 n2 = false); napply (neq_to_neqex n1 n2 ?);
860 nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
861 ##| ##31,32,34: #n; ##]
862 ##[ ##*: #H; nnormalize; napply refl_eq
866 nlemma neq_to_neqim34 : ∀n.∀i2.(MODE_SRT n) ≠ i2 → eq_im (MODE_SRT n) i2 = false.
868 ##[ ##34: #n2; #H; nchange with (eq_bit n1 n2 = false); napply (neq_to_neqbit n1 n2 ?);
869 nnormalize; #H1; nrewrite > H1 in H:(%); #H; nelim (H (refl_eq …))
870 ##| ##31,32,33: #n; ##]
871 ##[ ##*: #H; nnormalize; napply refl_eq
875 nlemma neq_to_neqim : ∀i1,i2.i1 ≠ i2 → eq_im i1 i2 = false.
877 ##[ ##1: napply neq_to_neqim1 ##| ##2: napply neq_to_neqim2
878 ##| ##3: napply neq_to_neqim3 ##| ##4: napply neq_to_neqim4
879 ##| ##5: napply neq_to_neqim5 ##| ##6: napply neq_to_neqim6
880 ##| ##7: napply neq_to_neqim7 ##| ##8: napply neq_to_neqim8
881 ##| ##9: napply neq_to_neqim9 ##| ##10: napply neq_to_neqim10
882 ##| ##11: napply neq_to_neqim11 ##| ##12: napply neq_to_neqim12
883 ##| ##13: napply neq_to_neqim13 ##| ##14: napply neq_to_neqim14
884 ##| ##15: napply neq_to_neqim15 ##| ##16: napply neq_to_neqim16
885 ##| ##17: napply neq_to_neqim17 ##| ##18: napply neq_to_neqim18
886 ##| ##19: napply neq_to_neqim19 ##| ##20: napply neq_to_neqim20
887 ##| ##21: napply neq_to_neqim21 ##| ##22: napply neq_to_neqim22
888 ##| ##23: napply neq_to_neqim23 ##| ##24: napply neq_to_neqim24
889 ##| ##25: napply neq_to_neqim25 ##| ##26: napply neq_to_neqim26
890 ##| ##27: napply neq_to_neqim27 ##| ##28: napply neq_to_neqim28
891 ##| ##29: napply neq_to_neqim29 ##| ##30: napply neq_to_neqim30
892 ##| ##31: napply neq_to_neqim31 ##| ##32: napply neq_to_neqim32
893 ##| ##33: napply neq_to_neqim33 ##| ##34: napply neq_to_neqim34