let i, j be Nat; :: thesis: 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,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(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; :: thesis: ( 1 <= i & i < len (GoB f) & 1 <= j & j + 1 < width (GoB f) & LSeg (((GoB f) * (i,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(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,j)),((GoB f) * (i,(j + 1)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * (i,(j + 2)))) c= L~ f & LSeg (((GoB f) * (i,(j + 1))),((GoB f) * ((i + 1),(j + 1)))) c= L~ f ) ; :: thesis: contradiction
A6: i + 1 <= len (GoB f) by ;
j + (1 + 1) = (j + 1) + 1 ;
then A7: j + 2 <= width (GoB f) by ;
A8: 1 <= j + 1 by NAT_1:11;
A9: j < width (GoB f) by ;
A10: 1 <= i + 1 by NAT_1:11;
j + 1 <= j + 2 by XREAL_1:6;
then A11: 1 <= j + 2 by ;
per cases ( ( f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) & 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,(j + 2)) & f /. 2 = (GoB f) * (i,j) ) or ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. 2 = (GoB f) * ((i + 1),(j + 1)) ) or ( f /. 1 = (GoB f) * (i,(j + 1)) & ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( 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 Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) & f /. 1 = (GoB f) * (i,(j + 1)) ) or ( ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) & ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( 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, Th53, Th54;
suppose A12: ( f /. ((len f) -' 1) = (GoB f) * (i,(j + 2)) & f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 1)) ) ; :: thesis: contradiction
( [i,(j + 2)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then i = i + 1 by ;
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_0:30;
then i = i + 1 by ;
hence contradiction ; :: thesis: verum
end;
suppose A14: ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. 2 = (GoB f) * (i,j) ) ; :: thesis: contradiction
( [i,(j + 2)] in Indices (GoB f) & [i,j] in Indices (GoB f) ) by A1, A2, A3, A9, A7, A11, MATRIX_0:30;
then j = j + 2 by ;
hence contradiction ; :: thesis: verum
end;
suppose A15: ( f /. 2 = (GoB f) * (i,(j + 2)) & f /. 2 = (GoB f) * ((i + 1),(j + 1)) ) ; :: thesis: contradiction
( [i,(j + 2)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then i = i + 1 by ;
hence contradiction ; :: thesis: verum
end;
suppose that A16: f /. 1 = (GoB f) * (i,(j + 1)) and
A17: ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( 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 Nat such that
A18: 1 <= k and
A19: ( k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) ) 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 ;
hence contradiction by A16, A19, Th36; :: thesis: verum
end;
suppose that A20: ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) and
A21: f /. 1 = (GoB f) * (i,(j + 1)) ; :: thesis: contradiction
consider k being Nat such that
A22: 1 <= k and
A23: ( k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) ) and
( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) by A20;
1 < k + 1 by ;
hence contradiction by A21, A23, Th36; :: thesis: verum
end;
suppose that A24: ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( f /. k = (GoB f) * (i,j) & f /. (k + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k = (GoB f) * (i,(j + 2)) & f /. (k + 2) = (GoB f) * (i,j) ) ) ) and
A25: ex k being Nat st
( 1 <= k & k + 1 < len f & f /. (k + 1) = (GoB f) * (i,(j + 1)) & ( ( 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 Nat such that
1 <= k1 and
A26: k1 + 1 < len f and
A27: f /. (k1 + 1) = (GoB f) * (i,(j + 1)) and
A28: ( ( f /. k1 = (GoB f) * (i,j) & f /. (k1 + 2) = (GoB f) * (i,(j + 2)) ) or ( f /. k1 = (GoB f) * (i,(j + 2)) & f /. (k1 + 2) = (GoB f) * (i,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,(j + 1)) 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 :: thesis: not k1 <> k2
assume A33: k1 <> k2 ; :: thesis: contradiction
end;
per cases ( ( f /. (k1 + 2) = (GoB f) * (i,(j + 2)) & 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,(j + 2)) & f /. k2 = (GoB f) * (i,j) ) or ( f /. k1 = (GoB f) * (i,(j + 2)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) ) ) by ;
suppose A34: ( f /. (k1 + 2) = (GoB f) * (i,(j + 2)) & f /. (k2 + 2) = (GoB f) * ((i + 1),(j + 1)) ) ; :: thesis: contradiction
( [i,(j + 2)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then i = i + 1 by ;
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_0:30;
then i = i + 1 by ;
hence contradiction ; :: thesis: verum
end;
suppose A36: ( f /. k1 = (GoB f) * (i,(j + 2)) & f /. k2 = (GoB f) * (i,j) ) ; :: thesis: contradiction
( [i,(j + 2)] in Indices (GoB f) & [i,j] in Indices (GoB f) ) by A1, A2, A3, A9, A7, A11, MATRIX_0:30;
then j = j + 2 by ;
hence contradiction ; :: thesis: verum
end;
suppose A37: ( f /. k1 = (GoB f) * (i,(j + 2)) & f /. k2 = (GoB f) * ((i + 1),(j + 1)) ) ; :: thesis: contradiction
( [i,(j + 2)] in Indices (GoB f) & [(i + 1),(j + 1)] in Indices (GoB f) ) by A1, A2, A4, A6, A10, A8, A7, A11, MATRIX_0:30;
then i = i + 1 by ;
hence contradiction ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;