Progress

[helm.git] / matita / matita / lib / lambda / subterms.ma

diff --git a/matita/matita/lib/lambda/subterms.ma b/matita/matita/lib/lambda/subterms.ma
index 1b18f368ccad10ec65d435796d77309980777ba2..d2b7bee30b76c7fe82e634bd3d15e732f1aff629 100644 (file)
--- a/matita/matita/lib/lambda/subterms.ma
+++ b/matita/matita/lib/lambda/subterms.ma
@@ -128,3 +128,29 @@ theorem Telim: ∀P: T → Prop. (∀M. (∀N. subterm N M → P N) → P M) →
   ]  
 qed.
 
+let rec size M ≝
+match M with
+  [Sort N ⇒ 1
+  |Rel N ⇒ 1
+  |App P Q ⇒ size P + size Q + 1
+  |Lambda P Q ⇒ size P + size Q + 1
+  |Prod P Q ⇒ size P + size Q + 1
+  |D P ⇒ size P + 1
+  ]
+.
+
+(* axiom pos_size: ∀M. 1 ≤ size M. *)
+
+theorem Telim_size: ∀P: T → Prop. 
+ (∀M. (∀N. size N < size M → P N) → P M) → ∀M. P M.
+#P #H #M (cut (∀p,N. size N = p → P N))
+  [2: /2/]
+#p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size N0)) //
+qed.
+
+(* size of subterms *)
+
+lemma size_subterm : ∀N,M. subterm N M → size N < size M.
+#N #M #subH (elim subH) normalize //
+#M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
+qed.