| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 283 B |
|
Quelle sort_seq_lems.pvsSprache: PVS |
|||||||||||||||
|
sort_seq_lems[T: TYPE+, <= : (total_order?[T]) ]: THEORY BEGIN IMPORTING sort_seq[T,<=], min_seq[T,<=], max_seq[T,<=] s: VAR ne_seqs sort_seq_min : LEMMA seq(sort(s))(0) = min(s) sort_seq_max : LEMMA seq(sort(s))(length(s)-1) = max(s) END sort_seq_lems
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-14) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09