| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/co_structures/ (PVS Prover Version 6.0.9©) Datei vom 28.9.2014 mit Größe 789 B |
|
Quelle csequence_prefix_append.pvsSprache: 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.13 Sekunden (vorverarbeitet am 2026-06-14) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-09