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 + 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; :: thesis: ( 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 ) ; :: thesis: 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)) ) ; :: thesis: 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 ; :: thesis: verum
end;
suppose A13: ( f /. ((len f) -' 1) = (GoB f) * ((i + 1),(j + 2)) & f /. ((len f) -' 1) = (GoB f) * (i,(j + 1)) ) ; :: thesis: 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 ; :: thesis: verum
end;
suppose A14: ( f /. 2 = (GoB f) * ((i + 1),(j + 2)) & f /. 2 = (GoB f) * (i,(j + 1)) ) ; :: thesis: 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 ; :: thesis: verum
end;
suppose A15: ( f /. 2 = (GoB f) * ((i + 1),(j + 2)) & f /. 2 = (GoB f) * ((i + 1),j) ) ; :: thesis: 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 A15, GOBOARD1:5;
hence contradiction ; :: thesis: verum
end;
suppose that A16: f /. 1 = (GoB f) * ((i + 1),(j + 1)) and
A17: 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)) ) ) ) ; :: thesis: contradiction
consider k being Nat such that
A18: 1 <= k and
A19: ( k + 1 < len f & f /. (k + 1) = (GoB f) * ((i + 1),(j + 1)) ) and
( ( 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 A17;
1 < k + 1 by A18, NAT_1:13;
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 + 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
A21: f /. 1 = (GoB f) * ((i + 1),(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 + 1),(j + 1)) ) and
( ( 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) ) ) by A20;
1 < k + 1 by A22, NAT_1:13;
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 + 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)) ) ) ) ; :: thesis: contradiction
consider 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 :: thesis: not k1 <> k2
assume A33: k1 <> k2 ; :: thesis: contradiction
end;
now :: thesis: contradiction
per 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)) ) ; :: thesis: 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 ; :: thesis: verum
end;
suppose A35: ( f /. (k1 + 2) = (GoB f) * ((i + 1),(j + 2)) & f /. (k2 + 2) = (GoB f) * (i,(j + 1)) ) ; :: thesis: 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 ; :: thesis: verum
end;
suppose A36: ( f /. k1 = (GoB f) * ((i + 1),(j + 2)) & f /. k2 = (GoB f) * (i,(j + 1)) ) ; :: thesis: 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 ; :: thesis: verum
end;
suppose A37: ( f /. k1 = (GoB f) * ((i + 1),(j + 2)) & f /. k2 = (GoB f) * ((i + 1),j) ) ; :: thesis: 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 ; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;