proposition: Lemma graph_ramify_aux1_right: forall (g1 g2: Graph) x l r, vvalid g1 x -> vgamma g1 x = (true, l, r) -> edge_spanning_tree g1 (x, L) g2 -> (vertices_at (reachable g1 x) g2: pred) |-- reachable_vertices_at r g2 * (ALL g' : Graph , !!spanning_tree g2 r g' --> (vertices_at (reachable g2 r) g' -* vertices_at (reachable g1 x) g')).
proof: Proof. intros. eapply vertices_at_ramif_xQ; auto. eexists; split; [| split]. + eapply Prop_join_EST_right; eauto. + intros. eapply Prop_join_EST_right; eauto. + intros; rewrite vertices_identical_spec. intros. simpl. rewrite Intersection_spec in H3; unfold Complement, Ensembles.In in H3. destruct H3. f_equal; [f_equal |]. - apply vlabel_eq. destruct H2 as [? _]. specialize (H2 x0). pose proof reachable_by_is_reachable g2 r x0 (unmarked g2). tauto. - destruct H2 as [_ [? _]]. hnf in H2. simpl in H2. unfold predicate_weak_evalid in H2. destruct H2 as [_ [? [_ ?]]]. specialize (H2 (x0, L)). specialize (H5 (x0, L)). assert (src g2 (x0, L) = x0). 1: { apply (@left_sound _ _ _ _ _ _ g2 (binGraph g2) x0). rewrite <- (edge_spanning_tree_left_vvalid g1 g2 x x0 H H1). apply reachable_foot_valid in H3; auto. } change (lg_gg g2) with (g2: LGraph) in *. rewrite H6 in *. assert (evalid g2 (x0, L) /\ ~ g2 |= r ~o~> x0 satisfying (unmarked g2)). { split. + apply reachable_foot_valid in H3. apply (@left_valid _ _ _ _ _ _ g2 (binGraph g2)). rewrite <- (edge_spanning_tree_left_vvalid g1 g2 x); eauto. + intro; apply H4; apply reachable_by_is_reachable in H7; auto. } apply H5; intuition. - destruct H2 as [_ [? _]]. hnf in H2. simpl in H2. unfold predicate_weak_evalid in H2. destruct H2 as [_ [? [_ ?]]]. specialize (H2 (x0, R)). specialize (H5 (x0, R)). assert (src g2 (x0, R) = x0). 1: { apply (@right_sound _ _ _ _ _ _ g2 (binGraph g2) x0). rewrite <- (edge_spanning_tree_left_vvalid g1 g2 x x0 H H1). apply reachable_foot_valid in H3; auto. } change (lg_gg g2) with (g2: LGraph) in *. rewrite H6 in *. assert (evalid g2 (x0, R) /\ ~ g2 |= r ~o~> x0 satisfying (unmarked g2)). { split. + apply reachable_foot_valid in H3. apply (@right_valid _ _ _ _ _ _ g2 (binGraph g2)). rewrite <- (edge_spanning_tree_left_vvalid g1 g2 x); eauto. + intro; apply H4; apply reachable_by_is_reachable in H7; auto. } apply H5; intuition. Qed.
imports: VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext Coq.Lists.List CertiGraph.msl_ext.ramification_lemmas CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_ind CertiGraph.graph.spanning_tree CertiGraph.graph.BinGraph CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.msl_application.Graph CertiGraph.msl_application.GraphBin CertiGraph.msl_application.GraphBin_Mark