Quelle continuous_linear.prf
Sprache: Lisp
(continuous_linearnil 3430729650"" (skosimp*)"" (lemma "connected_domain" )"" (inst?) (("" (inst - "y!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil continuous_linear nil )"(total_order?[real])" nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear 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 3430729650"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil continuous_linear nil )) nil ))nil 3258280425"" (skosimp*)"" (expand "linear?" )"" (skosimp*)"" (replace -1 * lr)"" (hide -1)"" (expand "continuous?" )"" (skosimp*)"" (lemma "identity_continuous[T]" )"" (inst -1 "x0!1" )"" (lemma "scal_continuous[T]" )"" (inst -1 "I[T]" "m!1" "x0!1" )"" (assert )"" (hide -2)"" (lemma "sum_continuous[T]" )"" "m!1 * I[T]" "const_fun(k!1)" "x0!1" )"" assert )"" "1" expand "*" )"1" expand "const_fun" )"1" expand "+ " )"1" expand "I" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "const_continuous[T]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" linear_functions nil )"bool" continuous_functions nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil continuous_functions nil )nil continuous_functions nil )"real" reals nil )"continuous_fun" nil )nil continuous_functions nil )"continuous_fun" nil )"continuous_fun" nil )nil continuous_functions nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil ))nil )nil 3257796697"" (skosimp*)"" (replace -1)"" (hide -1)"" (expand "continuous?" )"" (skosimp*)"" (lemma "identity_continuous[T]" )"" (inst -1 "x0!1" )"" (lemma "scal_continuous[T]" )"" (inst -1 "I[T]" "m!1" "x0!1" )"" (assert )"" (hide -2)"" (lemma "sum_continuous[T]" )"" "m!1 * I[T]" "const_fun(c!1)" "x0!1" )"" (assert )"" "1" expand "*" )"1" expand "const_fun" )"1" expand "+ " )"1" expand "I" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "const_continuous[T]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil continuous_functions nil )nil continuous_functions nil )nil continuous_functions nil )nil continuous_functions nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" ))nil )nil 3257796139"" (skosimp*)"" (replace -1)"" (hide -1)"" (expand "continuous?" )"" (skosimp*)"" (lemma "identity_continuous[T]" )"" (inst -1 "x0!1" )"" (lemma "scal_continuous[T]" )"" (inst -1 "I[T]" "m!1" "x0!1" )"" (assert )"" (hide -2)"" (lemma "sum_continuous[T]" )"" "m!1 * I[T]" "const_fun(b!1)" "x0!1" )"" (assert )"" "1" expand "*" )"1" expand "const_fun" )"1" expand "+ " )"1" expand "I" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" rewrite "const_continuous[T]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil continuous_functions nil )nil continuous_functions nil )nil continuous_functions nil )nil continuous_functions nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" ))nil 3258990857"" (skosimp*)"" (expand "continuous_in?" )"" (skosimp*)"" (rewrite continuity_def)"" (expand "convergence" )"" (expand "convergence" )"" (expand "fullset" )"" (expand "linear_on?" )"" (skosimp*)"" (prop)"1" (expand "adh" )"1" (skosimp*)"1" (inst + "min(x!1+e!1/2,(x!1+b!1)/2)" )"1" (hide -1) (("1" (grind) nil nil ))nil )"2" (expand "min" )"2" "1" "connected_domain" )"1" "1" "a!1" "b!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "connected_domain" )"2" "2" "a!1" "b!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (case-replace "m!1 = 0" )"1" "min(epsilon!1,min(abs(x!1-a!1),abs(b!1-x!1)))" )"1" (skosimp*)"1" "x!1" )"1" "x!2" )"1" assert )"1" "1" replace -1)"1" "1" replace -3)"1" (assert ) nil nil ))nil ))nil ))nil )"2" expand "abs" )"2" assert )"2" "2" case "abs(x!2 - x!1) < abs(x!1 - a!1)" )"1" "1" (grind) nil nil ))nil )"2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" case "abs(x!2 - x!1) < abs(b!1 - x!1)" )"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil )"2" "min(epsilon!1/abs(m!1),min(abs(x!1-a!1),abs(b!1-x!1)))" )"1" (skosimp*)"1" "x!1" )"1" "x!2" )"1" assert )"1" "1" replace -1)"1" "1" replace -2)"1" "1" assert )"1" "m!1 * x!2 - m!1 * x!1 = m!1 * (x!2 - x!1)" )"1" rewrite "abs_mult" )"1" case "abs(x!2 - x!1) < epsilon!1 / abs(m!1)" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "abs(x!2 - x!1) < ") "1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"3" case "abs(x!2 - x!1) < abs(b!1 - x!1)" )"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "epsilon!1 / abs(m!1) > 0" )"1" "EOM" "epsilon!1 / abs(m!1)" )"1" (grind) nil nil ))nil )"2" "2" "2" (grind) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil )"3" (hide -1)"3" "abs_eq_0" )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuous_linear nil )nil continuous_functions 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]" continuous_linear nil )nil continuous_linear nil )"real" reals nil )"bool" convergence_functions nil )"real" reals nil )"bool" linear_functions nil )nil continuous_linear nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" continuous_linear nil )"T" continuous_linear nil )"T" continuous_linear nil )"posreal" nil )"real" reals nil )"real" reals nil )"setof[real]" convergence_functions nil )"[T, T -> boolean]" equalities nil )nil abs_lems "reals/" )"odd_int" integers nil )"real" reals nil )"bool" reals nil )"posreal" continuous_linear nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" continuous_linear nil )"{z: nonneg_real | z <= x AND z <= y}" real_defs nil )"(total_order?[real])" nil )nil abs_lems "reals/" )"nzreal" continuous_linear nil )nil reals nil )nil extra_real_props nil )nil abs_lems "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"nnreal" nil )nil real_props nil )"real" continuous_linear nil )"nzreal" nil )"set" sets nil )"bool" lim_of_functions nil ))nil ))nil 3258987029"" (skosimp*) (("" (assert ) nil nil )) nil )"real" reals nil )"real" reals nil ))nil 3258287121"" (skosimp*)"" (assert )"" (rewrite continuity_def)"" (expand "convergence" )"" (expand "fullset" )"" (expand "linear_on?" )"" (skosimp*)"" (expand "convergence" )"" (prop)"1" (expand "adh" )"1" (skosimp*)"1" (inst + "b!1" )"1" (expand "abs" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (case "m!1 = 0 AND m!2 = 0" )"1" (flatten)"1" (replace -1)"1" (replace -2)"1" assert )"1" "min(abs(b!1-a!1),abs(c!1-b!1))" )"1" "1" "1" "1" "1" "x!1" )"1" "b!1" )"1" assert )"1" replace -8)"1" "1" replace -1)"1" assert )nil nil ))nil )"2" expand "abs" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" "b!1" )"2" assert )"2" replace -4 * rl)"2" replace -7)"2" "1" replace -1)"1" expand "abs" )"1" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "Mabc" "min(abs(b!1-a!1),abs(c!1-b!1))" )"2" (case-replace "m!1 = 0" )"1" (assert )"1" "1" "min(epsilon!1/abs(m!2), Mabc)" )"1" "1" "1" case "x!1 <= b!1" )"1" assert )"1" replace -2 * rl)"1" "1" "1" "x!1" )"1" "b!1" )"1" assert )"1" replace -6)"1" "1" replace "1" assert )nil nil ))nil )"2" expand "abs" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "2" replace -2)"2" "x!1" )"2" "b!1" )"2" assert )"2" replace -5)"2" "1" replace "1" assert )"1" "m!2 * x!1 - m!2 * b!1 = m!2 * (x!1 - b!1)" )"1" rewrite "abs_mult" )"1" "abs(m!2)" )"1" "abs" )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "epsilon!1 / abs(m!2) > 0" )"1" (grind) nil nil )"2" case "abs(m!2) = 0" )"1" expand "abs" -1)"1" assert )"1" "1" (ground) nil nil ))nil ))nil ))nil )"2" "abs(m!2)" )"2" (assert ) nil nil ))nil ))nil )"3" expand "abs" 1)"3" assert )"3" "1" "1" (ground) nil nil ))nil )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "abs" 1)"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "m!2 = 0" )"1" "1" "min(epsilon!1/abs(m!1), Mabc)" )"1" "1" assert )"1" "1" case "x!1 <= b!1" )"1" assert )"1" replace -2 * rl)"1" "1" "1" "x!1" )"1" "b!1" )"1" replace -1)"1" "1" replace "1" "1" replace "1" assert )"1" "m!1 * x!1 - m!1 * b!1 = m!1 * (x!1 - b!1)" )"1" "1" rewrite "abs_mult" )"1" "abs(m!1)" )"1" "abs" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -1 * rl)"2" "2" "2" replace -2)"2" "x!1" )"2" "b!1" )"2" assert )"2" replace "2" "1" replace "1" expand "abs" )"1" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "epsilon!1 / abs(m!1) > 0" )"1" (grind) nil nil )"2" "2" case "abs(m!1) = 0" )"1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil )"3" expand "abs" 1)"3" assert )"3" "3" expand "abs" )"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "abs(m!1) > 0 AND abs(m!2) > 0" )"1" "1" "MEPS" "min(epsilon!1/abs(m!1),epsilon!1/abs(m!2))" )"1" "min(MEPS,Mabc)" )"1" "1" "1" case "x!1 <= b!1" )"1" assert )"1" "1" "x!1" )"1" "b!1" )"1" assert )"1" replace "1" "1" replace "1" "m!1 * x!1 - m!1 * b!1 = m!1 * (x!1 - b!1)" )"1" rewrite "abs_mult" )"1" "abs(m!1)" )"1" "abs((x!1 - b!1)) < MEPS" )"1" replace "1" "1" expand "min" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "abs" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" assert )"2" "2" "2" "2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -6)"2" "2" "x!1" )"2" "b!1" )"2" assert )"2" "1" replace "1" "1" replace "1" "1" assert )"1" "m!2 * x!1 - m!2 * b!1 = m!2 * (x!1 - b!1)" )"1" rewrite "abs_mult" )"1" "abs(m!2)" )"1" "1" "abs" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "MEPS > 0 AND Mabc > 0" )"1" "1" expand "min" 1)"1" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" "epsilon!1 / abs(m!1) > 0 AND epsilon!1 / abs(m!2) > 0 " )"1" "1" "1" "abs" )nil nil ))nil ))nil )"2" "1" case "abs(m!1) > 0" )"1" "1" assert )nil nil ))nil )"2" nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" expand "abs" -2)"2" "2" "1" "1" "1" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" expand "abs" 1)"2" "2" "1" "1" (ground) nil nil ))nil )"2" "2" (ground) nil nil ))nil )"3" "3" (ground) nil nil ))nil )"4" "4" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"bool" lim_of_functions nil )"real" reals nil )"bool" linear_functions nil )"real" reals nil )"bool" convergence_functions nil )"{z: nzreal | z <= epsilon!1 / abs(m!1) AND z <= epsilon!1 / abs(m!2)}" nil )"bool" reals nil )nil reals nil )"{z: nzreal | z <= x AND z <= y}" nil )nil extra_real_props nil )"real" continuous_linear nil )"nzreal" nil )"boolean" notequal nil )"real" continuous_linear nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" continuous_linear nil )"{z: nonneg_real | z <= abs(b!1 - a!1) AND z <= abs(c!1 - b!1)}" nil )nil real_props nil )"nnreal" nil )nil reals nil )nil extra_real_props nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil extra_real_propsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{z: nonneg_real | z <= x AND z <= y}" real_defs nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" continuous_linear nil )"T" continuous_linear nil )"T" continuous_linear nil )nil real_types nil )nil continuous_linear nil )"real" reals nil )"odd_int" integers nil )nil abs_lems "reals/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"setof[real]" convergence_functions nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"set" sets nil )"(total_order?[real])" nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" reals nil )nil booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil continuous_functions nil ))nil )nil 3258136168"" (skosimp*)"" (expand "continuous?" )"" (expand "convergence" )"" (expand "fullset" )"" (expand "linear_on?" )"" (skosimp*)"" (expand "convergence" )"" (prop)"1" (postpone) nil nil )"2" (skosimp*)"2" (case "m!1 = 0 AND m!2 = 0" )"1" (flatten)"1" (replace -1)"1" (replace -2)"1" (assert )"1" "abs(b!1-a!1)" )"1" "1" "1" "1" "1" "x!1" )"1" "b!1" )"1" assert )"1" replace -8)"1" "1" replace -1)"1" assert )"1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" "b!1" )"2" assert )"2" replace -4 * rl)"2" replace -7)"2" "1" replace -1)"1" expand "abs" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3258134941"" (skosimp*)"" (expand "continuous?" )"" (expand "convergence" )"" (expand "fullset" )"" (expand "linear_on?" )"" (skosimp*)"" (expand "convergence" )"" (prop)"1" (postpone) nil nil )"2" (skosimp*)"2" (case "m!1 = 0 AND m!2 = 0" )"1" (postpone) nil nil )"2" "min(epsilon!1/max(m!1,m!2),b!1-a!1)" )"1" (skosimp*)"1" (case "x!1 <= b!1" )"1" (hide -4 -6)"1" "x!1" )"1" "x!1" )"1" "b!1" )"1" "b!1" )"1" assert )"1" case "a!1 <= x!1" )"1" assert )"1" replace -6)"1" "1" replace -6)"1" "1" replace -4)"1" "1" replace -4)"1" "1" "m!1 * x!1 + c!2 - (m!1 * b!1 + c!2) = m!1*(x!1-b!1)" )"1" rewrite "abs_mult" )"1" assert )"1" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3258298500"" (skosimp*)"" (rewrite continuity_def)"" (rewrite continuity_def)"" (expand "convergence" )"" (expand "fullset" )"" (expand "convergence" )"" (flatten)"" (prop)"" (skosimp*)"" (inst -5 "epsilon!1" )"" (assert )"" (skosimp*)"" "min(delta!1,min(x!1 -a!1,b!1-x!1))" )"1" (skosimp*)"1" "x!1" )"1" "x!2" )"1" "x!2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil continuous_functions 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]" continuous_linear nil )nil continuous_linear nil )"bool" lim_of_functions nil )"real" reals nil )"bool" convergence_functions nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"setof[real]" convergence_functions nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil continuous_linear nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" continuous_linear nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"T" continuous_linear nil )"T" continuous_linear nil )"T" continuous_linear nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"set" sets nil ))nil 3259053981"" (skosimp*)"" (grind) (("" (inst -1 "a!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"R" extend nil )"set" sets nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3259053673"" (skosimp*)"" (expand "top" )"" (assert )"" (typepred "lub(extend[real, T, bool, FALSE](fullset[T]))" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" (expand "upper_bound?" )"1" (inst?)"1" (expand "extend" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "a!1" )"2" (expand "extend" )"2" (expand "fullset" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" continuous_linear nil )"set" sets nil )"R" extend nil )"bool" booleans nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"T" continuous_linear nil )"bool" bounded_real_defs nil )"(total_order?[real])" nil ))nil 3259056520"" (skosimp*)"" (expand "top" )"" (assert )"" (lift-if)"" (ground)"1" "lub(extend[real, T, bool, FALSE](fullset[T]))" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" (inst - "y!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst -1 "a!1" )"2" (expand "extend" )"2" (expand "fullset" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "upper_bound?" )"2" (inst -1 "a!1" )"2" (expand "extend" )"2" (expand "fullset" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" continuous_linear nil )"bool" bounded_real_defs nil )"T" continuous_linear nil )"set" sets nil )"R" extend nil )"bool" booleans nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 ))nil 3259057334"" (skosimp*)"" (expand "bot" )"" (assert )"" (typepred "glb(extend[real, T, bool, FALSE](fullset[T]))" )"1" (expand "greatest_lower_bound?" )"1" (flatten)"1" (expand "lower_bound?" )"1" (inst?)"1" (expand "extend" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "a!1" )"2" (expand "extend" )"2" (expand "fullset" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" continuous_linear nil )"set" sets nil )"R" extend nil )"bool" booleans nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 )"T" continuous_linear nil )"bool" bounded_real_defs nil )"(total_order?[real])" nil ))nil 3259057455"" (skosimp*)"" (expand "bot" )"" (assert )"" (lift-if)"" (prop)"1" "glb(extend[real, T, bool, FALSE](fullset[T]))" )"1" (expand "greatest_lower_bound?" )"1" (flatten)"1" (inst - "y!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "a!1" )"2" (assert )"2" (expand "extend" )"2" (expand "fullset" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "lower_bound?" )"2" (inst?)"2" (expand "extend" )"2" (expand "fullset" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" continuous_linear nil )"bool" bounded_real_defs nil )"T" continuous_linear nil )"set" sets nil )"R" extend nil )"bool" booleans nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets 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 ))nil 3259056967"" (stop-rewrite "abs_0" )"" (skosimp*)"" (rewrite continuity_def)"" (expand "convergence" )"" (expand "fullset" )"" (expand "convergence" )"" (prop)"1" (expand "adh" )"1" (skosimp*)"1" "IF x!1 - a!1 < e!1 THEN a!1 ELSE x!1 - e!1/2 ENDIF" )"1" (lift-if)"1" (expand "abs" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "connected_domain" )"2" (inst -1 "a!1" "x!1" "_" )"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "linear_on?" )"2" (skosimp*)"2" "IF m!1 = 0 THEN min(epsilon!1,x!1-a!1) min (epsilon!1/abs(m!1),x!1-a!1)") "1" (skosimp*)"1" (inst-cp - "x!1" )"1" (inst - "x!2" )"1" assert )"1" "1" "1" replace -1)"1" "1" replace -1)"1" "1" assert )"1" "m!1 * x!2 - m!1 * x!1 = m!1 * (x!2 - x!1)" )"1" rewrite "abs_mult" )"1" "1" "1" "1" case "abs(x!2 - x!1) < epsilon!1 / abs(m!1)" )"1" "1" assert )nil nil ))nil )"2" "2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "top_lem" )"2" "2" assert )"2" expand "fullset" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (grind) nil nil ))nil ))nil )"3" "3" "top_lem" )"3" "3" expand "fullset" )"3" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (hide -3 -5)"2" (assert )"2" case "min(epsilon!1 / abs(m!1), x!1 - a!1) > 0" )"1" (assert ) nil nil )"2" "2" "1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "abs" )"3" (ground)"3" (lift-if) (("3" (ground) nil nil ))nil ))nil ))nil )"4" (flatten)"4" (hide -4 -5 -6) (("4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" lim_of_functions nil )"real" reals nil )"bool" convergence_functions nil )nil extra_real_props nil )nil continuous_linear nil )"real" reals nil )"odd_int" integers nil )nil real_props nil )"nnreal" nil )nil real_props nil )nil abs_lems "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"real" continuous_linear nil )set type-eq-decl nil sets nil ) (extend const-decl "R" extend nil )"bool" booleans nil )"[numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" continuous_linear nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" continuous_linear nil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" linear_functions nil )"real" reals nil )"setof[real]" convergence_functions nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"posreal" continuous_linear nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"T" continuous_linear nil )"T" continuous_linear nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )nil continuous_linear nil )"nzreal" nil )nil continuous_linear nil )"(total_order?[real])" nil )"set" sets nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil continuous_functions nil ))nil )nil 3258990896"" (skosimp*)"" (hide -4)"" (expand "continuous?" )"" (expand "convergence" )"" (expand "fullset" )"" (expand "convergence" )"" (prop)"1" (expand "adh" )"1" (skosimp*)"1" "IF x!1 - a!1 < e!1 THEN a!1 ELSE x!1 - e!1/2 ENDIF" )"1" (lift-if)"1" (expand "abs" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "connected_domain" )"2" (inst -1 "a!1" "x!1" "_" )"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "linear_on?" )"2" (skosimp*)"2" "IF m!1 = 0 THEN min(epsilon!1,x!1-a!1) min (epsilon!1/abs(m!1),x!1-a!1)") "1" (skosimp*)"1" (inst-cp - "x!1" )"1" (inst - "x!2" )"1" assert )"1" "1" "1" replace -1)"1" "1" replace -1)"1" "1" assert )"1" "m!1 * x!2 - m!1 * x!1 = m!1 * (x!2 - x!1)" )"1" rewrite "abs_mult" )"1" "1" "1" "1" replace -1)"1" rewrite "abs_0" )"1" assert )nil nil ))nil ))nil )"2" case "abs(x!2 - x!1) < epsilon!1 / abs(m!1)" )"1" "1" assert )nil nil ))nil )"2" "2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "lub(extend[real, T, bool, FALSE]({x: T | TRUE}))" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "x!1" )"1" expand "extend" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x!1" )"2" expand "extend" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (grind) nil nil ))nil ))nil )"3" "3" "lub(extend[real, T, bool, FALSE]({x: T | TRUE}))" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "x!2" )"1" expand "extend" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x!1" )"2" expand "extend" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (hide -3 -4)"2" (grind)"1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (expand "abs" )"3" (lift-if) (("3" (ground) nil nil ))nil ))nil ))nil )"4" (flatten)"4" (hide -4 -5) (("4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setof[real]" convergence_functions nil )nil abs_lems "reals/" )"bool" convergence_functions nil ))nil ))nil 3258990926"" (skosimp*)"" (rewrite continuity_def)"" (hide -4)"" (expand "convergence" )"" (expand "fullset" )"" (expand "convergence" )"" (prop)"1" (expand "adh" )"1" (skosimp*)"1" "IF a!1 - x!1 < e!1 THEN a!1 ELSE x!1 + e!1/2 ENDIF" )"1" (lift-if)"1" (expand "abs" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "connected_domain" )"2" (inst -1 "x!1" "a!1" "_" )"2" (inst?) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "linear_on?" )"2" (skosimp*)"2" "IF m!1 = 0 THEN min(epsilon!1,a!1-x!1) min (epsilon!1/abs(m!1),a!1-x!1)") "1" (skosimp*)"1" (inst-cp - "x!1" )"1" (inst - "x!2" )"1" assert )"1" "1" "1" replace -1)"1" "1" replace -1)"1" "1" assert )"1" "m!1 * x!2 - m!1 * x!1 = m!1 * (x!2 - x!1)" )"1" rewrite "abs_mult" )"1" "1" "1" "1" case "abs(x!2 - x!1) < epsilon!1 / abs(m!1)" )"1" "1" assert )nil nil ))nil )"2" "2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "bot_lem" )"2" "2" assert )"2" expand "fullset" )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "bot_lem" )"2" expand "fullset" )"2" (inst?) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (hide -3 -4)"2" case "min(epsilon!1 / abs(m!1), a!1 - x!1) > 0" )"1" (assert ) nil nil )"2" "2" "1" "1" (assert ) nil nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" expand "abs" )"3" "3" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (flatten)"3" (expand "abs" -1)"3" (lift-if) (("3" (ground) nil nil ))nil ))nil ))nil )"4" (flatten)"4" (hide -4 -5) (("4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil continuous_functions 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]" continuous_linear nil )nil continuous_linear nil )"bool" lim_of_functions nil )"real" reals nil )"bool" convergence_functions nil )nil extra_real_props nil )nil continuous_linear nil )"odd_int" integers nil )nil real_props nil )"nnreal" nil )nil real_props nil )nil abs_lems "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" continuous_linear nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" continuous_linear nil )"nzreal" nil )"(total_order?[real])" nil )"bool" linear_functions nil )"real" reals nil )"setof[real]" convergence_functions nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" continuous_linear nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"T" continuous_linear nil )"T" continuous_linear nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil continuous_linear nil )nil continuous_linear nil )"(total_order?[real])" nil )"set" sets nil ))nil ))nil 3259057915"" (skosimp*) (("" (expand "top" ) (("" (assert ) nil nil )) nil ))nil )"real" continuous_linear nil )"(strict_total_order?[real])" real_props nil ))nil 3258990953"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (expand "piecewise_linear?" )"" (inst?)"" (split -1)"1" (lemma "cont_in_linear" )"1" (expand "on_linear_part?" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "continuous_in?" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "on_linear_top?" )"2" (skosimp*)"2" (typepred "x0!1" )"2" (lemma "cont_upto_lub" )"2" (inst?)"2" (assert )"2" (inst -1 "a!1" )"2" (assert )"2" expand "top" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "on_linear_bottom?" )"3" (flatten)"3" (typepred "x0!1" )"3" (skosimp*)"3" (lemma "cont_downto_glb" )"3" (inst?)"3" (inst -1 "a!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "on_junction?" )"4" (skosimp*)"4" (lemma "piecewise" )"4" "a!1" "x0!1" "c!1" "(LAMBDA (y: T): k1!1 + m1!1 * y)" "(LAMBDA (y: T): k2!1 + m2!1 * y)" )"4" (assert )"4" (split -1)"1" (lemma "cont_piece" )"1" "a!1" "c!1" "_" "f!1" "x0!1" )"1" "1" assert )"1" "1" "1" "1" "y!1" )"1" (assert ) nil nil ))nil )"2" "y!1" )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "linear_on?" )"2" (inst + "m1!1" "k1!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "linear_on?" )"3" (inst + "m2!1" "k2!1" )"3" "3" "x!1" )"3" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" continuous_functions nil )"bool" continuous_linear nil )"bool" continuous_linear nil )"bool" continuous_linear nil )"(strict_total_order?[real])" real_props nil )nil continuous_linear nil )nil continuous_linear nil )"real" continuous_linear nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )"bool" continuous_linear nil )"(strict_total_order?[real])" real_props nil )nil continuous_linear nil )"bool" continuous_linear nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"(total_order?[real])" nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )nil continuous_linear nil )"bool" linear_functions nil )nil continuous_linear nil )"bool" continuous_linear nil )"real" reals nil )nil continuous_linear nil )"[real -> boolean]" continuous_linear 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 3258987881"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (expand "piecewise_linear?" )"" (inst?)"" (split -1)"1" (lemma "continuous_in_linear" )"1" (expand "on_linear_part?" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "continuous_in?" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "on_linear_top?" )"2" (skosimp*)"2" (typepred "x0!1" )"2" (lemma "continuous_upto_lub" )"2" (inst?)"2" (assert )"2" (inst -1 "a!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "on_junction?" )"3" (skosimp*)"3" (lemma "piecewise" )"3" "a!1" "x0!1" "c!1" "(LAMBDA (y: T): k1!1 + m1!1 * y)" "(LAMBDA (y: T): k2!1 + m2!1 * y)" )"3" (assert )"3" (split -1)"1" (lemma "cont_piece" )"1" "a!1" "c!1" "_" "f!1" "x0!1" )"1" "1" assert )"1" "1" "1" "1" "y!1" )"1" (assert ) nil nil ))nil )"2" "y!1" )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "linear_on?" )"2" (inst + "m1!1" "k1!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "linear_on?" )"3" (inst + "m2!1" "k2!1" )"3" "3" "x!1" )"3" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3258820493"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (expand "piecewise_linear?" )"" (inst?)"" (split -1)"1" (lemma "continuous_on_linear" )"1" (expand "on_linear_part?" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "continuous_on?" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "on_linear_top?" )"2" (skosimp*)"2" (typepred "x0!1" )"2" (lemma "continuous_upto_lub" )"2" (inst?)"2" (assert )"2" (inst -1 "a!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "on_junction?" )"3" (skosimp*)"3" (lemma "piecewise" )"3" "a!1" "x0!1" "c!1" "(LAMBDA (y: T): k1!1 + m1!1 * y)" "(LAMBDA (y: T): k2!1 + m2!1 * y)" )"3" (assert )"3" (split -1)"1" (lemma "cont_piece" )"1" "a!1" "c!1" "_" "f!1" "x0!1" )"1" "1" assert )"1" "1" "1" "1" "y!1" )"1" (assert ) nil nil ))nil )"2" "y!1" )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "linear_on?" )"2" (inst + "m1!1" "k1!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "linear_on?" )"3" (inst + "m2!1" "k2!1" )"3" "3" "x!1" )"3" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3258820186"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (expand "piecewise_linear?" )"" (inst?)"" (split -1)"1" (lemma "continuous_in_linear" )"1" (expand "on_linear_part?" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "continuous_in?" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "on_junction?" )"2" (skosimp*)"2" (lemma "piecewise" )"2" "a!1" "x0!1" "c!1" "(LAMBDA (y: T): k1!1 + m1!1 * y)" "(LAMBDA (y: T): k2!1 + m2!1 * y)" )"2" (assert )"2" (split -1)"1" (lemma "cont_piece" )"1" "a!1" "c!1" "_" "f!1" "x0!1" )"1" "1" assert )"1" "1" "1" "1" "y!1" )"1" (assert ) nil nil ))nil )"2" "y!1" )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "linear_on?" )"2" (inst + "m1!1" "k1!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "linear_on?" )"3" (inst + "m2!1" "k2!1" )"3" "3" "x!1" )"3" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3258817490"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (expand "piecewise_linear?" )"" (inst?)"" (split -1)"1" (lemma "continuous_on_linear" )"1" (expand "on_linear_part?" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "continuous_on?" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "on_junction?" )"2" (skosimp*)"2" (lemma "piecewise" )"2" "a!1" "x0!1" "c!1" "(LAMBDA (y: T): k1!1 + m1!1 * y)" "(LAMBDA (y: T): k2!1 + m2!1 * y)" )"2" (assert )"2" (split -1)"1" (lemma "cont_piece" )"1" "a!1" "c!1" "_" "f!1" "x0!1" )"1" "1" assert )"1" "1" "1" "1" "y!1" )"1" (assert ) nil nil ))nil )"2" "y!1" )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "linear_on?" )"2" (inst + "m1!1" "k1!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "linear_on?" )"3" (inst + "m2!1" "k2!1" )"3" "3" "x!1" )"3" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3258805523"" (skosimp*)"" (expand "continuous?" )"" (skosimp*)"" (expand "piecewise_linear?" )"" (inst?)"" (split -1)"1" (lemma "continuous_in_linear" )"1" (expand "on_linear_part?" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (expand "continuous_in?" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "on_junction?" )"2" (skosimp*)"2" (lemma "piecewise" )"2" "a!1" "x0!1" "c!1" "(LAMBDA (y: T): k1!1 + m1!1 * y)" "(LAMBDA (y: T): k2!1 + m2!1 * y)" )"2" (assert )"2" (split -1)"1" (lemma "cont_piece" )"1" "a!1" "c!1" "_" "f!1" "x0!1" )"1" "1" assert )"1" "1" "1" "1" "y!1" )"1" (assert ) nil nil ))nil )"2" "y!1" )"2" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "linear_on?" )"2" (inst + "m1!1" "k1!1" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (expand "linear_on?" )"3" (inst + "m2!1" "k2!1" )"3" "3" "x!1" )"3" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.129Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
