(min_array_defnil 3249306196"" (expand ">=" )"" (typepred "min_array_def.<=" )"" (expand "total_order?" )"" (flatten)"" (expand "partial_order?" )"" (expand "preorder?" )"" (prop)"1" (expand "reflexive?" ) (("1" (propax) nil )))"2" (hide -1 -3 -4)"2" (expand "transitive?" )"2" (skosimp*)"2" (inst -3 "z!1" "y!1" "x!1" )"2" (assert ) nil )))))))))"3" (hide -1 -2 -4)"3" (expand "antisymmetric?" )"3" (skosimp*)"3" (inst?) (("3" (assert ) nil )))))))))"4" (expand "dichotomous?" )"4" (skosimp*)"4" (inst?)"4" (assert ) nil ))))))))))))))))))))nil )"(total_order?[T])" min_array_def nil )"bool" orders nil )nil defined_types nil )nil min_array_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" orders nil )"bool" orders nil )"bool" relations nil )"bool" relations nil )"bool" relations nil )"bool" orders nil )"bool" min_array_def nil ))nil ))nil 3249306276"" (rewrite "ge_total" ) nil nil )nil min_array_def nil )) shostak))nil 3249306196 ("" (subtype-tcc) nil nil ) nil nil ))nil 3249306196"" (inst 1 "(LAMBDA A,ii,(jj: abv(ii)): Imax(A,ii,jj))" )"1" (skosimp*)"1" (typepred "Imax(A!1, ii!1, jj!1)" )"1" (inst -3 "j!1" )"1" (assert ) (("1" (expand ">=" ) (("1" (propax) nil )))))))"2" (rewrite "ge_total" ) nil )))))"2" (skosimp*) (("2" (rewrite "ge_total" ) nil ))))nil )nil min_array_def nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(j) <= A(i))}" nil )nil max_array_def nil )"bool" min_array_def nil )"(total_order?[T])" min_array_def nil )"bool" orders nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil integers nil )nil min_array_def nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil min_array_def nil )nil naturalnumbers nil )"nat" min_array_def nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans 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 booleans nil )nil numbers nil ))nil ))nil 3249306196 ("" (subtype-tcc) nil nil ) nil nil ))nil 3249306196"" (skosimp*)"" (typepred "Imin(A!1, ii!1, ii!1)" )"" (inst?) (("1" (assert ) nil ) ("2" (assert ) nil ))))))nil )"{i: subrange(ii, jj) | (FORALL j: ii <= j AND j <= jj IMPLIES A(i) <= A(j))}" nil )"(total_order?[T])" min_array_def nil )"bool" orders nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil integers nil )nil min_array_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil min_array_def nil )nil naturalnumbers nil )"nat" min_array_def nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals 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 )"(total_order?[real])" nil )"[below(N) -> T]" min_array_def nil )"below(N)" min_array_def nil )"(strict_total_order?[real])" real_props nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
