Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/HOL/Library/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 18 kB

Quelle Nonpos_Ints.thy Sprache: Isabelle

(*  Title:    HOL/Library/Nonpos_Ints.thy
    Author:   Manuel Eberl, TU München
*)

section \<open>Non-negative, non-positive integers and reals\<close>

theory Nonpos_Ints
imports Complex_Main
begin

subsection\<open>Non-positive integers\<close>
text \<open>
  The set of non-positive integers on a ring. (in analogy to the set of non-negative
  integers \<^term>\<open>\<nat>\<close>) This is useful e.g. for the Gamma function.
\<close>

definition nonpos_Ints (\<open>\<int>\<^sub>\<le>\<^sub>0\<close>) where "\<int>\<^sub>\<le>\<^sub>0 = {of_int n |n. n \<le> 0}"

lemma zero_in_nonpos_Ints [simp,intro]: "0 \ \\<^sub>\\<^sub>0"
  unfolding nonpos_Ints_def by (auto intro!: exI[of _ "0::int"])

lemma neg_one_in_nonpos_Ints [simp,intro]: "-1 \ \\<^sub>\\<^sub>0"
  unfolding nonpos_Ints_def by (auto intro!: exI[of _ "-1::int"])

lemma neg_numeral_in_nonpos_Ints [simp,intro]: "-numeral n \ \\<^sub>\\<^sub>0"
  unfolding nonpos_Ints_def by (auto intro!: exI[of _ "-numeral n::int"])

lemma one_notin_nonpos_Ints [simp]: "(1 :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0"
  by (auto simp: nonpos_Ints_def)

lemma numeral_notin_nonpos_Ints [simp]: "(numeral n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0"
  by (auto simp: nonpos_Ints_def)

lemma minus_of_nat_in_nonpos_Ints [simp, intro]: "- of_nat n \ \\<^sub>\\<^sub>0"
proof -
  have "- of_nat n = of_int (-int n)" by simp
  also have "-int n \ 0" by simp
  hence "of_int (-int n) \ \\<^sub>\\<^sub>0" unfolding nonpos_Ints_def by blast
  finally show ?thesis .
qed

lemma of_nat_in_nonpos_Ints_iff: "(of_nat n :: 'a :: {ring_1,ring_char_0}) \ \\<^sub>\\<^sub>0 \ n = 0"
proof
  assume "(of_nat n :: 'a) \ \\<^sub>\\<^sub>0"
  then obtain m where "of_nat n = (of_int m :: 'a)" "m \ 0" by (auto simp: nonpos_Ints_def)
  hence "(of_int m :: 'a) = of_nat n" by simp
  also have "... = of_int (int n)" by simp
  finally have "m = int n" by (subst (asm) of_int_eq_iff)
  with \<open>m \<le> 0\<close> show "n = 0" by auto
qed simp

lemma nonpos_Ints_of_int: "n \ 0 \ of_int n \ \\<^sub>\\<^sub>0"
  unfolding nonpos_Ints_def by blast

lemma nonpos_IntsI:
  "x \ \ \ x \ 0 \ (x :: 'a :: linordered_idom) \ \\<^sub>\\<^sub>0"
  unfolding nonpos_Ints_def Ints_def by auto

lemma nonpos_Ints_subset_Ints: "\\<^sub>\\<^sub>0 \ \"
  unfolding nonpos_Ints_def Ints_def by blast

lemma nonpos_Ints_nonpos [dest]: "x \ \\<^sub>\\<^sub>0 \ x \ (0 :: 'a :: linordered_idom)"
  unfolding nonpos_Ints_def by auto

lemma nonpos_Ints_Int [dest]: "x \ \\<^sub>\\<^sub>0 \ x \ \"
  unfolding nonpos_Ints_def Ints_def by blast

lemma nonpos_Ints_cases:
  assumes "x \ \\<^sub>\\<^sub>0"
  obtains n where "x = of_int n" "n \ 0"
  using assms unfolding nonpos_Ints_def by (auto elim!: Ints_cases)

lemma nonpos_Ints_cases':
  assumes "x \ \\<^sub>\\<^sub>0"
  obtains n where "x = -of_nat n"
proof -
  from assms obtain m where "x = of_int m" and m: "m \ 0" by (auto elim!: nonpos_Ints_cases)
  hence "x = - of_int (-m)" by auto
  also from m have "(of_int (-m) :: 'a) = of_nat (nat (-m))" by simp_all
  finally show ?thesis by (rule that)
qed

