let f be V22() standard clockwise_oriented special_circular_sequence; :: thesis: for G being Go-board st f is_sequence_on G holds

for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

(f /. k) `1 <> W-bound (L~ f)

let G be Go-board; :: thesis: ( f is_sequence_on G implies for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

(f /. k) `1 <> W-bound (L~ f) )

assume A1: f is_sequence_on G ; :: thesis: for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

(f /. k) `1 <> W-bound (L~ f)

let i, j, k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies (f /. k) `1 <> W-bound (L~ f) )

assume that

A2: ( 1 <= k & k + 1 <= len f ) and

A3: [i,j] in Indices G and

A4: [i,(j + 1)] in Indices G and

A5: f /. k = G * (i,(j + 1)) and

A6: f /. (k + 1) = G * (i,j) and

A7: (f /. k) `1 = W-bound (L~ f) ; :: thesis: contradiction

A8: right_cell (f,k,G) = cell (G,(i -' 1),j) by A1, A2, A3, A4, A5, A6, GOBRD13:28;

A9: ( 1 <= i & i <= len G ) by A4, MATRIX_0:32;

A10: 1 <= j by A3, MATRIX_0:32;

A11: 1 <= j + 1 by A4, MATRIX_0:32;

A12: j + 1 <= width G by A4, MATRIX_0:32;

set p = (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))));

A13: i <= len G by A3, MATRIX_0:32;

A14: 0 + 1 <= i by A3, MATRIX_0:32;

then A15: (i -' 1) + 1 = i by XREAL_1:235;

for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

(f /. k) `1 <> W-bound (L~ f)

let G be Go-board; :: thesis: ( f is_sequence_on G implies for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

(f /. k) `1 <> W-bound (L~ f) )

assume A1: f is_sequence_on G ; :: thesis: for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) holds

(f /. k) `1 <> W-bound (L~ f)

let i, j, k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,(j + 1)) & f /. (k + 1) = G * (i,j) implies (f /. k) `1 <> W-bound (L~ f) )

assume that

A2: ( 1 <= k & k + 1 <= len f ) and

A3: [i,j] in Indices G and

A4: [i,(j + 1)] in Indices G and

A5: f /. k = G * (i,(j + 1)) and

A6: f /. (k + 1) = G * (i,j) and

A7: (f /. k) `1 = W-bound (L~ f) ; :: thesis: contradiction

A8: right_cell (f,k,G) = cell (G,(i -' 1),j) by A1, A2, A3, A4, A5, A6, GOBRD13:28;

A9: ( 1 <= i & i <= len G ) by A4, MATRIX_0:32;

A10: 1 <= j by A3, MATRIX_0:32;

A11: 1 <= j + 1 by A4, MATRIX_0:32;

A12: j + 1 <= width G by A4, MATRIX_0:32;

set p = (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))));

A13: i <= len G by A3, MATRIX_0:32;

A14: 0 + 1 <= i by A3, MATRIX_0:32;

then A15: (i -' 1) + 1 = i by XREAL_1:235;

per cases
( i = 1 or i > 1 )
by A14, XXREAL_0:1;

end;

suppose
i > 1
; :: thesis: contradiction

then
i >= 1 + 1
by NAT_1:13;

then A16: i - 1 >= (1 + 1) - 1 by XREAL_1:9;

i < (len G) + 1 by A13, NAT_1:13;

then A17: i - 1 < ((len G) + 1) - 1 by XREAL_1:9;

j < width G by A12, NAT_1:13;

then A18: Int (cell (G,(i -' 1),j)) = { |[r,s]| where r, s is Real : ( (G * ((i -' 1),1)) `1 < r & r < (G * (i,1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A15, A16, A17, GOBOARD6:26;

A19: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in Int (right_cell (f,k,G)) by A13, A10, A12, A8, A15, A16, GOBOARD6:31;

then consider r, s being Real such that

A20: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) = |[r,s]| and

(G * ((i -' 1),1)) `1 < r and

A21: r < (G * (i,1)) `1 and

(G * (1,j)) `2 < s and

s < (G * (1,(j + 1))) `2 by A8, A18;

((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 = r by A20, EUCLID:52;

then ((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 < W-bound (L~ f) by A5, A7, A9, A11, A12, A21, GOBOARD5:2;

then A22: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in LeftComp f by Th9;

Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;

then (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in (LeftComp f) /\ (RightComp f) by A19, A22, XBOOLE_0:def 4;

then LeftComp f meets RightComp f by XBOOLE_0:def 7;

hence contradiction by GOBRD14:14; :: thesis: verum

end;then A16: i - 1 >= (1 + 1) - 1 by XREAL_1:9;

i < (len G) + 1 by A13, NAT_1:13;

then A17: i - 1 < ((len G) + 1) - 1 by XREAL_1:9;

j < width G by A12, NAT_1:13;

then A18: Int (cell (G,(i -' 1),j)) = { |[r,s]| where r, s is Real : ( (G * ((i -' 1),1)) `1 < r & r < (G * (i,1)) `1 & (G * (1,j)) `2 < s & s < (G * (1,(j + 1))) `2 ) } by A10, A15, A16, A17, GOBOARD6:26;

A19: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in Int (right_cell (f,k,G)) by A13, A10, A12, A8, A15, A16, GOBOARD6:31;

then consider r, s being Real such that

A20: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) = |[r,s]| and

(G * ((i -' 1),1)) `1 < r and

A21: r < (G * (i,1)) `1 and

(G * (1,j)) `2 < s and

s < (G * (1,(j + 1))) `2 by A8, A18;

((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 = r by A20, EUCLID:52;

then ((1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1))))) `1 < W-bound (L~ f) by A5, A7, A9, A11, A12, A21, GOBOARD5:2;

then A22: (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in LeftComp f by Th9;

Int (right_cell (f,k,G)) c= RightComp f by A1, A2, JORDAN1H:25;

then (1 / 2) * ((G * ((i -' 1),j)) + (G * (i,(j + 1)))) in (LeftComp f) /\ (RightComp f) by A19, A22, XBOOLE_0:def 4;

then LeftComp f meets RightComp f by XBOOLE_0:def 7;

hence contradiction by GOBRD14:14; :: thesis: verum