Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: code_product.pvs Sprache: PVS

Original von: PVS^©

%-------------------------------------------------------------------------
% code product
%
%     Author: David Lester, Manchester University
%
%     Version 1.0           04/05/09    Initial (DRL)
%
%
% Diagonal traversal (through the indices of a doubly-indexed set)
%
% For the first ten naturals we get:
%    (double_index_i(n),double_index_j(n)) =
%   (0,0),(1,0),(0,1),(2,0),(1,1),(0,2),(3,0),(2,1),(1,2),(0,3),(4,0)
% and so on...
%-------------------------------------------------------------------------

code_product: THEORY

BEGIN

  IMPORTING reals@sqrt % proof only

  i,j,n,m: VAR nat

  double_index_n(i,j):nat = ((i+j)*(1+i+j))/2 + j

  double_index_triangle(n):nat = {i | (i*(i+1))/2 <= n AND n < ((i+1)*(i+2))/2}

  double_index_triangle_def: LEMMA
    (double_index_triangle(n)*(double_index_triangle(n)+1))/2 <= n AND
    n < ((double_index_triangle(n)+1)*(double_index_triangle(n)+2))/2

  double_index_triangle_increasing: LEMMA
    FORALL i,j: i <= j => double_index_triangle(i) <= double_index_triangle(j)

  double_index_triangle_bound:      LEMMA double_index_triangle(n) <= n

  double_index_j(n):nat
    = n - (double_index_triangle(n)*(double_index_triangle(n)+1))/2

  double_index_j_bound: LEMMA double_index_j(n) <= double_index_triangle(n)

  double_index_i(n):nat = double_index_triangle(n)-double_index_j(n)

  double_index_i_bound: LEMMA double_index_i(n) <= double_index_triangle(n)

  double_index_n_increasing: LEMMA
    FORALL n,m: n < m => double_index_n(n,j) < double_index_n(m,j)

  double_index_n_ij: LEMMA
    double_index_n(double_index_i(n),double_index_j(n)) = n

  double_index_ij_n: LEMMA
    double_index_i(double_index_n(i,j)) = i AND
    double_index_j(double_index_n(i,j)) = j

  double_index_n_bijective: LEMMA bijective?[[nat,nat],nat](double_index_n)

END code_product

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.