]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly2/num/oct.ma
freescale porting
[helm.git] / helm / software / matita / contribs / ng_assembly2 / num / oct.ma
index a8199dd53a97f22ccf0a740a7effe24e06f817ce..646227d93bc8877d047e178e8d82f637dc464fef 100755 (executable)
@@ -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