|
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
¤ Dauer der Verarbeitung: 0.32 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
