(* operatore Most Significant Bit *)
ndefinition getMSB_w32 ≝ getOPH_cn ? getMSB_w16.
ndefinition setMSB_w32 ≝ setOPH_cn ? setMSB_w16.
+ndefinition clrMSB_w32 ≝ setOPH_cn ? clrMSB_w16.
(* operatore Least Significant Bit *)
ndefinition getLSB_w32 ≝ getOPL_cn ? getLSB_w16.
ndefinition setLSB_w32 ≝ setOPL_cn ? setLSB_w16.
+ndefinition clrLSB_w32 ≝ setOPL_cn ? clrLSB_w16.
(* operatore estensione unsigned *)
ndefinition extu_w32 ≝ λw2.〈〈〈x0,x0〉:〈x0,x0〉〉.w2〉.