| 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 3 kB |
|
Quelle csequence_unzip.pvs Sprache: PVS |
|||||||||
|
%-----------------------------------------------------------------------------
% Unzip a countable sequence of pairs into a pair of sequences. % % 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_unzip[T1, T2: TYPE]: THEORY BEGIN IMPORTING csequence_nth[T1], csequence_nth[T2], csequence_nth[[T1, T2]] IMPORTING csequence_codt_coreduce[T1, csequence[[T1, T2]]] IMPORTING csequence_codt_coreduce[T2, csequence[[T1, T2]]] IMPORTING csequence_codt_map[[T1, T2], T1] IMPORTING csequence_codt_map[[T1, T2], T2] n: VAR nat t12: VAR [T1, T2] p1: VAR pred[T1] p2: VAR pred[T2] cseq, cseq1, cseq2: VAR csequence[[T1, T2]] fseq: VAR finite_csequence[[T1, T2]] iseq: VAR infinite_csequence[[T1, T2]] nseq: VAR nonempty_csequence[[T1, T2]] nfseq: VAR nonempty_finite_csequence[[T1, T2]] unzip_left_struct(cseq): csequence_struct[T1, csequence[[T1, T2]]] = IF empty?(cseq) THEN inj_empty_cseq ELSE inj_add(first(cseq)`1, rest(cseq)) ENDIF unzip_right_struct(cseq): csequence_struct[T2, csequence[[T1, T2]]] = IF empty?(cseq) THEN inj_empty_cseq ELSE inj_add(first(cseq)`2, rest(cseq)) ENDIF unzip(cseq): [csequence[T1], csequence[T2]] = (coreduce(unzip_left_struct)(cseq), coreduce(unzip_right_struct)(cseq)) unzip_finite: JUDGEMENT unzip(fseq) HAS_TYPE [finite_csequence[T1], finite_csequence[T2]] unzip_infinite: JUDGEMENT unzip(iseq) HAS_TYPE [infinite_csequence[T1], infinite_csequence[T2]] unzip_nonempty: JUDGEMENT unzip(nseq) HAS_TYPE [nonempty_csequence[T1], nonempty_csequence[T2]] unzip_empty_left: THEOREM FORALL cseq: empty?(unzip(cseq)`1) IFF empty?(cseq) unzip_empty_right: THEOREM FORALL cseq: empty?(unzip(cseq)`2) IFF empty?(cseq) unzip_first_left: THEOREM FORALL nseq: first(unzip(nseq)`1) = first(nseq)`1 unzip_first_right: THEOREM FORALL nseq: first(unzip(nseq)`2) = first(nseq)`2 unzip_rest_left: THEOREM FORALL nseq: rest(unzip(nseq)`1) = unzip(rest(nseq))`1 unzip_rest_right: THEOREM FORALL nseq: rest(unzip(nseq)`2) = unzip(rest(nseq))`2 unzip_length_left: THEOREM FORALL fseq: length(unzip(fseq)`1) = length(fseq) unzip_length_right: THEOREM FORALL fseq: length(unzip(fseq)`2) = length(fseq) unzip_index_left: THEOREM FORALL cseq, n: index?(unzip(cseq)`1)(n) IFF index?(cseq)(n) unzip_index_right: THEOREM FORALL cseq, n: index?(unzip(cseq)`2)(n) IFF index?(cseq)(n) unzip_nth_left: THEOREM FORALL cseq, (n: indexes(cseq)): nth(unzip(cseq)`1, n) = nth(cseq, n)`1 unzip_nth_right: THEOREM FORALL cseq, (n: indexes(cseq)): nth(unzip(cseq)`2, n) = nth(cseq, n)`2 unzip_map: THEOREM FORALL cseq: unzip(cseq) = (map[[T1, T2], T1](PROJ_1, cseq), map[[T1, T2], T2](PROJ_2, cseq)) unzip_extensionality: THEOREM FORALL cseq1, cseq2: unzip(cseq1) = unzip(cseq2) IMPLIES cseq1 = cseq2 unzip_add: THEOREM FORALL cseq, t12: unzip(add(t12, cseq)) = (add(t12`1, unzip(cseq)`1), add(t12`2, unzip(cseq)`2)) unzip_last_left: THEOREM FORALL nfseq: last(unzip(nfseq)`1) = last(nfseq)`1 unzip_last_right: THEOREM FORALL nfseq: last(unzip(nfseq)`2) = last(nfseq)`2 unzip_some: THEOREM FORALL cseq, p1, p2: some(p1)(unzip(cseq)`1) OR some(p2)(unzip(cseq)`2) IFF some(LAMBDA t12: p1(t12`1) OR p2(t12`2))(cseq) unzip_every: THEOREM FORALL cseq, p1, p2: every(p1)(unzip(cseq)`1) AND every(p2)(unzip(cseq)`2) IFF every(LAMBDA t12: p1(t12`1) AND p2(t12`2))(cseq) END csequence_unzip ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28