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]
   S: VAR finite_set[T]
   f: VAR [T -> real]
   B: VAR real

   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)


   sum_gt_bound : THEOREM (FORALL (t: (S)): f(t) >= B) 
                             IMPLIES sum(S,f) >= B*card(S)

   deg_gt_one   : THEOREM (FORALL (v:(vert(G))): deg(v,G) > 1) 
                                     IMPLIES num_edges(G)>=size(G)

 
END graph_deg_sum