let f be non constant standard special_circular_sequence; :: thesis: for k being Nat st 1 <= k & k + 2 <= len f holds
for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) & ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f
let k be Nat; :: thesis: ( 1 <= k & k + 2 <= len f implies for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) & ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f )
assume that
A1: k >= 1 and
A2: k + 2 <= len f ; :: thesis: for i being Nat st 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) & ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) holds
LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f
A3: (k + 1) + 1 = k + (1 + 1) ;
then k + 1 < len f by A2, NAT_1:13;
then A4: ( LSeg (f,(k + 1)) c= L~ f & LSeg (f,k) = LSeg ((f /. k),(f /. (k + 1))) ) by A1, TOPREAL1:def 3, TOPREAL3:19;
1 <= k + 1 by NAT_1:11;
then A5: LSeg (f,(k + 1)) = LSeg ((f /. (k + 1)),(f /. (k + 2))) by A2, A3, TOPREAL1:def 3;
let i be Nat; :: thesis: ( 1 <= i & i + 2 <= len (GoB f) & f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) & ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) implies LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f )
assume that
A6: 1 <= i and
A7: i + 2 <= len (GoB f) and
A8: f /. (k + 1) = (GoB f) * ((i + 1),(width (GoB f))) and
A9: ( ( f /. k = (GoB f) * ((i + 2),(width (GoB f))) & f /. (k + 2) = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) or ( f /. (k + 2) = (GoB f) * ((i + 2),(width (GoB f))) & f /. k = (GoB f) * ((i + 1),((width (GoB f)) -' 1)) ) ) ; :: thesis: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) misses L~ f
(i + 1) + 1 = i + (1 + 1) ;
then A10: i + 1 < len (GoB f) by A7, NAT_1:13;
then A11: i < len (GoB f) by NAT_1:13;
then A12: L~ f misses Int (cell ((GoB f),i,(width (GoB f)))) by GOBOARD7:12;
assume A13: LSeg (((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|)) meets L~ f ; :: thesis: contradiction
A14: 1 < width (GoB f) by GOBOARD7:33;
then A15: ((width (GoB f)) -' 1) + 1 = width (GoB f) by XREAL_1:235;
then A16: (width (GoB f)) -' 1 < width (GoB f) by NAT_1:13;
then L~ f misses Int (cell ((GoB f),i,((width (GoB f)) -' 1))) by A11, GOBOARD7:12;
then A17: L~ f misses (Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ (Int (cell ((GoB f),i,(width (GoB f))))) by A12, XBOOLE_1:70;
A18: 1 <= (width (GoB f)) -' 1 by A14, A15, NAT_1:13;
then (1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f))))) = (1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),((width (GoB f)) -' 1)))) by A6, A15, A10, GOBOARD7:9;
then L~ f meets ((Int (cell ((GoB f),i,((width (GoB f)) -' 1)))) \/ (Int (cell ((GoB f),i,(width (GoB f)))))) \/ {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A6, A14, A11, A13, GOBOARD6:67, XBOOLE_1:63;
then L~ f meets {((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f))))))} by A17, XBOOLE_1:70;
then consider k0 being Nat such that
1 <= k0 and
k0 + 1 <= len f and
A19: LSeg ((f /. (k + 1)),((GoB f) * (i,(width (GoB f))))) = LSeg (f,k0) by A6, A8, A14, A10, GOBOARD7:40, ZFMISC_1:50;
( LSeg (f,k0) c= L~ f & LSeg (f,k) c= L~ f ) by TOPREAL3:19;
hence contradiction by A6, A8, A9, A15, A18, A16, A10, A19, A4, A5, GOBOARD7:62; :: thesis: verum