lemma of_real_in_nonpos_Ints_iff: "(of_real x :: 'a :: real_algebra_1) \ \\<^sub>\\<^sub>0 \ x \ \\<^sub>\\<^sub>0"
proof
  assume "of_real x \ (\\<^sub>\\<^sub>0 :: 'a set)"
  then obtain n where "(of_real x :: 'a) = of_int n" "n \ 0" by (erule nonpos_Ints_cases)
  note \<open>of_real x = of_int n\<close>
  also have "of_int n = of_real (of_int n)" by (rule of_real_of_int_eq [symmetric])
  finally have "x = of_int n" by (subst (asm) of_real_eq_iff)
  with \<open>n \<le> 0\<close> show "x \<in> \<int>\<^sub>\<le>\<^sub>0" by (simp add: nonpos_Ints_of_int)
qed (auto elim!: nonpos_Ints_cases intro!: nonpos_Ints_of_int)

lemma nonpos_Ints_altdef: "\\<^sub>\\<^sub>0 = {n \ \. (n :: 'a :: linordered_idom) \ 0}"
  by (auto intro!: nonpos_IntsI elim!: nonpos_Ints_cases)

lemma uminus_in_Nats_iff: "-x \ \ \ x \ \\<^sub>\\<^sub>0"
proof
  assume "-x \ \"
  then obtain n where "n \ 0" "-x = of_int n" by (auto simp: Nats_altdef1)
  hence "-n \ 0" "x = of_int (-n)" by (simp_all add: eq_commute minus_equation_iff[of x])
  thus "x \ \\<^sub>\\<^sub>0" unfolding nonpos_Ints_def by blast
next
  assume "x \ \\<^sub>\\<^sub>0"
  then obtain n where "n \ 0" "x = of_int n" by (auto simp: nonpos_Ints_def)
  hence "-n \ 0" "-x = of_int (-n)" by (simp_all add: eq_commute minus_equation_iff[of x])
  thus "-x \ \" unfolding Nats_altdef1 by blast
qed

lemma uminus_in_nonpos_Ints_iff: "-x \ \\<^sub>\\<^sub>0 \ x \ \"
  using uminus_in_Nats_iff[of "-x"] by simp

lemma nonpos_Ints_mult: "x \ \\<^sub>\\<^sub>0 \ y \ \\<^sub>\\<^sub>0 \ x * y \ \"
  using Nats_mult[of "-x" "-y"] by (simp add: uminus_in_Nats_iff)

lemma Nats_mult_nonpos_Ints: "x \ \ \ y \ \\<^sub>\\<^sub>0 \ x * y \ \\<^sub>\\<^sub>0"
  using Nats_mult[of x "-y"] by (simp add: uminus_in_Nats_iff)

lemma nonpos_Ints_mult_Nats:
  "x \ \\<^sub>\\<^sub>0 \ y \ \ \ x * y \ \\<^sub>\\<^sub>0"
  using Nats_mult[of "-x" y] by (simp add: uminus_in_Nats_iff)

lemma nonpos_Ints_add:
  "x \ \\<^sub>\\<^sub>0 \ y \ \\<^sub>\\<^sub>0 \ x + y \ \\<^sub>\\<^sub>0"
  using Nats_add[of "-x" "-y"] uminus_in_Nats_iff[of "y+x", simplified minus_add]
  by (simp add: uminus_in_Nats_iff add.commute)

lemma nonpos_Ints_diff_Nats:
  "x \ \\<^sub>\\<^sub>0 \ y \ \ \ x - y \ \\<^sub>\\<^sub>0"
  using Nats_add[of "-x" "y"] uminus_in_Nats_iff[of "x-y", simplified minus_add]
  by (simp add: uminus_in_Nats_iff add.commute)

lemma Nats_diff_nonpos_Ints:
  "x \ \ \ y \ \\<^sub>\\<^sub>0 \ x - y \ \"
  using Nats_add[of "x" "-y"] by (simp add: uminus_in_Nats_iff add.commute)

lemma plus_of_nat_eq_0_imp: "z + of_nat n = 0 \ z \ \\<^sub>\\<^sub>0"
proof -
  assume "z + of_nat n = 0"
  hence A: "z = - of_nat n" by (simp add: eq_neg_iff_add_eq_0)
  show "z \ \\<^sub>\\<^sub>0" by (subst A) simp
qed

subsection\<open>Non-negative reals\<close>

definition nonneg_Reals :: "'a::real_algebra_1 set"  (\<open>\<real>\<^sub>\<ge>\<^sub>0\<close>)
  where "\\<^sub>\\<^sub>0 = {of_real r | r. r \ 0}"

