Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Tools/Code/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 23 kB

Quellcode-Bibliothek 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

quality97%

¤ 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.7Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.