proposition: Lemma mark_partial_labeled_graph_equiv: forall x (g g': Graph), mark x g g' -> ((predicate_partial_labeledgraph g (Complement _ (reachable g x))) ~=~ (predicate_partial_labeledgraph g' (Complement _ (reachable g x))))%LabeledGraph.
proof: Proof. intros. split; [| split]. + destruct H. simpl; rewrite <- H0. reflexivity. + destruct H as [[? ?] _]. simpl in *; intros. specialize (H0 v). assert (~ g |= x ~o~> v satisfying (WeakMarkGraph.unmarked g)). 1: { destruct H1. intro; apply H3. apply reachable_by_is_reachable in H4; auto. } clear - H0 H3. destruct (vlabel g v), (vlabel g' v). - auto. - rewrite H0; auto. - symmetry; tauto. - auto. + intros; simpl. destruct (elabel g e), (elabel g' e); auto. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.List_ext CertiGraph.lib.relation_list CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.dag CertiGraph.graph.weak_mark_lemmas CertiGraph.msl_application.Graph Coq.Logic.Classical