lemma nonneg_Reals_of_real_iff [simp]: "of_real r \ \\<^sub>\\<^sub>0 \ r \ 0"
  by (force simp add: nonneg_Reals_def)

lemma nonneg_Reals_subset_Reals: "\\<^sub>\\<^sub>0 \ \"
  unfolding nonneg_Reals_def Reals_def by blast

lemma nonneg_Reals_Real [dest]: "x \ \\<^sub>\\<^sub>0 \ x \ \"
  unfolding nonneg_Reals_def Reals_def by blast

lemma nonneg_Reals_of_nat_I [simp]: "of_nat n \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_of_real_iff of_nat_0_le_iff of_real_of_nat_eq)

lemma nonneg_Reals_cases:
  assumes "x \ \\<^sub>\\<^sub>0"
  obtains r where "x = of_real r" "r \ 0"
  using assms unfolding nonneg_Reals_def by (auto elim!: Reals_cases)

lemma nonneg_Reals_zero_I [simp]: "0 \ \\<^sub>\\<^sub>0"
  unfolding nonneg_Reals_def by auto

lemma nonneg_Reals_one_I [simp]: "1 \ \\<^sub>\\<^sub>0"
  by (metis (mono_tags, lifting) nonneg_Reals_of_nat_I of_nat_1)

lemma nonneg_Reals_minus_one_I [simp]: "-1 \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_of_real_iff le_minus_one_simps(3) of_real_1 of_real_def real_vector.scale_minus_left)

lemma nonneg_Reals_numeral_I [simp]: "numeral w \ \\<^sub>\\<^sub>0"
  by (metis (no_types) nonneg_Reals_of_nat_I of_nat_numeral)

lemma nonneg_Reals_minus_numeral_I [simp]: "- numeral w \ \\<^sub>\\<^sub>0"
  using nonneg_Reals_of_real_iff not_zero_le_neg_numeral by fastforce

lemma nonneg_Reals_add_I [simp]: "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a + b \ \\<^sub>\\<^sub>0"
apply (simp add: nonneg_Reals_def)
apply clarify
apply (rename_tac r s)
apply (rule_tac x="r+s" in exI, auto)
done

lemma nonneg_Reals_mult_I [simp]: "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a * b \ \\<^sub>\\<^sub>0"
  unfolding nonneg_Reals_def  by (auto simp: of_real_def)

lemma nonneg_Reals_inverse_I [simp]:
  fixes a :: "'a::real_div_algebra"
  shows "a \ \\<^sub>\\<^sub>0 \ inverse a \ \\<^sub>\\<^sub>0"
  by (simp add: nonneg_Reals_def image_iff) (metis inverse_nonnegative_iff_nonnegative of_real_inverse)

lemma nonneg_Reals_divide_I [simp]:
  fixes a :: "'a::real_div_algebra"
  shows "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a / b \ \\<^sub>\\<^sub>0"
  by (simp add: divide_inverse)

lemma nonneg_Reals_pow_I [simp]: "a \ \\<^sub>\\<^sub>0 \ a^n \ \\<^sub>\\<^sub>0"
  by (induction n) auto

lemma complex_nonneg_Reals_iff: "z \ \\<^sub>\\<^sub>0 \ Re z \ 0 \ Im z = 0"
  by (auto simp: nonneg_Reals_def) (metis complex_of_real_def complex_surj)

lemma ii_not_nonneg_Reals [iff]: "\ \ \\<^sub>\\<^sub>0"
  by (simp add: complex_nonneg_Reals_iff)

subsection\<open>Non-positive reals\<close>

definition nonpos_Reals :: "'a::real_algebra_1 set"  (\<open>\<real>\<^sub>\<le>\<^sub>0\<close>)
  where "\\<^sub>\\<^sub>0 = {of_real r | r. r \ 0}"

lemma nonpos_Reals_of_real_iff [simp]: "of_real r \ \\<^sub>\\<^sub>0 \ r \ 0"
  by (force simp add: nonpos_Reals_def)

lemma nonpos_Reals_subset_Reals: "\\<^sub>\\<^sub>0 \ \"
  unfolding nonpos_Reals_def Reals_def by blast

lemma nonpos_Ints_subset_nonpos_Reals: "\\<^sub>\\<^sub>0 \ \\<^sub>\\<^sub>0"
  by (metis nonpos_Ints_cases nonpos_Ints_nonpos nonpos_Ints_of_int
    nonpos_Reals_of_real_iff of_real_of_int_eq subsetI)

