proposition: Lemma mark1_unmarked : forall m1 root m2 n, mark1 m1 root m2 -> g |= root ~o~> n satisfying (negateP m1) -> n = root \/ exists child, edge g root child /\ g |= child ~o~> n satisfying (negateP m2).
proof: Proof. intros. rewrite reachable_acyclic in H0. destruct H0 as [p [? ?]]. destruct p as [v p]. assert (v = root) by (destruct H1 as [[? _] _]; simpl in H1; auto). subst v. destruct p. + left. destruct H1 as [[? ?] _]. simpl in H2. auto. + right. exists (dst g e). change (root, e :: p) with (path_glue (root, e :: nil) (dst g e, p)) in H1. apply (reachable_by_path_split_glue g) with (n := dst g e) in H1. 2: red; simpl; auto. destruct H1. split. - destruct H1 as [_ [[? [? [? ?]]] _]]. hnf. subst root. rewrite step_spec. do 2 (split; auto). exists e; auto. - exists (dst g e, p). destruct H2 as [? [? ?]]. split; [|split]; auto. rewrite path_prop_equiv in H4 |-* ; auto. rewrite epath_to_vpath_cons_eq in H0. 2: destruct H1 as [_ [[? _] _]]; auto. apply NoDup_cons_2 in H0. rewrite in_path_eq_epath_to_vpath in H0; auto. intros. specialize (H4 _ H5). destruct H as [? [? ?]]. rewrite negateP_spec in H4 |- *. rewrite <- H7; auto. intro. apply H0. subst; auto. Qed.
imports: Coq.Logic.ProofIrrelevance CertiGraph.lib.Ensembles_ext Coq.Lists.List Coq.Classes.Morphisms CertiGraph.lib.Coqlib CertiGraph.lib.List_ext CertiGraph.lib.EquivDec_ext VST.msl.Coqlib2 CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2