(reduce_walksnil 3254571090 ("" (subtype-tcc) nil nil ) nil nil ))nil 3254571090 ("" (subtype-tcc) nil nil ) nil nil ))nil 3254571090 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3254571090 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3254571090 ("" (grind) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3254571372"" (skosimp*)"" (expand "finseq_appl" )"" (typepred "w!1" )"" (expand "walk?" )"" (expand "finseq_appl" )"" (flatten)"" (split +)"1" (hide -3)"1" (expand "verts_in?" )"1" (skosimp*)"1" (ground)"1" (inst?) nil nil ) ("2" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lift-if)"2" (typepred "k!1" )"2" (lift-if)"2" (ground)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (case-replace "k!1=n!1+1" )"1" (assert )"1" replace -10)"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (inst?) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[below[length(fs)] -> T]" finite_sequencesnil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" walks nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )nil reduce_walks nil )nil finite_sequences nil )nil walks nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" walks nil )nil walks nil )nil reduce_walks nil ))nil 3254571090 ("" (subtype-tcc) nil nil ) nil nil ))nil 3254571090 ("" (subtype-tcc) nil nil ) nil nil ))nil 3254571090 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3559559064 ("" (subtype-tcc) nil nil )"[below[length(fs)] -> T]" finite_sequencesnil ))nil ))nil 3254571090"" (skosimp*)"" (expand "o " )"" (expand * "^" min empty_seq)"" (auto-rewrite "finseq_appl" )"" (typepred "k!1" )"" (apply-extensionality 1 :hide? t)"1" (expand "reduce" )"1" (lift-if)"1" (lift-if) (("1" (ground) nil nil )) nil )) nil ))nil )"2" (apply-extensionality 1 :hide? t)"1" (typepred "x!1" )"1" (lift-if) (("1" (grind) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand * "^" min empty_seq)"2" (expand "reduce" )"2" (lift-if)"2" (assert ) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (typepred "n!1" )"3" (expand * "^" min empty_seq)"3" (lift-if) (("3" (ground) nil nil )) nil ))nil ))nil ))nil )"4" (skosimp*)"4" (assert )"4" (typepred "n!1" )"4" (expand * "^" min empty_seq)"4" (lift-if) (("4" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"5" (skosimp*)"5" (typepred "n!1" )"5" (expand * "^" min empty_seq)"5" (lift-if) (("5" (ground) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (expand * "^" min empty_seq) nil nil )) nil )"4" (skosimp*)"4" (typepred "n!1" )"4" (expand * "^" min empty_seq)"4" (lift-if) (("4" (ground) nil nil )) nil ))nil ))nil ))nil )"5" (skosimp*)"5" (typepred "n!1" )"5" (expand * "^" min empty_seq)"5" (lift-if) (("5" (ground) nil nil )) nil ))nil ))nil ))nil )"6" (skosimp*)"6" (typepred "n!1" )"6" (expand * "^" min empty_seq)"6" (lift-if) (("6" (ground) nil nil )) nil ))nil ))nil ))nil )"7" (lift-if) (("7" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"finseq" finite_sequences nil )nil reduce_walks nil )"Walk(G)" reduce_walks nil )nil defined_types nil )"T" epsilons nil )"[bool, bool -> bool]" booleans nil )"bool" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{n: nat | n > 0 AND n < length(w!1) - 1}" nil )"Walk[T](G!1)" reduce_walks nil )"graph[T]" reduce_walks nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"nonneg_int" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(strict_total_order?[real])" real_props nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil nat_types nil )nil reduce_walks nil )nil finite_sequences nil )nil walks nil )set type-eq-decl nil sets nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )nil finite_sets nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )"bool" walks nil )nil walks nil )"finseq" finite_sequences nil )"{k: nat | k <= i AND k <= j}" nil )"int" integers nil )"posint" nil )"finseq" finite_sequences nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
