| products/sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: cyclic_group.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(cyclic_group
(IMP_group_TCC1 0 (IMP_group_TCC1-1 nil 3407083357 ("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil) ((fullset_is_group formula-decl nil cyclic_group nil)) nil)) (generated_by_lem 0 (generated_by_lem-1 nil 3396976913 ("" (skosimp*) (("" (expand "generated_by") (("" (inst?) nil nil)) nil)) nil) ((generated_by const-decl "group" group nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (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)) shostak)) (generated_is_subgroup 0 (generated_is_subgroup-1 nil 3293271210 ("" (skosimp*) (("" (typepred "generated_by(a!1)") (("" (expand "subgroup?") (("" (expand "subset?") (("" (skosimp*) (("" (assert) (("" (expand "generated_by" -3) (("" (expand "member") (("" (skosimp) (("" (lemma "expt_member" ("G" "G!1" "a" "a!1" "i" "i!1")) (("" (expand "member") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((generated_by const-decl "group" group nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (one formal-const-decl "T" cyclic_group nil) (* formal-const-decl "[T, T -> T]" cyclic_group nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil cyclic_group nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (expt_member formula-decl nil group 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) (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) (subgroup? const-decl "bool" group_def nil)) shostak)) (generated_by_is_finite 0 (generated_by_is_finite-2 nil 3407003916 ("" (skosimp*) (("" (assert) (("" (rewrite "finite_group_surj") (("" (hide 2) (("" (expand "generated_by") (("" (inst + "k!1" "(LAMBDA (n: below[k!1]): a!1^n)") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (replace -2) (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (lemma "euclid_int") (("1" (inst - "k!1" "i!1") (("1" (skosimp*) (("1" (replace -1) (("1" (typepred "r!1") (("1" (inst + "r!1") (("1" (lemma "expt_mult") (("1" (inst - "a!1" "k!1*q!1" "r!1") (("1" (assert) (("1" (replace -1 + rl) (("1" (lemma "expt_expt") (("1" (inst?) (("1" (replace -1 + rl) (("1" (replace -7) (("1" (assert) (("1" (rewrite "one_expt") (("1" (rewrite "left_identity") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1) (("2" (assert) (("2" (inst + "n!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((a!1 skolem-const-decl "T" cyclic_group nil) (^ const-decl "T" group nil) (S!1 skolem-const-decl "set[T]" cyclic_group nil) (below type-eq-decl nil nat_types nil) (k!1 skolem-const-decl "posnat" cyclic_group nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (euclid_int formula-decl nil euclidean_division nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (expt_mult formula-decl nil group nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_expt formula-decl nil group nil) (left_identity formula-decl nil monad nil) (one_expt formula-decl nil group nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (NOT const-decl "[bool -> bool]" booleans nil) (surjective? const-decl "bool" functions nil) (generated_by const-decl "group" group nil) (one formal-const-decl "T" cyclic_group nil) (* formal-const-decl "[T, T -> T]" cyclic_group nil) (T formal-nonempty-type-decl nil cyclic_group nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (finite_group_surj formula-decl nil group_def nil)) nil) (generated_by_is_finite-1 nil 3407003019 ("" (skosimp*) (("" (assert) (("" (rewrite "finite_group_surj") (("" (hide 2) (("" (expand "generated_by") (("" (inst + "k!1" "(LAMBDA (n: below[k!1]): group[T,*,one].^(a!1,n))") (("1" (expand "surjective?") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (replace -2) (("1" (assert) (("1" (skosimp*) (("1" (replace -1) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cyclic_abelian 0 (cyclic_abelian-1 nil 3407083506 ("" (skosimp*) (("" (expand "abelian_group?") (("" (assert) (("" (expand "cyclic?") (("" (skosimp*) (("" (assert) (("" (expand "commutative?") (("" (skosimp*) (("" (expand "restrict") (("" (typepred "x!1") (("" (typepred "y!1") (("" (replace -3) (("" (hide -3) (("" (expand "generated_by") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (rewrite "expt_mult") (("" (rewrite "expt_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abelian_group? const-decl "bool" group_def nil) (cyclic? const-decl "boolean" group nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (one formal-const-decl "T" cyclic_group nil) (* formal-const-decl "[T, T -> T]" cyclic_group nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil cyclic_group nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (generated_by const-decl "group" group nil) (expt_mult formula-decl nil group 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) (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) (int_plus_int_is_int application-judgement "int" integers nil) (restrict const-decl "R" restrict nil) (commutative? const-decl "bool" operator_defs nil)) nil)) (cyclic_subgroup 0 (cyclic_subgroup-1 nil 3407147440 ("" (skosimp*) (("" (case "H!1 = one_group") (("1" (expand "cyclic?" 1) (("1" (inst + "one") (("1" (hide -2 -3) (("1" (replace -1) (("1" (hide -1) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "one_group") (("1" (expand "singleton") (("1" (expand "generated_by") (("1" (iff 1) (("1" (prop) (("1" (inst + "1") (("1" (grind) (("1" (rewrite "right_identity") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "one_expt") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "one_in") nil nil)) nil)) nil) ("2" (expand "cyclic?") (("2" (skosimp*) (("2" (case "(EXISTS (h:T),(m:posnat): H!1(h) AND h /= one AND h = a!1^m)") (("1" (skosimp*) (("1" (name s "min({n: posnat | H!1(a!1^n)})") (("1" (inst + "a!1^s") (("1" (apply-extensionality 3 :hide? t) (("1" (iff 1) (("1" (prop) (("1" (expand "subgroup?") (("1" (expand "subset?") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (replace -6 -5) (("1" (expand "generated_by") (("1" (skosimp*) (("1" (lemma "euclid_int") (("1" (inst - "s" "i!1") (("1" (skosimp*) (("1" (typepred "r!1") (("1" (case "a!1^r!1 = (a!1^i!1)*(a!1^s)^(-q!1)") (("1" (inst + "q!1") (("1" (case "r!1 = 0") (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (replace -4) (("1" (rewrite "expt_expt") (("1" (rewrite "expt_expt") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "min({n: posnat | H!1(a!1 ^ n)})") (("2" (inst -3 "r!1") (("1" (assert) (("1" (replace -7) (("1" (lemma "expt_member") (("1" (inst - "H!1" "a!1^s" "-q!1") (("1" (assert) (("1" (replace -4) (("1" (rewrite "star_closed") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -6 -7 -8 2 3 4) (("2" (case "a!1 ^ i!1 = a!1^(s * q!1 + r!1)") (("1" (hide -3 -4) (("1" (rewrite "expt_mult" - :dir rl) (("1" (rewrite "expt_expt" - :dir rl) (("1" (lemma "cancel_left") (("1" (inst - "a!1 ^ i!1" "(a!1 ^ s) ^ q!1 * a!1 ^ r!1" "(a!1 ^ s) ^ (-q!1)") (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (case-replace "(a!1 ^ s) ^ (-q!1) * ((a!1 ^ s) ^ q!1 * a!1 ^ r!1) = a!1^r!1") (("1" (hide -1) (("1" (lemma "cyclic_abelian") (("1" (inst - "G!1") (("1" (assert) (("1" (split -1) (("1" (expand "abelian_group?") (("1" (ground) (("1" (expand "commutative?") (("1" (assert) (("1" (expand "restrict") (("1" (assert) (("1" (inst - "(a!1 ^ s) ^ (-q!1)" "a!1 ^ i!1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (reveal -10) (("2" (replace -1 +) (("2" (assert) (("2" (inst + "i!1") nil nil)) nil)) nil)) nil)) nil) ("3" (reveal -10) (("3" (replace -1 +) (("3" (assert) (("3" (inst + "-s*q!1") (("3" (assert) (("3" (rewrite "expt_expt") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "cyclic?") (("2" (reveal -9) (("2" (expand "generated_by") (("2" (assert) (("2" (inst + "a!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "assoc") (("2" (rewrite "expt_neg") (("2" (rewrite "expt_inv_left") (("2" (assert) (("2" (rewrite "one_left") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "generated_by") (("2" (skosimp*) (("2" (typepred "min({n: posnat | H!1(a!1 ^ n)})") (("2" (replace -5) (("2" (lemma "expt_member") (("2" (assert) (("2" (inst - "H!1" "a!1^s" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "min({n: posnat | H!1(a!1 ^ n)})") (("2" (replace -4) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (assert) (("2" (inst - "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (apply-extensionality 2 :hide? t) (("2" (expand "one_group") (("2" (expand "singleton") (("2" (iff 1) (("2" (prop) (("1" (expand "subgroup?") (("1" (expand "subset?") (("1" (assert) (("1" (inst? -) (("1" (assert) (("1" (replace -3 -) (("1" (expand "generated_by") (("1" (skosimp*) (("1" (case "i!1 >= 0") (("1" (inst + "a!1^i!1" "i!1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "i!1 = 0") (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "inv(a!1)^i!1" "-i!1") (("1" (rewrite "expt_neg") (("1" (replace -2) (("1" (lemma "inv_in") (("1" (inst - "H!1" "a!1^i!1") (("1" (assert) (("1" (rewrite "inv_expt") (("1" (assert) (("1" (flatten) (("1" (lemma "cancel_left") (("1" (inst - "x!1" "a!1 ^ i!1" "one") (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (rewrite "one_left" -1) (("1" (replace -4 - :dir rl) (("1" (rewrite "expt_inv_left") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one_group const-decl "finite_group" group nil) (finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (one formal-const-decl "T" cyclic_group nil) (* formal-const-decl "[T, T -> T]" cyclic_group nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil cyclic_group nil) (H!1 skolem-const-decl "group[T, *, one]" cyclic_group nil) (generated_by const-decl "group" group nil) (singleton const-decl "(singleton?)" sets nil) (one_expt formula-decl nil group 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) (number nonempty-type-decl nil numbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (^ const-decl "T" group nil) (left_identity formula-decl nil monad nil) (power def-decl "T" monoid_def nil) (one_in formula-decl nil monad nil) (monad? const-decl "bool" monad_def nil) (monad nonempty-type-eq-decl nil monad nil) (cyclic? const-decl "boolean" group nil) (i!1 skolem-const-decl "int" cyclic_group nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (inv_in formula-decl nil group nil) (one_left formula-decl nil group nil) (inv_expt formula-decl nil group nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (empty? const-decl "bool" sets nil) (G!1 skolem-const-decl "group[T, *, one]" cyclic_group nil) (a!1 skolem-const-decl "(G!1)" cyclic_group nil) (s skolem-const-decl "{a | H!1(a!1 ^ a) AND (FORALL (x: posnat): H!1(a!1 ^ x) IMPLIES a <= x)}" cyclic_group nil) (subgroup? const-decl "bool" group_def nil) (member const-decl "bool" sets nil) (euclid_int formula-decl nil euclidean_division nil) (minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (expt_expt formula-decl nil group nil) (int_plus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (r!1 skolem-const-decl "mod(s)" cyclic_group nil) (star_closed formula-decl nil groupoid nil) (star_closed? const-decl "bool" groupoid_def nil) (groupoid nonempty-type-eq-decl nil groupoid nil) (expt_member formula-decl nil group nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt_mult formula-decl nil group nil) (cancel_left formula-decl nil group nil) (expt_neg formula-decl nil group nil) (expt_inv_left formula-decl nil group nil) (assoc formula-decl nil group nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (i!1 skolem-const-decl "int" cyclic_group nil) (q!1 skolem-const-decl "int" cyclic_group nil) (restrict const-decl "R" restrict nil) (commutative? const-decl "bool" operator_defs nil) (abelian_group? const-decl "bool" group_def nil) (cyclic_abelian formula-decl nil cyclic_group nil) (mod nonempty-type-eq-decl nil euclidean_division nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (>= const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil)) shostak)) (is_cyclic 0 (is_cyclic-1 nil 3407083622 ("" (skosimp*) (("" (expand "cyclic?") (("" (inst + "a!1") (("" (apply-extensionality 1 :hide? t) (("" (iff 1) (("" (inst?) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (ground) (("1" (expand "generated_by") (("1" (inst?) nil nil)) nil) ("2" (lemma "generated_is_subgroup") (("2" (inst?) (("2" (assert) (("2" (inst - "G!1") (("2" (assert) (("2" (expand "subgroup?") (("2" (expand "subset?") (("2" (inst - "a!1 ^ n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "generated_is_subgroup") (("2" (inst - "G!1" "a!1") (("2" (assert) (("2" (expand "subgroup?") (("2" (expand "subset?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cyclic? const-decl "boolean" group nil) (generated_by const-decl "group" group nil) (x!1 skolem-const-decl "T" cyclic_group nil) (G!1 skolem-const-decl "group[T, *, one]" cyclic_group nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (subgroup? const-decl "bool" group_def nil) (^ const-decl "T" group nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (generated_is_subgroup formula-decl nil cyclic_group nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (one formal-const-decl "T" cyclic_group nil) (* formal-const-decl "[T, T -> T]" cyclic_group nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil cyclic_group nil)) nil))) ¤ Dauer der Verarbeitung: 0.37 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.Bot Zugriff |
