proposition: Lemma is_guarded_BinMaFin'_labeledgraph_add_edge: forall (g: LGraph) PV PE PE' e s d data_e, ~ evalid g e -> Same_set PE' (Intersection _ PE (fun e0 => e0 <> e)) -> is_guarded_BinMaFin' PV PE g -> is_guarded_BinMaFin' PV PE' (labeledgraph_add_edge g e s d data_e).
proof: Proof. unfold is_guarded_BinMaFin'. intros. eapply is_BinMaFin_si'; [| eassumption]. simpl. rewrite Same_set_spec in H0. split; [| split; [| split]]. + intros; simpl; reflexivity. + intros; simpl. specialize (H0 e0). rewrite !Intersection_spec in *. unfold addValidFunc. rewrite H0. destruct_eq_dec e0 e; [subst |]; try tauto. + simpl; intros. unfold updateEdgeFunc. destruct_eq_dec e e0; auto; subst. specialize (H0 e0). rewrite Intersection_spec in *. destruct H3. tauto. + simpl; intros. unfold updateEdgeFunc. destruct_eq_dec e e0; auto; subst. specialize (H0 e0). rewrite Intersection_spec in *. destruct H3. tauto. 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