proposition: Lemma edge_spanning_tree_left_null: forall (g: Graph) x d l r, vvalid g x -> vgamma g x = (d, l, r) -> (marked g) l -> edge_spanning_tree g (x, L) (Graph_gen_left_null g x).
proof: Proof. intros. assert (l = dst g (x, L)) by (simpl in H0; inversion H0; auto). hnf. change (lg_gg g) with (g: LGraph). destruct (node_pred_dec (marked g) (dst g (x, L))). 2: subst l; exfalso; auto. split. + hnf. simpl. split; [| split; [|split; [| split]]]; [tauto | tauto | tauto | | ]. - intros. unfold updateEdgeFunc. destruct (equiv_dec (x, L) e); intuition. - right. unfold updateEdgeFunc. destruct (equiv_dec (x, L) (x, L)); intuition. * apply (valid_not_null g) in H3; auto. reflexivity. * apply (@left_valid _ _ _ _ _ _ g (binGraph g)) in H; auto. + simpl. tauto. 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