proposition: Lemma gamma_step: forall (g : Graph) x (d: DV) (l r: addr), vvalid g x -> vgamma g x = (d, l, r) -> forall y, step g x y <-> y = l \/ y = r.
proof: Proof. intros. simpl in H0; inversion H0; subst. rewrite step_spec; split; intros. + destruct H1 as [e [? [? ?]]]. pose proof (only_two_edges x e H). cbv beta in H4. pose proof (proj1 H4 (conj H2 H1)). destruct H5; subst e; auto. + destruct H1. - exists (x, L). s_rewrite (left_sound g); auto. apply (left_valid g) in H. auto. - exists (x, R). s_rewrite (right_sound g); auto. apply (right_valid g) in H. auto. Qed.
imports: CertiGraph.lib.Ensembles_ext Coq.Lists.List VST.msl.seplog VST.msl.log_normalize CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.msl_ext.seplog CertiGraph.graph.graph_model CertiGraph.graph.path_lemmas CertiGraph.graph.reachable_computable CertiGraph.graph.reachable_ind CertiGraph.graph.subgraph2 CertiGraph.graph.graph_gen CertiGraph.graph.BinGraph CertiGraph.graph.MathGraph CertiGraph.graph.FiniteGraph CertiGraph.msl_application.Graph Coq.Logic.Classical