proposition: Lemma uf_under_bound_redirect_parent_lt: forall (g: UFGraph) root x (Hw : weak_valid g root) (Hv : vvalid g x) (Hr: ~ reachable g root x), vlabel g x < vlabel g root -> (forall y, reachable g root y -> root = y) -> uf_under_bound id g -> uf_under_bound id (Graph_gen_redirect_parent g x root Hw Hv Hr).
proof: Proof. intros. hnf in H1 |-* . simpl. unfold uf_bound, id in *. intros. destruct p as [p l]. destruct (redirect_to_root g (liGraph g) _ _ _ _ _ Hv Hr H0 H3 H4). - destruct H5; apply H1; auto. - destruct H5 as [? [l1 [? ?]]]. subst l. clear H4. subst v. simpl. destruct H7 as [[_ ?] [? _]]. specialize (H1 _ Hv _ H5 H4). simpl in H1. rewrite app_length. simpl length. clear - H H1. unfold UFGraph_LGraph in H. assert (vlabel (lg_gg g) x < vlabel (lg_gg g) root) by intuition. intuition. Qed.
imports: Coq.Logic.Classical Coq.Lists.List Coq.Sets.Ensembles VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.Ensembles_ext CertiGraph.lib.EquivDec_ext CertiGraph.lib.Relation_ext CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.graph_gen CertiGraph.graph.graph_relation CertiGraph.graph.subgraph2 CertiGraph.graph.reachable_computable CertiGraph.msl_application.Graph CertiGraph.msl_application.UnionFindGraph CertiGraph.msl_application.GList