(sort_seq_lemsnil 3254568023"" (skosimp*)"" (rewrite "sort_length" ) (("" (assert ) nil nil )) nil )) nil )nil sort_seq nil )nil naturalnumbers nil )nil nat_types nil )nil sort_seq nil )nil finite_sequences nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil ) (ne_seqs type-eq-decl nil seqs nil )nil sort_seq_lems nil )nil booleans nil )nil booleans nil )nil defined_types nil )"bool" orders nil )"(total_order?[T])" sort_seq_lems nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3254568023"" (skosimp*)"" (typepred "sort(s!1)" )"" (typepred "min(s!1)" )"" (expand "increasing?" )"" (skosimp*)"" (expand "permutation?" )"" (assert )"" (rewrite "sort_length" )"" (assert )"" (skosimp*)"" (expand "bijective?" )"" (flatten)"" (expand "surjective?" )"" (inst -4 "0" )"1" "1" "x!1" )"1" replace -4)"1" "1" "x!1" )"1" "1" "jj!1" )"1" "0" "f!1(jj!1)" )"1" replace -1 * rl)"1" assert )"1" "1" replace -2)"1" replace -4)"1" "1" "sort_seq_lems.<=" )"1" expand "total_order?" )"1" expand "partial_order?" )"1" "1" expand "antisymmetric?" )"1" "1" assert )"1" "f!1(jj!1)" )"1" rewrite "sort_length" )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" rewrite "sort_length" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}" nil )"bool" sort_seq nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sort_seq nil )nil seqs nil ) (> const-decl "bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" permutations_seq nil )"(total_order?[T])" sort_seq_lems nil )"bool" orders nil )nil defined_types nil )nil finite_sequences nil )nil sort_seq_lems nil )nil nat_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"bool" relations nil )"bool" orders nil )"bool" functions nil )"bool" functions nil )nil sort_seq nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil min_seq nil )"[T, T -> boolean]" equalities nil )min const-decl "{t: T | AND " min_seq nil)) nil ))nil 3254568023"" (skosimp*)"" (assert ) (("" (rewrite "sort_length" ) (("" (assert ) nil ))))))nil )"(total_order?[real])" nil )"int" integers nil )nil sort_seq nil )nil sort_seq_lems nil )nil booleans nil )nil booleans nil )nil defined_types nil )"bool" orders nil )"(total_order?[T])" sort_seq_lems nil ))nil ))nil 3254568023"" (skosimp*)"" (typepred "sort(s!1)" )"" (typepred "max(s!1)" )"" (expand "increasing?" )"" (skosimp*)"" (expand "permutation?" )"" (rewrite "sort_length" )"" (assert )"" (skosimp*)"" (inst-cp -4 "jj!1" )"" (expand "bijective?" )"" (flatten)"" (expand "surjective?" )"" (inst -4 "length(sort(s!1))-1" )"1" "1" "x!1" )"1" replace -4)"1" "1" "x!1" )"1" replace -4)"1" "1" "f!1(jj!1)" "length(sort(s!1))-1" )"1" assert )"1" replace -2)"1" "1" replace -3 * rl)"1" "1" "sort_seq_lems.<=" )"1" expand "total_order?" )"1" expand "partial_order?" )"1" "1" expand "antisymmetric?" )"1" "1" assert )"1" rewrite "sort_length" )"1" "f!1(jj!1)" )"1" rewrite "sort_length" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "sort_length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sort_length" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sort_length" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}" nil )"bool" sort_seq nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil sort_seq nil )nil seqs nil ) (> const-decl "bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" permutations_seq nil )"(total_order?[T])" sort_seq_lems nil )"bool" orders nil )nil defined_types nil )nil finite_sequences nil )nil sort_seq_lems nil )nil nat_types nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" orders nil )"bool" relations nil )"bool" functions nil )"bool" functions nil )nil sort_seq nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil max_seq nil )"[T, T -> boolean]" equalities nil )max const-decl "{t: T | AND " max_seq nil)) nil )))quality 100%
¤ 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.0.15Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
