:: Adjacency Concept for Pairs of Natural Numbers :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received June 10, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, ARYTM_3, XXREAL_0, ARYTM_1, CARD_1, FINSEQ_2, FINSEQ_1, FUNCT_1, RELAT_1, PARTFUN1, NAT_1, TARSKI, ORDINAL4, MATRIX_1, ZFMISC_1, GOBRD10, CHORD; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, MATRIX_0, XXREAL_0; constructors NAT_1, NAT_D, MATRIX_0, FUNCOP_1, RELSET_1; registrations SUBSET_1, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, XBOOLE_0, FINSEQ_1, FINSEQ_2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve i,j,k,k1,k2,n,m,i1,i2,j1,j2 for Element of NAT, x for set; definition let i1,i2 be Nat; pred i1,i2 are_adjacent means :: GOBRD10:def 1 i2=i1+1 or i1=i2+1; symmetry; irreflexivity; end; notation let i,j be Nat; antonym i,j aren't_adjacent for i,j are_adjacent; end; theorem :: GOBRD10:1 for i1,i2 being Nat st i1,i2 are_adjacent holds i1+1,i2+1 are_adjacent; theorem :: GOBRD10:2 for i1,i2 being Nat st i1,i2 are_adjacent & 1<=i1 & 1<=i2 holds i1-'1,i2-'1 are_adjacent; definition let i1,j1,i2,j2 be Nat; pred i1,j1,i2,j2 are_adjacent means :: GOBRD10:def 2 i1,i2 are_adjacent & j1=j2 or i1=i2 & j1,j2 are_adjacent; end; theorem :: GOBRD10:3 for i1,i2,j1,j2 being Nat st i1,j1,i2,j2 are_adjacent holds i1+1,j1+1,i2+1,j2+1 are_adjacent; theorem :: GOBRD10:4 for i1,i2,j1,j2 being Nat st i1,j1,i2,j2 are_adjacent & 1<=i1 & 1<=i2 & 1<=j1 & 1<=j2 holds i1-'1,j1-'1,i2-'1,j2-'1 are_adjacent; theorem :: GOBRD10:5 for n,i,j st i<=n & j<=n holds ex fs1 being FinSequence of NAT st fs1.1=i & fs1.(len fs1)=j & len fs1=(i-'j)+(j-'i)+1 & (for k,k1 st 1<=k & k<= len fs1 & k1=fs1.k holds k1<=n) & for i1 st 1<=i1 & i1