fact: Definition Chemin_A (q d : Ensf) (e1 e2 : Elt) (w : Word) : Prop := match w return Prop with | nil => dans e1 q /\ e1 = e2 :>Elt \/ (exists e : Elt, chemin_A q d e e2 nil /\ dans e1 q /\ dans (couple e1 (couple epsilon e)) d) | cons a w => (exists e : Elt, chemin_A q d e e2 w /\ dans e1 q /\ dans a alph /\ dans (couple e1 (couple a e)) d) \/ (exists e : Elt, chemin_A q d e e2 w /\ dans e1 q /\ dans (couple e1 (couple epsilon e)) d) end.
imports: Ensf Max Words Dec