| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/HOLCF/Library/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 6 kB |
|
Quelle fseqs_aux_vertical.pvs Sprache: PVS |
|||||||||
|
fseqs_aux_vertical[vsmin,vsmax:real] : THEORY
BEGIN IMPORTING structures@sort_fseq[real,<=], structures@fseqs_ops[real], trig_fnd@to2pi vs,fs : VAR fseq %%%%% Vertical Speed %%%%% vs_fseq?(vs): bool = FORALL (i:below(vs`length)): vsmin<=vs`seq(i) AND vs`seq(i)<=vsmax vsb,vsb1,vsb2 : VAR (vs_fseq?) empty_vs_fseq : JUDGEMENT emptyseq HAS_TYPE (vs_fseq?) comp_vs_fseq : JUDGEMENT o(vsb1,vsb2) HAS_TYPE (vs_fseq?) sort_vs_fseq : JUDGEMENT sort(vsb) HAS_TYPE (vs_fseq?) END fseqs_aux_vertical ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28