(reals_complete_morenil 3506273121"" (skosimp*)"" (lemma "real_complete" )"" (inst -1 "S!1" )"1" (assert )"1" (split -1)"1" (skosimp*)"1" (inst 1 "y!2" )"1" (hide -2)"1" (expand "extend" )"1" (expand "least_upper_bound" )"1" (expand "least_upper_bound?" )"1" (prop)"1" (hide -2)"1" (expand "upper_bound" )"1" expand "upper_bound?" )"1" "1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (skosimp*)"2" "y!3" )"2" assert )"2" "2" expand "upper_bound" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" assert )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst 1 "y!1" )"2" (hide 2)"2" (expand "upper_bound?" )"2" (expand "upper_bound" )"2" (skosimp*)"2" (inst?)"2" (typepred "s!1" )"2" (expand "extend" )"2" (assert ) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "S!1" )"2" (hide -2 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )nil bounded_real_defs nil )"(total_order?[real])" nil )"(extend[real, T, bool, FALSE](S!1))" nil )"(nonempty?[T])" reals_complete_more nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" bound_defs nil )"bool" bound_defs nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" bounded_real_defs nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bounded_real_defs nil )"R" extend nil )"bool" booleans nil )nil reals_complete_more nil )"[real -> boolean]" reals_complete_more nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(nonempty?[T])" nil ))nil ))nil 3506273121"" (skosimp*)"" (lemma "real_lower_complete" )"" (inst -1 "S!1" )"1" (split -1)"1" (skosimp*)"1" (inst 1 "x!1" )"1" (hide -2)"1" (expand "greatest_lower_bound" )"1" (expand "greatest_lower_bound?" )"1" (prop)"1" (hide -2)"1" (expand "lower_bound" )"1" (expand "lower_bound?" )"1" (skosimp*)"1" "1" expand "extend" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (skosimp*)"2" (inst -2 "y!2" )"2" (assert )"2" "2" expand "lower_bound" )"2" expand "lower_bound?" )"2" "2" "2" "s!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (inst?)"2" (expand "lower_bound?" )"2" (expand "lower_bound" )"2" (skosimp*)"2" (inst?)"2" (typepred "s!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "S!1" )"2" (hide -2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil bounded_real_defs nil )"bool" bound_defs nil )"bool" bound_defs nil )"{x: T | S!1(x)}" reals_complete_more nil )"(nonempty?[T])" reals_complete_more nil )"bool" bounded_real_defs nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"(extend[real, T, bool, FALSE](S!1))" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" bounded_real_defs nil )"(extend[real, T, bool, FALSE](S!1))" nil )"R" extend nil )"bool" booleans nil )nil reals_complete_more nil )"[real -> boolean]" reals_complete_more nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(nonempty?[T])" nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
