| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/extended_nnreal/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle 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 ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28