include "basics/lists/list.ma".
-(* labelled reflexive and transitive closure ********************************)
+(* labeled reflexive and transitive closure *********************************)
definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,B,R.
∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1@l2) b1 b2.
+definition inv_ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝
+ λA,B,R. ∀l1,l2,b1,b2. R (l1@l2) b1 b2 →
+ ∃∃b. R l1 b1 b & R l2 b b2.
+
inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
| lstar_nil : ∀b. lstar A B R ([]) b b
| lstar_cons: ∀a,b1,b. R a b1 b →
#A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/
qed-.
+lemma lstar_inv_ltransitive: ∀A,B,R. inv_ltransitive … (lstar A B R).
+#A #B #R #l1 elim l1 -l1 normalize /2 width=3/
+#a #l1 #IHl1 #l2 #b1 #b2 #H
+elim (lstar_inv_cons … b2 H ???) -H [4: // |2,3: skip ] #b #Hb1 #Hb2 (**) (* simplify line *)
+elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
+qed-.
+
lemma lstar_app: ∀A,B,R,l,b1,b. lstar A B R l b1 b → ∀a,b2. R a b b2 →
lstar A B R (l@[a]) b1 b2.
#A #B #R #l #b1 #b #H @(lstar_ind_l ????????? H) -l -b1 /2 width=1/