Quellcode-Bibliothek code_product.pvs Sprache: 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

quality89%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.