]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly2/num/oct.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly2 / num / oct.ma
old mode 100755 (executable)
new mode 100644 (file)
index a8199dd..646227d
@@ -142,6 +142,11 @@ ndefinition xor_oct ≝
   | 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