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 A N) on t : nat \def
28 (TSort y k) \Rightarrow O
29 | (TLRef y i) \Rightarrow (map i)
30 | (TWag y z w u) \Rightarrow
35 (S ((weight_map A N map w) + (weight_map A N (wadd map (S (weight_map A N map w))) u)))
37 (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
39 (S ((weight_map A N map w) + (weight_map A N (wadd map O) u)))
41 | (Flat a) \Rightarrow
42 (S ((weight_map A N map w) + (weight_map A N map u)))
44 | (TGRef y n) \Rightarrow O
47 definition weight: \forall A,N. T A N \to nat \def
49 (weight_map A N (\lambda _.O)).
51 definition tlt: \forall A,N. T A N \to T A N \to Prop \def
53 weight A N t1 < weight A N t2.