let f be non constant standard special_circular_sequence; :: thesis: for k being Element of NAT st 1 <= k & k + 2 <= len f holds
for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * i,1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * i,1 & f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) misses L~ f
let k be Element of NAT ; :: thesis: ( 1 <= k & k + 2 <= len f implies for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * i,1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * i,1 & f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; :: thesis: for i being Element of NAT st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * i,1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * i,1 & f /. k = (GoB f) * (i + 1),2 ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) misses L~ f
A3: 1 <= k + 1 by NAT_1:11;
A4: (k + 1) + 1 = k + (1 + 1) ;
then A5: k + 1 < len f by A2, NAT_1:13;
let i be Element of NAT ; :: thesis: ( 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * (i + 1),1 & ( ( f /. k = (GoB f) * i,1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * i,1 & f /. k = (GoB f) * (i + 1),2 ) ) implies LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) misses L~ f )
assume that
A6: ( 1 <= i & i + 2 <= len (GoB f) ) and
A7: f /. (k + 1) = (GoB f) * (i + 1),1 and
A8: ( ( f /. k = (GoB f) * i,1 & f /. (k + 2) = (GoB f) * (i + 1),2 ) or ( f /. (k + 2) = (GoB f) * i,1 & f /. k = (GoB f) * (i + 1),2 ) ) ; :: thesis: LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) misses L~ f
width (GoB f) <> 0 by GOBOARD1:def 5;
then A9: 0 + 1 <= width (GoB f) by NAT_1:14;
A10: (i + 1) + 1 = i + (1 + 1) ;
then A11: i + 1 < len (GoB f) by A6, NAT_1:13;
A12: 1 < width (GoB f) by GOBOARD7:35;
A13: 0 < width (GoB f) by A9, NAT_1:13;
A14: 1 <= i + 1 by NAT_1:11;
assume LSeg (((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1))) - |[0 ,1]|),((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),2))) meets L~ f ; :: thesis: contradiction
then A15: L~ f meets ((Int (cell (GoB f),(i + 1),0 )) \/ (Int (cell (GoB f),(i + 1),1))) \/ {((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1)))} by A10, A11, A12, A14, GOBOARD6:69, XBOOLE_1:63;
A16: L~ f misses Int (cell (GoB f),(i + 1),0 ) by A11, A13, GOBOARD7:14;
L~ f misses Int (cell (GoB f),(i + 1),1) by A9, A11, GOBOARD7:14;
then L~ f misses (Int (cell (GoB f),(i + 1),0 )) \/ (Int (cell (GoB f),(i + 1),1)) by A16, XBOOLE_1:70;
then L~ f meets {((1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1)))} by A15, XBOOLE_1:70;
then (1 / 2) * (((GoB f) * (i + 1),1) + ((GoB f) * (i + 2),1)) in L~ f by ZFMISC_1:56;
then consider k0 being Element of NAT such that
( 1 <= k0 & k0 + 1 <= len f ) and
A17: LSeg (f /. (k + 1)),((GoB f) * (i + 2),1) = LSeg f,k0 by A6, A7, A9, A10, A14, GOBOARD7:42;
A18: ( LSeg f,k0 c= L~ f & LSeg f,k c= L~ f & LSeg f,(k + 1) c= L~ f ) by TOPREAL3:26;
A19: LSeg f,k = LSeg (f /. k),(f /. (k + 1)) by A1, A5, TOPREAL1:def 5;
A20: 1 + 1 = 2 ;
LSeg f,(k + 1) = LSeg (f /. (k + 1)),(f /. (k + 2)) by A2, A3, A4, TOPREAL1:def 5;
hence contradiction by A6, A7, A8, A11, A12, A17, A18, A19, A20, GOBOARD7:63; :: thesis: verum