(sort_array_lemsnil 3506271670 ("" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3506271670"" (skosimp*)"" (typepred "sort(A!1)" )"" (typepred "min(A!1)" )"" (skosimp*)"" (expand "permutation_of?" )"" (skosimp*)"" (expand "bijective?" )"" (flatten)"" (expand "surjective?" )"" (inst -4 "0" )"" (skosimp*)"" (inst -5 "x!1" )"" (replace -4)"" (hide -4)"" "x!1" )"" "" "jj!1" )"" expand "sorted?" )"" "0" "f!1(jj!1)" )"" replace -1 * rl)"" assert )"" "" replace -2)"" replace -4)"" "" "sort_array_lems.<=" )"" expand "total_order?" )"" expand "partial_order?" )"" "" expand "antisymmetric?" )"" "" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )"{a | permutation_of?(A, a) AND sorted?(a)}" nil )"bool" sort_array nil )"(total_order?[T])" sort_array_lems nil )"bool" orders nil )nil defined_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil below_arrays nil )"bool" permutations nil )nil sort_array_lems nil )nil naturalnumbers nil )"posnat" sort_array_lems nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil nat_types nil )"bool" orders nil )"bool" relations nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"bool" functions nil )min const-decl"{t: T | (FORALL ii: t <= A(ii)) AND (EXISTS jj: A(jj) = t)}" nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3506271670 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3506271670"" (skosimp*)"" (typepred "sort(A!1)" )"" (typepred "max(A!1)" )"" (expand "sorted?" )"" (skosimp*)"" (expand "permutation_of?" )"" (skosimp*)"" (inst-cp -4 "jj!1" )"" (expand "bijective?" )"" (flatten)"" (expand "surjective?" )"" (inst -4 "N-1" )"" (skosimp*)"" (inst -5 "x!1" )"" replace -4)"" "" "x!1" )"" replace -4)"" "" "f!1(jj!1)" "N-1" )"" assert )"" replace -2)"" "" replace -3 * rl)"" "" "sort_array_lems.<=" )"" expand "total_order?" )"" expand "partial_order?" )"" "" expand "antisymmetric?" )"" "" assert )nil ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))nil )"{a | permutation_of?(A, a) AND sorted?(a)}" nil )"bool" sort_array nil )"(total_order?[T])" sort_array_lems nil )"bool" orders nil )nil defined_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil below_arrays nil )"bool" permutations nil )nil sort_array_lems nil )nil naturalnumbers nil )"posnat" sort_array_lems nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil nat_types nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" orders nil )"bool" relations nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"bool" functions nil )max const-decl"{t: T | (FORALL ii: A(ii) <= t) AND (EXISTS jj: A(jj) = t)}" nil )"[T, T -> boolean]" equalities nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
