proposition: Lemma edge_spanning_tree_spanning_tree: forall (g g1 g2 g3 : Graph) x l r, vvalid g x -> vvalid g1 x -> vvalid g2 x -> vgamma g x = (false, l, r) -> vgamma g1 x = (true, l, r) -> mark1 x g g1 -> edge_spanning_tree g1 (x, L) g2 -> edge_spanning_tree g2 (x, R) g3 -> spanning_tree g x g3.
proof: Proof. intros. apply (spanning_list_spanning_tree2 _ g1 _ _ (x, L) (x, R)); auto; intros. + intro. inversion H7. + pose proof (only_two_edges x e H). simpl in H7 |-* . split; intros. - destruct H8 as [? | [? | ?]]; [subst e..|exfalso; auto]. * split; [|intuition]. apply (@left_valid _ _ _ _ _ _ g (binGraph g)); auto. * split; [|intuition]. apply (@right_valid _ _ _ _ _ _ g (binGraph g)); auto. - destruct H8. intuition. + apply Graph_reachable_by_dec. apply weak_valid_vvalid_dec. pose proof H3. simpl in H3. inversion H3. subst l. apply (gamma_left_weak_valid g1 x true (dst g1 (x, L)) r); auto. + unfold unmarked. rewrite negateP_spec. unfold marked. simpl. simpl in H2. inversion H2. change (lg_gg g) with (g: LGraph). rewrite H8. intuition. + apply spanning_list_cons with g2; auto. apply spanning_list_cons with g3; auto. apply spanning_list_nil. auto. 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