|
(subterm
(subtermOF_TCC1 0
(subtermOF_TCC1-1 nil 3388757677
("" (skosimp*)
(("" (typepred "p!1")
(("" (expand "positionsOF")
(("" (assert)
(("" (expand "only_empty_seq")
(("" (rewrite "empty_0") nil nil)) nil))
nil))
nil))
nil))
nil)
nil nil))
(subtermOF_TCC2 0
(subtermOF_TCC2-1 nil 3388757677
("" (skosimp*)
(("" (typepred "p!1")
(("" (expand "positionsOF")
(("" (lift-if) (("" (grind) nil nil)) nil)) nil))
nil))
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)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" subterm 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 subterm nil)
(variable formal-nonempty-type-decl nil subterm nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(rest const-decl "finseq" seq_extras "structures/")
(^ const-decl "finseq" finite_sequences nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(first const-decl "T" seq_extras "structures/")
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(catenate const-decl "positions" positions nil)
(add_first const-decl "finseq" seq_extras "structures/")
(insert? const-decl "finseq" seq_extras "structures/")
(member const-decl "bool" sets nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(only_empty_seq const-decl "positions" positions nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(subtermOF_TCC3 0
(subtermOF_TCC3-1 nil 3388757677
("" (skosimp*)
(("" (typepred "p!1")
(("" (expand "positionsOF" -1)
(("" (lift-if)
(("" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "only_empty_seq")
(("2" (rewrite "empty_0") nil nil)) nil)
("3" (expand* "union" "member")
(("3" (prop)
(("1" (expand "only_empty_seq")
(("1" (rewrite "empty_0") nil nil)) nil)
("2" (expand "IUnion")
(("2" (skolem * "i1")
(("2" (expand "catenate")
(("2" (skolem * "y1")
(("2" (expand "member")
(("2" (flatten)
(("2" (replace -3 -1 rl)
(("2"
(typepred "i1")
(("2"
(lemma "fsepn.first_equal")
(("2"
(inst -1 "q!1" "y1" "i!1" "i1")
(("2"
(prop)
(("1" (assert) nil nil)
("2"
(lemma "fsepn.seq_first_rest")
(("2"
(inst -1 "p!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" subterm 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 subterm nil)
(variable formal-nonempty-type-decl nil subterm nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(catenate const-decl "positions" positions nil)
(first_equal formula-decl nil seq_extras "structures/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(<= const-decl "bool" reals nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(only_empty_seq const-decl "positions" positions nil)
(finseq type-eq-decl nil finite_sequences nil)
(empty_0 formula-decl nil seq_extras "structures/"))
nil))
(subtermOF_TCC4 0
(subtermOF_TCC4-1 nil 3388757677
("" (skosimp*)
(("" (replaces -3) (("" (rewrite "length_rest") 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)
(positions? type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions type-eq-decl nil positions nil)
(term type-decl nil term_adt nil)
(position type-eq-decl nil positions nil)
(arity formal-const-decl "[symbol -> nat]" subterm nil)
(symbol formal-nonempty-type-decl nil subterm nil)
(variable formal-nonempty-type-decl nil subterm 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)
(length_rest formula-decl nil seq_extras "structures/"))
nil))
(subtermOF_TCC5 0
(subtermOF_TCC5-1 nil 3388757677
("" (skosimp*)
(("" (typepred "p!1")
(("" (expand "positionsOF")
(("" (assert)
(("" (expand "only_empty_seq")
(("" (rewrite "empty_0") nil nil)) nil))
nil))
nil))
nil))
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)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil)
(term type-decl nil term_adt nil)
(arity formal-const-decl "[symbol -> nat]" subterm 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 subterm nil)
(variable formal-nonempty-type-decl nil subterm nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty_0 formula-decl nil seq_extras "structures/")
(finseq type-eq-decl nil finite_sequences nil)
(only_empty_seq const-decl "positions" positions nil))
nil))
(pos_vars_subset_pos 0
(pos_vars_subset_pos-1 nil 3411906619
("" (skosimp*)
(("" (skoletin* 1)
(("" (expand* subset? member)
(("" (skosimp*)
(("" (expand "Posv") (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(variable formal-nonempty-type-decl nil subterm nil)
(symbol formal-nonempty-type-decl nil subterm nil)
(arity formal-const-decl "[symbol -> nat]" subterm nil)
(position type-eq-decl nil positions nil)
(positions type-eq-decl nil positions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(Pos_var const-decl "positions" subterm nil)
(subset? const-decl "bool" sets nil)
(positionsOF def-decl "positions" positions nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(extend const-decl "R" extend nil)
(Posv skolem-const-decl "positions[variable, symbol, arity]"
subterm nil)
(member const-decl "bool" sets nil))
shostak))
(Pos_var_is_finite 0
(Pos_var_is_finite-1 nil 3414630433
("" (skosimp*)
(("" (skoletin* 1)
(("" (replaces -1)
(("" (lemma "pos_vars_subset_pos")
(("" (inst?)
(("" (assert)
(("" (lemma "positions_of_terms_finite")
(("" (inst?)
(("" (lemma "finite_sets[position].finite_subset")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(variable formal-nonempty-type-decl nil subterm nil)
(symbol formal-nonempty-type-decl nil subterm nil)
(arity formal-const-decl "[symbol -> nat]" subterm nil)
(position type-eq-decl nil positions nil)
(positions type-eq-decl nil positions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(term type-decl nil term_adt nil) (set type-eq-decl nil sets nil)
(V const-decl "set[term]" variables_term nil)
(Pos_var const-decl "positions" subterm nil)
(is_finite const-decl "bool" finite_sets nil)
(pos_vars_subset_pos formula-decl nil subterm nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(positionsOF def-decl "positions" positions nil)
(t!1 skolem-const-decl "term[variable, symbol, arity]" subterm nil)
(finite_set type-eq-decl nil finite_sets nil)
(finite_subset formula-decl nil finite_sets nil)
(positions_of_terms_finite formula-decl nil positions nil))
shostak))
(Vars_is_var 0
(Vars_is_var-1 nil 3402241169
("" (skeep)
(("" (decompose-equality)
(("" (expand "Vars")
(("" (expand "restrict")
(("" (iff)
(("" (prop)
(("1" (skosimp*)
(("1" (typepred "p!1")
(("1" (expand "positionsOF")
(("1" (expand* "only_empty_seq" "subtermOF")
(("1" (lift-if)
(("1" (rewrite "empty_0")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 1 "empty_seq")
(("1" (expand "subtermOF")
(("1" (rewrite "empty_0") (("1" (assert) nil nil))
nil))
nil)
("2" (expand "positionsOF")
(("2" (expand "only_empty_seq")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Vars const-decl "set[(V)]" subterm nil)
(= const-decl "[T, T -> boolean]" equalities 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]" subterm 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 subterm nil)
(variable formal-nonempty-type-decl nil subterm nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(t skolem-const-decl "term[variable, symbol, arity]" subterm nil)
(empty_0 formula-decl nil seq_extras "structures/")
(finseq type-eq-decl nil finite_sequences nil)
(only_empty_seq const-decl "positions" positions nil)
(subtermOF def-decl "term" subterm nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(position type-eq-decl nil positions nil)
(positions type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(positions? type-eq-decl nil positions nil))
shostak))
(vars_term_is_union 0
(vars_term_is_union-1 nil 3415054747
("" (skosimp*)
(("" (lift-if)
(("" (prop)
(("1" (decompose-equality 1)
(("1" (expand "restrict")
(("1" (lemma "Vars_is_var")
(("1" (inst?)
(("1" (assert)
(("1" (replaces -1)
(("1" (expand "singleton") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (decompose-equality 2)
(("2" (iff)
(("2" (prop)
(("1" (expand "finseq_appl")
(("1" (expand "IUnion")
(("1" (expand "Vars")
(("1" (skosimp*)
(("1" (expand "subtermOF" -1)
(("1" (lift-if)
(("1" (prop)
(("1" (typepred "x!1")
(("1"
(expand "V")
(("1" (assert) nil nil))
nil))
nil)
("2" (expand "finseq_appl")
(("2"
(inst 2 "first(p!1) - 1")
(("1" (inst 2 "rest(p!1)") nil nil)
("2"
(typepred "first[posnat](p!1)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "finseq_appl")
(("2" (expand "IUnion")
(("2" (skosimp*)
(("2" (expand "Vars")
(("2" (skosimp*)
(("2" (inst 1 "add_first(i!1 + 1, p!1)")
(("1" (expand "subtermOF" 1)
(("1" (lift-if)
(("1"
(prop)
(("1"
(hide (-2 1 2))
(("1" (grind) nil nil))
nil)
("2"
(expand "finseq_appl")
(("2"
(rewrite "rest_add_first")
(("2"
(rewrite "first_add")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (typepred "p!1")
(("2"
(expand "positionsOF" 1)
(("2"
(expand* "union" "member")
(("2"
(prop)
(("2"
(hide 1)
(("2"
(expand "IUnion")
(("2"
(expand "finseq_appl")
(("2"
(inst 1 "i!1 + 1")
(("2"
(expand "catenate")
(("2"
(expand "member")
(("2"
(inst 1 "p!1")
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)
((t1!1 skolem-const-decl "term[variable, symbol, arity]" subterm
nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt 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)
(IUnion const-decl "set[T]" indexed_sets nil)
(finseq type-eq-decl nil finite_sequences nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rest const-decl "finseq" seq_extras "structures/")
(p!1 skolem-const-decl "positions?[variable, symbol, arity](t1!1)"
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)
(first const-decl "T" seq_extras "structures/")
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(/= const-decl "boolean" notequal 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(subtermOF def-decl "term" subterm nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(p!1 skolem-const-decl
"positions?[variable, symbol, arity](args(t1!1)`seq(i!1))" subterm
nil)
(i!1 skolem-const-decl "below[length(args(t1!1))]" subterm nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(add_first const-decl "finseq" seq_extras "structures/")
(first_add formula-decl nil seq_extras "structures/")
(rest_add_first formula-decl nil seq_extras "structures/")
(insert? const-decl "finseq" seq_extras "structures/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(catenate const-decl "positions" positions nil)
(<= const-decl "bool" reals nil)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[term[variable, symbol, arity]]" subterm nil)
(finite_restrict application-judgement "finite_set[S]"
restrict_set_props nil)
(Vars const-decl "set[(V)]" subterm nil)
(vars? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil)
(v adt-accessor-decl "[(vars?) -> variable]" term_adt nil)
(restrict const-decl "R" restrict nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets 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]" subterm 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 subterm nil)
(variable formal-nonempty-type-decl nil subterm nil)
(Vars_is_var formula-decl nil subterm nil))
shostak))
(vars_of_term_finite 0
(vars_of_term_finite-1 nil 3415056088
("" (induct "t")
(("1" (skosimp*)
(("1" (lemma "vars_term_is_union")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (skosimp*)
(("2" (case "length(app2_var!1) = 0")
(("1" (hide -2)
(("1"
(case-replace
"Vars(app(app1_var!1, app2_var!1)) = emptyset" :hide? T)
(("1" (rewrite "finite_emptyset") nil nil)
("2" (hide 2)
(("2" (decompose-equality 1)
(("2" (iff)
(("2" (prop)
(("1" (expand "Vars")
(("1" (skosimp*)
(("1" (typepred "p!1")
(("1" (expand "positionsOF")
(("1" (expand "only_empty_seq")
(("1"
(replaces -1)
(("1"
(expand "subtermOF")
(("1"
(rewrite "empty_0")
(("1"
(typepred "x!1")
(("1"
(expand "V")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "vars_term_is_union")
(("2" (inst?)
(("2" (assert)
(("2" (replaces -1 2)
(("2" (expand "finseq_appl")
(("2"
(lemma
"IUnion_extra[(V)].IUnion_of_finite_is_finite1")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(< const-decl "bool" reals nil)
(IUnion_of_finite_is_finite1 formula-decl nil IUnion_extra nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(only_empty_seq const-decl "positions" positions nil)
(subtermOF def-decl "term" subterm nil)
(empty_0 formula-decl nil seq_extras "structures/")
(finseq type-eq-decl nil finite_sequences nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(finite_emptyset judgement-tcc nil finite_sets nil)
(emptyset const-decl "set" sets 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)
(finite_emptyset name-judgement "finite_set" finite_sets 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)
(vars adt-constructor-decl "[variable -> (vars?)]" term_adt nil)
(vars? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(finite_restrict application-judgement "finite_set[S]"
restrict_set_props nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[term[variable, symbol, arity]]" subterm nil)
(vars_term_is_union formula-decl nil subterm nil)
(term_induction formula-decl nil term_adt nil)
(variable formal-nonempty-type-decl nil subterm nil)
(symbol formal-nonempty-type-decl nil subterm 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)
(arity formal-const-decl "[symbol -> nat]" subterm nil)
(Vars const-decl "set[(V)]" subterm nil)
(is_finite const-decl "bool" finite_sets nil)
(V const-decl "set[term]" variables_term nil)
(set type-eq-decl nil sets nil) (term type-decl nil term_adt nil))
shostak))
(pos_subterm_ax_TCC1 0
(pos_subterm_ax_TCC1-1 nil 3388757677
("" (skosimp*)
(("" (lemma "closed_positions")
(("" (inst -1 "p!1" "p!1 o q!1" "t!1")
(("" (assert)
(("" (expand "<=") (("" (inst 1 "q!1") nil nil)) nil)) nil))
nil))
nil))
nil)
((arity formal-const-decl "[symbol -> nat]" subterm 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 subterm nil)
(variable formal-nonempty-type-decl nil subterm nil)
(closed_positions formula-decl nil positions nil)
(<= const-decl "bool" positions nil)
(term type-decl nil term_adt nil)
(O const-decl "finseq" finite_sequences nil)
(finseq type-eq-decl nil finite_sequences nil)
(position type-eq-decl nil positions nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil))
nil))
(pos_subterm_ax 0
(pos_subterm_ax-1 nil 3388757678
("" (measure-induct+ "length(p)" "p")
(("1" (skeep)
(("1" (expand "subtermOF" 1)
(("1" (prop)
(("1" (hide -2)
(("1" (rewrite "empty_0")
(("1" (replaces -1)
(("1" (rewrite "empty_o_seq") nil nil)) nil))
nil))
nil)
("2" (inst -1 "rest(x!1)" "q" "args(t)(first(x!1) - 1)")
(("1" (rewrite "length_rest")
(("1" (prop)
(("1" (hide 3)
(("1" (expand "positionsOF" -1)
(("1" (lift-if)
(("1" (prop)
(("1" (expand "only_empty_seq")
(("1" (lemma "fsepn.seq_empty")
(("1" (inst -1 "x!1" "q")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "only_empty_seq")
(("2" (lemma "fsepn.seq_empty")
(("2" (inst -1 "x!1" "q")
(("2" (assert) nil nil)) nil))
nil))
nil)
("3" (expand* "union" "member")
(("3" (prop)
(("1" (expand "only_empty_seq")
(("1"
(lemma "fsepn.seq_empty")
(("1"
(inst -1 "x!1" "q")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "IUnion")
(("2"
(skolem * "i1")
(("2"
(expand "catenate")
(("2"
(skolem * "y1")
(("2"
(expand "member")
(("2"
(flatten)
(("2"
(lemma
"fsepn.seq_first_rest")
(("2"
(inst -1 "x!1")
(("2"
(assert)
(("2"
(replaces -1 -3)
(("2"
(lemma
"fsepn.add_first_compo")
(("2"
(inst
-1
"rest(x!1)"
"q"
"first(x!1)")
(("2"
(replaces -1 -3)
(("2"
(lemma
"fsepn.first_equal")
(("2"
(inst
-1
"rest(x!1) o q"
"y1"
"first(x!1)"
"i1")
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
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))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (hide (-2 -3 2))
(("2" (lemma "pos_ax")
(("2" (inst -1 "y!1" "q!1" "t!1") (("2" (assert) nil nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "pos_ax")
(("3" (inst -1 "p!1" "q!1" "t!1") (("3" (assert) nil nil))
nil))
nil))
nil))
nil)
((pos_ax formula-decl nil positions nil)
(empty_0 formula-decl nil seq_extras "structures/")
(empty_o_seq formula-decl nil seq_extras "structures/")
(length_rest formula-decl nil seq_extras "structures/")
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(catenate const-decl "positions" positions nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(add_first_compo formula-decl nil seq_extras "structures/")
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(<= const-decl "bool" reals nil)
(first_equal formula-decl nil seq_extras "structures/")
(only_empty_seq const-decl "positions" positions nil)
(seq_empty formula-decl nil seq_extras "structures/")
(rest const-decl "finseq" seq_extras "structures/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(first const-decl "T" seq_extras "structures/")
(x!1 skolem-const-decl "position[variable, symbol, arity]" subterm
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)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subtermOF def-decl "term" subterm nil)
(positions? type-eq-decl nil positions nil)
(term type-decl nil term_adt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(positions type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
(finseq type-eq-decl nil finite_sequences nil)
(O const-decl "finseq" finite_sequences nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(naturalnumber type-eq-decl nil naturalnumbers nil)
(position type-eq-decl nil positions nil)
(arity formal-const-decl "[symbol -> nat]" subterm nil)
(symbol formal-nonempty-type-decl nil subterm nil)
(variable formal-nonempty-type-decl nil 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 "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)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(pos_subterm_TCC1 0
(pos_subterm_TCC1-1 nil 3388757677
("" (skosimp*)
(("" (lemma "pos_subterm_ax")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((pos_subterm_ax formula-decl nil subterm nil)
(term type-decl nil term_adt nil)
(position type-eq-decl nil positions nil)
(arity formal-const-decl "[symbol -> nat]" subterm nil)
(symbol formal-nonempty-type-decl nil subterm nil)
(variable formal-nonempty-type-decl nil 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 "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)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(pos_subterm 0
(pos_subterm-1 nil 3388769744
("" (measure-induct+ "length(p)" ("p"))
(("1" (skeep)
(("1" (lemma "fsepn.seq_first_rest")
(("1" (inst -1 "x!1")
(("1" (case "x!1`length /= 0")
(("1" (assert)
(("1" (name-replace "subtemp" "subtermOF(t, x!1)")
(("1" (replace -2 1)
(("1" (rewrite "add_first_compo")
(("1" (expand "subtermOF" 1 1)
(("1" (lift-if)
(("1" (prop)
(("1" (lemma "fsepn.empty_0")
(("1"
(inst -1
"add_first(first(x!1), rest(x!1) o q)")
(("1"
(assert)
(("1"
(hide-all-but (-1 -3 2))
(("1"
(lemma "fsepn.add_first_compo")
(("1"
(inst
-1
"rest(x!1)"
"q"
"first(x!1)")
(("1"
(replace -1 -2 rl)
(("1"
(hide -1)
(("1"
(replace -2 -1 rl)
(("1"
(hide -2)
(("1"
(lemma
"fsepn.seq_empty")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"first(add_first(first(x!1), rest(x!1) o q)) = first(x!1)"
:hide? t)
(("1" (rewrite "fsepn.rest_add_first")
(("1"
(expand "subtemp")
(("1"
(inst
-2
"rest(x!1)"
"q"
"args(t)(first(x!1) - 1)")
(("1"
(rewrite "length_rest")
(("1"
(prop)
(("1"
(replaces -1)
(("1"
(case-replace
"subtermOF(t, x!1) = subtermOF(args(t)(first(x!1) - 1), rest(x!1))")
(("1"
(hide-all-but 1)
(("1"
(expand "subtermOF" 1 1)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide (2 3))
(("2"
(expand "positionsOF" -2)
(("2"
(lift-if)
(("2"
(prop)
(("1"
(expand
"only_empty_seq")
(("1"
(hide (-1 -3 1))
(("1"
(lemma
"fsepn.seq_empty")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide (-1 -3 1 2))
(("2"
(expand
"only_empty_seq")
(("2"
(lemma
"fsepn.seq_empty")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(expand*
"union"
"member")
(("3"
(prop)
(("1"
(hide (-2 1 2 3))
(("1"
(expand
"only_empty_seq")
(("1"
(lemma
"fsepn.seq_empty")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand "IUnion")
(("2"
(skolem * "i1")
(("2"
(expand
"catenate")
(("2"
(skolem
*
"y1")
(("2"
(expand
"member")
(("2"
(flatten)
(("2"
(replace
-3
-2)
(("2"
(rewrite
"fsepn.add_first_compo")
(("2"
(hide
(-3
1
2))
(("2"
(lemma
"fsepn.first_equal")
(("2"
(inst
-1
"rest(x!1) o q"
"y1"
"first(x!1)"
"i1")
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
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)
("2" (hide-all-but (1 4))
(("2" (rewrite "first_add") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (prop)
(("1" (hide-all-but (-2 1))
(("1" (expand "subtermOF" 1 3)
(("1" (lift-if)
(("1" (prop)
(("1" (hide -2)
(("1" (rewrite "empty_0")
(("1" (replaces -1)
(("1" (rewrite "empty_o_seq") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (expand "subtermOF" 1 3)
(("2" (lift-if)
(("2" (prop)
(("2" (hide -2)
(("2" (rewrite "empty_0")
(("2" (replaces -1)
(("2" (rewrite "empty_o_seq") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (lemma "pos_subterm_ax")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (hide-all-but (-1 1))
(("3" (lemma "pos_ax")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil)
("4" (hide 2)
(("4" (lemma "pos_subterm_ax")
(("4" (inst?) (("4" (assert) nil nil)) nil)) nil))
nil)
("5" (hide 2)
(("5" (lemma "pos_ax")
(("5" (inst?) (("5" (assert) nil nil)) nil)) nil))
nil))
nil)
((pos_ax formula-decl nil positions nil)
(pos_subterm_ax formula-decl nil subterm nil)
(empty_o_seq formula-decl nil seq_extras "structures/")
(add_first const-decl "finseq" seq_extras "structures/")
(seq_empty formula-decl nil seq_extras "structures/")
(empty_0 formula-decl nil seq_extras "structures/")
(first_add formula-decl nil seq_extras "structures/")
(rest_add_first formula-decl nil seq_extras "structures/")
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(app? adt-recognizer-decl "[term -> boolean]" term_adt nil)
(finite_sequence type-eq-decl nil finite_sequences 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(only_empty_seq const-decl "positions" positions nil)
(first_equal formula-decl nil seq_extras "structures/")
(<= const-decl "bool" reals nil)
(upto? nonempty-type-eq-decl nil IUnion_extra nil)
(catenate const-decl "positions" positions nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(length_rest formula-decl nil seq_extras "structures/")
(subtemp skolem-const-decl "term[variable, symbol, arity]" subterm
nil)
(add_first_compo formula-decl nil seq_extras "structures/")
(rest const-decl "finseq" seq_extras "structures/")
(not_empty_seq type-eq-decl nil seq_extras "structures/")
(first const-decl "T" seq_extras "structures/")
(/= const-decl "boolean" notequal nil)
(seq_first_rest formula-decl nil seq_extras "structures/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(positions? type-eq-decl nil positions nil)
(subtermOF def-decl "term" subterm nil)
(term type-decl nil term_adt nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(positions type-eq-decl nil positions nil)
(positionsOF def-decl "positions" positions nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.82 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.
|
