[STATEMENT]
lemma add_delete_edges: "wf_graph (G::'v graph) \<Longrightarrow> (a,b) \<in> edges G \<Longrightarrow> (a,b) \<notin> fs \<Longrightarrow>
    add_edge a b (delete_edges G (insert (a, b) fs)) = (delete_edges G fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph G; (a, b) \<in> edges G; (a, b) \<notin> fs\<rbrakk> \<Longrightarrow> add_edge a b (delete_edges G (insert (a, b) fs)) = delete_edges G fs
[PROOF STEP]
by(auto simp add: delete_edges_simp2 add_edge_def wf_graph_def)


 \<comment> \<open>fully_connected\<close>