+(**************************************************************************)
+(* ___ *)
+(* ||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) : nat \def
+ match t with [
+ (TSort A N y k) \Rightarrow O
+ | (TLRef A N y i) \Rightarrow (map i)
+ | (TWag A N y z w u) \Rightarrow
+ match z with [
+ (Bind b) \Rightarrow
+ match b with [
+ Abbr \Rightarrow
+ (S (plus (weight_map A N map w) (weight_map A N (wadd map (S (weight_map A N map w))) u)))
+ | Abst \Rightarrow
+ (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
+ | Void \Rightarrow
+ (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
+ ]
+ | (Flat a) \Rightarrow
+ (S (plus (weight_map A N map w) (weight_map A N map u)))
+ ]].(*
+ | (TGRef A N y n) \Rightarrow O
+ ].*)
+(*
+ Definition weight : T \to nat := (weight_map [_](0)).
+
+ Definition tlt : T \to T \to Prop := [t1,t2](lt (weight t1) (weight t2)).
+
+*)