let i, j be Nat; for f being V8() standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * ((i + 1),(j + 2)))) c= L~ f holds
not LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f
let f be V8() standard special_circular_sequence; ( 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * ((i + 1),(j + 2)))) c= L~ f implies not LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f )
assume that
A1:
1 <= i
and
A2:
i < len (GoB f)
and
A3:
1 <= j
and
A4:
j + 1 < width (GoB f)
and
A5:
( LSeg (((GoB f) * ((i + 1),j)),((GoB f) * ((i + 1),(j + 1)))) c= L~ f & LSeg (((GoB f) * ((i + 1),(j + 1))),((GoB f) * ((i + 1),(j + 2)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f )
; contradiction
A6:
i + 1 <= len (GoB f)
by A2, NAT_1:13;
j + (1 + 1) = (j + 1) + 1
;
then A7:
j + 2 <= width (GoB f)
by A4, NAT_1:13;
A8:
1 <= j + 1
by NAT_1:11;
A9:
j < width (GoB f)
by A4, NAT_1:13;
A10:
1 <= i + 1
by NAT_1:11;
j + 1 <= j + 2
by XREAL_1:6;
then A11:
1 <= j + 2
by A8, XXREAL_0:2;
per cases
( ( f /. 2 = (GoB f) * ((i + 1),j) & f /. 2 = (GoB f) * (i,(j + 1)) ) or ( f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 2)) & f /. 2 = (GoB f) * (i,(j + 1)) ) or ( f /. 2 = (GoB f) * ((i + 1),(j + 2)) & f /. 2 = (GoB f) * ((i + 1),j) ) or ( f /. 1 = (GoB f) * ((i + 1),(j + 1)) & ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) ) ) ) or ( ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) ) ) & f /. 1 = (GoB f) * ((i + 1),(j + 1)) ) or ( ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * ((i + 1),(j + 2)) ) or ( f /. k = (GoB f) * ((i + 1),(j + 2)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) ) ) & ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) & ( ( f /. k = (GoB f) * (i,(j + 1)) & f /. (k + 2) = (GoB f) * ((i + 1),j) ) or ( f /. k = (GoB f) * ((i + 1),j) & f /. (k + 2) = (GoB f) * (i,(j + 1)) ) ) ) ) )
by A1, A3, A4, A5, A6, A10, Th53, Th55;
suppose A12:
(
f /. 2
= (GoB f) * (
(i + 1),
j) &
f /. 2
= (GoB f) * (
i,
(j + 1)) )
;
contradiction
(
[(i + 1),j] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A3, A4, A6, A10, A9, A8, MATRIX_0:30;
then
i = i + 1
by A12, GOBOARD1:5;
hence
contradiction
;
verum end; suppose A13:
(
f /. ((len f) -' 1) = (GoB f) * (
(i + 1),
(j + 2)) &
f /. ((len f) -' 1) = (GoB f) * (
i,
(j + 1)) )
;
contradiction
(
[(i + 1),(j + 2)] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then
i = i + 1
by A13, GOBOARD1:5;
hence
contradiction
;
verum end; suppose A14:
(
f /. 2
= (GoB f) * (
(i + 1),
(j + 2)) &
f /. 2
= (GoB f) * (
i,
(j + 1)) )
;
contradiction
(
[(i + 1),(j + 2)] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then
i = i + 1
by A14, GOBOARD1:5;
hence
contradiction
;
verum end; suppose that A24:
ex
k being
Nat st
( 1
<= k &
k + 1
< len f &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) & ( (
f /. k = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
(i + 1),
(j + 2)) ) or (
f /. k = (GoB f) * (
(i + 1),
(j + 2)) &
f /. (k + 2) = (GoB f) * (
(i + 1),
j) ) ) )
and A25:
ex
k being
Nat st
( 1
<= k &
k + 1
< len f &
f /. (k + 1) = (GoB f) * (
(i + 1),
(j + 1)) & ( (
f /. k = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
(i + 1),
j) ) or (
f /. k = (GoB f) * (
(i + 1),
j) &
f /. (k + 2) = (GoB f) * (
i,
(j + 1)) ) ) )
;
contradictionconsider k1 being
Nat such that
1
<= k1
and A26:
k1 + 1
< len f
and A27:
f /. (k1 + 1) = (GoB f) * (
(i + 1),
(j + 1))
and A28:
( (
f /. k1 = (GoB f) * (
(i + 1),
j) &
f /. (k1 + 2) = (GoB f) * (
(i + 1),
(j + 2)) ) or (
f /. k1 = (GoB f) * (
(i + 1),
(j + 2)) &
f /. (k1 + 2) = (GoB f) * (
(i + 1),
j) ) )
by A24;
consider k2 being
Nat such that
1
<= k2
and A29:
k2 + 1
< len f
and A30:
f /. (k2 + 1) = (GoB f) * (
(i + 1),
(j + 1))
and A31:
( (
f /. k2 = (GoB f) * (
i,
(j + 1)) &
f /. (k2 + 2) = (GoB f) * (
(i + 1),
j) ) or (
f /. k2 = (GoB f) * (
(i + 1),
j) &
f /. (k2 + 2) = (GoB f) * (
i,
(j + 1)) ) )
by A25;
A32:
now not k1 <> k2assume A33:
k1 <> k2
;
contradiction end; now contradictionper cases
( ( f /. k1 = (GoB f) * ((i + 1),j) & f /. k2 = (GoB f) * (i,(j + 1)) ) or ( f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,(j + 1)) ) or ( f /. k1 = (GoB f) * ((i + 1),(j + 2)) & f /. k2 = (GoB f) * (i,(j + 1)) ) or ( f /. k1 = (GoB f) * ((i + 1),(j + 2)) & f /. k2 = (GoB f) * ((i + 1),j) ) )
by A28, A31;
suppose A34:
(
f /. k1 = (GoB f) * (
(i + 1),
j) &
f /. k2 = (GoB f) * (
i,
(j + 1)) )
;
contradiction
(
[(i + 1),j] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A3, A4, A6, A10, A9, A8, MATRIX_0:30;
then
i = i + 1
by A32, A34, GOBOARD1:5;
hence
contradiction
;
verum end; suppose A35:
(
f /. (k1 + 2) = (GoB f) * (
(i + 1),
(j + 2)) &
f /. (k2 + 2) = (GoB f) * (
i,
(j + 1)) )
;
contradiction
(
[(i + 1),(j + 2)] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then
i = i + 1
by A32, A35, GOBOARD1:5;
hence
contradiction
;
verum end; suppose A36:
(
f /. k1 = (GoB f) * (
(i + 1),
(j + 2)) &
f /. k2 = (GoB f) * (
i,
(j + 1)) )
;
contradiction
(
[(i + 1),(j + 2)] in Indices (GoB f) &
[i,(j + 1)] in Indices (GoB f) )
by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then
i = i + 1
by A32, A36, GOBOARD1:5;
hence
contradiction
;
verum end; suppose A37:
(
f /. k1 = (GoB f) * (
(i + 1),
(j + 2)) &
f /. k2 = (GoB f) * (
(i + 1),
j) )
;
contradiction
(
[(i + 1),(j + 2)] in Indices (GoB f) &
[(i + 1),j] in Indices (GoB f) )
by A3, A6, A10, A9, A7, A11, MATRIX_0:30;
then
j = j + 2
by A32, A37, GOBOARD1:5;
hence
contradiction
;
verum end; end; end; hence
contradiction
;
verum end; end;