graph_deg_sum[T: TYPE]: THEORY BEGIN IMPORTING graph_deg[T], % fslib@finite_sets_sum_real[T] finite_sets@finite_sets_sum_real[T] v: VAR T G,GS: VAR graph[T] x,y: VAR T V_reduced: VAR set[T] P : VAR pred[graph[T]] n : VAR nat e: VAR doubleton[T] deg_lem0: LEMMA num_edges(G) = 0 IMPLIES sum(vert(G), (LAMBDA (v: T): deg(v, G))) = 0 deg_lem2: LEMMA remove(x, remove(y, vert(G))) = V_reduced AND e = dbl[T](x, y) AND nonempty?(edges(G)) AND choose(edges(G)) = e IMPLIES sum(V_reduced, (LAMBDA (v:T): deg(v,G))) = sum(V_reduced,(LAMBDA (v:T): deg(v,del_edge(G,e)))) edge_induction : LEMMA (FORALL G : P(G)) IFF (FORALL n, G: num_edges(G) = n IMPLIES P(G)) deg_thm: THEOREM sum(vert(G), (LAMBDA (v: T): deg(v,G))) = 2 * num_edges(G) IMPORTING subgraphs[T] subgraph_deg: THEOREM subgraph?(GS,G) AND vert(G)(v) IMPLIES deg(v,GS) <= deg(v,G) END graph_deg_sum