--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+
+
+include "datatypes/List.ma".
+include "NPlus/defs.ma".
+
+
+inductive NPlusList: (List Nat) \to Nat \to Prop \def
+ | nplus_nil: NPlusList (nil ?) zero
+ | nplus_cons: \forall l,p,q,r.
+ NPlusList l p \to NPlus p q r \to NPlusList (cons ? l q) r
+.
+
+definition NPlusListEq: (List Nat) \to (List Nat) \to Prop \def
+ \lambda ns1,ns2. \exists n. NPlusList ns1 n \land NPlusList ns2 n.
+
+(*
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "ternary natural plus predicate" 'rel_plus3 x y z =
+ (cic:/matita/RELATIONAL/NPlus/defs/NPlus3.con w x y z).
+
+notation "hvbox(a break + b break + c == d)"
+ non associative with precedence 95
+for @{ 'rel_plus3 $a $b $c $d}.
+*)