fact: Axiom auto_cons : forall (q qa d : Ensf) (e0 e a : Elt) (w0 : Word), dans a alph -> automate q (singleton e) qa d -> eqwordset (reconnait q (singleton e) qa d) (lword w0) -> ~ dans e0 q -> eqwordset (reconnait (add e0 q) (singleton e0) qa (add (couple e0 (couple a e)) d)) (lword (cons a w0)).
imports: Ensf Max Words Dec Reg Rat