lemma alluopairs_set1: "set (alluopairs xs) \ {(x, y). x\ set xs \ y\ set xs}" by (induct xs) auto
lemma alluopairs_set: "x\ set xs \ y \ set xs \ (x, y) \ set (alluopairs xs) \ (y, x) \ set (alluopairs xs)" by (induct xs) auto
lemma alluopairs_bex: assumes Pc: "\x \ set xs. \y \ set xs. P x y = P y x" shows"(\x \ set xs. \y \ set xs. P x y) \ (\(x, y) \ set (alluopairs xs). P x y)" proof assume"\x \ set xs. \y \ set xs. P x y" thenobtain x y where x: "x \ set xs" and y: "y \ set xs" and P: "P x y" by blast from alluopairs_set[OF x y] P Pc x y show"\(x, y) \ set (alluopairs xs). P x y" by auto next assume"\(x, y) \ set (alluopairs xs). P x y" thenobtain x and y where xy: "(x, y) \ set (alluopairs xs)" and P: "P x y" by blast+ from xy have"x \ set xs \ y \ set xs" using alluopairs_set1 by blast with P show"\x\set xs. \y\set xs. P x y" by blast qed
lemma alluopairs_ex: "\x y. P x y = P y x \
(\<exists>x \<in> set xs. \<exists>y \<in> set xs. P x y) = (\<exists>(x, y) \<in> set (alluopairs xs). P x y)" by (blast intro!: alluopairs_bex)
end
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.13Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
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.
