|
subtrees[T: TYPE]: THEORY
BEGIN
IMPORTING max_subtrees[T], graph_conn_defs[T]
G: VAR Graph[T] % not empty?(G)
S: VAR graph[T]
n: VAR nat
walk_acr: LEMMA FORALL (w: Walk(G)): n < length(w) AND
vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n))
IMPLIES
(EXISTS (j: posnat): (j <= n
AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j)))))
walk_acr2: LEMMA FORALL (w: Walk(G)): n < length(w) AND
vert(S)(seq(w)(0)) AND NOT vert(S)(seq(w)(n))
IMPLIES
(EXISTS (j: posnat): (j <= n
AND (vert(S)(seq(w)(j - 1)) AND NOT vert(S)(seq(w)(j)))))
e: VAR doubleton[T]
v,w: VAR T
add_dbl: LEMMA vert(G)(v) AND v /= w AND
add(dbl[T](v, w), edges(G))(e)
IMPLIES (FORALL (x: T): e(x) IMPLIES add(w, vert(G))(x))
max_tree_all_verts: LEMMA path_connected?(G) IMPLIES
vert(max_subtree(G)) = vert(G)
END subtrees
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.21Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
