proposition: Lemma graph_ramify_aux1_left: forall (g: Graph) x d l r, vvalid g x -> vgamma g x = (d, l, r) -> (reachable_vertices_at x g : pred) |-- reachable_vertices_at l g * (ALL g' : Graph , !!spanning_tree g l g' --> (vertices_at (reachable g l) g' -* vertices_at (reachable g x) g')).
proof: Proof. intros. eapply vertices_at_ramif_xQ; auto. eexists; split; [| split]. + eapply Prop_join_reachable_left; eauto. + intros. eapply Prop_join_reachable_left; eauto. + intros; rewrite vertices_identical_spec. intros. rewrite Intersection_spec in H2. unfold Complement, Ensembles.In in H2. destruct H2. simpl. f_equal; [f_equal |]. - apply vlabel_eq. destruct H1. specialize (H1 x0). pose proof reachable_by_is_reachable g l x0 (unmarked g). tauto. - destruct H1 as [_ [? _]]. hnf in H1. simpl in H1. unfold predicate_weak_evalid in H1. destruct H1 as [_ [? [_ ?]]]. specialize (H1 (x0, L)). specialize (H4 (x0, L)). assert (src g (x0, L) = x0) by (apply (@left_sound _ _ _ _ _ _ g (binGraph g) x0); apply reachable_foot_valid in H2; auto). change (lg_gg g) with (g: LGraph) in *. rewrite H5 in *. assert (evalid g (x0, L) /\ ~ g |= l ~o~> x0 satisfying (unmarked g)). { split. + apply reachable_foot_valid in H2. apply (@left_valid _ _ _ _ _ _ g (binGraph g)); auto. + intro; apply H3; apply reachable_by_is_reachable in H6; auto. } apply H4; intuition. - destruct H1 as [_ [? _]]. hnf in H1. simpl in H1. unfold predicate_weak_evalid in H1. destruct H1 as [_ [? [_ ?]]]. specialize (H1 (x0, R)). specialize (H4 (x0, R)). assert (src g (x0, R) = x0) by (apply (@right_sound _ _ _ _ _ _ g (binGraph g) x0); apply reachable_foot_valid in H2; auto). change (lg_gg g) with (g: LGraph) in *. rewrite H5 in *. assert (evalid g (x0, R) /\ ~ g |= l ~o~> x0 satisfying (unmarked g)). { split. + apply reachable_foot_valid in H2. apply (@right_valid _ _ _ _ _ _ g (binGraph g)); auto. + intro; apply H3; apply reachable_by_is_reachable in H6; auto. } apply H4; 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