| products/sources/formale Sprachen/Coq/dev/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: update-require Sprache: SML
|
(unification
(IMP_substitution_TCC1 0 (IMP_substitution_TCC1-1 nil 3463226130 ("" (lemma "var_countable") (("" (propax) nil nil)) nil) ((var_countable formula-decl nil unification nil)) nil)) (mg_po 0 (mg_po-1 nil 3455279452 ("" (expand "preorder?") (("" (split) (("1" (expand "reflexive?") (("1" (skeep) (("1" (expand "<=") (("1" (inst 1 "identity") (("1" (decompose-equality) (("1" (expand "comp") (("1" (rewrite "ext_iden") nil nil)) nil)) nil) ("2" (rewrite "iden_subs") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (skeep) (("2" (expand "<=") (("2" (skosimp*) (("2" (inst 1 "comp(tau!2,tau!1)") (("1" (replaces -1) (("1" (replaces -1) (("1" (rewrite "o_ass") nil nil)) nil)) nil) ("2" (rewrite "subs_o") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((identity const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (Sub type-eq-decl nil substitution nil) (ext_iden formula-decl nil substitution nil) (comp const-decl "term" substitution nil) (iden_subs formula-decl nil substitution nil) (<= const-decl "bool" unification nil) (reflexive? const-decl "bool" relations nil) (subs_o formula-decl nil substitution nil) (o_ass formula-decl nil substitution nil) (tau!2 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (tau!1 skolem-const-decl "Sub[variable, symbol, arity]" unification nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil)) shostak)) (uni_diff_equal_length_arg 0 (uni_diff_equal_length_arg-1 nil 3448191147 ("" (skosimp*) (("" (typepred t!1) (("" (expand unifiable) (("" (skeep -1) (("" (expand unifier) (("" (replace -2 -1) (("" (replace -3 -1) (("" (expand ext) (("" (lift-if) (("" (assert) (("" (decompose-equality -1) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (ext def-decl "term" substitution nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (< const-decl "bool" reals nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (unifier const-decl "bool" unification nil)) shostak)) (resolving_diff_TCC1 0 (resolving_diff_TCC1-1 nil 3447690997 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "s!1" "k!1") (("1" (typepred "k!1") (("1" (lemma "uni_diff_equal_length_arg") (("1" (inst -1 "s!1" "t!1" "f!1" "st!1") (("1" (assert) (("1" (inst -1 "fp!1" "stp!1") (("1" (assert) (("1" (flatten) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (resolving_diff_TCC2 0 (resolving_diff_TCC2-1 nil 3447690997 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "t!1" "k!1") (("1" (typepred "k!1") (("1" (replace -3 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (resolving_diff_TCC3 0 (resolving_diff_TCC3-1 nil 3447690997 ("" (skosimp*) (("" (assert) (("" (typepred "t!1") (("" (expand "unifiable" -1) (("" (skeep -1) (("" (replace -2 -1) (("" (replace -3 -1) (("" (expand "unifier" -1) (("" (decompose-equality -1) (("" (assert) (("" (prop) (("1" (hide-all-but (-1 -2 -4 -5)) (("1" (expand "ext") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "ext" -3) (("2" (replace -3 (-2 -4 -6) rl) (("2" (expand "ext" -4) (("2" (flatten) (("2" (decompose-equality -5) (("2" (inst -1 "k!1") (("1" (expand "unifiable") (("1" (inst 3 "sigma") (("1" (grind) nil nil)) nil)) nil) ("2" (expand "unifiable") (("2" (inst 4 "sigma") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (unifier const-decl "bool" unification nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (finseq type-eq-decl nil finite_sequences nil) (< const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (int_minus_int_is_int application-judgement "int" integers 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 "finite_sequence[T]" set2seq "structures/") (first const-decl "T" seq_extras "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (subtermOF def-decl "term" subterm nil) (st!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(f!1)}" unification nil) (f!1 skolem-const-decl "symbol" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (fp!1 skolem-const-decl "symbol" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (v adt-accessor-decl "[(vars?) -> variable]" term_adt nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (ext def-decl "term" substitution nil) (Sub type-eq-decl nil substitution nil) (Sub? const-decl "bool" substitution nil) (V const-decl "set[term]" variables_term nil) (set type-eq-decl nil sets nil) (vars? adt-recognizer-decl "[term -> boolean]" term_adt nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification 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) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil)) nil)) (resolving_diff_TCC4 0 (resolving_diff_TCC4-1 nil 3449937385 ("" (skosimp*) (("" (expand "<<") (("" (lift-if) (("" (prop) (("1" (hide-all-but (-1 -2)) (("1" (assert) nil nil)) nil) ("2" (inst 2 k!1) (("1" (assert) (("1" (grind) nil nil)) nil) ("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f!1" "st!1") (("2" (assert) (("2" (inst -1 "fp!1" "stp!1") (("2" (assert) (("2" (flatten) (("2" (replace -3 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<< adt-def-decl "(strict_well_founded?[term])" term_adt nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (unifiable const-decl "bool" unification nil) (/= const-decl "boolean" notequal nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (real_gt_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) (subterm adt-def-decl "boolean" term_adt nil) (subtermOF def-decl "term" subterm nil) (rest const-decl "finseq" seq_extras "structures/") (^ const-decl "finseq" finite_sequences nil) (empty_seq const-decl "finseq" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers 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) (bool nonempty-type-eq-decl nil booleans 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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (variable formal-nonempty-type-decl nil unification nil) (symbol formal-nonempty-type-decl nil unification nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (term type-decl nil term_adt nil) (finite_sequence type-eq-decl nil finite_sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (k!1 skolem-const-decl "below[length(stp!1)]" unification nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (resolving_diff_TCC5 0 (resolving_diff_TCC5-1 nil 3449937623 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "s!1" "kk!1") (("1" (typepred "kk!1") (("1" (lemma "uni_diff_equal_length_arg") (("1" (inst -1 "s!1" "t!1" "f!1" "st!1") (("1" (assert) (("1" (inst -1 "fp!1" "stp!1") (("1" (assert) (("1" (flatten) (("1" (replace -4 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (kk!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (resolving_diff_TCC6 0 (resolving_diff_TCC6-1 nil 3516387398 ("" (skosimp*) (("" (lemma "positions_of_arg") (("" (inst -1 "t!1" "kk!1") (("1" (typepred "kk!1") (("1" (replace -3 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (positions_of_arg formula-decl nil positions nil) (NOT const-decl "[bool -> bool]" booleans nil) (fp!1 skolem-const-decl "symbol" unification nil) (stp!1 skolem-const-decl "{args: finite_sequence[term[variable, symbol, arity]] | args`length = arity(fp!1)}" unification nil) (kk!1 skolem-const-decl "below[length(stp!1)]" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (term type-decl nil term_adt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (resolving_diff_TCC7 0 (resolving_diff_TCC7-1 nil 3516387398 ("" (skosimp*) (("" (lemma "uni_diff_equal_length_arg") (("" (inst -1 "s!1" "t!1" "f!1" "st!1") (("" (assert) (("" (inst -1 "fp!1" "stp!1") (("" (assert) (("" (flatten) (("" (replace -1 -4 rl) (("" (hide -1) (("" (typepred t!1) (("" (hide -1) (("" (case "st!1 = stp!1") (("1" (hide +) (("1" (grind) nil nil)) nil) ("2" (decompose-equality 1) (("2" (decompose-equality 1) (("2" (typepred x!1) (("2" (expand* "nonempty?" "empty?") (("2" (inst -6 "x!1") (("2" (expand "member") (("2" (replace -5 -6) (("2" (replace -4 -6) (("2" (assert) (("2" (expand subtermOF) (("2" (lift-if) (("2" (assert) (("2" (grind) 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)) nil) ((uni_diff_equal_length_arg formula-decl nil unification nil) (NOT const-decl "[bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (< const-decl "bool" reals nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subtermOF def-decl "term" subterm 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 "finite_sequence[T]" set2seq "structures/") (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (first const-decl "T" seq_extras "structures/") (empty_seq const-decl "finseq" finite_sequences nil) (^ const-decl "finseq" finite_sequences nil) (rest const-decl "finseq" seq_extras "structures/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_min application-judgement "{k: nat | k <= i AND k <= j}" real_defs nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs 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) (= const-decl "[T, T -> boolean]" equalities nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification 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) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil)) nil)) (resol_diff_nonempty_implies_funct_terms 0 (resol_diff_nonempty_implies_funct_terms-1 nil 3450707436 ("" (skeep) (("" (expand "resolving_diff") (("" (lift-if) (("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (resol_diff_to_rest_resol_diff_TCC1 0 (resol_diff_to_rest_resol_diff_TCC1-1 nil 3451131001 ("" (skeep) (("" (lemma "empty_0[posnat]") (("" (inst -1 "rd") (("" (assert) nil nil)) nil)) nil)) 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) (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) (empty_0 formula-decl nil seq_extras "structures/") (position type-eq-decl nil positions nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (resol_diff_to_rest_resol_diff_TCC2 0 (resol_diff_to_rest_resol_diff_TCC2-1 nil 3451131001 ("" (skosimp) (("" (expand "resolving_diff" -1) (("" (lift-if) (("" (prop) (("" (assert) (("" (replace -1 5) (("" (rewrite "first_add") (("1" (hide -1 4) (("1" (lemma "resolving_diff_TCC1") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (hide 5 2 3 4 5) (("1" (lemma "resolving_diff_TCC7") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4 5) (("2" (skosimp*) (("2" (lemma "positions_of_arg") (("2" (inst -1 "t!1" "kk!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2 3 4 5) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 5 6) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 5 6) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "t!1" "kk!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide -1 5 6) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (assert) (("1" (hide-all-but (1 4)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (resolving_diff_TCC1 subtype-tcc nil unification 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) (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) (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) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (first_add formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (resol_diff_to_rest_resol_diff_TCC3 0 (resol_diff_to_rest_resol_diff_TCC3-1 nil 3451131001 ("" (skosimp) (("" (expand "resolving_diff") (("" (lift-if) (("" (prop) (("" (assert) (("" (replace -1 5) (("" (rewrite "first_add") (("1" (hide -1 4) (("1" (lemma "resolving_diff_TCC2") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (hide 2 3 4 5) (("1" (lemma "resolving_diff_TCC7") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (assert) (("1" (inst -1 "f(t!1)" "args(t!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 3 4 5) (("2" (skosimp*) (("2" (lemma "positions_of_arg") (("2" (inst -1 "t!1" "kk!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2 3 4 5) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (inst -1 "f(t!1)" "args(t!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 4)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 5 6) (("2" (lemma "resolving_diff_TCC7") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app( f(t!1), args(t!1))") (("1" (assert) nil nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -1 5 6) (("3" (skosimp*) (("3" (lemma "positions_of_arg") (("3" (inst -1 "t!1" "kk!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide -1 5 6) (("4" (skosimp*) (("4" (lemma "positions_of_arg") (("4" (inst -1 "s!1" "kk!1") (("1" (assert) nil nil) ("2" (typepred "kk!1") (("2" (lemma "uni_diff_equal_length_arg") (("2" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("2" (assert) (("2" (case "s!1 = app( f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (assert) (("1" (hide-all-but (1 5)) (("1" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 6)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((resolving_diff def-decl "position" unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (app adt-constructor-decl "[[f: symbol, {args: finite_sequence[term] | args`length = arity(f)}] -> (app?)]" term_adt nil) (term_app_extensionality formula-decl nil term_adt nil) (uni_diff_equal_length_arg formula-decl nil unification nil) (kk!1 skolem-const-decl "below[length(args[variable, symbol, arity](t!1))]" unification nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (positions_of_arg formula-decl nil positions nil) (resolving_diff_TCC7 subtype-tcc nil unification nil) (t!1 skolem-const-decl "{t: term | unifiable(s!1, t) & s!1 /= t}" unification nil) (s!1 skolem-const-decl "term[variable, symbol, arity]" unification nil) (resolving_diff_TCC2 subtype-tcc nil unification 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) (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) (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) (set type-eq-decl nil sets nil) (args adt-accessor-decl "[d: (app?) -> {args: finite_sequence[term] | args`length = arity(f(d))}]" term_adt nil) (f adt-accessor-decl "[(app?) -> symbol]" term_adt nil) (= const-decl "[T, T -> boolean]" equalities nil) (app? adt-recognizer-decl "[term -> boolean]" term_adt nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (|#| const-decl "finite_sequence[T]" set2seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (subtermOF def-decl "term" subterm nil) (positions? type-eq-decl nil positions nil) (positionsOF def-decl "positions" positions nil) (positions type-eq-decl nil positions nil) (position type-eq-decl nil positions nil) (/= const-decl "boolean" notequal nil) (unifiable const-decl "bool" unification nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (term type-decl nil term_adt nil) (arity formal-const-decl "[symbol -> nat]" unification nil) (symbol formal-nonempty-type-decl nil unification nil) (variable formal-nonempty-type-decl nil unification nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (first_add formula-decl nil seq_extras "structures/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil)) (resol_diff_to_rest_resol_diff_TCC4 0 (resol_diff_to_rest_resol_diff_TCC4-1 nil 3451131001 ("" (skosimp) (("" (expand "resolving_diff") (("" (lift-if) (("" (hide 2) (("" (prop) (("" (reveal 1) (("" (assert) (("" (hide 5) (("" (name-replace "k1" "min({kk: below[length(args(t!1))] | NOT subtermOF(s!1, #(1 + kk)) = subtermOF(t!1, #(1 + kk))})") (("1" (name-replace "k" "1+k1") (("1" (replace -1 1) (("1" (hide -1) (("1" (rewrite "first_add[posnat]") (("1" (lemma "resolving_diff_TCC3") (("1" (inst -1 "s!1" "t!1" "f(s!1)" "args(s!1)") (("1" (case "s!1 = app(f(s!1), args(s!1))") (("1" (assert) (("1" (inst -2 "f(t!1)" "args(t!1)") (("1" (case "t!1 = app(f(t!1), args(t!1))") (("1" (assert) (("1" (inst -3 "k - 1") (("1" (reveal -6) (("1" (reveal -5) (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -6) (("2" (reveal -5) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 3)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 5)) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) --> -------------------- --> maximum size reached --> -------------------- [ Verzeichnis aufwärts0.116unsichere Verbindung Übersetzung europäischer Sprachen durch Browser ] |