| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle step_fun_scaf.pvs Sprache: PVS |
|||||||||
|
step_fun_scaf[T: TYPE+ FROM real]: THEORY
BEGIN ASSUMING IMPORTING deriv_domain_def[T] connected_domain : ASSUMPTION connected?[T] not_one_element : ASSUMPTION not_one_element?[T] ENDASSUMING % AUTO_REWRITE+ not_one_element IMPORTING integral_step, partitions_scaf[T] a,b,c,d,x,y,z: VAR T f,f1,f2,g: VAR [T -> real] eps, delta: VAR posreal xv,yv: VAR real UP_prep: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b)): LET UP = union[T](part2set(a,b,P1), part2set(a,b,P2)) IN card(UP) > 1 AND UP(a) AND UP(b) UnionPart(a:T,b:{x:T|a<x},P1,P2: partition[T](a,b)): partition[T](a,b) = set2part(union(part2set(a, b, P1), part2set(a, b, P2))) UnionPart_lem: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b), kk: below(length(P1)-1)): EXISTS (nn: below(length(UnionPart(a,b,P1,P2)))): UnionPart(a,b,P1,P2)`seq(nn) = P1`seq(kk) Union_sym: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b)): UnionPart(a,b,P1,P2) = UnionPart(a,b,P2,P1) Union_lem: LEMMA FORALL (a:T, b: {x:T|a<x}, P1,P2: partition[T](a, b), nn: below(length(UnionPart(a,b,P1,P2))-1)): in_sect?(a,b,UnionPart(a,b,P1,P2),nn,x) IMPLIES (EXISTS (kk: below(length(P1)-1)): seq(P1)(kk) <= UnionPart(a,b,P1,P2)(nn) AND UnionPart(a,b,P1,P2)(nn+1) <= seq(P1)(kk+1) ) END step_fun_scaf ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28