(* *)
(* ********************************************************************** *)
-include "freescale/aux_bases.ma".
+include "freescale/oct.ma".
+include "freescale/bitrigesim.ma".
include "freescale/word16.ma".
include "freescale/theory.ma".
| MODE_SRT : bitrigesim → instr_mode
.
-ndefinition eq_instrmode ≝
+ndefinition eq_im ≝
λi1,i2:instr_mode.
match i1 with
[ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
| MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
| MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eq_oct n1 n2 | _ ⇒ false ]
| MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eq_ex e1 e2 | _ ⇒ false ]
- | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bitrig t1 t2 | _ ⇒ false ]
+ | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
].
(* enumerazione delle istruzioni di tutte le ALU *)