X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Flib%2Flstar_2a.ma;h=dc3ed1ef34ff6c81ef09525f6953c9833ff90cf7;hb=ae626612bff9c3746dd7647bbada791c737e348c;hp=ae707f2b96038cb5aed1a5206b3a702778961e49;hpb=68b4f2490c12139c03760b39895619e63b0f38c9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
index ae707f2b9..dc3ed1ef3 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/lstar_2a.ma
@@ -12,9 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "arithmetics/lstar.ma".
+include "ground/lib/ltc.ma".
+include "ground/arith/nat_plus.ma".
 
-(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************)
+(* NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE FOR λδ-2A *******************)
 
-definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝
-                   λA,B,R,l,a. lstar … (R a) l.
+definition lstar_aux (B) (R:relation B) (l): relation B ≝
+           λb1,b2. ∨∨ (∧∧ l = 𝟎 & b1 = b2) | (∧∧ l = 𝟏  & R b1 b2).
+
+definition lstar (B) (R:relation B): nat → relation B ≝
+           ltc … nplus … (lstar_aux … R).
+
+definition llstar (A) (B) (R:relation3 A B B) (l:nat): relation3 A B B ≝
+           λa. lstar … (R a) l.