products/sources/formale sprachen/PVS/co_structures/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: root.tex   Sprache: PVS

Original von: PVS©
%-----------------------------------------------------------------------------
% The combination of the merge and split operators on sequences of countable
% length.
%
% Author: Jerry James <[email protected]>
%
% 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_merge_split[T: TYPE]: THEORY
 BEGIN

  IMPORTING csequence_merge[T], csequence_split[T]

  cseq, cseq1, cseq2: VAR csequence

  merge_split_eta: THEOREM FORALL cseq: merge(split(cseq)) = cseq

  split_merge_eta: THEOREM
    FORALL cseq1, cseq2:
      length_eq(cseq1, cseq2) IMPLIES
       split(merge(cseq1, cseq2)) = (cseq1, cseq2)

 END csequence_merge_split

¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff