X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fsyntax%2Fweight.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Fsyntax%2Fweight.ma;h=d076dea9d68734c30b00667001d6a4eafd0b5032;hb=e4f11cddf44dd9bba21f689d4f56e2d00d8d7bb5;hp=0000000000000000000000000000000000000000;hpb=fefe8d334012230f8e8b9d90976d9411a58d4ba8;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma b/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma
new file mode 100644
index 000000000..d076dea9d
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/syntax/weight.ma
@@ -0,0 +1,44 @@
+(*
+    ||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 tw_wf_ind: ∀P:term→Prop.
+                 (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
+                 ∀T. P 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.