proposition: Lemma restriction_aut : forall (w : Word) (e0 e e2 e3 a : Elt) (q d : Ensf), ~ dans e0 q -> dans e q -> inclus d (prodcart q (prodcart alph q)) -> chemin e e2 (add e0 q) (add (couple e0 (couple a e3)) d) w -> chemin e e2 q d w.
proof: Proof. simple induction w. intros. cut (Chemin e e2 (add e0 q) (add (couple e0 (couple a e3)) d) nil); auto. intro. cut (dans e (add e0 q) /\ e = e2 :>Elt); auto. intro H4; elim H4; auto. intros x w0 H e0 e e2 e3 a q d H0 H1 H2 H3. cut (Chemin e e2 (add e0 q) (add (couple e0 (couple a e3)) d) (cons x w0)); auto. intro. cut (exists e12 : Elt, chemin e12 e2 (add e0 q) (add (couple e0 (couple a e3)) d) w0 /\ dans e (add e0 q) /\ dans x alph /\ dans (couple e (couple x e12)) (add (couple e0 (couple a e3)) d)); auto. intro H5; elim H5; clear H5. intros e12 H5; elim H5; clear H5. intros H5 H6; elim H6; clear H6. intros H6 H7; elim H7; clear H7. intros H7 H8. apply (chemin_cons e12 e2 q d w0 e x); auto. apply (H e0 e12 e2 e3 a q d); auto. cut (couple e0 (couple a e3) = couple e (couple x e12) :>Elt \/ dans (couple e (couple x e12)) d). 2: apply dans_add; auto. intro H9; elim H9; clear H9. intro H9; injection H9 as H12 H11 H10. absurd (dans e0 q); auto. rewrite H12; auto. intro. cut (dans (couple e (couple x e12)) (prodcart q (prodcart alph q))). 2: apply (dans_trans (couple e (couple x e12)) d (prodcart q (prodcart alph q))); auto. intro. cut (dans e q /\ dans (couple x e12) (prodcart alph q)); auto. 2: apply coupl2; auto. intro H11; elim H11; clear H11. intros. cut (dans x alph /\ dans e12 q). 2: apply coupl2; auto. tauto. cut (couple e0 (couple a e3) = couple e (couple x e12) :>Elt \/ dans (couple e (couple x e12)) d). 2: apply dans_add; auto. intro H9; elim H9; clear H9. intro H9; injection H9 as H12 H11 H10. absurd (dans e0 q); auto. rewrite H12; auto. auto. Qed.
imports: Ensf Max Words Dec Reg Rat