| 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 |
|
Quellcodebibliothek csequence_add.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Properties of the add operator on sequences of countable length 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_add[T: TYPE]: THEORY BEGIN IMPORTING csequence_nth[T] n: VAR nat t: VAR T p: VAR pred[T] cseq: VAR csequence fseq: VAR finite_csequence iseq: VAR infinite_csequence add_finite: JUDGEMENT add(t, fseq) HAS_TYPE nonempty_finite_csequence add_infinite: JUDGEMENT add(t, iseq) HAS_TYPE infinite_csequence add_length: THEOREM FORALL t, fseq: length(add(t, fseq)) = length(fseq) + 1 add_index: THEOREM FORALL t, cseq, n: index?(add(t, cseq))(n) IFF n = 0 OR index?(cseq)(n - 1) add_nth: THEOREM FORALL t, cseq, (n: indexes(cseq)): nth(add(t, cseq), n + 1) = nth(cseq, n) add_last: THEOREM FORALL t, fseq: last(add(t, fseq)) = IF empty?(fseq) THEN t ELSE last(fseq) ENDIF add_some: THEOREM FORALL t, cseq, p: some(p)(add(t, cseq)) IFF p(t) OR some(p)(cseq) add_every: THEOREM FORALL t, cseq, p: every(p)(add(t, cseq)) IFF p(t) AND every(p)(cseq) END csequence_add ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28