X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Foct.ma;h=646227d93bc8877d047e178e8d82f637dc464fef;hb=433d9c9612c1557e03a549e004c796c1137d4b4a;hp=a8199dd53a97f22ccf0a740a7effe24e06f817ce;hpb=bd112857523fc543c78cd29b74417585033ec464;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/num/oct.ma b/helm/software/matita/contribs/ng_assembly2/num/oct.ma
index a8199dd53..646227d93 100755
--- a/helm/software/matita/contribs/ng_assembly2/num/oct.ma
+++ b/helm/software/matita/contribs/ng_assembly2/num/oct.ma
@@ -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