freescale porting

[helm.git] / helm / software / matita / contribs / ng_assembly2 / num / word24.ma

diff --git a/helm/software/matita/contribs/ng_assembly2/num/word24.ma b/helm/software/matita/contribs/ng_assembly2/num/word24.ma
index f523e996e108441f10f3aefa35f9dff67bd16fc8..cdfc185335a1174f11f18d65eca60c4a5f0f19e4 100755 (executable)
--- 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.