X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Flstar.ma;h=e3dcd55d6b86ac03e6c7ab48330b77698ae120d2;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=ddd4113e325b8028b013c14c231f1d958007e31f;hpb=774c5e125eb44693a5a760226713067c41baf09f;p=helm.git

diff --git a/matita/matita/lib/arithmetics/lstar.ma b/matita/matita/lib/arithmetics/lstar.ma
index ddd4113e3..e3dcd55d6 100644
--- a/matita/matita/lib/arithmetics/lstar.ma
+++ b/matita/matita/lib/arithmetics/lstar.ma
@@ -48,6 +48,11 @@ lemma lstar_step: ∀B,R,b1,b2. R b1 b2 → lstar B R 1 b1 b2.
 /2 width=3/
 qed.
 
+lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
+                lstar B R (l+1) b1 b2.
+#B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
+qed.
+
 lemma lstar_inv_O: ∀B,R,l,b1,b2. lstar B R l b1 b2 → 0 = l → b1 = b2.
 #B #R #l #b1 #b2 * -l -b1 -b2 //
 #b1 #b #_ #l #b2 #_ <plus_n_Sm #H destruct
@@ -90,10 +95,12 @@ elim (lstar_inv_S … b2 H (l1+l2)) -H // #b #Hb1 #Hb2
 elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
 qed-.
 
-lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
-                lstar B R (l+1) b1 b2.
-#B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
-qed.
+lemma lstar_inv_S_dx: ∀B,R,l,b1,b2. lstar B R (l+1) b1 b2 →
+                      ∃∃b. lstar B R l b1 b & R b b2.
+#B #R #l #b1 #b2 #H
+elim (lstar_inv_ltransitive B R … H) -H #b #Hb1 #H
+lapply (lstar_inv_step B R … H) -H /2 width=3/
+qed-.
 
 inductive lstar_r (B:Type[0]) (R: relation B): ℕ → relation B ≝
 | lstar_r_O: ∀b. lstar_r B R 0 b b
@@ -133,3 +140,7 @@ lemma lstar_ind_r: ∀B,R,b1. ∀P:relation2 ℕ B.
 #B #R #b1 #P #H1 #H2 #l #b2 #Hb12
 @(lstar_ind_r_aux … H1 H2 … Hb12) //
 qed-.
+
+lemma lstar_Conf3: ∀A,B,S,R. Conf3 A B S R → ∀l. Conf3 A B S (lstar … R l).
+#A #B #S #R #HSR #l #b #a1 #Ha1 #a2 #H @(lstar_ind_r … l a2 H) -l -a2 // /2 width=3/
+qed-.