1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/tlt_defs".
17 include "terms_defs.ma".
19 definition wadd: (nat \to nat) \to nat \to (nat \to nat) \def
23 | (S m) \Rightarrow (map m)
26 let rec weight_map (A:Set) (N:Set) (map:nat \to nat) (t:T) : nat \def
28 (TSort A N y k) \Rightarrow O
29 | (TLRef A N y i) \Rightarrow (map i)
30 | (TWag A N y z w u) \Rightarrow
35 (S (plus (weight_map A N map w) (weight_map A N (wadd map (S (weight_map A N map w))) u)))
37 (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
39 (S (plus (weight_map A N map w) (weight_map A N (wadd map O) u)))
41 | (Flat a) \Rightarrow
42 (S (plus (weight_map A N map w) (weight_map A N map u)))
44 | (TGRef A N y n) \Rightarrow O
47 Definition weight : T \to nat := (weight_map [_](0)).
49 Definition tlt : T \to T \to Prop := [t1,t2](lt (weight t1) (weight t2)).