| 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 1 kB |
|
Quelle csequence_singleton.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Singleton sequences, defined as coalgebraic datatypes. % % 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_singleton[T: TYPE]: THEORY BEGIN IMPORTING csequence_nth[T] t: VAR T p: VAR pred[T] n: VAR nat cseq: VAR csequence singleton_cseq?(cseq): bool = nonempty?(cseq) AND empty?(rest(cseq)) singleton_is_nonempty_finite: JUDGEMENT (singleton_cseq?) SUBTYPE_OF nonempty_finite_csequence singleton_cseq_length: THEOREM FORALL cseq: singleton_cseq?(cseq) IMPLIES length(cseq) = 1 singleton_cseq_index: THEOREM FORALL (single: (singleton_cseq?)), n: index?(single)(n) IFF n = 0 singleton_cseq(t): (singleton_cseq?) = add(t, empty_cseq) singleton_def: THEOREM FORALL cseq: singleton_cseq?(cseq) IMPLIES cseq = singleton_cseq(first(cseq)) singleton_cseq_first: THEOREM FORALL t: first(singleton_cseq(t)) = t singleton_cseq_rest: THEOREM FORALL t: rest(singleton_cseq(t)) = empty_cseq singleton_cseq_last: THEOREM FORALL t: last(singleton_cseq(t)) = t singleton_cseq_some: THEOREM FORALL t, p: some(p)(singleton_cseq(t)) IFF p(t) singleton_cseq_every: THEOREM FORALL t, p: every(p)(singleton_cseq(t)) IFF p(t) END csequence_singleton ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28