:: Adjacency Concept for Pairs of Natural Numbers :: by Yatsuka Nakamura and Andrzej Trybulec :: :: Received June 10, 1996 :: Copyright (c) 1996-2019 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; definitions TARSKI; equalities FINSEQ_2; theorems TARSKI, NAT_1, FINSEQ_1, FINSEQ_4, FUNCT_1, FINSEQ_2, FINSEQ_3, ZFMISC_1, XREAL_1, XXREAL_0, PARTFUN1, XREAL_0, NAT_D, CARD_1; schemes NAT_1, FINSEQ_1, FINSEQ_2; 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 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 for i1,i2 being Nat st i1,i2 are_adjacent holds i1+1,i2+1 are_adjacent; theorem Th2: for i1,i2 being Nat st i1,i2 are_adjacent & 1<=i1 & 1<=i2 holds i1-'1,i2-'1 are_adjacent proof let i1,i2 be Nat; assume that A1: i1,i2 are_adjacent and A2: 1<=i1 and A3: 1<=i2; 0<=i1-1 by A2,XREAL_1:48; then A4: i1-'1=i1-1 by XREAL_0:def 2; 0<=i2-1 by A3,XREAL_1:48; then A5: i2-'1=i2-1 by XREAL_0:def 2; i2=i1+1 or i1=i2+1 by A1; then i2-1=i1-1+1 or i1-1=i2-1+1; hence thesis by A4,A5; end; definition let i1,j1,i2,j2 be Nat; pred i1,j1,i2,j2 are_adjacent means i1,i2 are_adjacent & j1=j2 or i1=i2 & j1,j2 are_adjacent; end; theorem Th3: 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 proof let i1,i2,j1,j2 be Nat; assume i1,j1,i2,j2 are_adjacent; then i1,i2 are_adjacent & j1=j2 or i1=i2 & j1,j2 are_adjacent; then i1+1,i2+1 are_adjacent & j1+1=j2+1 or i1+1=i2+1 & j1+1,j2+1 are_adjacent; hence thesis; end; theorem 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 by Th2; Lm1: for n,i,j st 1 <= j & j <= n holds (n|->i).j = i by FINSEQ_1:1,FINSEQ_2:57; theorem Th5: 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 & i10 by A3,XREAL_1:50; then A5: j-i+1>0+1 by XREAL_1:6; then j+1-i>=0; then A6: (j+1)-'i=j-i+1 by XREAL_0:def 2; then A7: i+(j+1-'i)-'1=i+(j+1-'i)-1 by XREAL_0:def 2; deffunc F(Nat) = i+$1-'1; ex p being FinSequence st len p = (j+1)-'i & for k be Nat st k in dom p holds p.k=F(k) from FINSEQ_1:sch 2; then consider p being FinSequence such that A8: len p = (j+1)-'i and A9: for k be Nat st k in dom p holds p.k=i+k-'1; j-i>=i-i by A3,XREAL_1:9; then A10: len p=(i-'j)+(j-'i)+1 by A8,A6,A4,XREAL_0:def 2; A11: (j+1)-'i=j+1-i by A5,XREAL_0:def 2; then 1 in dom p by A5,A8,FINSEQ_3:25; then p.1=i+1-'1 by A9; then A12: p.1=i by NAT_D:34; rng p c=NAT proof let x be object; assume x in rng p; then consider y being object such that A13: y in dom p and A14: p.y=x by FUNCT_1:def 3; y in Seg len p by A13,FINSEQ_1:def 3; then y in {k where k is Nat:1<=k & k<=len p} by FINSEQ_1:def 1; then consider k being Nat such that A15: k=y and 1<=k and k<=len p; p.k=i+k-'1 by A9,A13,A15; hence thesis by A14,A15; end; then reconsider fs2=p as FinSequence of NAT by FINSEQ_1:def 4; A16: for i1 st 1<=i1 & i1=1 by NAT_1:11; then 1+(i+i1)-1>=1-1 by XREAL_1:9; then A21: (1+(i+i1))-'1=i+i1 by XREAL_0:def 2; i+i1>=1+0 by A17,XREAL_1:7; then i+i1-1>=1-1 by XREAL_1:9; then A22: 1+(i+i1-'1)=1+(i+i1-1) by XREAL_0:def 2 .=i+i1; i1 in dom fs2 & fs2/.i1 = fs2.i1 by A17,A18,FINSEQ_3:25,FINSEQ_4:15; hence thesis by A9,A20,A22,A21; end; A23: for k,k1 st 1<=k & k<=len p & k1=p.k holds k1<=n proof let k,k1; assume that A24: 1<=k and A25: k<=len p and A26: k1=p.k; k in dom p by A24,A25,FINSEQ_3:25; then A27: k1=k+i-'1 by A9,A26; k+i-1=k+(i-1); then 1+(i-1)<=k+i-1 by A24,XREAL_1:6; then A28: k1=k+i-1 by A27,XREAL_0:def 2; k+i<=(j+1)-'i +i by A8,A25,XREAL_1:6; then k+i<=j+1-i+i by A5,XREAL_0:def 2; then k1<=j+1-1 by A28,XREAL_1:9; hence thesis by A2,XXREAL_0:2; end; len p in dom p by A5,A8,A11,FINSEQ_3:25; then p.(len p)=j by A8,A9,A11,A7; hence thesis by A23,A12,A10,A16; end; case A29: i=j; then i-j=0; then A30: i-'j=0 by XREAL_0:def 2; consider f being Function such that A31: dom f=Seg 1 and A32: rng f={i} by FUNCT_1:5; rng f c=NAT & f is FinSequence-like by A31,A32,FINSEQ_1:def 2,ZFMISC_1:31 ; then reconsider fs1=f as FinSequence of NAT by FINSEQ_1:def 4; A33: for i1 st 1<=i1 & i1=j-j by XREAL_1:9; A38: now per cases by A37; case i-j=0; hence j-'i=0 by XREAL_0:def 2; end; case i-j>0; then --(i-j)>0; then j-i<0; hence j-'i=0 by XREAL_0:def 2; end; end; j-i=0; i-j>0 by A36,XREAL_1:50; then A41: i-j+1>0+1 by XREAL_1:6; then A42: i+1-(i+1-'j)=i+1-(i+1-j) by XREAL_0:def 2 .=j; ex p being FinSequence st len p = i+1-'j & for k be Nat st k in dom p holds p.k=F(k) from FINSEQ_1:sch 2; then consider p being FinSequence such that A43: len p = i+1-'j and A44: for k be Nat st k in dom p holds p.k=i+1-'k; A45: i+1-'j=i+1-j by A41,XREAL_0:def 2; then 1 in dom p by A41,A43,FINSEQ_3:25; then p.1=i+1-'1 by A44; then A46: p.1=i by A40,XREAL_0:def 2; rng p c=NAT proof let x be object; assume x in rng p; then consider y being object such that A47: y in dom p and A48: p.y=x by FUNCT_1:def 3; y in Seg len p by A47,FINSEQ_1:def 3; then y in {k where k is Nat:1<=k & k<=len p} by FINSEQ_1:def 1; then consider k being Nat such that A49: k=y and A50: 1<=k & k<=len p; k in dom p by A50,FINSEQ_3:25; then p.k=i+1-'k by A44; hence thesis by A48,A49; end; then reconsider fs2=p as FinSequence of NAT by FINSEQ_1:def 4; i-j+1>=0+1 by A37,XREAL_1:6; then A51: i+1-j>=0; A52: for i1 st 1<=i1 & i1=1-1 by XREAL_1:9; set hs1=gs1^((len gs2-'1) |-> i2), hs2=((len gs1-'1) |-> j1)^gs2; A17: len hs1=len gs1 + len ((len gs2-'1) |-> i2) by FINSEQ_1:22 .=len gs1 + (len gs2-'1) by CARD_1:def 7 .=len gs1 + (len gs2-1) by A16,XREAL_0:def 2 .=(len gs1-1)+ len gs2; A18: 1<=len gs1 by A7,NAT_1:11; then A19: len gs1 -1>=1-1 by XREAL_1:9; then A20: (len gs1-1) + len gs2 =(len gs1-'1)+ len gs2 by XREAL_0:def 2 .=len ((len gs1-'1) |-> j1) + len gs2 by CARD_1:def 7 .=len hs2 by FINSEQ_1:22; A21: for i,k1,k2 st i in dom hs1 & k1=hs1.i & k2=hs2.i holds k1<=n & k2<=m proof dom hs2=Seg(len ((len gs1-'1) |-> j1)+ len gs2) by FINSEQ_1:def 7; then len hs2=len ((len gs1-'1) |-> j1) + len gs2 by FINSEQ_1:def 3; then A22: len hs2=(len gs1 -'1)+len gs2 by CARD_1:def 7; let i,k1,k2; assume that A23: i in dom hs1 and A24: k1=hs1.i and A25: k2=hs2.i; i in Seg len hs1 by A23,FINSEQ_1:def 3; then 1<=i & i<=len gs1-'1 or (len gs1 -'1)+1<=i & i<=len hs2 by A17,A20, FINSEQ_1:1,NAT_1:13; then 1<=i & i<=len gs1-'1 or len gs1-1+1<=i & i<=len hs2 by A19, XREAL_0:def 2; then 1<=i & i<=len gs1-1 or len gs1 -(len gs1-1)<=i-(len gs1-1) & i <=len hs2 by XREAL_0:def 2,XREAL_1:9; then 1<=i & i<=len gs1-1 or 1<=i-(len gs1-1) & i-(len gs1-1) <=len hs2-( len gs1-1) by XREAL_1:9; then A26: 1<=i & i<=len gs1-1 or 1<=i-len gs1+1 & i-len gs1+1 <=len hs2-len gs1 +1; A27: now per cases by A26,XREAL_1:6; case A28: 1<=i-len gs1+1 & i-len gs1 <=len hs2 - len gs1; then A29: i+1-len gs1<=len hs2 - len gs1+1 by XREAL_1:6; A30: len ((len gs1-'1) |-> j1)=len gs1-'1 by CARD_1:def 7; A31: len hs2+1 - len gs1=(len gs1 -1)+len gs2+1 - len gs1 by A19,A22, XREAL_0:def 2 .=len gs2; A32: i+1-len gs1=i+1-'len gs1 by A28,XREAL_0:def 2; i-len gs1+1<=len hs2 - len gs1+1 by A28,XREAL_1:6; then i+1-'len gs1 in Seg len gs2 by A28,A31,A32,FINSEQ_1:1; then A33: i+1-'len gs1 in dom gs2 by FINSEQ_1:def 3; i=len gs1-1+(i+1-len gs1) .=(len ((len gs1-'1) |-> j1)+(i+1-'len gs1)) by A19,A32,A30, XREAL_0:def 2; then hs2.i= gs2.(i+1-'len gs1) by A33,FINSEQ_1:def 7; hence k2<=m by A13,A25,A28,A29,A31,A32; end; case A34: 1<=i & i<=len gs1-1; then A35: i<=len gs1-'1 by XREAL_0:def 2; then i in Seg (len gs1 -'1) by A34,FINSEQ_1:1; then i in Seg len ((len gs1-'1) |-> j1) by CARD_1:def 7; then i in dom ((len gs1-'1) |-> j1) by FINSEQ_1:def 3; then hs2.i= ((len gs1-'1) |-> j1).i by FINSEQ_1:def 7 .=j1 by A34,A35,Lm1; hence k2<=m by A2,A25; end; end; dom hs1=Seg(len gs1 + len ((len gs2-'1) |-> i2)) by FINSEQ_1:def 7; then A36: len hs1=len gs1 + len ((len gs2-'1) |-> i2) by FINSEQ_1:def 3; then A37: len hs1 -' len gs1 = len hs1 - len gs1 by XREAL_0:def 2; A38: len hs1=len gs1 + (len gs2 -'1) by A36,CARD_1:def 7; A39: 1<=i & i<=len gs1 or len gs1 -len gs1 i2) by A44,CARD_1:def 7; then A47: (i-'len gs1) in dom ((len gs2-'1) |-> i2) by FINSEQ_1:def 3; i-'len gs1=i- len gs1 by A41,XREAL_0:def 2; then hs1.i= ((len gs2-'1) |-> i2).(i-'len gs1) by A47,A46, FINSEQ_1:def 7 .=i2 by A43,A45,Lm1; hence k1<=n by A3,A24; end; end; hence thesis by A27; end; A48: for i st 1<=i & ilen gs1-'1; 0+1<=i+1 by NAT_1:13; then A60: (i+1) in dom gs1 by A52,FINSEQ_3:25; A61: dom gs1 c= dom hs1 by FINSEQ_1:26; then A62: hs1/.(i+1)=hs1.(i+1) by A60,PARTFUN1:def 6 .=gs1.(i+1) by A60,FINSEQ_1:def 7 .=gs1/.(i+1)by A60,PARTFUN1:def 6; A63: i in dom gs1 by A49,A51,FINSEQ_3:25; then hs1/.i=hs1.i by A61,PARTFUN1:def 6 .=gs1.i by A63,FINSEQ_1:def 7 .=gs1/.i by A63,PARTFUN1:def 6; hence hs1/.i,hs1/.(i+1) are_adjacent by A9,A49,A51,A62; end; end; A64: 1<=i+1 by A49,NAT_1:13; A65: now per cases; case A66: i+1<=len gs1-'1; A67: len ((len gs1-'1) |-> j1)=len gs1-'1 by CARD_1:def 7; A68: dom ((len gs1-'1) |-> j1) c= dom hs2 by FINSEQ_1:26; i+1 in Seg (len gs1 -'1) by A64,A66,FINSEQ_1:1; then A69: i+1 in dom ((len gs1-'1) |-> j1) by A67,FINSEQ_1:def 3; then hs2.(i+1)= ((len gs1-'1) |-> j1).(i+1) by FINSEQ_1:def 7 .=j1 by A64,A66,Lm1; hence hs2/.(i+1)=j1 by A69,A68,PARTFUN1:def 6; end; case A70: i+1>len gs1-'1; A71: len gs1-'1+1=len gs1-1+1 by A7,XREAL_0:def 2 .=len gs1; len gs1-'1+1 <=i+1 by A70,NAT_1:13; then A72: len gs1=i+1 by A52,A71,XXREAL_0:1; dom hs2=Seg(len ((len gs1-'1) |-> j1)+len gs2) by FINSEQ_1:def 7; then len hs2=len ((len gs1-'1) |-> j1)+len gs2 by FINSEQ_1:def 3 .=(len gs1-'1)+len gs2 by CARD_1:def 7 .=len gs1-1+len gs2 by A7,XREAL_0:def 2 .=len gs1+(len gs2-1) .=len gs1+(len gs2-'1) by A12,XREAL_0:def 2; then len gs1 <= len hs2 by NAT_1:11; then len gs1 in Seg len hs2 by A18,FINSEQ_1:1; then A73: (i+1) in dom hs2 by A72,FINSEQ_1:def 3; 1 in Seg len gs2 by A15,FINSEQ_1:1; then A74: 1 in dom gs2 by FINSEQ_1:def 3; len ((len gs1-'1) |-> j1)+1=i+1 by A71,A72,CARD_1:def 7; then hs2.(i+1)=j1 by A10,A74,FINSEQ_1:def 7; hence hs2/.(i+1)=j1 by A73,PARTFUN1:def 6; end; end; A75: len ((len gs1-'1) |-> j1)=len gs1-'1 by CARD_1:def 7; A76: dom ((len gs1-'1) |-> j1) c= dom hs2 by FINSEQ_1:26; i+1-1<=len gs1 -1 by A52,XREAL_1:9; then A77: i<=len gs1-'1 by XREAL_0:def 2; then i in Seg (len gs1 -'1) by A49,FINSEQ_1:1; then A78: i in dom ((len gs1-'1) |-> j1) by A75,FINSEQ_1:def 3; then hs2.i= ((len gs1-'1) |-> j1).i by FINSEQ_1:def 7 .=j1 by A49,A77,Lm1; hence hs1/.i,hs1/.(i+1) are_adjacent & hs2/.i=hs2/.(i+1) or hs1/.i=hs1 /.(i+1) & hs2/.i,hs2/.(i+1) are_adjacent by A78,A76,A65,A53, PARTFUN1:def 6; end; case A79: i>=len gs1; then A80: 0<=i+1-len gs1 by NAT_1:12,XREAL_1:48; A81: len ((len gs1-'1) |-> j1)+(i+1-'len gs1+1) =(len gs1-'1)+(i+1-' len gs1+1) by CARD_1:def 7 .=len gs1 -1+(i+1-'len gs1+1) by A19,XREAL_0:def 2 .=len gs1 -1+(i+1-len gs1+1) by A80,XREAL_0:def 2 .=i+1; A82: i+1 =len gs1+(i+1-len gs1) .=len gs1+(i+1-'len gs1) by A80,XREAL_0:def 2; A83: i-len gs1>=0 by A79,XREAL_1:48; then 0+1<=i-len gs1 +1 by XREAL_1:6; then A84: 1<=i+1-'len gs1 by A80,XREAL_0:def 2; A85: i-len gs1=i-'len gs1 by A83,XREAL_0:def 2; A86: now assume not 1<=(i-'len gs1); then i-'len gs1<0+1; then A87: i-'len gs1=0 by NAT_1:13; len gs1 in Seg len gs1 by A7,FINSEQ_1:3; then i in dom gs1 by A85,A87,FINSEQ_1:def 3; hence hs1.i=i2 by A6,A85,A87,FINSEQ_1:def 7; end; A88: i+1-len gs1+len gs1<=len gs2 -1+len gs1 by A17,A50,NAT_1:13; then i+1-len gs1<=len gs2 -1 by XREAL_1:6; then i+1-len gs1<=len gs2 -'1 by XREAL_0:def 2; then A89: (i+1-'len gs1)<=len gs2-'1 by XREAL_0:def 2; i-len gs1+1>=0+1 by A83,XREAL_1:6; then A90: 1<=(i+1-'len gs1) by A88,XREAL_0:def 2; len ((len gs2-'1) |-> i2)=len gs2-'1 by CARD_1:def 7; then (i+1-'len gs1) in Seg len ((len gs2-'1) |-> i2) by A90,A89, FINSEQ_1:1; then (i+1-'len gs1) in dom ((len gs2-'1) |-> i2) by FINSEQ_1:def 3; then A91: hs1.(i+1)= ((len gs2-'1) |-> i2).((i+1)-'len gs1) by A82,FINSEQ_1:def 7 .=i2 by A90,A89,Lm1; A92: len ((len gs1-'1) |-> j1)+(i+1-'len gs1) =(len gs1-'1)+(i+1-'len gs1) by CARD_1:def 7 .=len gs1 -1+(i+1-'len gs1) by A19,XREAL_0:def 2 .=len gs1 -1+(i-len gs1+1) by A80,XREAL_0:def 2 .=i; len hs1=len gs1+len ((len gs2-'1) |-> i2) by FINSEQ_1:22 .=len gs1 + (len gs2-'1) by CARD_1:def 7; then i-len gs1 < len gs1 + (len gs2 -'1) - len gs1 by A50,XREAL_1:9; then A93: (i-'len gs1)<=len gs2 -'1 by XREAL_0:def 2; i-(len gs1-1)=i+1-'len gs1+1 by NAT_1:11,13; then i+1-'len gs1+1 in Seg len gs2 by FINSEQ_1:1; then A95: i+1-'len gs1+1 in dom gs2 by FINSEQ_1:def 3; len gs2-'1<=len gs2-'1+1 by NAT_1:11; then (i+1-'len gs1)<=(len gs2-'1)+1 by A89,XXREAL_0:2; then (i+1-'len gs1)<=(len gs2-1)+1 by A16,XREAL_0:def 2; then A96: i+1-'len gs1 in dom gs2 by A90,FINSEQ_3:25; A97: len ((len gs2-'1) |-> i2)=len gs2-'1 by CARD_1:def 7; A98: now A99: i =len gs1+(i-len gs1) .=len gs1+(i-'len gs1) by A83,XREAL_0:def 2; assume A100: 1<=(i-'len gs1); then (i-'len gs1) in Seg len ((len gs2-'1) |-> i2) by A93,A97, FINSEQ_1:1; then (i-'len gs1) in dom ((len gs2-'1) |-> i2) by FINSEQ_1:def 3; then hs1.i= ((len gs2-'1) |-> i2).(i-'len gs1)by A99,FINSEQ_1:def 7 .=i2 by A93,A100,Lm1; hence hs1.i=i2; end; i in dom hs2 by A17,A20,A49,A50,FINSEQ_3:25; then A101: hs2/.i=hs2.(len ((len gs1-'1) |-> j1)+(i+1-'len gs1)) by A92, PARTFUN1:def 6 .=gs2.(i+1-'len gs1) by A96,FINSEQ_1:def 7 .=gs2/.(i+1-'len gs1) by A96,PARTFUN1:def 6; i in dom hs1 by A49,A50,FINSEQ_3:25; then A102: hs1/.i=i2 by A86,A98,PARTFUN1:def 6; i+1<=len hs1 & 0+1<=i+1 by A50,NAT_1:13; then A103: i+1 in Seg len hs1 by FINSEQ_1:1; then i+1 in dom hs2 by A17,A20,FINSEQ_1:def 3; then A104: hs2 /.(i+1)=hs2.(len ((len gs1-'1) |-> j1)+(i+1-'len gs1+1)) by A81, PARTFUN1:def 6 .=gs2.((i+1-'len gs1+1)) by A95,FINSEQ_1:def 7 .=gs2/.(i+1-'len gs1+1) by A95,PARTFUN1:def 6; i+1 in dom hs1 by A103,FINSEQ_1:def 3; hence hs1/.i,hs1/.(i+1) are_adjacent & hs2/.i=hs2/.(i+1) or hs1/.i=hs1 /.(i+1) & hs2/.i, hs2/.(i+1) are_adjacent by A14,A102,A91,A84,A94,A104 ,A101,PARTFUN1:def 6; end; end; hence thesis; end; A105: now per cases; case len gs1-'1=0; then ((len gs1-'1) |-> j1)^gs2=<*>(NAT)^gs2 .=gs2 by FINSEQ_1:34; hence hs2.1=j1 & hs2.len hs2=j2 by A10,A11; end; case A106: len gs1-'1<>0; len ((len gs1-'1) |-> j1)=len gs1-'1 by CARD_1:def 7; then A107: 0+1<= len ((len gs1-'1) |-> j1) by A106,NAT_1:13; then 1 in dom ((len gs1-'1) |-> j1) by FINSEQ_3:25; then A108: hs2.1 = ((len gs1-'1) |-> j1).1 by FINSEQ_1:def 7; 1<=len gs2 by A12,NAT_1:11; then A109: len gs2 in dom gs2 by FINSEQ_3:25; len ((len gs1-'1) |-> j1) = len gs1-'1 & len hs2=len ((len gs1-'1) |-> j1) + len gs2 by CARD_1:def 7,FINSEQ_1:22; hence hs2.1=j1 & hs2.len hs2=j2 by A11,A107,A108,A109,Lm1,FINSEQ_1:def 7; end; end; A110: 1 in dom gs1 by A18,FINSEQ_3:25; now per cases; case len gs2-'1=0; then gs1^((len gs2-'1) |-> i2) = gs1^<*>(NAT) .=gs1 by FINSEQ_1:34; hence hs1.1=i1 & hs1.len hs1=i2 by A5,A6; end; case len gs2-'1<>0; then A111: 0+1<=len gs2-'1 by NAT_1:13; A112: len hs1=len gs1+len ((len gs2-'1) |-> i2) by FINSEQ_1:22; len ((len gs2-'1) |-> i2) = len gs2-'1 by CARD_1:def 7; then len ((len gs2-'1) |-> i2) in dom ((len gs2-'1) |-> i2) & ((len gs2 -'1) |-> i2).len ((len gs2-'1) |-> i2) = i2 by A111,Lm1,FINSEQ_3:25; hence hs1.1=i1 & hs1.len hs1=i2 by A5,A110,A112,FINSEQ_1:def 7; end; end; hence thesis by A7,A12,A17,A20,A105,A21,A48; end; reserve S for set; theorem for Y being Subset of S,F being Matrix of n,m, bool S st (ex i,j st i in Seg n & j in Seg m & F*(i,j) c= Y) & (for i1,j1,i2,j2 st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds F*(i1,j1)c= Y iff F*(i2,j2)c=Y) holds for i,j st i in Seg n & j in Seg m holds F*(i,j)c=Y proof let Y be Subset of S,F be Matrix of n,m, (bool S); assume that A1: ex i,j st i in Seg n & j in Seg m & F*(i,j) c= Y and A2: for i1,j1,i2,j2 st i1 in Seg n & i2 in Seg n & j1 in Seg m & j2 in Seg m & i1,j1,i2,j2 are_adjacent holds F*(i1,j1)c=Y iff F*(i2,j2)c=Y; consider i1,j1 such that A3: i1 in Seg n and A4: j1 in Seg m and A5: F*(i1,j1) c= Y by A1; A6: j1<=m by A4,FINSEQ_1:1; 1<=i1 by A3,FINSEQ_1:1; then i1-1>=1-1 by XREAL_1:9; then A7: i1-'1=i1-1 by XREAL_0:def 2; 1<=j1 by A4,FINSEQ_1:1; then j1-1>=1-1 by XREAL_1:9; then A8: j1-'1=j1-1 by XREAL_0:def 2; A9: i1<=n by A3,FINSEQ_1:1; thus for i,j st i in Seg n & j in Seg m holds F*(i,j)c=Y proof let i2,j2; assume that A10: i2 in Seg n and A11: j2 in Seg m; A12: j2<=m by A11,FINSEQ_1:1; 1<=i2 by A10,FINSEQ_1:1; then i2-1>=1-1 by XREAL_1:9; then A13: i2-'1=i2-1 by XREAL_0:def 2; 1<=j2 by A11,FINSEQ_1:1; then j2-1>=1-1 by XREAL_1:9; then A14: j2-'1=j2-1 by XREAL_0:def 2; A15: i2<=n by A10,FINSEQ_1:1; now per cases; case n=0 or m=0; hence contradiction by A3,A4; end; case A16: n<>0 & m<>0; then m>=0+1 by NAT_1:13; then m-1>=0 by XREAL_1:19; then A17: m-'1=m-1 by XREAL_0:def 2; then A18: j1-'1<=m-'1 & j2-'1<=m-'1 by A6,A8,A12,A14,XREAL_1:9; n>=0+1 by A16,NAT_1:13; then n-1>=0 by XREAL_1:19; then A19: n-'1=n-1 by XREAL_0:def 2; then i1-'1<=n-'1 & i2-'1<=n-'1 by A9,A7,A15,A13,XREAL_1:9; then consider fs1,fs2 being FinSequence of NAT such that A20: for i,k1,k2 st i in dom fs1 & k1=fs1.i & k2=fs2.i holds k1 <= n-'1 & k2 <= m-'1 and A21: fs1.1=i1-'1 and A22: fs1.(len fs1)=i2-'1 and A23: fs2.1=j1-'1 and A24: fs2.(len fs2)=j2-'1 and A25: len fs1=len fs2 and A26: len fs1=((i1-'1)-'(i2-'1))+((i2-'1)-'(i1-'1)) +((j1-'1)-'(j2 -'1))+( (j2-'1)-'(j1-'1))+1 and A27: for i st 1<=i & ilen p1; hence thesis; end; end; hence thesis; end; case k+1>len p1; hence thesis by NAT_1:13; end; end; hence thesis; end; A60: 1<=len fs1 by A26,NAT_1:11; then A61: 1 in Seg len fs1 by FINSEQ_1:1; then 1 in dom fs2 by A25,FINSEQ_1:def 3; then A62: fs2/.1=j1-'1 by A23,PARTFUN1:def 6; 1 in dom p2 by A25,A30,A61,FINSEQ_1:def 3; then A63: p2/.1=p2.1 by PARTFUN1:def 6 .=j1-'1 +1 by A25,A31,A32,A61,A62 .=j1 by A8; 1 in dom fs1 by A61,FINSEQ_1:def 3; then A64: fs1/.1=i1-'1 by A21,PARTFUN1:def 6; 1 in dom p1 by A28,A61,FINSEQ_1:def 3; then p1/.1=p1.1 by PARTFUN1:def 6 .=i1-'1 +1 by A29,A33,A61,A64 .= i1 by A7; then A65: P[0] by A5,A63; A66: for i being Nat holds P[i] from NAT_1:sch 2(A65,A34); 1-1<=len fs1-1 by A60,XREAL_1:9; then len fs1 -'1=len fs1 -1 by XREAL_0:def 2; then A67: len fs1 -'1+1=len fs1; A68: len fs1 in Seg len fs1 by A60,FINSEQ_1:1; then len fs1 in dom fs2 by A25,FINSEQ_1:def 3; then A69: fs2/.len fs1=j2-'1 by A24,A25,PARTFUN1:def 6; len fs1 in dom p1 by A28,A68,FINSEQ_1:def 3; then A70: (p1/.len fs1)=p1.(len fs1) by PARTFUN1:def 6 .= (fs1/.len fs1)+1 by A29,A33,A68; len fs1 in dom fs1 by A68,FINSEQ_1:def 3; then A71: fs1/.len fs1=i2-'1 by A22,PARTFUN1:def 6; len fs1 in dom p2 by A25,A30,A68,FINSEQ_1:def 3; then (p2/.len fs1)=p2.(len fs1) by PARTFUN1:def 6 .= (fs2/.len fs1)+1 by A25,A31,A32,A68; hence thesis by A13,A14,A28,A66,A67,A70,A71,A69; end; end; hence thesis; end; end;