| products/sources/formale sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sturmsquarefree.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(sturmsquarefree
(sturm_sequence?_TCC1 0 (sturm_sequence?_TCC1-1 nil 3583755671 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (sturm_sequence?_TCC2 0 (sturm_sequence?_TCC2-1 nil 3583755671 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (poly_deriv const-decl "real" polynomials "reals/") (^ const-decl "real" exponentiation nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (/= const-decl "boolean" notequal nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (sturm_sequence_degree_1 0 (sturm_sequence_degree_1-1 nil 3588942625 ("" (skeep) (("" (expand "sturm_sequence?") (("" (assert) (("" (split +) (("1" (skeep) (("1" (assert) nil nil)) nil) ("2" (skeep) (("2" (case "i = 1") (("1" (replaces -1) (("1" (replace -5) (("1" (expand "poly_deriv" -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (skeep) (("3" (assert) nil nil)) nil) ("4" (skeep) (("4" (assert) (("4" (replaces -1) (("4" (replace -2) (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sturm_sequence? const-decl "bool" sturmsquarefree nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (poly_deriv const-decl "real" polynomials "reals/") (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (polynomial const-decl "[real -> real]" polynomials "reals/") (sigma def-decl "real" sigma "reals/") (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (max_npreal_0 formula-decl nil min_max "reals/") (int_minus_int_is_int application-judgement "int" integers nil)) shostak)) (sturm_seq_repeated_root 0 (sturm_seq_repeated_root-1 nil 3584191381 ("" (skeep) (("" (case "FORALL (i:nat): i-1>=0 AND i+1<=m AND polynomial(p(i),n(i))(x)=0 IMPLIES (polynomial(p(i-1),n(i-1))(x)=0 IFF polynomial(p(i+1),n(i+1))(x)=0)") (("1" (skeep) (("1" (case "FORALL (j:nat): i-j>=0 IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i-k), n(i-k))(x) = 0") (("1" (case "FORALL (j:nat): i+j<=m IMPLIES FORALL (k:nat): k<=j IMPLIES polynomial(p(i+k), n(i+k))(x) = 0") (("1" (skeep) (("1" (case "j>=i") (("1" (inst - "j-i") (("1" (assert) (("1" (inst - "j-i") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (inst -2 "i-j") (("1" (assert) (("1" (inst -2 "i-j") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-1 2)) (("2" (induct "j") (("1" (assert) (("1" (skeep) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) (("2" (case "k!1=0 OR k!1=1") (("1" (ground) nil nil) ("2" (flatten) (("2" (inst-cp - "k!1-1") (("2" (inst - "k!1-2") (("1" (assert) (("1" (assert) (("1" (inst - "i-1+k!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (case "k!1=0") (("1" (assert) nil nil) ("2" (assert) (("2" (inst-cp - "k!1-1") (("2" (case "k!1=1") (("1" (hide -2) (("1" (assert) (("1" (inst - "i") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (inst - "k!1-2") (("1" (assert) (("1" (inst - "i-k!1+1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (assert) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) nil nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil) ("7" (skosimp*) (("7" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (assert) (("2" (expand "sturm_sequence?") (("2" (flatten) (("2" (inst - "x" "i") (("2" (assert) (("2" (expand "sign_ext" -7) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (polynomial const-decl "[real -> real]" polynomials "reals/") (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (k!1 skolem-const-decl "nat" sturmsquarefree nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (m skolem-const-decl "nat" sturmsquarefree nil) (j skolem-const-decl "upto(m)" sturmsquarefree nil) (i skolem-const-decl "nat" sturmsquarefree nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (k!1 skolem-const-decl "nat" sturmsquarefree nil) (sturm_sequence? const-decl "bool" sturmsquarefree nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sturm_seq_last_nonzero 0 (sturm_seq_last_nonzero-1 nil 3588410248 ("" (skeep) (("" (skeep) (("" (case "NOT FORALL (xyzp:real): polynomial(p(m),n(m))(xyzp) = 0") (("1" (skeep) (("1" (expand "sturm_sequence?") (("1" (flatten) (("1" (inst -6 "xyz" "xyzp") (("1" (expand "sign_ext" -6) (("1" (assert) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "polynomial_eq_coeff") (("2" (inst - "p(m)" "LAMBDA (i:nat): 0" "n(m)") (("2" (assert) (("2" (flatten) (("2" (hide -2) (("2" (split -) (("1" (inst - "n(m)") (("1" (expand "sturm_sequence?") (("1" (flatten) (("1" (inst -5 "m") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (decompose-equality 1) (("2" (inst - "x!1") (("2" (assert) (("2" (replaces -1) (("2" (expand "polynomial" +) (("2" (rewrite "sigma_restrict_eq_0") (("2" (skosimp*) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((polynomial_eq_coeff formula-decl nil polynomials "reals/") (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma_restrict_eq_0 formula-decl nil sigma "reals/") (real_times_real_is_real application-judgement "real" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (sign_ext const-decl "{sig: real | (sig = -1 OR sig = 1 OR sig = 0) AND sig * x = abs(x)}" sign "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sturm_sequence? const-decl "bool" sturmsquarefree nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (polynomial const-decl "[real -> real]" polynomials "reals/")) shostak)) (sturm_seq_first_signs_eq 0 (sturm_seq_first_signs_eq-1 nil 3587370024 ("" (skeep) (("" (case "NOT (polynomial(p(0), n(0))(x) /= 0 AND polynomial(p(0), n(0))(y) /= 0)") (("1" (hide 2) (("1" (inst-cp - "x") (("1" (inst - "y") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (inst-cp - "b") (("2" (assert) (("2" (flatten) (("2" (case "polynomial(poly_deriv(p(0)),max(n(0)-1,0))(b) = 0") (("1" (expand "sturm_sequence?") (("1" (flatten) (("1" (inst -8 "b") (("1" (assert) (("1" (expand "sign_ext" -8) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "poly_continuous") (("2" (inst - "poly_deriv(p(0))" "max(n(0)-1,0)" "b" "abs(polynomial(poly_deriv(p(0)),n(0)-1)(b))") (("1" (skeep -) (("1" (case "EXISTS (deltiv:posreal): FORALL (x1:real): abs(b-x1) (("1" (case "sign_ext(polynomial(p(0), n(0))(x)) = -sign_ext(polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)) AND sign_ext(polynomial(p(0), n(0))(y)) = sign_ext(polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b))") (("1" (hide (-2 -3)) (("1" (flatten) (("1" (expand "sturm_sequence?") (("1" (flatten) (("1" (inst -9 "b") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 6) (("2" (case "polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)>0") (("1" (skeep -2) (("1" (case "FORALL (x1,x2:real): abs(x1-b) (("1" (inst-cp - "b-deltiv/2" "b") (("1" (inst-cp - "b" "b+deltiv/2") (("1" (label "hyplem" -1) (("1" (hide "hyplem") (("1" (assert) (("1" (split +) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (assert) (("1" (split 1) (("1" (propax) nil nil) ("2" (assert) (("2" (hide -1) (("2" (split -) (("1" (replace -7) (("1" (assert) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(0)" "0" "n(0)" "x" "b-deltiv/2") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst - "cc") (("1" (inst - "cc") (("1" (inst - "cc") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "b-deltiv/2") (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sign_ext") (("2" (lift-if) (("2" (assert) (("2" (split 1) (("1" (assert) (("1" (hide -3) (("1" (split -) (("1" (replace -8) (("1" (assert) (("1" (lemma "poly_intermediate_value_dec") (("1" (inst - "p(0)" "0" "n(0)" "b+deltiv/2" "y") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst - "cc") (("1" (inst - "cc") (("1" (inst - "cc") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "b+deltiv/2") (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "poly_strictly_increasing") (("2" (inst - "p(0)" "n(0)" "x1" "x2") (("2" (assert) (("2" (case "n(0)=0") (("1" (replaces -1) (("1" (expand "polynomial") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skeep) (("2" (expand "max") (("2" (assert) (("2" (inst - "c") (("2" (assert) (("2" (split -) (("1" (inst - "c") (("1" (flatten) (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" (-1 -2 -3 -4 -5 1)) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "polynomial(poly_deriv(p(0)), max(n(0)-1,0))(b)<0") (("1" (hide 1) (("1" (skeep -2) (("1" (case "FORALL (x1,x2:real): abs(x1-b) (("1" (inst-cp - "b-deltiv/2" "b") (("1" (inst-cp - "b" "b+deltiv/2") (("1" (label "hyplem" -1) (("1" (hide "hyplem") (("1" (assert) (("1" (split +) (("1" (expand "sign_ext") (("1" (lift-if) (("1" (assert) (("1" (split 1) (("1" (replace -9) (("1" (assert) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(0)" "0" "n(0)" "x" "b-deltiv/2") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst - "cc") (("1" (inst - "cc") (("1" (inst - "cc") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "b-deltiv/2") (("2" (split -3) (("1" (assert) (("1" (hide-all-but 2) (("1" (grind) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide-all-but 2) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "sign_ext") (("2" (lift-if) (("2" (assert) (("2" (split 1) (("1" (propax) nil nil) ("2" (assert) (("2" (hide -2) (("2" (split -) (("1" (replace -7) (("1" (assert) (("1" (lemma "poly_intermediate_value_inc") (("1" (inst - "p(0)" "0" "n(0)" "b+deltiv/2" "y") (("1" (assert) (("1" (split -) (("1" (skeep -1) (("1" (inst - "cc") (("1" (inst - "cc") (("1" (inst - "cc") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "b+deltiv/2") (("2" (split -) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (lemma "poly_strictly_decreasing") (("2" (inst - "p(0)" "n(0)" "x1" "x2") (("2" (assert) (("2" (case "n(0)=0") (("1" (replaces -1) (("1" (expand --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
