ninductive IP2022_instr_mode: Type ≝
(* nessun operando : formato xxxxxxxx xxxxxxxx *)
MODE_INH : IP2022_instr_mode
+ (* operando implicito [ADDR] : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDR : IP2022_instr_mode
+ (* operando implicito [ADDR]/ADDR+=2 : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDRpp : IP2022_instr_mode
(* #lit3 → / : formato xxxxxxxx xxxxxkkk *)
| MODE_IMM3 : oct → IP2022_instr_mode
λi1,i2:IP2022_instr_mode.
match i1 with
[ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+ | MODE_INHADDR ⇒ match i2 with [ MODE_INHADDR ⇒ true | _ ⇒ false ]
+ | MODE_INHADDRpp ⇒ match i2 with [ MODE_INHADDRpp ⇒ true | _ ⇒ false ]
| MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eq_oct o1 o2 | _ ⇒ false ]
| MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ]
| MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eq_bit t1 t2 | _ ⇒ false ]
ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool.
P MODE_INH
+⊗ P MODE_INHADDR
+⊗ P MODE_INHADDRpp
⊗ forall_oct (λo.P (MODE_IMM3 o))
⊗ P MODE_IMM8
⊗ forall_bit (λt.P (MODE_IMM13 t))