| 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 789 B |
|
Quelle csequence_prefix_append.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Prefix of an appended sequence 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_prefix_append[T: TYPE]: THEORY BEGIN IMPORTING csequence_prefix[T], csequence_append[T] prefix_append_eta: THEOREM FORALL (fseq: finite_csequence), (t: T): prefix(append(t, fseq), length(fseq)) = fseq END csequence_prefix_append ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28