SSL real_continuity.prf
Interaktion und
(real_continuitynil 3429890484"" (expand "metric?" )"" (expand "metric_zero?" )"" (expand "metric_symmetric?" )"" (expand "metric_triangle?" ) (("" (grind) nil nil )) nil ))nil ))nil ))nil )"real" reals nil )"bool" metric_def nil )"bool" metric_def nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"(strict_total_order?[real])" real_props 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 )"bool" metric_def nil )"bool" metric_def nil ))nil ))nil 3429893655"" (skosimp)"" (typepred "g2!1" )"" (typepred "g1!1" )"" (expand "metric_continuous?" )"" (skosimp)"" (inst - "x!1" )"" (inst - "x!1" )"" (expand "metric_continuous_at?" )"" (skosimp)"" (inst - "epsilon!1/2" )"" (inst - "epsilon!1/2" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" (skosimp)"" "x!2" )"" "x!2" )"" expand "member" )"" expand "ball" )"" expand "+" )"" assert )"" "triangle" "x" "g1!1(x!1) - g1!1(x!2)" "y" "g2!1(x!1) - g2!1(x!2)" ))"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil real_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" metric_continuity nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil real_types nil )"bool" reals nil )"real" reals nil )"set[T]" metric_space_def nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" nil )nil real_props nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"bool" sets nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{z: posreal | z <= x AND z <= y}" real_defs nil ))nil ))nil 3429893655"" (skosimp)"" (typepred "g!1" )"" (expand "metric_continuous?" )"" (skosimp)"" (inst - "x!1" )"" (expand "metric_continuous_at?" )"" (skosimp)"" (inst - "epsilon!1" )"" (skosimp)"" (inst + "delta!1" )"" (skosimp)"" (inst - "x!2" ) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil real_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" metric_continuity nil )nil real_types nil )"bool" reals nil )"real" reals nil )"metric_open" nil )"(strict_total_order?[real])" real_props nil )"metric_open" nil )"set[T]" metric_space_def nil )"bool" sets nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil ))nil ))nil 3429893655"" (skosimp)"" (lemma "opp_continuous" ("g" "g2!1" ))"" (lemma "sum_continuous" ("g1" "g1!1" "g2" "-g2!1" ))"" (expand "+" )"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def 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 )nil real_continuity nil )nil real_continuity nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"metric_continuous" nil )nil real_continuity nil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3429893655"" (skosimp)"" (typepred "g!1" )"" (expand "*" )"" (expand "metric_continuous?" )"" (skosimp)"" (inst - "x!1" )"" (expand "metric_continuous_at?" )"" (skosimp)"" (case-replace "c!1=0" )"1" (inst + "1" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp)"1" (expand "abs" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "member" )"2" (expand "ball" )"2" "posreal_div_posreal_is_posreal" "px" "epsilon!1" "py" "abs(c!1)" ))"1" (inst - "epsilon!1 / abs(c!1)" )"1" (skosimp)"1" "delta!1" )"1" "1" "x!2" )"1" assert )"1" rewrite "div_mult_pos_lt2" -2)"1" rewrite "abs_mult" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 3 -1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil real_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"nnreal" nil )nil real_props nil )"real" real_continuity nil )"posreal" real_continuity nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"nzreal" nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )"real" reals nil )"set[T]" metric_space_def nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"bool" metric_continuity nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil ))nil ))nil 3429890484"" (skosimp)"" (typepred "g!1" )"" (expand "metric_continuous?" )"" (expand "metric_continuous_at?" )"" (skosimp)"" (skosimp)"" (inst - "x!1" )"" (inst - "epsilon!1" )"" (skosimp)"" (inst + "delta!1" )"" (expand "member" )"" (skosimp)"" (inst - "x!2" )"" (assert )"" "" expand "ball" )"" expand "abs" )"" expand "abs" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil real_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" metric_continuity nil )nil real_types nil )"bool" reals nil )"metric_open" nil )"metric_open" nil )"real" reals nil )"set[T]" metric_space_def nil )"odd_int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"[T -> nonneg_real]" real_fun_ops "reals/" )"bool" sets nil ))nil ))nil 3433761206"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_continuity nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" real_continuity nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" metric_continuity nil )nil metric_continuity nil )"(strict_total_order?[real])" real_props nil )"bool" metric_continuity nil )"bool" sets nil )"set[T]" metric_space_def nil )"(total_order?[real])" nil )"real" reals nil ))nil ))nil 3429893655"" case "forall (a,eps:posreal,x:nnreal): exists (delta:posreal): forall (y:nnreal): abs(x-y) < delta => abs(x^a-y^a) < eps" )"1" (skosimp)"1" (expand "metric_continuous?" )"1" (expand "^" 1)"1" (expand "metric_continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (typepred "a!1" )"1" (typepred "h!1" )"1" (inst -5 "a!1" "epsilon!1" "h!1(x!1)" )"1" (skosimp)"1" (expand "metric_continuous?" )"1" (expand "metric_continuous_at?" )"1" "x!1" )"1" "delta!1" )"1" "1" expand "member" )"1" expand "ball" )"1" "delta!2" )"1" "1" "x!2" )"1" "h!1(x!2)" )"1" (assert ) nil nil )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (case-replace "x!1=0" )"1" (rewrite "real_expt_0x" )"1" case "EXISTS (delta: posreal): ") "1" (skosimp)"1" (inst + "delta!1" )"1" (skosimp)"1" (inst - "y!1" )"1" (expand "abs" )"1" (assert )"1" (case-replace "y!1=0" )"1" (assert )"1" rewrite "real_expt_0x" )"1" (assert ) nil nil ))nil ))nil )"2" (assert )"2" assert )"2" "real_expt_pos" "px" "y!1" "a" "a!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (inst + "eps!1^(1/a!1)" )"1" (skosimp)"1" "real_expt_strict_increasing" "x" "y!1" "y" "eps!1 ^ (1 / a!1)" "pa" "a!1" ))"1" (assert )"1" (rewrite "real_expt_times" -1 :dir rl)"1" (assert )"1" (rewrite "real_expt_x1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "real_expt_pos" ) nil nil ))nil ))nil ))nil ))nil )"2" (case "x!1>0" )"1" (hide 1)"1" case "EXISTS (delta: posreal): ") "1" case "EXISTS (delta: posreal): ") "1" (skosimp*)"1" (inst + "min(delta!1,delta!2)" )"1" (skosimp)"1" (lemma "trich_lt" ("x" "x!1" "y" "y!1" ))"1" (split -1)"1" (inst -3 "y!1" )"1" assert )"1" "real_expt_strict_increasing" "x" "x!1" "y" "y!1" "pa" "a!1" ))"1" expand "abs" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" assert )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" (inst - "y!1" )"3" assert )"3" "real_expt_strict_increasing" "y" "x!1" "x" "y!1" "pa" "a!1" ))"3" expand "abs" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" "trich_lt" ("x" "x!1^a!1" "y" "eps!1" ))"2" (split -1)"1" (inst + "1" )"1" (skosimp)"1" "real_expt_pos" "px" "y!1" "a" "a!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (replace -1)"2" (inst + "x!1/2" )"1" (skosimp)"1" "real_expt_pos" "px" "y!1" "a" "a!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (inst + "x!1-(x!1^a!1-eps!1)^(1/a!1)" )"1" (skosimp)"1" "real_expt_strict_increasing" "x" "(x!1 ^ a!1 - eps!1) ^ (1 / a!1)" "y" "y!1" "pa" "a!1" ))"1" assert )"1" rewrite "real_expt_times" "1" rewrite "real_expt_x1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "real_expt_strict_increasing" "x" "x!1 ^ a!1 - eps!1" "y" "x!1 ^ a!1" "pa" "1/a!1" ))"1" (assert )"1" rewrite "real_expt_times" -1 :dir rl)"1" rewrite "real_expt_x1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"3" (flatten) (("3" (assert ) nil nil )) nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (inst + "(eps!1+x!1^a!1)^(1/a!1)-x!1" )"1" (skosimp)"1" "real_expt_strict_increasing" "x" "y!1" "y" "(eps!1 + x!1 ^ a!1) ^ (1 / a!1)" "pa" "a!1" ))"1" (assert )"1" (rewrite "real_expt_times" -1 :dir rl)"1" (rewrite "real_expt_x1" -1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" "real_expt_strict_increasing" "x" "x!1^a!1" "y" "x!1 ^ a!1 + eps!1" "pa" "1/a!1" ))"2" (assert )"2" (rewrite "real_expt_times" -1 :dir rl)"2" (rewrite "real_expt_x1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (flatten) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )nil real_expt "power/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posreal" nil )"posreal" real_continuity nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" real_continuity nil )nil real_expt "power/" )nil real_expt "power/" )"posreal" nil )nil real_expt "power/" )nil real_expt "power/" )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"posreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )nil real_props nil )"nnreal" real_continuity nil )"nnreal" nil )"[T -> nnreal]" real_fun_power "power/" )"bool" sets nil )nil real_continuity nil )"bool" metric_def nil )nil metric_def nil )"metric" real_continuity nil )nil metric_continuity nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"T" real_continuity nil )"T" real_continuity nil )"{g | FORALL x: g(x) >= 0}" real_continuitynil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"set[T]" metric_space_def nil )"bool" metric_continuity nil )"bool" metric_continuity nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nnreal" real_expt "power/" ))nil ))nil 3429907898"" (skosimp)"" (case-replace "n!1=0" )"1" (expand "expt" )"1" (expand "expt" )"1" (lemma "const_continuous" ("a" "1" ))"1" (rewrite "metric_continuous_def" )"1" (expand "const_fun" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (case "n!1>0" )"1" (hide 1)"1" (typepred "g!1" )"1" case "FORALL (epsilon:posreal,x:real): EXISTS (delta:posreal): FORALL (y:real): abs(x-y)<delta => abs(expt(x,n!1)-expt(y,n!1))<epsilon" )"1" (expand "metric_continuous?" )"1" (skosimp)"1" (inst - "x!1" )"1" (expand "metric_continuous_at?" )"1" (expand "ball" )"1" (expand "member" )"1" (skosimp)"1" (inst - "epsilon!1" "g!1(x!1)" )"1" "1" "delta!1" )"1" "1" "delta!2" )"1" "1" "x!2" )"1" assert )"1" "g!1(x!2)" )"1" assert )"1" expand "expt" 1)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (skosimp)"2" case "forall (n:nat,x:nnreal): EXISTS (delta: posreal): ") "1" case "forall (n:nat,x:negreal): EXISTS (delta: posreal): ") "1" (case "x!1>=0" )"1" (hide -2)"1" (inst - "n!1" "x!1" )"1" (skosimp)"1" expand ">=" -1)"1" expand "<=" -1)"1" "1" "min(x!1,delta!1)" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" replace -1 * rl)"2" expand "expt" -2 1)"2" expand "expt" 1 1)"2" assert )"2" "delta!1" )"2" "2" "abs(y!1)" )"2" "1" rewrite "expt_of_abs" )"1" "YN" "expt(y!1, n!1)" )"1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2)"2" (inst - "n!1" "x!1" )"1" (skosimp)"1" "min(delta!1,-x!1)" )"1" "1" "y!1" )"1" "1" (propax) nil nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -2)"2" (skosimp)"2" (lemma "odd_or_even_int" ("x" "n!2" ))"2" "1" case "forall (x:real): expt(-x,n!2)=-expt(x,n!2)" )"1" "n!2" "-x!2" )"1" "1" "min(delta!1,-x!2)" )"1" "1" "-y!1" )"1" "1" "x!2" )"1" "y!1" )"1" replace -2)"1" replace -3)"1" "1" "XN" "expt(x!2, n!2)" )"1" "YN" "expt(y!1, n!2)" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (j:nat,x:real): expt(-x, 1+2*j) = -expt(x, 1+2*j)" )"1" expand "odd?" )"1" "1" replace -2)"1" "j!1" "x!3" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "j" )"1" expand "expt" )"1" expand "expt" )"1" (propax) nil nil ))nil ))nil )"2" "2" expand "expt" 1)"2" expand "expt" 1)"2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "forall (x:real): expt(-x,n!2)=expt(x,n!2)" )"1" "x!2" )"1" "n!2" "-x!2" )"1" "1" "min(delta!1,-x!2)" )"1" "1" "-y!1" )"1" "1" "x!2" )"1" "y!1" )"1" replace -4)"1" replace -5)"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (x:real,j:nat): expt(-x,2*j) = expt(x,2*j)" )"1" expand "even?" )"1" "1" "1" replace -2)"1" "x!3" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j" )"1" "1" expand "expt" )"1" (propax) nil nil ))nil ))nil )"2" "2" expand "expt" 1)"2" expand "expt" 1)"2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (hide -1)"2" (case-replace "n!2=0" )"1" (expand "expt" )"1" expand "abs" )"1" (propax) nil nil ))nil ))nil )"2" (case "n!2>0" )"1" "1" case "EXISTS (delta: posreal): ") "1" case "EXISTS (delta: posreal): ") "1" "1" "min(delta!1,delta!2)" )"1" "1" "y!1" )"1" "y!1" )"1" "x!2=0" )"1" expand "expt" 1 1)"1" expand "expt" "1" expand "expt" "1" assert )"1" "YN" "expt(y!1, n!2)" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "x!2>0" )"1" "1" "y!1=0" )"1" expand "expt" "1" expand "expt" "1" assert )"1" "XN" "expt(x!2, n!2)" )"1" nil nil ))nil ))nil ))nil ))nil )"2" case "y!1>0" )"1" "1" "trich_lt" "x" "x!2" "y" "y!1" ))"1" "1" "both_sides_expt_pos_lt_aux" "px" "x!2" "py" "y!1" "m" "n!2-1" ))"1" assert )"1" "XN" "expt(x!2, n!2)" )"1" "YN" "expt(y!1, n!2)" )"1" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" assert )nil nil ))nil )"2" assert )"2" replace "2" assert )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "both_sides_expt_pos_lt_aux" "py" "x!2" "px" "y!1" "m" "n!2-1" ))"1" assert )"1" "XN" "expt(x!2, n!2)" )"1" "YN" "expt(y!1, n!2)" )"1" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!2=0" )"1" expand "expt" 1 1)"1" assert )"1" "1" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "x!2>0" )"1" "1" case "expt(x!2, n!2) - epsilon!1>0" )"1" "posreal_div_posreal_is_posreal" "px" "1" "py" "n!2" ))"1" "real_expt_pos" "px" "expt(x!2, n!2) - epsilon!1" "a" "1/n!2" ))"1" "real_expt_strict_increasing" "x" "expt(x!2, n!2) - epsilon!1" "y" "expt(x!2, n!2)" "pa" "1 / n!2" ))"1" assert )"1" "real_expt_times" "x" "x!2" "a" "n!2" "b" "1/n!2" ))"1" rewrite "real_expt_x1" )"1" rewrite "real_expt_int_rew" "1" expand "^" "1" replace "1" "1" "x!2-(expt(x!2, n!2) - epsilon!1) ^ (1 / n!2)" )"1" "1" assert )"1" "real_expt_strict_increasing" "x" "(expt(x!2, n!2) - epsilon!1) ^ (1 / n!2)" "y" "y!1" "pa" "n!2" ))"1" assert )"1" rewrite "real_expt_times" "1" rewrite "real_expt_x1" )"1" rewrite "real_expt_int_rew" "1" expand "^" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil )"2" "x!2/2" )"1" "1" assert )"1" "expt_pos_aux" "px" "y!1" "n" "n!2" ))"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "real_expt_pos" "px" "expt(x!2, n!2) + epsilon!1" "a" "1/n!2" ))"1" "real_expt_strict_increasing" "x" "expt(x!2, n!2)" "y" "expt(x!2, n!2) + epsilon!1" "pa" "1 / n!2" ))"1" assert )"1" "real_expt_times" "x" "x!2" "a" "n!2" "b" "1/n!2" ))"1" rewrite "real_expt_x1" )"1" rewrite "real_expt_int_rew" "1" expand "^" -1 1)"1" replace -1 * rl)"1" "1" "(expt(x!2, n!2) + epsilon!1) ^ (1 / n!2)-x!2" )"1" "1" assert )"1" "real_expt_strict_increasing" "x" "y!1" "y" "(expt(x!2, n!2) + epsilon!1) ^ (1 / n!2)" "pa" "n!2" ))"1" assert )"1" rewrite "real_expt_times" "1" rewrite "real_expt_x1" "1" rewrite "real_expt_int_rew" "1" expand "^" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "posreal_div_posreal_is_posreal" "px" "1" "py" "n!2" ))"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "n!2" ))"2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" exponentiation nil )"[S -> T]" const_fun_def "structures/" )nil metric_continuity nil )"continuous LAMBDA (x, y: real): abs(x - y))]]" nil )nil constant_continuity "topology/" )nil real_continuity nil )nil defined_types nil )nil sets nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" real_continuity nil )"setofsets[T]" metric_space_defnil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" real_fun_power "power/" )"real" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" metric_continuity nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def nil )"posreal" nil )"nzrat" rationalsnil )nil real_expt "power/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_expt "power/" )"real" exponentiation nil )"rat" rationals nil )"posreal" real_continuity nil )"nat" real_continuity nil )"nnreal" real_continuity nil )"nnreal" exponentiation nil )nil real_expt "power/" )"nnreal" real_expt "power/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_expt "power/" )nil real_expt "power/" )nil real_types nil )nil exponentiation nil )"nnreal" nil )"int" integers nil )nil exponentiation nil )nil real_props nil )"nzreal" nil )"int" integers nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )"real" reals nil )"nzreal" exponentiation nil )"bool" reals nil )nil real_types nil )nil real_types nil )"real" real_continuity nil )"posreal" real_continuity nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"nat" exponentiation nil )nil exponentiation nil )"real" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" real_continuity nil )"real" real_continuity nil )"real" real_continuity nil )"(total_order?[real])" nil )nil naturalnumbers nil )"posreal" real_continuity nil )"bool" integers nil )"int" real_continuity nil )nil reals nil )"boolean" notequal nil )"negreal" real_continuity nil )"posreal" real_continuity nil )"{z: nzreal | z <= x AND z <= y}" nil )"nzreal" real_typesnil )"posint" nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" real_continuity nil )"nonneg_int" nil )"bool" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil defined_types nil )nil naturalnumbers nil )"nnreal" exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" metric_continuity nil )nil metric_continuity nil )"bool" reals nil ))nil ))nil 3429893655"" (skosimp)"" (lemma "expt_nat_continuous" ("g" "g!1" "n" "2" ))"" (expand "sq" )"" (expand "sq" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def 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 )nil real_continuity nil )nil real_continuity nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" exponentiation nil )"[T -> real]" real_fun_power "power/" )"[T -> nnreal]" real_fun_ops_aux "reals/" ))nil ))nil 3429890484"" (skosimp)"" (typepred "g2!1" )"" (typepred "g1!1" )"" (expand "metric_continuous?" )"" (skosimp)"" (inst - "x!1" )"" (inst - "x!1" )"" (expand "min" )"" (expand "metric_continuous_at?" )"" (skosimp)"" (inst - "epsilon!1" )"" (inst - "epsilon!1" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" "" "x!2" )"" "x!2" )"" expand "member" )"" expand "ball" )"" expand "min" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil real_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )min const-decl "[T -> real]" real_fun_ops_aux "reals/" )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" reals nil )"set[T]" metric_space_def nil )"real" reals nil )"bool" reals nil )nil real_types nil )"bool" metric_continuity nil ))nil ))nil 3429890484"" (skosimp)"" (typepred "g2!1" )"" (typepred "g1!1" )"" (expand "metric_continuous?" )"" (skosimp)"" (inst - "x!1" )"" (inst - "x!1" )"" (expand "metric_continuous_at?" )"" (skosimp)"" (inst - "epsilon!1" )"" (inst - "epsilon!1" )"" (skosimp*)"" (inst + "min(delta!1,delta!2)" )"" (skosimp)"" "x!2" )"" "x!2" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil real_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" metric_continuity nil )nil real_types nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"metric_open" nil )"(strict_total_order?[real])" real_props nil )"metric_open" nil )"set[T]" metric_space_def nil )"bool" sets nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )max const-decl "[T -> real]" real_fun_ops_aux "reals/" )"odd_int" integers nil )"real" reals nil )"real" reals nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{z: posreal | z <= x AND z <= y}" real_defs nil ))nil ))nil 3429890484"" (induct "n" )"1" (skosimp)"1" (expand "minimum" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "minimum" 1)"2" (inst - "u!1" )"2" "min_continuous" "g1" "u!1(1+j!1)" "g2" "minimum(u!1, j!1)" ))"1" (propax) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp)"3" (expand "metric?" ) (("3" (grind) nil nil )) nil )) nil ))nil ))nil )"bool" metric_def nil )"odd_int" integers nil )"bool" metric_def nil )"bool" metric_def nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_continuity nil )"posint" nil )nil naturalnumbers nil )"[T -> real]" real_fun_ops_aux "reals/" )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil real_continuity nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" real_continuity nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" metric_continuity nil )nil metric_continuity nil )nil sequences nil )"real" reals nil ))nil ))nil 3429890484"" (induct "n" )"1" (skosimp)"1" (expand "maximum" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*)"2" (inst - "u!1" )"2" (expand "maximum" 1)"2" "max_continuous" "g1" "u!1(1+j!1)" "g2" "maximum(u!1, j!1)" ))"1" (propax) nil nil ) ("2" (propax) nil nil )) nil ))nil ))nil ))nil )"3" (hide 2) (("3" (grind) nil nil )) nil ))nil )"odd_int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"bool" metric_def nil )"bool" metric_def nil )"bool" metric_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_continuity nil )"posint" nil )nil naturalnumbers nil )"[T -> real]" real_fun_ops_aux "reals/" )nil defined_types nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil real_continuity nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" real_continuity nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" metric_continuity nil )nil metric_continuity nil )nil sequences nil )"real" reals nil ))nil ))nil 3429890484"" (skosimp)"" "max_continuous" ("g1" "g!1" "g2" "const_fun[T,real](0)" ))"1" (expand "plus" )"1" (expand "const_fun" )"1" (expand "max" -1) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (expand "const_fun" )"2" (expand "metric_continuous?" )"2" (expand "metric_continuous_at?" )"2" (skosimp*)"2" (inst + "1" ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"[S -> T]" const_fun_def "structures/" )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def 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 )nil real_continuity nil )nil real_continuity nil )"continuous LAMBDA (x, y: real): abs(x - y))]]" nil )max const-decl "[T -> real]" real_fun_ops_aux "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" ))nil ))nil 3429890484"" (skosimp)"" (expand "minus" )"" "min_continuous" "g1" "g!1" "g2" "const_fun[T,real](0)" ))"1" (expand "min" -1)"1" (expand "const_fun" )"1" "opp_continuous" "g" "LAMBDA (x_1: T): min(g!1(x_1), 0)" ))"1" (expand "-" -1) (("1" (propax) nil nil )) nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "const_fun" )"2" (expand "metric_continuous?" )"2" (expand "metric_continuous_at?" )"2" (skosimp*)"2" (inst + "1" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )min const-decl "[T -> real]" real_fun_ops_aux "reals/" )nil real_continuity nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"[T -> real]" real_fun_ops "reals/" )"continuous LAMBDA (x, y: real): abs(x - y))]]" nil )nil real_continuity nil )nil real_continuity nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" metric_def nil )nil metric_def nil )"metric" real_continuity nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" metric_continuity nil )nil metric_continuity nil )"[S -> T]" const_fun_def "structures/" ))nil ))nil 3429890484"" (skosimp)"" (lemma "sum_continuous" ("g1" "g1!1" "g2" "g2!1" ))"" (lemma "diff_continuous" ("g1" "g1!1" "g2" "g2!1" ))"" (lemma "sq_continuous" ("g" "(+[T])(g1!1, g2!1)" ))"" (lemma "sq_continuous" ("g" "(-[T])(g1!1, g2!1)" ))"" (hide -3 -4)"" "diff_continuous" "g1" "sq[T]((+[T])(g1!1, g2!1))" "g2" "sq[T]((-[T])(g1!1, g2!1))" ))"" "scal_continuous" "c" "1/4" "g" "(-[T])(sq[T]((+[T])(g1!1, g2!1)), sq[T]((-[T])(g1!1, g2!1)))" ))"" "(*[T] ") "" (hide-all-but 1)"" (apply-extensionality :hide? t)"" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil metric_continuity nil )"bool" metric_continuity nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"metric" real_continuity nil )nil metric_def nil )"bool" metric_def 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 )nil real_continuity nil )nil real_continuity nil )"metric_continuous" nil )nil real_continuity nil )"[T -> real]" real_fun_ops "reals/" )"posrat" nil )nil real_continuity nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"metric_continuous" nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )"metric_continuous" nil )"[T -> real]" real_fun_ops "reals/" )"metric_continuous" nil )nil real_continuity nil ))nil )))
Messung V0.5 in Prozent C=97 H=99 G=97
¤ Dauer der Verarbeitung: 0.74 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
