|
graph_inductions[T: TYPE]: THEORY
BEGIN
IMPORTING graphs[T]
G,GG,GGG: VAR graph[T]
P: VAR pred[graph[T]]
n: VAR nat
size_prep : LEMMA (FORALL G : P(G)) IFF
(FORALL n, G : size(G) = n IMPLIES P(G))
graph_induction_vert : THEOREM (FORALL G:
(FORALL GG: size(GG) < size(G) IMPLIES P(GG))
IMPLIES P(G))
IMPLIES (FORALL G: P(G))
graph_induction_vert_not: THEOREM (FORALL G: P(G)
IMPLIES
(EXISTS GG: size(GG) < size(G) AND
P(GG)))
IMPLIES (FORALL G: NOT P(G))
IMPORTING graph_ops[T]
num_edges_prep : LEMMA (FORALL G : P(G)) IFF
(FORALL n, G : num_edges(G) = n IMPLIES P(G))
graph_induction_edge : THEOREM (FORALL G:
(FORALL GG: num_edges(GG) < num_edges(G) IMPLIES P(GG))
IMPLIES P(G))
IMPLIES (FORALL G: P(G))
END graph_inductions
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot
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
|
