--- /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 *)
+(* *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/tlt_defs".
+
+include "terms_defs.ma".
+
+definition wadd: (nat \to nat) \to nat \to (nat \to nat) \def
+ \lambda map,w,n.
+ match n with [
+ O \Rightarrow w
+ | (S m) \Rightarrow (map m)
+ ].
+
+let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T A N) on t : nat \def
+ match t with [
+ (TSort y k) \Rightarrow O
+ | (TLRef y i) \Rightarrow (map i)
+ | (TWag y z w u) \Rightarrow
+ match z with [
+ (Bind b) \Rightarrow
+ match b with [
+ Abbr \Rightarrow
+ (S ((weight_map A N map w) + (weight_map A N (wadd map (S (weight_map A N map w))) u)))
+ | Abst \Rightarrow
+ (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
+ | Void \Rightarrow
+ (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
+ ]
+ | (Flat a) \Rightarrow
+ (S ((weight_map A N map w) + (weight_map A N map u)))
+ ]
+ | (TGRef y n) \Rightarrow O
+ ].
+
+definition weight: \forall A,N. T A N \to nat \def
+ \lambda A,N.
+ (weight_map A N (\lambda _.O)).
+
+definition tlt: \forall A,N. T A N \to T A N \to Prop \def
+ \lambda A,N,t1,t2.
+ weight A N t1 < weight A N t2.