:: Adjacency Concept for Pairs of Natural Numbers
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received June 10, 1996
:: Copyright (c) 1996-2026 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 & i1<len fs1 holds fs1.(i1+1)
= (fs1/.i1)+1 or fs1.i1= (fs1/.(i1+1)) +1
proof
let n,i,j;
assume that
A1: i<=n and
A2: j<=n;
now
per cases by XXREAL_0:1;
case
A3: i<j;
then i-j<j-j by XREAL_1:9;
then
A4: i-'j=0 by XREAL_0:def 2;
j-i>0 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<len fs2 holds fs2.(i1+1)= (fs2/.i1)+1 or fs2.
i1= (fs2/.(i1+1)) +1
proof
let i1;
assume that
A17: 1<=i1 and
A18: i1<len fs2;
A19: 1<=1+i1 by NAT_1:11;
i1+1<=len fs2 by A18,NAT_1:13;
then i1+1 in dom p by A19,FINSEQ_3:25;
then
A20: fs2.(i1+1)=i+(i1+1)-'1 by A9;
1+(i+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<len fs1 holds fs1.(i1+1)=(fs1/.i1)+1 or fs1.i1
=(fs1/.(i1+1)) +1 by A31,FINSEQ_1:def 3;
1 in dom f by A31,FINSEQ_1:1;
then fs1.1 in rng f by FUNCT_1:def 3;
then
A34: fs1.1=i by A32,TARSKI:def 1;
A35: len fs1=1 by A31,FINSEQ_1:def 3;
then for k,k1 st 1<=k & k<=len fs1 & k1=fs1.k holds k1<=n by A1,A34,
XXREAL_0:1;
hence thesis by A29,A34,A35,A30,A33;
end;
case
A36: j<i;
then
A37: i-j>=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<i-i by A36,XREAL_1:9;
then j-'i=0 by XREAL_0:def 2;
then
A39: (i-'j)+(j-'i)+1 =i-j+1+(j-'i) by A37,XREAL_0:def 2
.=i+1-j by A38;
deffunc F(Nat) = i+1-'$1;
A40: i+1-1>=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<len fs2 holds fs2.(i1+1)= (fs2/.i1)+1 or fs2.
i1= (fs2/.(i1+1)) +1
proof
let i1;
assume that
A53: 1<=i1 and
A54: i1<len fs2;
A55: i1+1<=len fs2 by A54,NAT_1:13;
then i1+1<=i-j+1 by A43,A51,XREAL_0:def 2;
then i1<=i-j by XREAL_1:6;
then i1+j<=i by XREAL_1:19;
then j<=i-i1 by XREAL_1:19;
then
A56: 1+(i+1-'(i1+1))=1+(i+1-(i1+1)) by XREAL_0:def 2
.=i+1-i1;
A57: 1<=i1+1 by A53,NAT_1:13;
then (i1+1) in dom fs2 by A55,FINSEQ_3:25;
then fs2.(i1+1)=i+1-'(i1+1) by A44;
then
A58: (fs2/.(i1+1))+1=1+(i+1-'(i1+1)) by A57,A55,FINSEQ_4:15;
i1 in dom fs2 by A53,A54,FINSEQ_3:25;
then fs2.(i1)=i+1-'i1 by A44;
hence thesis by A58,A56,XREAL_0:def 2;
end;
A59: for k,k1 st 1<=k & k<=len p & k1=p.k holds k1<=n
proof
let k,k1;
assume that
A60: 1<=k and
A61: k<=len p and
A62: k1=p.k;
k<=i+1-j by A43,A60,A61,XREAL_0:def 2;
then k+j<=i+1-j+j by XREAL_1:6;
then
A63: k+j-k<=i+1-k by XREAL_1:9;
-k<=-1 by A60,XREAL_1:24;
then
A64: -k+(i+1)<= -1+(i+1) by XREAL_1:6;
k in dom p by A60,A61,FINSEQ_3:25;
then k1=i+1-'k by A44,A62;
then k1=i+1-k by A63,XREAL_0:def 2;
hence thesis by A1,A64,XXREAL_0:2;
end;
len p in dom p by A41,A43,A45,FINSEQ_3:25;
then p.(len p)=(i+1-'(i+1-'j)) by A43,A44
.= j by A42,XREAL_0:def 2;
hence thesis by A43,A59,A45,A46,A39,A52;
end;
end;
hence thesis;
end;
theorem Th6:
for n,i,j st i<=n & j<=n
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<len fs1 holds fs1/.i1,
fs1/.(i1+1) are_adjacent
proof
let n,i,j;
assume i<=n & j<=n;
then consider fs1 being FinSequence of NAT such that
A1: 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 ) and
A2: for i1 st 1<=i1 & i1<len fs1 holds fs1.(i1+1)= (fs1/.i1)+1 or fs1.i1
= (fs1/.(i1+1)) +1 by Th5;
for i1 st 1<=i1 & i1<len fs1 holds fs1/.i1,fs1/.(i1+1) are_adjacent
proof
let i1;
assume
A3: 1<=i1 & i1<len fs1;
then
A4: fs1.i1= fs1/.i1 by FINSEQ_4:15;
1<= i1+1 & i1+1<=len fs1 by A3,NAT_1:13;
then
A5: fs1.(i1+1)= fs1/.(i1+1) by FINSEQ_4:15;
fs1.(i1+1)= (fs1/.i1)+1 or fs1.i1= (fs1/.(i1+1)) +1 by A2,A3;
hence thesis by A5,A4;
end;
hence thesis by A1;
end;
theorem Th7:
for n,m,i1,j1,i2,j2 st i1<=n & j1<=m & i2<=n & j2<=m
ex fs1,fs2 being FinSequence of NAT
st (for i,k1,k2 st i in dom fs1 & k1=fs1.i & k2=fs2.i
holds k1 <= n & k2 <= m) & fs1.1=i1 & fs1.(len fs1)=i2 & fs2.1=j1 & fs2.(len
fs2)=j2 & len fs1=len fs2 & len fs1=(i1-'i2)+(i2-'i1)+(j1-'j2)+(j2-'j1)+1 & for
i st 1<=i & i<len fs1 holds fs1/.i,fs2/.i,fs1/.(i+1),fs2/.(i+1) are_adjacent
proof
let n,m,i1,j1,i2,j2;
assume that
A1: i1<=n and
A2: j1<=m and
A3: i2<=n and
A4: j2<=m;
consider gs1 being FinSequence of NAT such that
A5: gs1.1=i1 and
A6: gs1.(len gs1)=i2 and
A7: len gs1=(i1-'i2)+(i2-'i1)+1 and
A8: for k,k1 st 1<=k & k<=len gs1 & k1=gs1.k holds k1<=n and
A9: for k st 1<=k & k<len gs1 holds gs1/.k,gs1/.(k+1) are_adjacent by A1,A3,Th6
;
consider gs2 being FinSequence of NAT such that
A10: gs2.1=j1 and
A11: gs2.(len gs2)=j2 and
A12: len gs2=(j1-'j2)+(j2-'j1)+1 and
A13: for k,k1 st 1<=k & k<=len gs2 & k1=gs2.k holds k1<=m and
A14: for k st 1<=k & k<len gs2 holds gs2/.k,gs2/.(k+1) are_adjacent by A2,A4
,Th6;
A15: 1<=len gs2 by A12,NAT_1:11;
then
A16: len gs2 -1>=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<i-len gs1 & i <=len hs1 by A23,
FINSEQ_3:25,XREAL_1:9;
now
per cases by A37,A39,XREAL_1:9;
case
A40: 1<=i & i<=len gs1;
then i in dom gs1 by FINSEQ_3:25;
then hs1.i=gs1.i by FINSEQ_1:def 7;
hence k1<=n by A8,A24,A40;
end;
case
A41: 0<i-len gs1 & i-len gs1 <=len hs1 -' len gs1;
then
A42: i-len gs1=i-'len gs1 by XREAL_0:def 2;
then
A43: 0+1<=i-'len gs1 by A41,NAT_1:13;
then (i-'len gs1) in Seg (len hs1-'len gs1) by A41,A42,FINSEQ_1:1;
then
A44: (i-'len gs1)in Seg (len gs2-'1) by A38,NAT_D:34;
then
A45: i-'len gs1<=len gs2 -'1 by FINSEQ_1:1;
A46: i=len gs1+(i-len gs1);
(i-'len gs1)in Seg len ((len gs2-'1) |-> 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 & i<len hs1 holds hs1/.i,hs2/.i,hs1/.(i+1),hs2/.(i+1)
are_adjacent
proof
let i;
assume that
A49: 1<=i and
A50: i<len hs1;
now
per cases;
case
A51: i<len gs1;
then
A52: i+1<=len gs1 by NAT_1:13;
A53: now
per cases;
case
i+1<=len gs1-'1;
then i+1<=len gs1 -1 by XREAL_0:def 2;
then i+1+1<=len gs1-1+1 by XREAL_1:6;
then
A54: i+1<len gs1 by NAT_1:13;
then
A55: i<len gs1 by NAT_1:13;
then
A56: i in dom gs1 by A49,FINSEQ_3:25;
1<i+1 by A49,NAT_1:13;
then
A57: (i+1) in dom gs1 by A54,FINSEQ_3:25;
A58: dom gs1 c= dom hs1 by FINSEQ_1:26;
then
A59: hs1/.(i+1)=hs1.(i+1) by A57,PARTFUN1:def 6
.=gs1.(i+1) by A57,FINSEQ_1:def 7
.=gs1/.(i+1) by A57,PARTFUN1:def 6;
hs1/.i=hs1.i by A58,A56,PARTFUN1:def 6
.=gs1.i by A56,FINSEQ_1:def 7
.=gs1/.i by A56,PARTFUN1:def 6;
hence hs1/.i,hs1/.(i+1) are_adjacent by A9,A49,A55,A59;
end;
case
i+1>len 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)<len gs1-1+len gs2 -(len gs1-1) by A17,A50,XREAL_1:9;
then
A94: i+1-'len gs1<len gs2 by A80,XREAL_0:def 2;
then 1<=i+1-'len gs1 +1 & len gs2>=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 & i<len fs1 holds fs1/.i,fs2/.i,fs1/.(i+1),fs2
/.(i+1) are_adjacent by A18,Th7;
deffunc F(Nat) = (fs1/.$1)+1;
ex p being FinSequence of NAT st len p = len fs1 & for j be Nat
st j in dom p holds p.j = F(j) from FINSEQ_2:sch 1;
then consider p1 being FinSequence of NAT such that
A28: len p1 = len fs1 and
A29: for k be Nat st k in dom p1 holds p1.k=(fs1/.k)+1;
deffunc F(Nat) = (fs2/.$1)+1;
ex p being FinSequence of NAT st len p = len fs2 & for k be Nat
st k in dom p holds p.k=F(k) from FINSEQ_2:sch 1;
then consider p2 being FinSequence of NAT such that
A30: len p2 = len fs2 and
A31: for k be Nat st k in dom p2 holds p2.k=(fs2/.k)+1;
A32: dom p2 = Seg len fs2 by A30,FINSEQ_1:def 3;
defpred P[Nat] means $1+1<=len p1 implies F*(p1/.($1+1),p2
/.($1+1)) c= Y;
A33: dom p1 = Seg len fs1 by A28,FINSEQ_1:def 3;
A34: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
A35: 1<=k+1 by NAT_1:12;
assume
A36: k+1<=len p1 implies F*(p1/.(k+1),p2/.(k+1)) c= Y;
now
per cases;
case
A37: k+1<=len p1;
now
per cases;
case
A38: k+1+1<=len p1;
set lp11=fs1/.(k+1+1),lp21=fs2/.(k+1+1);
1<=k+1+1 by NAT_1:12;
then
A39: k+1+1 in Seg len p1 by A38,FINSEQ_1:1;
then k+1+1 in dom fs2 by A25,A28,FINSEQ_1:def 3;
then
A40: fs2/.(k+1+1)=fs2.(k+1+1) by PARTFUN1:def 6;
A41: k+1+1 in dom fs1 by A28,A39,FINSEQ_1:def 3;
then
A42: fs1/.(k+1+1)=fs1.(k+1+1) by PARTFUN1:def 6;
then lp11<=n-1 by A19,A20,A41,A40;
then
A43: lp11+1<=n-1+1 by XREAL_1:6;
k+1+1 in dom p2 by A25,A28,A30,A39,FINSEQ_1:def 3;
then p2.(k+1+1)=p2/.(k+1+1) by PARTFUN1:def 6;
then
A44: p2/.(k+1+1)=lp21+1 by A25,A28,A31,A32,A39;
lp21<=m-'1 by A20,A41,A42,A40;
then
A45: lp21+1<=m-1+1 by A17,XREAL_1:6;
1<=1+lp21 by NAT_1:11;
then
A46: p2/.(k+1+1) in Seg m by A44,A45,FINSEQ_1:1;
k+1+1 in dom p1 by A39,FINSEQ_1:def 3;
then
A47: p1/.(k+1+1)=p1.(k+1+1) by PARTFUN1:def 6
.=lp11+1 by A28,A29,A33,A39;
set lp1=fs1/.(k+1),lp2=fs2/.(k+1);
A48: k+1<len p1 by A38,NAT_1:13;
then
A49: k+1 in Seg len p1 by A35,FINSEQ_1:1;
then k+1 in dom fs2 by A25,A28,FINSEQ_1:def 3;
then
A50: lp2=fs2.(k+1) by PARTFUN1:def 6;
k+1 in dom p1 by A49,FINSEQ_1:def 3;
then
A51: p1/.(k+1)=p1.(k+1) by PARTFUN1:def 6
.=lp1+1 by A28,A29,A33,A49;
A52: k+1 in dom fs1 by A28,A49,FINSEQ_1:def 3;
then
A53: lp1=fs1.(k+1) by PARTFUN1:def 6;
then lp1<=n-1 by A19,A20,A52,A50;
then
A54: lp1+1<=n-1+1 by XREAL_1:6;
1<=1+lp1 by NAT_1:11;
then
A55: p1/.(k+1) in Seg n by A51,A54,FINSEQ_1:1;
k+1 in dom p2 by A25,A28,A30,A49,FINSEQ_1:def 3;
then
A56: p2/.(k+1)=p2.(k+1) by PARTFUN1:def 6
.=lp2+1 by A25,A28,A31,A32,A49;
lp2<=m-'1 by A20,A52,A53,A50;
then
A57: lp2+1<=m-1+1 by A17,XREAL_1:6;
1<=1+lp2 by NAT_1:11;
then
A58: p2/.(k+1) in Seg m by A56,A57,FINSEQ_1:1;
1<=1+lp11 by NAT_1:11;
then
A59: p1/.(k+1+1) in Seg n by A47,A43,FINSEQ_1:1;
k+1+1 in dom p2 by A25,A28,A30,A39,FINSEQ_1:def 3;
then p2/.(k+1+1)=p2.(k+1+1) by PARTFUN1:def 6
.=lp21+1 by A25,A28,A31,A32,A39;
then p1/.(k+1),p2/.(k+1),p1/.(k+1+1),p2/.(k+1+1)
are_adjacent by A27,A28,A35,A48,A51,A56,A47,Th3;
hence thesis by A2,A36,A37,A55,A58,A59,A46;
end;
case
k+1+1>len 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;