X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Fstar.ma;h=097151367c0686266bf03fe3c637c999ec1b13b4;hb=fc7af5f9ea2cd4a876b8babc6b691136799e3c87;hp=baed9b78e41d60f1ddd6c25b5770a346b7a142ef;hpb=55dc00c1c44cc21c7ae179cb9df03e7446002c46;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
index baed9b78e..097151367 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
@@ -13,10 +13,15 @@
 (**************************************************************************)
 
 include "basics/star.ma".
-include "Ground-2/xoa_props.ma".
+include "Ground_2/xoa_props.ma".
 
 (* PROPERTIES of RELATIONS **************************************************)
 
+definition predicate: Type[0] → Type[0] ≝ λA. A → Prop.
+
+definition Decidable: Prop → Prop ≝
+   λR. R ∨ (R → False). 
+
 definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
                       ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
                       ∃∃a. R2 a1 a & R1 a2 a.
@@ -102,8 +107,21 @@ qed.
 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
 /2/ qed.
 
-lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
+lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
                    P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
                    ∀a2. TC … R a1 a2 → P a2.
 #A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
 qed.
+
+definition NF: ∀A. relation A → relation A → predicate A ≝
+   λA,R,S,a1. ∀a2. R a1 a2 → S a1 a2.
+
+inductive SN (A) (R,S:relation A): predicate A ≝
+| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a1 a2 → False) → SN A R S a2) → SN A R S a1
+.
+
+lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
+#A #R #S #a1 #Ha1
+@SN_intro #a2 #HRa12 #HSa12
+elim (HSa12 ?) -HSa12 /2/
+qed.