| 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 |
|
Impressum csequence_sequence.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Conversions between sequences of countable length and the prelude sequence % type. % % 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_sequence[T: TYPE]: THEORY BEGIN IMPORTING sequences[T], csequence_nth[T] IMPORTING csequence_codt_coreduce[T, sequence] n: VAR nat seq: VAR sequence iseq: VAR infinite_csequence % Convert a sequence to an infinite_csequence from_sequence_struct(seq): csequence_struct = inj_add(seq(0), LAMBDA n: seq(1 + n)) from_sequence(seq): infinite_csequence = coreduce(from_sequence_struct)(seq) from_sequence_nth: THEOREM FORALL seq, n: nth(from_sequence(seq), n) = seq(n) % Convert an infinite_csequence to a sequence to_sequence(iseq): sequence = LAMBDA n: nth(iseq, n) to_sequence_nth: THEOREM FORALL iseq, n: to_sequence(iseq)(n) = nth(iseq, n) % Applying both conversions gives you back what you started with to_from_sequence: THEOREM FORALL seq: to_sequence(from_sequence(seq)) = seq from_to_sequence: THEOREM FORALL iseq: from_sequence(to_sequence(iseq)) = iseq END csequence_sequence ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.12Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28