| products/Sources/formale Sprachen/Delphi/Agenda 1.1/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: soccerSL.launch Sprache: XMLOriginal von: PVS© |
|
||||||
|
(csequence_limit
(prefix_chain_TCC1 0 (prefix_chain_TCC1-1 nil 3513785036 ("" (expand "ascending_chain?") (("" (skosimp*) (("" (use "prefix?_order") (("" (assert) nil nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (csequence type-decl nil csequence_codt 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (T formal-type-decl nil csequence_limit nil) (prefix?_order formula-decl nil csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil)) nil)) (suffix_chain_TCC1 0 (suffix_chain_TCC1-1 nil 3513785036 ("" (induct "n") (("1" (skolem-typepred) (("1" (expand* "suffix" "ascending_chain?") nil nil)) nil) ("2" (skosimp* t) (("2" (expand "ascending_chain?") (("2" (skolem!) (("2" (expand "suffix" +) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (expand "prefix?" +) (("1" (propax) nil nil)) nil) ("2" (expand "prefix?" +) (("2" (propax) nil nil)) nil) ("3" (inst - "n!1") (("3" (expand "prefix?" -2) (("3" (propax) nil nil)) nil)) nil) ("4" (inst -3 "LAMBDA n: IF empty?(chain!1(n)) THEN empty_cseq ELSE rest(chain!1(n)) ENDIF") (("1" (inst -3 "n!1") (("1" (assert) nil nil)) nil) ("2" (hide -2 2 3 4) (("2" (expand "ascending_chain?") (("2" (skolem!) (("2" (lift-if) (("2" (lift-if) (("2" (lift-if) (("2" (ground) (("1" (expand "prefix?" +) (("1" (propax) nil nil)) nil) ("2" (expand "prefix?" +) (("2" (propax) nil nil)) nil) ("3" (inst - "n!2") (("3" (expand "prefix?" -) (("3" (propax) nil nil)) nil)) nil) ("4" (inst - "n!2") (("4" (expand "prefix?" -) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (chain!1 skolem-const-decl "ascending_chain[csequence[T], prefix?[T]]" csequence_limit nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (empty_cseq adt-constructor-decl "(empty?)" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (suffix? inductive-decl "bool" csequence_suffix nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit nil) (pred type-eq-decl nil defined_types 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) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil)) nil)) (rest_chain_TCC1 0 (rest_chain_TCC1-1 nil 3513785036 ("" (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) (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) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (rest_chain_TCC2 0 (rest_chain_TCC2-1 nil 3513785036 ("" (skolem!) (("" (typepred "suffix_chain(chain!1, 1)") (("" (expand* "suffix_chain" "suffix" "suffix" "ascending_chain?") (("" (skolem!) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) ((suffix_chain const-decl "ascending_chain" csequence_limit nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil)) nil)) (ascending_chain?_nth 0 (ascending_chain?_nth-1 nil 3513785384 ("" (skosimp) (("" (lemma "ascending_chain?_def") (("" (inst - "chain!1" "n!1" "m!1") (("" (assert) (("" (forward-chain "prefix?_index") (("" (use "prefix?_nth") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((prefix? coinductive-decl "bool" csequence_prefix nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit nil) (ascending_chain?_def formula-decl nil ascending_chains nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (prefix?_nth formula-decl nil csequence_prefix nil) (index? def-decl "bool" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (prefix?_index formula-decl nil csequence_prefix nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains 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)) shostak)) (limit_struct_TCC1 0 (limit_struct_TCC1-1 nil 3513785036 ("" (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) (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) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil)) nil)) (limit_struct_TCC2 0 (limit_struct_TCC2-1 nil 3513785036 ("" (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) (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) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (limit_empty 0 (limit_empty-1 nil 3513785427 ("" (expand* "limit" "limit_struct" "coreduce") (("" (reduce) nil 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) (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) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (limit const-decl "csequence" csequence_limit nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (limit_struct const-decl "csequence_struct[T, ascending_chain]" csequence_limit nil)) shostak)) (limit_nonempty 0 (limit_nonempty-1 nil 3513785452 ("" (skolem!) (("" (use "limit_empty") (("" (reduce) nil nil)) nil)) nil) ((limit_empty formula-decl nil csequence_limit nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit 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) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (limit_first_TCC1 0 (limit_first_TCC1-1 nil 3513785036 ("" (skosimp) (("" (rewrite "limit_nonempty") (("" (inst + "n!1") nil nil)) nil)) nil) ((limit_nonempty formula-decl nil csequence_limit 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil)) nil)) (limit_first 0 (limit_first-1 nil 3513785517 ("" (skosimp) (("" (expand* "limit" "limit_struct" "coreduce") (("" (reduce) (("" (typepred "min({n | nonempty?(chain!1(n))})") (("1" (inst - "n!1") (("1" (assert) (("1" (lemma "ascending_chain?_nth") (("1" (inst - "chain!1" "min({n | nonempty?(chain!1(n))})" "n!1" 0) (("1" (assert) (("1" (expand* "index?" "nth") (("1" (assert) nil nil)) nil)) nil) ("2" (expand* "nonempty?" "empty?" "member") (("2" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "nonempty?" "empty?" "member") (("2" (inst - "n!1") nil nil)) nil)) nil)) nil)) nil)) nil) ((limit_struct const-decl "csequence_struct[T, ascending_chain]" csequence_limit nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (limit const-decl "csequence" csequence_limit 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit nil) (chain!1 skolem-const-decl "ascending_chain[csequence, prefix?]" csequence_limit nil) (nth def-decl "T" csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (ascending_chain?_nth formula-decl nil csequence_limit nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (limit_rest_chain 0 (limit_rest_chain-1 nil 3513785594 ("" (skosimp) (("" (expand* "limit" "limit_struct") (("" (expand "coreduce" -) (("" (expand "coreduce" 1 1) (("" (reduce) nil nil)) nil)) nil)) nil)) nil) ((limit_struct const-decl "csequence_struct[T, ascending_chain]" csequence_limit nil) (limit const-decl "csequence" csequence_limit nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil)) shostak)) (limit_suffix_chain 0 (limit_suffix_chain-1 nil 3513785625 ("" (induct "n") (("1" (skolem!) (("1" (expand* "suffix_chain" "suffix") (("1" (replace-eta "chain!1") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "suffix_chain") (("2" (expand "suffix" +) (("2" (lift-if) (("2" (ground) (("1" (expand "limit" +) (("1" (expand* "limit_struct" "coreduce") (("1" (smash) (("1" (skolem!) (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skolem!) (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skolem!) (("3" (inst - "n!1") (("3" (assert) (("3" (hide -3 2) (("3" (expand* "limit" "limit_struct" "coreduce") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide -2 -3 2 3) (("4" (expand* "limit" "limit_struct" "coreduce") (("4" (lift-if) (("4" (ground) nil nil)) nil)) nil)) nil) ("5" (hide -2 2 3 4) (("5" (expand* "limit" "limit_struct" "coreduce") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "rest_chain(chain!1)") (("2" (use "limit_rest_chain") (("2" (assert) (("2" (replace -1 :dir rl) (("2" (case-replace "(LAMBDA m: suffix(rest_chain(chain!1)(m), j!1)) = (LAMBDA m: IF empty?(chain!1( (("1" (hide -1 -2 3) (("1" (decompose-equality) (("1" (lift-if) (("1" (ground) (("1" (expand* "rest_chain" "suffix") (("1" (assert) nil nil)) nil) ("2" (expand "rest_chain") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "rest_chain") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil) ("4" (skosimp) (("4" (expand* "rest_chain" "suffix?") (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (limit_struct const-decl "csequence_struct[T, ascending_chain]" csequence_limit nil) (limit_rest_chain formula-decl nil csequence_limit nil) (suffix?_is_preorder name-judgement "(preorder?[csequence])" csequence_limit nil) (j!1 skolem-const-decl "nat" csequence_limit nil) (chain!1 skolem-const-decl "ascending_chain[csequence, prefix?]" csequence_limit nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (rest_chain const-decl "ascending_chain" csequence_limit nil) (nat_induction formula-decl nil naturalnumbers nil) (suffix_chain const-decl "ascending_chain" csequence_limit nil) (limit const-decl "csequence" csequence_limit nil) (suffix def-decl "(LAMBDA (cseq1): suffix?(cseq1, cseq))" csequence_suffix nil) (suffix? inductive-decl "bool" csequence_suffix nil) (= const-decl "[T, T -> boolean]" equalities nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit nil) (pred type-eq-decl nil defined_types 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)) shostak)) (limit_lub 0 (limit_lub-1 nil 3513785904 ("" (skolem!) (("" (expand "least_upperbound?") (("" (split) (("1" (expand "upperbound?") (("1" (skolem!) (("1" (rewrite "prefix?_prefix") (("1" (flatten) (("1" (lemma "coinduction") (("1" (inst - "LAMBDA (cseq1, cseq2: csequence): EXISTS chain, n: cseq1 = chain(n) AND cseq2 = "chain!1(n!1)" "limit(chain!1)") (("1" (assert) (("1" (inst + "chain!1" "n!1") nil nil)) nil) ("2" (delete 2 3) (("2" (expand "bisimulation?") (("2" (skosimp*) (("2" (replace*) (("2" (hide -1 -2) (("2" (smash) (("1" (inst + 0) (("1" (expand "prefix") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "limit_empty") (("2" (inst - "n!2") (("2" (assert) nil nil)) nil)) nil) ("3" (inst + "rest_chain(chain!2)" "n!2") (("3" (rewrite "limit_rest_chain") (("1" (expand "rest_chain" 2 1) (("1" (skolem!) (("1" (use "limit_rest_chain") (("1" (split) (("1" (replace -1 :dir rl) (("1" (hide -1) (("1" (inst + "1 + m!1") (("1" (expand "prefix" +) (("1" (lift-if) (("1" (prop) (("1" (rewrite "limit_empty") (("1" (inst - "n!2") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "rest_chain" -) (("2" (decompose-equality) (("2" (forward-chain "limit_first") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "limit_nonempty") (("2" (inst + "n!2") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "limit_nonempty") (("2" (inst + "n!2") nil nil)) nil)) nil)) nil) ("4" (forward-chain "limit_first") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "prefix?_coinduction") (("2" (inst - "LAMBDA (cseq1, cseq2: csequence): EXISTS chain: cseq1 = limit(chain) AND upperb (("2" (split) (("1" (skosimp) (("1" (inst - "limit(chain!1)" "u!1") (("1" (assert) (("1" (inst + "chain!1") nil nil)) nil)) nil)) nil) ("2" (delete 2) (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "limit_empty") (("2" (skolem!) (("2" (ground) (("1" (expand* "upperbound?" "prefix?") (("1" (inst - "n!1") nil nil)) nil) ("2" (expand* "limit" "limit_struct" "coreduce") (("2" (reduce) (("2" (expand* "upperbound?" "prefix?") (("2" (inst - "min({n | nonempty?(chain!2(n))})") (("1" (assert) nil nil) ("2" (expand* "nonempty?" "empty?" "member") (("2" (inst - "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst + "rest_chain(chain!2)") (("3" (rewrite "limit_rest_chain") (("1" (expand "upperbound?") (("1" (skolem!) (("1" (inst - "n!2") (("1" (expand "prefix?" -) (("1" (expand "rest_chain" 2) (("1" (lift-if) (("1" (expand "prefix?" 2 1) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "limit_nonempty") (("2" (inst + "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_upperbound? const-decl "bool" ascending_chains nil) (prefix?_coinduction formula-decl nil csequence_prefix nil) (limit_struct const-decl "csequence_struct[T, ascending_chain]" csequence_limit nil) (coreduce adt-def-decl "{c: csequence[T] | inj_empty?(op(x)) AND empty?(c) OR inj_nonempty?(op(x)) AND nonempty?(c)}" csequence_codt_coreduce nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" min_nat nil) (chain!2 skolem-const-decl "ascending_chain[csequence, prefix?]" csequence_limit nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (upperbound? const-decl "bool" ascending_chains nil) (prefix?_prefix formula-decl nil csequence_prefix nil) (csequence type-decl nil csequence_codt 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (limit const-decl "csequence" csequence_limit nil) (T formal-type-decl nil csequence_limit nil) (coinduction formula-decl nil csequence_codt nil) (rest_chain const-decl "ascending_chain" csequence_limit nil) (limit_nonempty formula-decl nil csequence_limit nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (limit_first formula-decl nil csequence_limit nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (csequence_add_extensionality formula-decl nil csequence_codt nil) (add adt-constructor-decl "[[T, csequence] -> (nonempty?)]" csequence_codt nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (rest adt-accessor-decl "[(nonempty?) -> csequence]" csequence_codt nil) (limit_rest_chain formula-decl nil csequence_limit nil) (limit_empty formula-decl nil csequence_limit nil) (PRED type-eq-decl nil defined_types nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (is_finite inductive-decl "bool" csequence_props nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix nil)) shostak)) (limit_nth 0 (limit_nth-1 nil 3513786305 ("" (skosimp) (("" (use "limit_lub") (("" (expand "least_upperbound?") (("" (flatten) (("" (expand "upperbound?" -1) (("" (inst - "n!1") (("" (forward-chain "prefix?_index") (("" (use "prefix?_nth") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((limit_lub formula-decl nil csequence_limit nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit 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) (prefix?_nth formula-decl nil csequence_prefix nil) (indexes type-eq-decl nil csequence_nth nil) (m!1 skolem-const-decl "nat" csequence_limit nil) (n!1 skolem-const-decl "nat" csequence_limit nil) (chain!1 skolem-const-decl "ascending_chain[csequence, prefix?]" csequence_limit nil) (index? def-decl "bool" csequence_nth nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (prefix?_index formula-decl nil csequence_prefix nil) (limit const-decl "csequence" csequence_limit nil) (upperbound? const-decl "bool" ascending_chains nil) (least_upperbound? const-decl "bool" ascending_chains nil)) shostak)) (limit_def 0 (limit_def-1 nil 3513786368 ("" (skolem!) (("" (prop) (("1" (skolem!) (("1" (use "limit_lub") (("1" (replace -2) (("1" (expand "least_upperbound?") (("1" (prop) (("1" (use "limit_suffix_chain") (("1" (lemma "limit_empty" ("chain" "suffix_chain(chain!1, n!1)")) (("1" (prop) (("1" (inst - "n!1") (("1" (expand "suffix_chain" -2) (("1" (replace -3 -1 :dir rl) (("1" (rewrite "suffix_empty" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst + "n!2") (("2" (expand "suffix_chain" 1) (("2" (rewrite "suffix_empty") (("2" (assert) (("2" (forward-chain "limit_nth") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (forward-chain "limit_nth") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (forward-chain "limit_nth") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "coinduction") (("2" (inst - "LAMBDA (cseq1, cseq2: csequence): EXISTS chain: cseq1 = limit(chain) AND (FORAL "limit(chain!1)" "cseq!1") (("1" (assert) (("1" (inst + "chain!1") nil nil)) nil) ("2" (delete -1 2) (("2" (expand "bisimulation?") (("2" (skosimp*) (("2" (replace -1) (("2" (hide -1) (("2" (case "empty?(y!1)") (("1" (reduce) (("1" (rewrite "limit_empty") (("1" (skolem!) (("1" (inst - "first(chain!2(n!1))" 0) (("1" (expand* "index?" "nth") (("1" (inst + "n!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (smash) (("1" (rewrite "limit_empty") (("1" (inst - "first(y!1)" 0) (("1" (expand* "index?" "nth") (("1" (skosimp) (("1" (inst - "m!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "rest_chain(chain!2)") (("2" (rewrite "limit_rest_chain") (("1" (skolem!) (("1" (prop) (("1" (inst - "nth(y!1, n!1 + 1)" "n!1 + 1") (("1" (expand "index?" -4) (("1" (assert) (("1" (skosimp) (("1" (inst + "m!1") (("1" (expand "rest_chain") (("1" (expand "nth" -6) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "index?" 1) (("2" (propax) nil nil)) nil)) nil) ("2" (skosimp) (("2" (expand "rest_chain") (("2" (lift-if) (("2" (ground) (("1" (expand "index?" -4) (("1" (propax) nil nil)) nil) ("2" (inst - "t!1" "n!1 + 1") (("2" (expand "index?" -4) (("2" (expand "nth" +) (("2" (inst + "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (expand "rest_chain") (("3" (lift-if) (("3" (ground) (("1" (expand "index?" -4) (("1" (propax) nil nil)) nil) ("2" (inst - "t!1" "n!1 + 1") (("2" (expand "index?" -4) (("2" (expand "nth" -4) (("2" (inst + "m!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "limit_nonempty") (("2" (inst - "first(y!1)" 0) (("2" (expand "index?" -) (("2" (expand "nth" -) (("2" (skosimp) (("2" (inst + "m!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "first(y!1)" 0) (("3" (expand "index?" -) (("3" (expand "nth" -) (("3" (skosimp) (("3" (forward-chain "limit_first") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((limit_lub formula-decl nil csequence_limit nil) (ascending_chain type-eq-decl nil ascending_chains nil) (ascending_chain? const-decl "bool" ascending_chains nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (csequence type-decl nil csequence_codt nil) (T formal-type-decl nil csequence_limit 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) (least_upperbound? const-decl "bool" ascending_chains nil) (limit_suffix_chain formula-decl nil csequence_limit nil) (limit const-decl "csequence" csequence_limit nil) (suffix_empty formula-decl nil csequence_suffix nil) (limit_nth formula-decl nil csequence_limit nil) (suffix_chain const-decl "ascending_chain" csequence_limit nil) (limit_empty formula-decl nil csequence_limit nil) (nth def-decl "T" csequence_nth nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bisimulation? adt-def-decl "boolean" csequence_codt nil) (PRED type-eq-decl nil defined_types nil) (empty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (nonempty? adt-recognizer-decl "[csequence -> boolean]" csequence_codt nil) (chain!2 skolem-const-decl "ascending_chain[csequence, prefix?]" csequence_limit nil) (n!1 skolem-const-decl "nat" csequence_limit nil) (first adt-accessor-decl "[(nonempty?) -> T]" csequence_codt nil) (limit_first formula-decl nil csequence_limit nil) (rest_chain const-decl "ascending_chain" csequence_limit nil) (limit_nonempty formula-decl nil csequence_limit nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (y!1 skolem-const-decl "csequence[T]" csequence_limit nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (n!1 skolem-const-decl "nat" csequence_limit nil) (limit_rest_chain formula-decl nil csequence_limit nil) (coinduction formula-decl nil csequence_codt nil)) shostak)) (limit_prefix_chain 0 (limit_prefix_chain-1 nil 3513786783 ("" (skolem!) (("" (rewrite "limit_def") (("" (expand "prefix_chain") (("" (skolem!) (("" (prop) (("1" (inst + "n!1 + 1") (("1" (rewrite "prefix_index") (("1" (assert) (("1" (lemma "prefix?_nth") (("1" (inst - "prefix(cseq!1, 1 + n!1)" "cseq!1" "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (rewrite "prefix_index") (("2" (flatten) nil nil)) nil)) nil) ("3" (skosimp) (("3" (rewrite "prefix_index") (("3" (flatten) (("3" (lemma "prefix?_nth") (("3" (inst - "prefix(cseq!1, m!1)" "cseq!1" "n!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((limit_def formula-decl nil csequence_limit 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (prefix_chain const-decl "ascending_chain" csequence_limit nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (indexes type-eq-decl nil csequence_nth nil) (index? def-decl "bool" csequence_nth nil) (prefix def-decl "{fseq | prefix?(fseq, cseq)}" csequence_prefix nil) (finite_csequence nonempty-type-eq-decl nil csequence_props nil) (is_finite inductive-decl "bool" csequence_props nil) (prefix?_is_partial_order name-judgement "(partial_order?[csequence])" csequence_limit nil) (prefix?_nth formula-decl nil csequence_prefix nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (prefix_index formula-decl nil csequence_prefix nil)) shostak)) (limit_prefix_compact_TCC1 0 (limit_prefix_compact_TCC1-1 nil 3513785036 ("" (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) (T formal-type-decl nil csequence_limit nil) (csequence type-decl nil csequence_codt nil) (prefix? coinductive-decl "bool" csequence_prefix nil) (ascending_chain? const-decl "bool" ascending_chains nil) (ascending_chain type-eq-decl nil ascending_chains nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (limit_prefix_compact 0 (limit_prefix_compact-1 nil 3513786874 ("" (induct "n") (("1" (skosimp) (("1" (inst + 0) (("1" (expand* "prefix" "prefix?") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (expand "prefix" +) (("2" (expand "prefix?" +) (("2" (assert) (("2" (inst - "rest(cseq!1)" "rest_chain(chain!1)") (("1" (expand "rest_chain") (("1" (expand "index?" -2) (("1" (case "j!1 = 0") (("1" (smash) (("1" (skolem!) (("1" (lift-if) (("1" (ground) (("1" (expand* "prefix" "prefix" "prefix?" "prefix?") (("1" (flatten) (("1" (hide -2) (("1" (rewrite "limit_nonempty") (("1" (skolem!) (("1" (inst + "n!1") (("1" (assert) (("1" (forward-chain "limit_first") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.132 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 |
