X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly2%2Fnum%2Fword24.ma;h=cdfc185335a1174f11f18d65eca60c4a5f0f19e4;hb=8a2b0d520b7863694130de56c5bf30fdd07696bd;hp=f523e996e108441f10f3aefa35f9dff67bd16fc8;hpb=bd112857523fc543c78cd29b74417585033ec464;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly2/num/word24.ma b/helm/software/matita/contribs/ng_assembly2/num/word24.ma
index f523e996e..cdfc18533 100755
--- a/helm/software/matita/contribs/ng_assembly2/num/word24.ma
+++ b/helm/software/matita/contribs/ng_assembly2/num/word24.ma
@@ -44,6 +44,13 @@ ndefinition eq_w24 ≝
        (eqc ? (w24h w1) (w24h w2)) ⊗
        (eqc ? (w24l w1) (w24l w2)).
 
+ndefinition succ_w24 ≝
+λw.match eqc ? (predc ? (zeroc ?)) (w24l w) with
+ [ true ⇒ match eqc ? (predc ? (zeroc ?)) (w24h w) with
+  [ true ⇒ 〈(succc ? (w24x w));(succc ? (w24h w));(succc ? (w24l w))〉
+  | false ⇒ 〈(w24x w);(succc ? (w24h w));(succc ? (w24l w))〉 ]
+ | false ⇒ 〈(w24x w);(w24h w);(succc ? (w24l w))〉 ].
+
 nlemma word24_destruct_1 :
 ∀x1,x2,y1,y2,z1,z2.
  mk_word24 x1 y1 z1 = mk_word24 x2 y2 z2 → x1 = x2.