proposition: Lemma edge_spanning_tree_left_vgamma: forall (g1 g2: Graph) x l r, vvalid g1 x -> vgamma g1 x = (true, l, r) -> edge_spanning_tree g1 (x, L) g2 -> exists l', vgamma g2 x = (true, l', r).
proof: Proof. intros. simpl. exists (dst g2 (x, L)). assert (Hvg2: vvalid g2 x) by (rewrite <- edge_spanning_tree_left_vvalid; eauto). unfold edge_spanning_tree in H1. change (lg_gg g1) with (g1: LGraph) in H1. destruct (node_pred_dec (marked g1) (dst g1 (x, L))). + destruct H1 as [[_ [_ [_ [? _]]]] ?]. simpl in H0, H2. inversion H0. rewrite H4. symmetry in H4. rewrite H2 in H4. change (lg_gg g2) with (g2: LGraph) in H4. rewrite <- H4. f_equal. symmetry. apply H1. - intro. inversion H3. - apply (@right_valid _ _ _ _ _ _ g1 (binGraph g1)) in H; auto. - apply (@right_valid _ _ _ _ _ _ g2 (binGraph g2)) in Hvg2; auto. + destruct H1 as [? [[_ [_ [_ ?]]] _]]. assert (marked g1 x) by (simpl in *; inversion H0; auto). assert (~ g1 |= dst g1 (x, L) ~o~> x satisfying (unmarked g1)) by (intro HS; apply reachable_by_foot_prop in HS; auto). assert (marked g2 x) by (specialize (H1 x); tauto). simpl in H5. rewrite <- H5. f_equal. simpl in H2. unfold predicate_weak_evalid in H2. simpl in H0. inversion H0. symmetry. change (lg_gg g1) with (g1: LGraph) in *. change (lg_gg g2) with (g2: LGraph) in *. apply H2; split. - apply (@right_valid _ _ _ _ _ _ g1 (binGraph g1) x); auto. - rewrite (@right_sound _ _ _ _ _ _ g1 (binGraph g1) x); auto. - apply (@right_valid _ _ _ _ _ _ g2 (binGraph g2) x); auto. - rewrite (@right_sound _ _ _ _ _ _ g2 (binGraph g2) x); 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