|
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
