| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ACCoRD/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 996 B |
|
Quelle divergence.pvs Sprache: PVS |
|||||||||
|
%
% Divergence % divergence[D:posreal] : THEORY BEGIN IMPORTING horizontal, predicate_coordination_2D s : VAR Vect2 v,vo,vi, nv,nw : VAR Vect2 nvo,nvi : VAR Vect2 eps : VAR Sign divergence_crit?: Criterion_2D = (LAMBDA (s,v,eps): (LAMBDA (nv): s*nv > 0)) divergence_pred?: Vector_Predicate_2D = (LAMBDA (s,v): (LAMBDA (nv): NOT divergent?(s,nv divergence_crit_oriented: LEMMA symmetric_oriented_2D?(divergence_crit?) divergence_crit_sum_indep: LEMMA sum_independent_2D?(divergence_crit?, divergence_p divergence_pred_sum_closed: LEMMA sum_closed_2D?(divergence_pred?) divergence_crit_coordinated: LEMMA coordinated_oriented_2D?(divergence_crit?,diver divergence_crit_coordinated2: LEMMA NOT divergent?(s, zero, vo - vi, zero) AND divergence_crit?(s, vo - vi, eps)(nvo - vi) AND divergence_crit?(-s, vi - vo, eps)(nvi - vo) IMPLIES divergent?(s, zero, nvo - nvi, zero) END divergence ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28