let k be Element of NAT ; :: thesis: for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special & 1 <= k & k + 1 <= len f holds
( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )
let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special & 1 <= k & k + 1 <= len f holds
( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & f is special & 1 <= k & k + 1 <= len f implies ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f ) )
assume that
A1:
( f is_sequence_on G & f is special )
and
A2:
1 <= k
and
A3:
k + 1 <= len f
; :: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )
consider i1, j1, i2, j2 being Element of NAT such that
A4:
[i1,j1] in Indices G
and
A5:
f /. k = G * i1,j1
and
A6:
[i2,j2] in Indices G
and
A7:
f /. (k + 1) = G * i2,j2
and
A8:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A1, A2, A3, JORDAN8:6;
A9:
( i1 + 1 > i1 & j1 + 1 > j1 & i2 + 1 > i2 & j2 + 1 > j2 )
by NAT_1:13;
A10:
( i1 <= len G & j1 <= width G )
by A4, MATRIX_1:39;
A11:
( i2 <= len G & j2 <= width G )
by A6, MATRIX_1:39;
A12:
( i1 -' 1 <= len G & j1 -' 1 <= width G )
by A10, NAT_D:44;
A13:
( i2 -' 1 <= len G & j2 -' 1 <= width G )
by A11, NAT_D:44;
per cases
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A8;
suppose A14:
(
i1 = i2 &
j1 + 1
= j2 )
;
:: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )then A15:
right_cell f,
k,
G = cell G,
i1,
j1
by A1, A2, A3, A4, A5, A6, A7, A9, GOBRD13:def 2;
left_cell f,
k,
G = cell G,
(i1 -' 1),
j1
by A1, A2, A3, A4, A5, A6, A7, A9, A14, GOBRD13:def 3;
hence
(
Int (left_cell f,k,G) misses L~ f &
Int (right_cell f,k,G) misses L~ f )
by A1, A10, A12, A15, Th16;
:: thesis: verum end; suppose A16:
(
i1 + 1
= i2 &
j1 = j2 )
;
:: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )then A17:
right_cell f,
k,
G = cell G,
i1,
(j1 -' 1)
by A1, A2, A3, A4, A5, A6, A7, A9, GOBRD13:def 2;
left_cell f,
k,
G = cell G,
i1,
j1
by A1, A2, A3, A4, A5, A6, A7, A9, A16, GOBRD13:def 3;
hence
(
Int (left_cell f,k,G) misses L~ f &
Int (right_cell f,k,G) misses L~ f )
by A1, A10, A12, A17, Th16;
:: thesis: verum end; suppose A18:
(
i1 = i2 + 1 &
j1 = j2 )
;
:: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )then A19:
right_cell f,
k,
G = cell G,
i2,
j2
by A1, A2, A3, A4, A5, A6, A7, A9, GOBRD13:def 2;
left_cell f,
k,
G = cell G,
i2,
(j2 -' 1)
by A1, A2, A3, A4, A5, A6, A7, A9, A18, GOBRD13:def 3;
hence
(
Int (left_cell f,k,G) misses L~ f &
Int (right_cell f,k,G) misses L~ f )
by A1, A11, A13, A19, Th16;
:: thesis: verum end; suppose A20:
(
i1 = i2 &
j1 = j2 + 1 )
;
:: thesis: ( Int (left_cell f,k,G) misses L~ f & Int (right_cell f,k,G) misses L~ f )then A21:
right_cell f,
k,
G = cell G,
(i1 -' 1),
j2
by A1, A2, A3, A4, A5, A6, A7, A9, GOBRD13:def 2;
left_cell f,
k,
G = cell G,
i1,
j2
by A1, A2, A3, A4, A5, A6, A7, A9, A20, GOBRD13:def 3;
hence
(
Int (left_cell f,k,G) misses L~ f &
Int (right_cell f,k,G) misses L~ f )
by A1, A10, A11, A12, A21, Th16;
:: thesis: verum end;