|
los_graph[T: TYPE]: THEORY
BEGIN
x,y,z: VAR T
P,Q: VAR[T,T->bool]
los_graphic: LEMMA (FORALL x,y,z: P(x,y)&P(y,z)=>P(x,z)) &
(FORALL x,y: P(x,y) => P(y,x)) &
(FORALL x,y,z: Q(x,y)&Q(y,z)=>Q(x,z)) &
(FORALL x,y: Q(x,y) => Q(y,x)) &
(FORALL x,y: P(x,y) OR Q(x,y)) =>
(FORALL x,y:P(x,y)) OR (FORALL x,y: Q(x,y))
% Adjacy: LEMMA (FORALL x,y,z: P(x,y)&P(y,z)=>P(x,z)) &
% (FORALL x,y,z: Q(x,y)&Q(y,z)=>Q(x,z)) &
% (FORALL x,y: Q(x,y) => Q(y,x)) &
% (FORALL x,y: P(x,y) OR Q(x,y)) =>
% (FORALL x,y,z:P(x,y) OR (Q(y,z) AND Q(z,y)))
% Adjacx: LEMMA (FORALL x,y,z: P(x,y)&P(y,z)=>P(x,z)) &
% (FORALL x,y,z: Q(x,y)&Q(y,z)=>Q(x,z)) &
% (FORALL x,y: Q(x,y) => Q(y,x)) &
% (FORALL x,y: P(x,y) OR Q(x,y)) =>
% (FORALL x,y,z:P(x,y) OR (Q(x,z) AND Q(z,x)))
Los: LEMMA (FORALL x,y,z: P(x,y)&P(y,z)=>P(x,z)) &
(FORALL x,y,z: Q(x,y)&Q(y,z)=>Q(x,z)) &
(FORALL x,y: Q(x,y) => Q(y,x)) &
(FORALL x,y: P(x,y) OR Q(x,y)) =>
(FORALL x,y:P(x,y)) OR (FORALL x,y: Q(x,y))
END los_graph
¤ Dauer der Verarbeitung: 0.2 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.
|
