| 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_strict_prefix.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Proper prefixes of sequences of countable length. % % 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_strict_prefix[T: TYPE]: THEORY BEGIN IMPORTING csequence_prefix[T] p: VAR pred[T] n: VAR nat cseq, cseq1, cseq2: VAR csequence nseq: VAR nonempty_csequence fseq: VAR finite_csequence strict_prefix?(cseq1, cseq2): INDUCTIVE bool = nonempty?(cseq2) AND (empty?(cseq1) OR (first(cseq1) = first(cseq2) AND strict_prefix?(rest(cseq1), rest(cseq2)))) strict_prefix?(cseq2)(cseq1): MACRO bool = strict_prefix?(cseq1, cseq2) strict_prefix?_prefix?: THEOREM FORALL cseq1, cseq2: strict_prefix?(cseq1, cseq2) IFF prefix?(cseq1, cseq2) AND cseq1 /= cseq2 strict_prefix?_finite: THEOREM FORALL cseq1, cseq2: strict_prefix?(cseq1, cseq2) IMPLIES is_finite(cseq1) strict_prefix?_first: THEOREM FORALL nseq, cseq: strict_prefix?(nseq, cseq) IMPLIES first(nseq) = first(cseq) strict_prefix?_rest: THEOREM FORALL nseq, cseq: strict_prefix?(nseq, cseq) IMPLIES strict_prefix?(rest(nseq), rest(cseq)) strict_prefix?_length: THEOREM FORALL cseq, fseq: strict_prefix?(cseq, fseq) IMPLIES length(cseq) < length(fseq) strict_prefix?_index: THEOREM FORALL cseq1, cseq2, n: strict_prefix?(cseq1, cseq2) AND index?(cseq1)(n) IMPLIES index?(cseq2)(n) strict_prefix?_nth: THEOREM FORALL cseq1, cseq2, (n: indexes(cseq1)): strict_prefix?(cseq1, cseq2) IMPLIES nth(cseq1, n) = nth(cseq2, n) strict_prefix?_concatenate: THEOREM FORALL fseq, nseq: strict_prefix?(fseq, fseq o nseq) strict_prefix?_def: THEOREM FORALL cseq1, cseq2: strict_prefix?(cseq1, cseq2) IFF is_finite(cseq1) AND (EXISTS nseq: cseq1 o nseq = cseq2) strict_prefix?_is_strict_order: JUDGEMENT strict_prefix? HAS_TYPE (strict_order?[csequence]) % Strict prefixes of a given sequence are well-ordered strict_prefix?_well_ordered: THEOREM FORALL cseq: well_ordered?(restrict [[csequence, csequence], [(strict_prefix?(cseq)), (strict_prefix?(cseq))], bool] (strict_prefix?)) strict_prefix?_prefix: THEOREM FORALL cseq1, cseq2: strict_prefix?(cseq1, cseq2) IFF (EXISTS n: cseq1 = prefix(cseq2, n) AND (is_finite(cseq2) IMPLIES n < length(cseq2))) END csequence_strict_prefix ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28