let j, i be Element of NAT ; :: thesis: for f being non constant standard special_circular_sequence st 1 <= j & j < width (GoB f) & 1 <= i & i + 1 < len (GoB f) & LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) c= L~ f & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) c= L~ f holds
not LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f
let f be non constant standard special_circular_sequence; :: thesis: ( 1 <= j & j < width (GoB f) & 1 <= i & i + 1 < len (GoB f) & LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) c= L~ f & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) c= L~ f implies not LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f )
assume that
A1: 1 <= j and
A2: j < width (GoB f) and
A3: 1 <= i and
A4: i + 1 < len (GoB f) and
A5: ( LSeg ((GoB f) * i,j),((GoB f) * (i + 1),j) c= L~ f & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 2),j) c= L~ f & LSeg ((GoB f) * (i + 1),j),((GoB f) * (i + 1),(j + 1)) c= L~ f ) ; :: thesis: contradiction
A6: j + 1 <= width (GoB f) by A2, NAT_1:13;
i + (1 + 1) = (i + 1) + 1 ;
then A7: i + 2 <= len (GoB f) by A4, NAT_1:13;
A8: 1 <= i + 1 by NAT_1:11;
A9: i < len (GoB f) by A4, NAT_1:13;
A10: 1 <= j + 1 by NAT_1:11;
i + 1 <= i + 2 by XREAL_1:8;
then A11: 1 <= i + 2 by A8, XXREAL_0:2;
per cases ( ( f /. ((len f) -' 1) = (GoB f) * (i + 2),j & f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 1) ) or ( f /. 2 = (GoB f) * i,j & f /. 2 = (GoB f) * (i + 1),(j + 1) ) or ( f /. 2 = (GoB f) * (i + 2),j & f /. 2 = (GoB f) * i,j ) or ( f /. 2 = (GoB f) * (i + 2),j & f /. 2 = (GoB f) * (i + 1),(j + 1) ) or ( f /. 1 = (GoB f) * (i + 1),j & ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 2) = (GoB f) * i,j ) ) ) ) or ( ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) ) & f /. 1 = (GoB f) * (i + 1),j ) or ( ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) ) & ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 2) = (GoB f) * i,j ) ) ) ) ) by A1, A2, A3, A4, A5, A6, Th58, Th59;
suppose A12: ( f /. ((len f) -' 1) = (GoB f) * (i + 2),j & f /. ((len f) -' 1) = (GoB f) * (i + 1),(j + 1) ) ; :: thesis: contradiction
( [(i + 2),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_1:37;
then j = j + 1 by A12, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose A13: ( f /. 2 = (GoB f) * i,j & f /. 2 = (GoB f) * (i + 1),(j + 1) ) ; :: thesis: contradiction
( [i,j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A3, A4, A6, A10, A9, A8, MATRIX_1:37;
then j = j + 1 by A13, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose A14: ( f /. 2 = (GoB f) * (i + 2),j & f /. 2 = (GoB f) * i,j ) ; :: thesis: contradiction
( [(i + 2),j] in Indices (GoB f) & [i,j] in Indices (GoB f) ) by A1, A2, A3, A9, A7, A11, MATRIX_1:37;
then i = i + 2 by A14, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose A15: ( f /. 2 = (GoB f) * (i + 2),j & f /. 2 = (GoB f) * (i + 1),(j + 1) ) ; :: thesis: contradiction
( [(i + 2),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_1:37;
then j = j + 1 by A15, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose that A16: f /. 1 = (GoB f) * (i + 1),j and
A17: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 2) = (GoB f) * i,j ) ) ) ; :: thesis: contradiction
consider k being Element of NAT such that
A18: 1 <= k and
A19: ( k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j ) and
( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 2) = (GoB f) * i,j ) ) by A17;
1 < k + 1 by A18, NAT_1:13;
hence contradiction by A16, A19, Th38; :: thesis: verum
end;
suppose that A20: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) ) and
A21: f /. 1 = (GoB f) * (i + 1),j ; :: thesis: contradiction
consider k being Element of NAT such that
A22: 1 <= k and
A23: ( k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j ) and
( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) by A20;
1 < k + 1 by A22, NAT_1:13;
hence contradiction by A21, A23, Th38; :: thesis: verum
end;
suppose that A24: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 2),j ) or ( f /. k = (GoB f) * (i + 2),j & f /. (k + 2) = (GoB f) * i,j ) ) ) and
A25: ex k being Element of NAT st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i + 1),j & ( ( f /. k = (GoB f) * i,j & f /. (k + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k = (GoB f) * (i + 1),(j + 1) & f /. (k + 2) = (GoB f) * i,j ) ) ) ; :: thesis: contradiction
consider k1 being Element of NAT such that
1 <= k1 and
A26: k1 + 1 < len f and
A27: f /. (k1 + 1) = (GoB f) * (i + 1),j and
A28: ( ( f /. k1 = (GoB f) * i,j & f /. (k1 + 2) = (GoB f) * (i + 2),j ) or ( f /. k1 = (GoB f) * (i + 2),j & f /. (k1 + 2) = (GoB f) * i,j ) ) by A24;
consider k2 being Element of NAT such that
1 <= k2 and
A29: k2 + 1 < len f and
A30: f /. (k2 + 1) = (GoB f) * (i + 1),j and
A31: ( ( f /. k2 = (GoB f) * i,j & f /. (k2 + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k2 = (GoB f) * (i + 1),(j + 1) & f /. (k2 + 2) = (GoB f) * i,j ) ) by A25;
A32: now
assume A33: k1 <> k2 ; :: thesis: contradiction
end;
now
per cases ( ( f /. (k1 + 2) = (GoB f) * (i + 2),j & f /. (k2 + 2) = (GoB f) * (i + 1),(j + 1) ) or ( f /. k1 = (GoB f) * i,j & f /. k2 = (GoB f) * (i + 1),(j + 1) ) or ( f /. k1 = (GoB f) * (i + 2),j & f /. k2 = (GoB f) * i,j ) or ( f /. k1 = (GoB f) * (i + 2),j & f /. k2 = (GoB f) * (i + 1),(j + 1) ) ) by A28, A31;
suppose A34: ( f /. (k1 + 2) = (GoB f) * (i + 2),j & f /. (k2 + 2) = (GoB f) * (i + 1),(j + 1) ) ; :: thesis: contradiction
( [(i + 2),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_1:37;
then j = j + 1 by A32, A34, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose A35: ( f /. k1 = (GoB f) * i,j & f /. k2 = (GoB f) * (i + 1),(j + 1) ) ; :: thesis: contradiction
( [i,j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A3, A4, A6, A10, A9, A8, MATRIX_1:37;
then j = j + 1 by A32, A35, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose A36: ( f /. k1 = (GoB f) * (i + 2),j & f /. k2 = (GoB f) * i,j ) ; :: thesis: contradiction
( [(i + 2),j] in Indices (GoB f) & [i,j] in Indices (GoB f) ) by A1, A2, A3, A9, A7, A11, MATRIX_1:37;
then i = i + 2 by A32, A36, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
suppose A37: ( f /. k1 = (GoB f) * (i + 2),j & f /. k2 = (GoB f) * (i + 1),(j + 1) ) ; :: thesis: contradiction
( [(i + 2),j] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_1:37;
then j = j + 1 by A32, A37, GOBOARD1:21;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;