X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fsyntax%2Fweight.ma;fp=matita%2Fmatita%2Flib%2Flambda-delta%2Fsyntax%2Fweight.ma;h=8d5ed68352678151054cbcdcfa262254d2a53ac9;hb=ec897a47d5c194a068ee76f9251958950371876b;hp=0000000000000000000000000000000000000000;hpb=5a0bffcc89e1215ed051b515dc276f6b8111fc9d;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/syntax/weight.ma b/matita/matita/lib/lambda-delta/syntax/weight.ma
new file mode 100644
index 000000000..8d5ed6835
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/syntax/weight.ma
@@ -0,0 +1,40 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic
+    ||A||  Library of Mathematics, developed at the Computer Science
+    ||T||  Department of the University of Bologna, Italy.
+    ||I||
+    ||T||
+    ||A||  This file is distributed under the terms of the
+    \   /  GNU General Public License Version 2
+     \ /
+      V_______________________________________________________________ *)
+
+include "lambda-delta/syntax/lenv.ma".
+
+(* WEIGHTS ******************************************************************)
+
+(* the weight of a term *)
+let rec tw T ≝ match T with
+[ TSort _     ⇒ 1
+| TLRef _     ⇒ 1
+| TPair _ V T ⇒ tw V + tw T + 1
+].
+
+interpretation "weight (term)" 'Weight T = (tw T).
+
+(* the weight of a local environment *)
+let rec lw L ≝ match L with
+[ LSort       ⇒ 0
+| LPair L _ V ⇒ lw L + #V
+].
+
+interpretation "weight (local environment)" 'Weight L = (lw L).
+
+(* the weight of a closure *)
+definition cw: lenv → term → ? ≝ λL,T. #L + #T.
+
+interpretation "weight (closure)" 'Weight L T = (cw L T).
+
+axiom cw_wf_ind: ∀P:lenv→term→Prop.
+                 (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
+                 ∀L,T. P L T.