|
%-------------------------------------------------------------------------
% 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.19 Sekunden
(vorverarbeitet)
¤
|
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.
|
