| x8 ⇒ x8 | x9 ⇒ x7 | xA ⇒ x6 | xB ⇒ x5
| xC ⇒ x4 | xD ⇒ x3 | xE ⇒ x2 | xF ⇒ x1 ].
+(* operatore x in [inf,sup] *)
+ndefinition inrange_ex ≝
+λx,inf,sup:exadecim.(le_ex inf x) ⊗ (le_ex x sup).
+
(* iteratore sugli esadecimali *)
ndefinition forall_ex ≝ λP.
P x0 ⊗ P x1 ⊗ P x2 ⊗ P x3 ⊗ P x4 ⊗ P x5 ⊗ P x6 ⊗ P x7 ⊗