%-------------------------------------------------------------------------
% doubly index sequences
%
%     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...
%-------------------------------------------------------------------------
double_index[T:TYPE]: THEORY

BEGIN

  IMPORTING code_product

  i,j,n: VAR nat
  u: VAR [[nat,nat]->T]
  v: VAR [nat->T]

  single_index(u):[nat->T] = (lambda n: u(double_index_i(n),double_index_j(n)))

  double_index(v):[[nat,nat]->T] = v o double_index_n

  single_double: LEMMA single_index(double_index(v)) = v

  double_single: LEMMA double_index(single_index(u)) = u

END double_index