lemma nonpos_Reals_of_nat_iff [simp]: "of_nat n \ \\<^sub>\\<^sub>0 \ n=0"
  by (metis nonpos_Reals_of_real_iff of_nat_le_0_iff of_real_of_nat_eq)

lemma nonpos_Reals_Real [dest]: "x \ \\<^sub>\\<^sub>0 \ x \ \"
  unfolding nonpos_Reals_def Reals_def by blast

lemma nonpos_Reals_cases:
  assumes "x \ \\<^sub>\\<^sub>0"
  obtains r where "x = of_real r" "r \ 0"
  using assms unfolding nonpos_Reals_def by (auto elim!: Reals_cases)

lemma uminus_nonneg_Reals_iff [simp]: "-x \ \\<^sub>\\<^sub>0 \ x \ \\<^sub>\\<^sub>0"
  apply (auto simp: nonpos_Reals_def nonneg_Reals_def)
  apply (metis nonpos_Reals_of_real_iff minus_minus neg_le_0_iff_le of_real_minus)
  done

lemma uminus_nonpos_Reals_iff [simp]: "-x \ \\<^sub>\\<^sub>0 \ x \ \\<^sub>\\<^sub>0"
  by (metis (no_types) minus_minus uminus_nonneg_Reals_iff)

lemma nonpos_Reals_zero_I [simp]: "0 \ \\<^sub>\\<^sub>0"
  unfolding nonpos_Reals_def by force

lemma nonpos_Reals_one_I [simp]: "1 \ \\<^sub>\\<^sub>0"
  using nonneg_Reals_minus_one_I uminus_nonneg_Reals_iff by blast

lemma nonpos_Reals_numeral_I [simp]: "numeral w \ \\<^sub>\\<^sub>0"
  using nonneg_Reals_minus_numeral_I uminus_nonneg_Reals_iff by blast

lemma nonpos_Reals_add_I [simp]: "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a + b \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_add_I add_uminus_conv_diff minus_diff_eq minus_minus uminus_nonpos_Reals_iff)

lemma nonpos_Reals_mult_I1: "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a * b \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_mult_I mult_minus_right uminus_nonneg_Reals_iff)

lemma nonpos_Reals_mult_I2: "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a * b \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_mult_I mult_minus_left uminus_nonneg_Reals_iff)

lemma nonpos_Reals_mult_of_nat_iff:
  fixes a:: "'a :: real_div_algebra" shows "a * of_nat n \ \\<^sub>\\<^sub>0 \ a \ \\<^sub>\\<^sub>0 \ n=0"
  apply (auto intro: nonpos_Reals_mult_I2)
  apply (auto simp: nonpos_Reals_def)
  apply (rule_tac x="r/n" in exI)
  apply (auto simp: field_split_simps)
  done

lemma nonpos_Reals_inverse_I:
    fixes a :: "'a::real_div_algebra"
    shows "a \ \\<^sub>\\<^sub>0 \ inverse a \ \\<^sub>\\<^sub>0"
  using nonneg_Reals_inverse_I uminus_nonneg_Reals_iff by fastforce

lemma nonpos_Reals_divide_I1:
    fixes a :: "'a::real_div_algebra"
    shows "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a / b \ \\<^sub>\\<^sub>0"
  by (simp add: nonpos_Reals_inverse_I nonpos_Reals_mult_I1 divide_inverse)

lemma nonpos_Reals_divide_I2:
    fixes a :: "'a::real_div_algebra"
    shows "\a \ \\<^sub>\\<^sub>0; b \ \\<^sub>\\<^sub>0\ \ a / b \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_divide_I minus_divide_left uminus_nonneg_Reals_iff)

lemma nonpos_Reals_divide_of_nat_iff:
  fixes a:: "'a :: real_div_algebra" shows "a / of_nat n \ \\<^sub>\\<^sub>0 \ a \ \\<^sub>\\<^sub>0 \ n=0"
  apply (auto intro: nonpos_Reals_divide_I2)
  apply (auto simp: nonpos_Reals_def)
  apply (rule_tac x="r*n" in exI)
  apply (auto simp: field_split_simps mult_le_0_iff)
  done

lemma nonpos_Reals_inverse_iff [simp]:
  fixes a :: "'a::real_div_algebra"
  shows "inverse a \ \\<^sub>\\<^sub>0 \ a \ \\<^sub>\\<^sub>0"
  using nonpos_Reals_inverse_I by fastforce

lemma nonpos_Reals_pow_I: "\a \ \\<^sub>\\<^sub>0; odd n\ \ a^n \ \\<^sub>\\<^sub>0"
  by (metis nonneg_Reals_pow_I power_minus_odd uminus_nonneg_Reals_iff)

