proposition: Lemma spanning_tree_left_reachable: forall (g1 g2: Graph) x l r, vvalid g1 x -> vgamma g1 x = (true, l, r) -> spanning_tree g1 l g2 -> Included (reachable g2 r) (reachable g1 x).
proof: Proof. intros. intro v. unfold Ensembles.In . intros. assert (X: ReachDecidable g1 l (unmarked g1)). { apply Graph_reachable_by_dec. apply weak_valid_vvalid_dec. apply (gamma_left_weak_valid g1 x true l r); auto. } destruct (X v). + apply reachable_by_is_reachable in r0. apply edge_reachable_by with l; auto. split; [|split]; auto. - apply reachable_head_valid in r0. auto. - simpl in H0. inversion H0. exists (x, L); auto. * apply (@left_valid _ _ _ _ _ _ g1 (binGraph g1)); auto. * apply (@left_sound _ _ _ _ _ _ g1 (binGraph g1)); auto. + apply edge_reachable_by with r; auto. - split; [|split]; auto. * apply reachable_head_valid in H2. rewrite (spanning_tree_vvalid g1 l g2); auto. * rewrite (gamma_step g1 x true l r); auto. - apply (spanning_tree_not_reachable g1 l g2 r v) in H2; auto. rewrite reachable_by_eq_partialgraph_reachable in H2. destruct H1 as [? [? ?]]. rewrite <- H3 in H2. rewrite <- reachable_by_eq_partialgraph_reachable in H2. apply reachable_by_is_reachable in H2. apply H2. 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