Quelle integral_pulse.prf
Sprache: Lisp
(integral_pulsenil 3260699953"" (skosimp*)"" (lemma "connected_domain" )"" (inst -1 "x!1" "y!1" "z!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil integral_pulse nil )) nil ))nil 3260699953"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil integral_pulse nil )) nil ))nil 3262360238"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3262360239 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3262360239 ("" (subtype-tcc) nil nil ) nil shostak))nil 3262360239 ("" (assuming-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3262360240 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )nil naturalnumbers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3262360240 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil 3352532343 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nat_types nil )nil naturalnumbers nil )"bool" reals nil ))nil ))nil 3262360246"" (skosimp*)"" case "FORALL (P: partition(a!1,b!1),p,q:nat): AND p+q <= length(P) - 1 IMPLIESLAMBDA (n: upto(length(P) - 1)):IF n = 0 THEN 0 ELSE seq(P)(n) - seq(P)(n - 1) ENDIF)) =") "1" (inst -1 "P!1" "p!1" "q!1-p!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide 2)"2" (induct "q" )"1" (skosimp*)"1" (expand "sigma" )"1" (ground)"1" (expand "sigma" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "P!2" "p!2" )"2" (assert )"2" (expand "sigma" 1)"2" (replace -1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (skosimp*) (("6" (assert ) nil nil )) nil )"7" (skosimp*) nil nil )"8" (skosimp*) (("8" (assert ) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil )"6" (skosimp*) (("6" (assert ) nil nil )) nil )"7" (skosimp*) nil nil )"8" (hide 2)"8" (skosimp*)"8" (inst + "0" ) (("8" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil naturalnumbers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil finite_sequences nil )nil intervals_real "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integral_pulse nil )"[real -> boolean]" integral_pulse nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nat_types nil )nil naturalnumbers nil )"real" reals nil )"int" integers nil )"nonneg_int" nil )NOT const-decl "[bool -> bool]" booleans nil )nil integers nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" integral_pulse nil )"nat" integral_pulse nil )"(total_order?[real])" nil )"T" integral_pulse nil )"T" integral_pulse nil )nil defined_types nil )nil naturalnumbers nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"posint" nil )"posint" nil ))nil 3262447218"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3280253181"" (skosimp*)"" (expand "Rie_sec" )"" (typepred "P!1" )"" (assert )"" (inst - "ii!1-1" )"" (name "FF" "f!1(xis!1(ii!1 - 1))" )"" (replace -1)"" (lemma "width_lem" )"" (expand "finseq_appl" )"" (inst -1 "a!1" "b!1" "P!1" "ii!1-1" )"" (assert )"" (case " FF >= 0 AND FF <= 1" )"1" (flatten)"1" (assert )"1" "1" assert )"1" expand "abs" )"1" "1" assert )"1" "FF = 0" )"1" (assert ) nil nil )"2" "FF" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "xis!1(ii!1-1)" )"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"real" integral_def nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" integral_def nil )nil integral_def nil )"(total_order?[real])" nil )"[bool, bool -> bool]" booleans nil )"real" integral_pulse nil )nil real_props nil )nil extra_real_props nil )nil abs_lems "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"posreal" integral_def nil )"int" integers nil )"[below[length(fs)] -> T]" finite_sequencesnil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil naturalnumbers nil )nil nat_types nil )"[real -> boolean]" integral_pulse nil )nil integral_pulse nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil intervals_real "reals/" )nil finite_sequences nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integral_def nil ))nil )nil 3262529290"" (skosimp*)"" (expand "Rie_sec" )"" (typepred "P!1" )"" (assert )"" (inst - "ii!1-1" )"" (name "FF" "f!1(xis!1`seq(ii!1 - 1))" )"1" (replace -1)"1" (lemma "width_lem" )"1" (expand "finseq_appl" )"1" (inst -1 "a!1" "b!1" "P!1" "ii!1-1" )"1" (assert )"1" (case " FF >= 0 AND FF <= 1" )"1" (flatten)"1" (assert )"1" "1" assert )"1" expand "abs" )"1" "1" assert )"1" "FF = 0" )"1" (assert ) nil nil )"2" "FF" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "xis!1`seq(ii!1-1)" )"1" (ground) nil nil )"2" (assert )"2" "xis!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "xis!1" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" integral_def nil )"bool" integral_def nil )nil integral_def nil )"posreal" integral_def nil )nil integral_def nil ))nil )nil 3262440806"" (skosimp*)"" (expand "section" )"" (typepred "P!1" )"" (inst - "ii!1-1" )"1" "FF" "f!1(x_in(seq(P!1)(ii!1 - 1), seq(P!1)(ii!1)))" )"1" (replace -1)"1" (lemma "width_lem" )"1" (expand "finseq_appl" )"1" (inst -1 "a!1" "b!1" "P!1" "ii!1-1" )"1" (assert )"1" (case " FF >= 0 AND FF <= 1" )"1" (flatten)"1" (assert )"1" (mult-ineq -2 -3)"1" assert )"1" expand "abs" )"1" "1" assert )"1" "FF = 0" )"1" (assert ) nil nil )"2" "FF" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x_in(seq(P!1)(ii!1-1), seq(P!1)(ii!1))" )"2" (ground) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (propax) nil nil )"4" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"posreal" integral_def nil )nil integral_def nil )"{t: T | aa <= t AND t <= bb}" integral_def nil )nil integral_def nil ))nil 3262529445"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3282559921"" (auto-rewrite "xis?" )"" (auto-rewrite "xis_lem" )"" (skosimp*)"" (rewrite "integral_def" )"" (expand "integral?" )"" (skosimp*)"" (inst + "epsi!1/1000" )"" (skosimp*)"" (typepred "R!1" )"" (expand "Riemann_sum?" )"" (skosimp*)"" (replace -1)"" (hide -1)"" (lemma "Rie_sum_alt_lem" )"" "a!1" "b!1" "f!1" )"" assert )"" "" replace -1)"" "" "N" "length(P!1)" )"" case "(EXISTS (k: below(N-1)): xl!1 < seq(P!1)(k) AND seq(P!1)(k+1) < xh!1)" )"1" "1" case "EXISTS (p,q: nat): p >= 1 AND p <= length(P!1) -1 AND seq(P!1)(p-1) <= xl!1 AND xl!1 < seq(P!1)(p)AND q >= 1 AND q <= length(P!1) - 1AND seq(P!1)(q-1) < xh!1 AND xh!1 <= seq(P!1)(q) AND p+1 <= q-1") "1" "1" expand "Rie_sum_alt" )"1" expand "Rie_sec" )"1" assert )"1" "SEC" " LAMBDA (n: upto(length(P!1) - 1)): IF n = 0 THEN 0") "1" replace "1" "SS" "sigma[upto(length(P!1) - 1)](1, length(P!1) - 1, SEC)" )"1" replace "1" case "sigma(p!1+1,q!1-1,SEC) <= SS AND SS <= sigma(p!1,q!1,SEC)" )"1" "1" case "sigma(p!1+1, q!1 - 1, SEC) = seq(P!1)(q!1-1) - seq(P!1)(p!1)" )"1" case "sigma(p!1, q!1, SEC) <= seq(P!1)(q!1) - seq(P!1)(p!1-1)" )"1" "abs(-1 * SS - xl!1 + xh!1) = abs(SS - xh!1 + xl!1)" )"1" "1" expand "abs" )"1" "1" "1" "width_lem" )"1" expand "finseq_appl" )"1" "a!1" "b!1" "P!1" "p!1-1" )"1" "a!1" "b!1" "P!1" "p!1" )"1" "a!1" "b!1" "P!1" "q!1-1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "abs_neg" )"2" "SS - xh!1 + xl!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "EX3p" )"2" "a!1" "b!1" )"2" "2" assert )"2" "P!1" "p!1" "q!1" )"2" assert )"2" assert )"2" replace "2" rewrite "sigma_le" )"1" "1" "1" replace "1" assert )"1" "1" case "f!1(xis!1(n!1 - 1)) <= 1" )"1" assert )"1" "seq(P!1)(n!1) - seq(P!1)(n!1 - 1)" )"1" assert )nil nil )"2" "2" "xis!1" )"2" assert )"2" "n!1-1" )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "xis!1(n!1 - 1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "EX3p" )"2" "a!1" "b!1" )"2" assert )"2" "P!1" "p!1+1" "q!1-1" )"2" assert )"2" case "1 + p!1 <= q!1 - 1" )"1" assert )"1" "1" replace "1" "1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" "1" "1" "1" replace "1" assert )"1" "xis!1(x!1 - 1)" )"1" "1" "parts_order" )"1" "a!1" "b!1" "P!1" "p!1" "x!1-1" )"1" "a!1" "b!1" "P!1" "x!1" "q!1-1" )"1" quality 100%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
