| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/co_structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle csequence_length_comp.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Operators for convenience in writing length comparisons that include % possibly infinite csequences. % % It might be nicer to have an "extended nat" type that includes a special % "infinity" value. Then we could define the length operator on all % sequences, which would simplify some other definitions. If you are % interested in trying this approach, please contact me. % % Author: Jerry James <loganjerry@gmail.com> % % This file and its accompanying proof file are distributed under the CC0 1.0 % Universal license: http://creativecommons.org/publicdomain/zero/1.0/. % % Version history: % 2007 Feb 14: PVS 4.0 version % 2011 May 6: PVS 5.0 version % 2013 Jan 14: PVS 6.0 version %----------------------------------------------------------------------------- csequence_length_comp[T1, T2: TYPE]: THEORY BEGIN IMPORTING csequence_length[T1], csequence_length[T2] cseq1: VAR csequence[T1] cseq2: VAR csequence[T2] nseq1: VAR nonempty_csequence[T1] nseq2: VAR nonempty_csequence[T2] length_lt(cseq1, cseq2): bool = is_finite(cseq1) AND (is_finite(cseq2) IMPLIES length(cseq1) < length(cseq2)) length_le(cseq1, cseq2): bool = is_finite(cseq2) IMPLIES is_finite(cseq1) AND length(cseq1) <= length(cseq2) length_eq(cseq1, cseq2): bool = (is_infinite(cseq1) AND is_infinite(cseq2)) OR (is_finite(cseq1) AND is_finite(cseq2) AND length(cseq1) = length(cseq2)) length_ge(cseq1, cseq2): bool = is_finite(cseq1) IMPLIES is_finite(cseq2) AND length(cseq1) >= length(cseq2) length_gt(cseq1, cseq2): bool = is_finite(cseq2) AND (is_finite(cseq1) IMPLIES length(cseq1) > length(cseq2)) length_lt_le: THEOREM FORALL cseq1, cseq2: length_lt(cseq1, cseq2) IMPLIES length_le(cseq1, cseq2) length_gt_ge: THEOREM FORALL cseq1, cseq2: length_gt(cseq1, cseq2) IMPLIES length_ge(cseq1, cseq2) length_eq_le: THEOREM FORALL cseq1, cseq2: length_eq(cseq1, cseq2) IMPLIES length_le(cseq1, cseq2) length_eq_ge: THEOREM FORALL cseq1, cseq2: length_eq(cseq1, cseq2) IMPLIES length_ge(cseq1, cseq2) length_lt_neq: THEOREM FORALL cseq1, cseq2: length_lt(cseq1, cseq2) IMPLIES NOT length_eq(cseq1, cseq2) length_gt_neq: THEOREM FORALL cseq1, cseq2: length_gt(cseq1, cseq2) IMPLIES NOT length_eq(cseq1, cseq2) length_eq_empty: THEOREM FORALL cseq1, cseq2: length_eq(cseq1, cseq2) IMPLIES (empty?(cseq1) IFF empty?(cseq2)) length_eq_rest: THEOREM FORALL nseq1, nseq2: length_eq(nseq1, nseq2) IFF length_eq(rest(nseq1), rest(nseq2)) END csequence_length_comp ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28