proposition: Lemma mark_proper_strong: forall (g g': PreGraph V E) m1 root m2, ((predicate_partialgraph g (reachable_by g root (negateP m1))) ~=~ (predicate_partialgraph g' (reachable_by g' root (negateP m1)))) -> (mark g m1 root m2 <-> mark g' m1 root m2).
proof: Proof. assert (forall (g g': PreGraph V E) m1 root m2, ((predicate_partialgraph g (reachable_by g root (negateP m1))) ~=~ (predicate_partialgraph g' (reachable_by g' root (negateP m1)))) -> mark g m1 root m2 -> mark g' m1 root m2). 2: intros; split; apply H; auto; symmetry; auto. unfold mark; intros. split; intros; destruct H0. + apply H0. pose proof partialgraph_si_node_prop n g g' _ _ H. spec H3. 1: { intros ? ?. apply reachable_by_foot_valid in H4. auto. } spec H3. 1: { intros ? ?. apply reachable_by_foot_valid in H4. auto. } tauto. + apply H2. pose proof partialgraph_si_node_prop n g g' _ _ H. spec H3. 1: { intros ? ?. apply reachable_by_foot_valid in H4. auto. } spec H3. 1: { intros ? ?. apply reachable_by_foot_valid in H4. auto. } tauto. 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