(sqrt_derivativenil 3262649437"" (expand "deriv_domain?" )"" (skosimp*) (("" (inst + "e!1/2" ) (("" (grind) nil nil )) nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{y: posreal | y >= x}" nil )"(strict_total_order?[real])" real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(total_order?[real])" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"bool" deriv_domain_def nil )"real" reals nil ))nil 3262649447"" (expand "not_one_element?" )"" (skolem!) (("" (inst + "x!1+1" ) (("" (assert ) nil nil )) nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 )"posreal" nil )"bool" deriv_domain_def nil ))nil 3262648257"" "inverse_derivable_fun" "F" "LAMBDA (x:posreal):sq(x)" "G" "LAMBDA (x:posreal):sqrt(x)" "f" "LAMBDA (x:posreal): 2*x" ))"1" (split -1)"1" (expand "restrict" ) (("1" (propax) nil nil )) nil )"2" (hide 2)"2" (expand "sq" )"2" (lemma "identity_derivable_fun[posreal]" )"2" (expand "I" )"2" "prod_derivable_fun" "f1" "LAMBDA (x: posreal): x" "f2" "LAMBDA (x: posreal): x" ))"2" (expand "*" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (expand "bijective?" )"3" (split)"1" (expand "injective?" )"1" (skosimp*) (("1" (rewrite "sq_eq" ) nil nil )) nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (inst + "sqrt(y!1)" )"2" (rewrite "sq_sqrt" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (expand "sq" )"4" (lemma "deriv_id_fun[posreal]" )"4" "deriv_prod_fun" "ff1" "LAMBDA (x: posreal): x" "ff2" "LAMBDA (x: posreal): x" ))"1" (expand "*" )"1" (expand "+" )"1" (replace -2 -1)"1" (simplify -1) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "identity_derivable_fun[posreal]" )"2" (expand "I" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"5" (hide 2)"5" (expand "inverse?" )"5" (skosimp*) (("5" (rewrite "sq_sqrt" ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"3" (expand "connected?" )"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil )nil derivatives nil )nil derivatives nil )nil sqrt "reals/" )nil sq "reals/" )nil derivatives nil )"bool" derivatives nil )nil derivatives nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )"posreal" sq "reals/" )"posreal" sqrt "reals/" )"nonneg_real" sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" ))nil 3262649471"" (lemma "sqrt_derivable_fun" ) (("" (propax) nil nil )) nil )nil sqrt_derivative nil ))nil 3262649090"" (lemma "sqrt_derivable_fun" )"" "deriv_inverse_fun[posreal,posreal]" "F" "LAMBDA (x:posreal): sq(x)" "G" "LAMBDA (x:posreal): sqrt(x)" "f" "LAMBDA (x:posreal):2*x" ))"1" (split -1)"1" (simplify -1)"1" (expand "restrict" ) (("1" (propax) nil nil )) nil )) nil )"2" (hide-all-but 1)"2" (expand "sq" )"2" (lemma "identity_derivable_fun[posreal]" )"2" (expand "I" )"2" "prod_derivable_fun" "f1" "LAMBDA (x: posreal): x" "f2" "LAMBDA (x: posreal): x" ))"2" (expand "*" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (lemma "identity_derivable_fun[posreal]" )"3" "prod_derivable_fun" "f1" "LAMBDA (x: posreal): x" "f2" "LAMBDA (x: posreal): x" ))"3" "deriv_prod_fun" "ff1" "LAMBDA (x: posreal): x" "ff2" "LAMBDA (x: posreal): x" ))"1" (lemma "deriv_id_fun[posreal]" )"1" (expand "I" )"1" (replace -1)"1" (expand "*" )"1" (expand "+" )"1" (expand "sq" 1)"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "I" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (expand "bijective?" )"4" (expand "injective?" )"4" (expand "surjective?" )"4" (split)"1" (skosimp*) (("1" (rewrite "sq_eq" ) nil nil ))nil )"2" (skosimp*)"2" (inst + "sqrt(y!1)" )"2" (rewrite "sq_sqrt" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide-all-but 1)"5" (expand "inverse?" )"5" (skosimp*) (("5" (rewrite "sq_sqrt" ) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "not_one_element?" )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (expand "connected?" )"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"nonneg_real" sq "reals/" )"posreal" sqrt "reals/" )"posreal" sq "reals/" )"bool" deriv_domain_def nil )"bool" deriv_domain_def nil )nil sq "reals/" )nil sqrt "reals/" )nil derivatives nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives nil )"bool" derivatives nil )nil derivatives nil )nil derivatives nil )nil derivatives nil ))nil 3297787282"" (lemma "sqrt_derivable_fun" )"" (lemma "deriv_sqrt_fun" ) (("" (assert ) nil nil )) nil )) nil )"posreal" sqrt "reals/" )) shostak))nil 3297787309"" (rewrite "derivable_cont_fun[posreal]" )"" (hide 2) (("" (rewrite "sqrt_derivable_fun" ) nil nil )) nil ))nil )nil sqrt_derivative nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"R" restrict nil )nil derivatives nil ))quality 100%
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
