proposition: Lemma subgraph_update: forall (g g': Graph) {rfg: ReachableFiniteGraph g} {rfg': ReachableFiniteGraph g'} (S1 S1' S2: list V), (forall x : V, In x (S1 ++ S2) -> Decidable (vvalid g x)) -> (forall x : V, In x (S1' ++ S2) -> Decidable (vvalid g' x)) -> vertices_identical2 (reachable_through_set (predicate_partialgraph g (Intersection V (vvalid g) (Complement V (reachable_through_set g S1)))) S2) (reachable_through_set (predicate_partialgraph g' (Intersection V (vvalid g') (Complement V (reachable_through_set g' S1')))) S2) (Graph_PointwiseGraph g) (Graph_PointwiseGraph g') -> Included (reachable_through_set (predicate_partialgraph g (Intersection V (vvalid g) (Complement V (reachable_through_set g S1)))) S2) (vguard g) -> Included (reachable_through_set (predicate_partialgraph g' (Intersection V (vvalid g') (Complement V (reachable_through_set g' S1')))) S2) (vguard g') -> graphs S1 g ⊗ graphs S2 g |-- graphs S1 g * (graphs S1' g' -* graphs S1' g' ⊗ graphs S2 g').
proof: Proof. intros. rewrite <- !graphs_app. rewrite !graphs_graphs'; auto. 2: intros; apply X0; rewrite in_app_iff; left; auto. 2: intros; apply X; rewrite in_app_iff; left; auto. apply partialgraph_update; auto. Qed.
imports: Coq.Logic.Classical VST.msl.seplog VST.msl.log_normalize VST.msl.ramification_lemmas CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext CertiGraph.lib.Relation_ext CertiGraph.lib.Equivalence_ext CertiGraph.lib.Morphisms_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.ramification_lemmas CertiGraph.msl_ext.abs_addr CertiGraph.msl_ext.seplog CertiGraph.graph.graph_model CertiGraph.graph.graph_gen CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.dag CertiGraph.graph.FiniteGraph