| o4 ⇒ o3 | o5 ⇒ o2 | o6 ⇒ o1 | o7 ⇒ o0 ]
].
+(* operatore predecessore *)
+ndefinition pred_oct ≝
+λn.match n with
+ [ o0 ⇒ o7 | o1 ⇒ o0 | o2 ⇒ o1 | o3 ⇒ o2 | o4 ⇒ o3 | o5 ⇒ o4 | o6 ⇒ o5 | o7 ⇒ o6 ].
+
(* operatore successore *)
ndefinition succ_oct ≝
λn.match n with