lemma complex_nonpos_Reals_iff: "z \ \\<^sub>\\<^sub>0 \ Re z \ 0 \ Im z = 0"
   using complex_is_Real_iff by (force simp add: nonpos_Reals_def)

lemma ii_not_nonpos_Reals [iff]: "\ \ \\<^sub>\\<^sub>0"
  by (simp add: complex_nonpos_Reals_iff)

lemma plus_one_in_nonpos_Ints_imp: "z + 1 \ \\<^sub>\\<^sub>0 \ z \ \\<^sub>\\<^sub>0"
  using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all

lemma of_int_in_nonpos_Ints_iff:
  "(of_int n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0 \ n \ 0"
  by (auto simp: nonpos_Ints_def)

lemma one_plus_of_int_in_nonpos_Ints_iff:
  "(1 + of_int n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0 \ n \ -1"
proof -
  have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp
  also have "\ \ \\<^sub>\\<^sub>0 \ n + 1 \ 0" by (subst of_int_in_nonpos_Ints_iff) simp_all
  also have "\ \ n \ -1" by presburger
  finally show ?thesis .
qed

lemma one_minus_of_nat_in_nonpos_Ints_iff:
  "(1 - of_nat n :: 'a :: ring_char_0) \ \\<^sub>\\<^sub>0 \ n > 0"
proof -
  have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp
  also have "\ \ \\<^sub>\\<^sub>0 \ n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger
  finally show ?thesis .
qed

lemma fraction_not_in_Nats:
  assumes "\n dvd m" "n \ 0"
  shows   "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)"
proof
  assume "of_int m / of_int n \ (\ :: 'a set)"
  also note Nats_subset_Ints
  finally have "of_int m / of_int n \ (\ :: 'a set)" .
  moreover have "of_int m / of_int n \ (\ :: 'a set)"
    using assms by (intro fraction_not_in_Ints)
  ultimately show False by contradiction
qed

lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \ \ \ z \ \\<^sub>\\<^sub>0"
  by (auto simp: Ints_def nonpos_Ints_def)

lemma double_in_nonpos_Ints_imp:
  assumes "2 * (z :: 'a :: field_char_0) \ \\<^sub>\\<^sub>0"
  shows   "z \ \\<^sub>\\<^sub>0 \ z + 1/2 \ \\<^sub>\\<^sub>0"
proof-
  from assms obtain k where k: "2 * z = - of_nat k" by (elim nonpos_Ints_cases')
  thus ?thesis by (cases "even k") (auto elim!: evenE oddE simp: field_simps)
qed

lemma fraction_numeral_Ints_iff [simp]:
  "numeral a / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)
   \<longleftrightarrow> (numeral b :: int) dvd numeral a"  (is "?L=?R")
proof
  show "?L \ ?R"
    by (metis fraction_not_in_Ints of_int_numeral zero_neq_numeral)
  assume ?R
  then obtain k::int where "numeral a = numeral b * (of_int k :: 'a)"
    unfolding dvd_def by (metis of_int_mult of_int_numeral)
  then show ?L
    by (metis Ints_of_int divide_eq_eq mult.commute of_int_mult of_int_numeral)
qed

lemma fraction_numeral_Ints_iff1 [simp]:
  "1 / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)
   \<longleftrightarrow> b = Num.One"  (is "?L=?R")
  using fraction_numeral_Ints_iff [of Num.One, where 'a='a] by simp

lemma fraction_numeral_Nats_iff [simp]:
  "numeral a / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)
   \<longleftrightarrow> (numeral b :: int) dvd numeral a"  (is "?L=?R")
proof
  show "?L \ ?R"
    using Nats_subset_Ints fraction_numeral_Ints_iff by blast
  assume ?R
  then obtain k::nat where "numeral a = numeral b * (of_nat k :: 'a)"
    unfolding dvd_def
    by (metis dvd_def int_dvd_int_iff of_nat_mult of_nat_numeral)
  then show ?L
    by (metis mult_of_nat_commute nonzero_divide_eq_eq of_nat_in_Nats
        zero_neq_numeral)
qed

lemma fraction_numeral_Nats_iff1 [simp]:
  "1 / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)
   \<longleftrightarrow> b = Num.One"  (is "?L=?R")
  using fraction_numeral_Nats_iff [of Num.One, where 'a='a] by simp

end

quality98%

¤ Dauer der Verarbeitung: 0.7 Sekunden ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.