:: by Yatsuka Nakamura and Andrzej Trybulec

::

:: Received June 10, 1996

:: Copyright (c) 1996-2019 Association of Mizar Users

definition

let i1, i2 be Nat;

symmetry

for i1, i2 being Nat holds

( ( not i2 = i1 + 1 & not i1 = i2 + 1 ) or i1 = i2 + 1 or i2 = i1 + 1 ) ;

irreflexivity

for i1 being Nat holds

( not i1 = i1 + 1 & not i1 = i1 + 1 ) ;

end;
symmetry

for i1, i2 being Nat holds

( ( not i2 = i1 + 1 & not i1 = i2 + 1 ) or i1 = i2 + 1 or i2 = i1 + 1 ) ;

irreflexivity

for i1 being Nat holds

( not i1 = i1 + 1 & not i1 = i1 + 1 ) ;

:: deftheorem defines are_adjacent GOBRD10:def 1 :

for i1, i2 being Nat holds

( i1,i2 are_adjacent iff ( i2 = i1 + 1 or i1 = i2 + 1 ) );

for i1, i2 being Nat holds

( i1,i2 are_adjacent iff ( i2 = i1 + 1 or i1 = i2 + 1 ) );

definition

let i1, j1, i2, j2 be Nat;

end;
pred i1,j1,i2,j2 are_adjacent means :: GOBRD10:def 2

( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) );

( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) );

:: deftheorem defines are_adjacent GOBRD10:def 2 :

for i1, j1, i2, j2 being Nat holds

( i1,j1,i2,j2 are_adjacent iff ( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) ) );

for i1, j1, i2, j2 being Nat holds

( i1,j1,i2,j2 are_adjacent iff ( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) ) );

theorem Th3: :: 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

i1 + 1,j1 + 1,i2 + 1,j2 + 1 are_adjacent

proof end;

theorem :: GOBRD10:4

Lm1: for n, i, j being Element of NAT st 1 <= j & j <= n holds

(n |-> i) . j = i

by FINSEQ_1:1, FINSEQ_2:57;

theorem Th5: :: GOBRD10:5

for n, i, j being Element of NAT 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 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 & not fs1 . (i1 + 1) = (fs1 /. i1) + 1 holds

fs1 . i1 = (fs1 /. (i1 + 1)) + 1 ) )

proof end;

theorem Th6: :: GOBRD10:6

for n, i, j being Element of NAT 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 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds

fs1 /. i1,fs1 /. (i1 + 1) are_adjacent ) )

ex fs1 being FinSequence of NAT st

( fs1 . 1 = i & fs1 . (len fs1) = j & len fs1 = ((i -' j) + (j -' i)) + 1 & ( for k, k1 being Element of NAT st 1 <= k & k <= len fs1 & k1 = fs1 . k holds

k1 <= n ) & ( for i1 being Element of NAT st 1 <= i1 & i1 < len fs1 holds

fs1 /. i1,fs1 /. (i1 + 1) are_adjacent ) )

proof end;

theorem Th7: :: GOBRD10:7

for n, m, i1, j1, i2, j2 being Element of NAT st i1 <= n & j1 <= m & i2 <= n & j2 <= m holds

ex fs1, fs2 being FinSequence of NAT st

( ( for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds

fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent ) )

ex fs1, fs2 being FinSequence of NAT st

( ( for i, k1, k2 being Element of NAT 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 being Element of NAT st 1 <= i & i < len fs1 holds

fs1 /. i,fs2 /. i,fs1 /. (i + 1),fs2 /. (i + 1) are_adjacent ) )

proof end;

theorem :: GOBRD10:8

for n, m being Element of NAT

for S being set

for Y being Subset of S

for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st

( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT 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 being Element of NAT st i in Seg n & j in Seg m holds

F * (i,j) c= Y

for S being set

for Y being Subset of S

for F being Matrix of n,m,(bool S) st ex i, j being Element of NAT st

( i in Seg n & j in Seg m & F * (i,j) c= Y ) & ( for i1, j1, i2, j2 being Element of NAT 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 being Element of NAT st i in Seg n & j in Seg m holds

F * (i,j) c= Y

proof end;