proposition: Lemma partialgraph_update: forall (g g': Graph) (S1 S1' S2: list V), (vertices_identical2 (reachable_through_set (predicate_partialgraph g (Intersection _ (vvalid g) (Complement _ (reachable_through_set g S1)))) S2) (reachable_through_set (predicate_partialgraph g' (Intersection _ (vvalid g') (Complement _ (reachable_through_set g' S1')))) S2) (Graph_PointwiseGraph g) (Graph_PointwiseGraph g')) -> Included (reachable_through_set (predicate_partialgraph g (Intersection _ (vvalid g) (Complement _ (reachable_through_set g S1)))) S2) (vguard g) -> Included (reachable_through_set (predicate_partialgraph g' (Intersection _ (vvalid g') (Complement _ (reachable_through_set g' S1')))) S2) (vguard g') -> reachable_through_vertices_at (S1 ++ S2) g |-- reachable_through_vertices_at S1 g * (reachable_through_vertices_at S1' g' -* reachable_through_vertices_at (S1' ++ S2) g').
proof: Proof. intros. unfold reachable_through_vertices_at. apply vertices_at_ramif_x. exists (reachable_through_set (predicate_partialgraph g (Intersection _ (vvalid g) (Complement _ (reachable_through_set g S1)))) S2). split; [| split]. + split. - intros. rewrite <- (unreachable_eq' g S1 S2). rewrite <- reachable_through_set_app. tauto. - intros. rewrite <- (unreachable_eq' g S1 S2) in H3. tauto. + split. - intros. destruct H as [? _]. rewrite (app_same_set H). rewrite <- (unreachable_eq' g' S1' S2). rewrite <- reachable_through_set_app; tauto. - intros. destruct H as [? _]. rewrite (app_same_set H) in H3. rewrite <- (unreachable_eq' g' S1' S2) in H3. tauto. + destruct H; 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