goboard8.miz



    begin

    reserve i,j,k,i1,j1 for Nat,

p for Point of ( TOP-REAL 2),

x for set;

    reserve f for non constant standard special_circular_sequence;

    theorem :: GOBOARD8:1

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= i & (i + 1) <= ( len ( GoB f)) & 1 <= j & (j + 2) <= ( width ( GoB 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 + 2)) = (( GoB f) * ((i + 1),j)) & (f /. k) = (( GoB f) * ((i + 1),(j + 2)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= i and

       A7: (i + 1) <= ( len ( GoB f)) and

       A8: 1 <= j and

       A9: (j + 2) <= ( width ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 1),j)) & (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) & (f /. k) = (( GoB f) * ((i + 1),(j + 2)));

      

       A12: i < ( len ( GoB f)) by A7, NAT_1: 13;

      j < (j + 2) by XREAL_1: 29;

      then j <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then

       A13: ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A12, GOBOARD7: 12;

      (j + 1) <= (j + 2) by XREAL_1: 6;

      then

       A14: (j + 1) <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),i,(j + 1)))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) by A13, XBOOLE_1: 70;

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A16: (j + 1) < ( width ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) \/ {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A16, A12, GOBOARD6: 64, XBOOLE_1: 63;

      then 1 <= (j + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))} by A15, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A17: ( LSeg ((f /. (k + 1)),(( GoB f) * (i,(j + 1))))) = ( LSeg (f,k0)) by A6, A7, A10, A14, 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, A10, A11, A16, A12, A17, A4, A5, GOBOARD7: 60;

    end;

    theorem :: GOBOARD8:2

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= i & (i + 2) <= ( len ( GoB f)) & 1 <= j & (j + 2) <= ( width ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * ((i + 2),(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) or (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),(j + 2)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= i and

       A7: (i + 2) <= ( len ( GoB f)) and

       A8: 1 <= j and

       A9: (j + 2) <= ( width ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 2),(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) or (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),(j + 2)));

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A12: (i + 1) < ( len ( GoB f)) by A7, NAT_1: 13;

      then

       A13: i < ( len ( GoB f)) by NAT_1: 13;

      j < (j + 2) by XREAL_1: 29;

      then j < ( width ( GoB f)) by A9, XXREAL_0: 2;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A13, GOBOARD7: 12;

      (j + 1) <= (j + 2) by XREAL_1: 6;

      then

       A15: (j + 1) <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),i,(j + 1)))) by A13, GOBOARD7: 12;

      then

       A16: ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) by A14, XBOOLE_1: 70;

      

       A17: 1 <= (j + 1) by NAT_1: 11;

      

       A18: ((j + 1) + 1) = (j + (1 + 1));

      then

       A19: (j + 1) < ( width ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) \/ {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A19, A13, GOBOARD6: 64, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))} by A16, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A20: ( LSeg ((f /. (k + 1)),(( GoB f) * (i,(j + 1))))) = ( LSeg (f,k0)) by A6, A10, A17, A15, A12, GOBOARD7: 40, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A10, A11, A17, A12, A18, A19, A20, A4, A5, GOBOARD7: 61;

    end;

    theorem :: GOBOARD8:3

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= i & (i + 2) <= ( len ( GoB f)) & 1 <= j & (j + 2) <= ( width ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * ((i + 2),(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) or (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),j))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= i and

       A7: (i + 2) <= ( len ( GoB f)) and

       A8: 1 <= j and

       A9: (j + 2) <= ( width ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 2),(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) or (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),j));

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A12: (i + 1) < ( len ( GoB f)) by A7, NAT_1: 13;

      then

       A13: i < ( len ( GoB f)) by NAT_1: 13;

      (j + 1) <= (j + 2) by XREAL_1: 6;

      then

       A14: (j + 1) <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then

       A15: ( L~ f) misses ( Int ( cell (( GoB f),i,(j + 1)))) by A13, GOBOARD7: 12;

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A16: (j + 1) < ( width ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) meets ( L~ f);

      then

       A17: ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) \/ {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A16, A13, GOBOARD6: 64, XBOOLE_1: 63;

      j < (j + 2) by XREAL_1: 29;

      then

       A18: j < ( width ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A13, GOBOARD7: 12;

      then ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) by A15, XBOOLE_1: 70;

      then 1 <= (j + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))} by A17, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A19: ( LSeg ((f /. (k + 1)),(( GoB f) * (i,(j + 1))))) = ( LSeg (f,k0)) by A6, A10, A14, A12, 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, A10, A11, A18, A12, A19, A4, A5, GOBOARD7: 62;

    end;

    theorem :: GOBOARD8:4

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= i & (i + 1) <= ( len ( GoB f)) & 1 <= j & (j + 2) <= ( width ( GoB 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 + 2)) = (( GoB f) * (i,j)) & (f /. k) = (( GoB f) * (i,(j + 2)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= i and

       A7: (i + 1) <= ( len ( GoB f)) and

       A8: 1 <= j and

       A9: (j + 2) <= ( width ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * (i,(j + 1))) and

       A11: (f /. k) = (( GoB f) * (i,j)) & (f /. (k + 2)) = (( GoB f) * (i,(j + 2))) or (f /. (k + 2)) = (( GoB f) * (i,j)) & (f /. k) = (( GoB f) * (i,(j + 2)));

      

       A12: i < ( len ( GoB f)) by A7, NAT_1: 13;

      j < (j + 2) by XREAL_1: 29;

      then j <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then

       A13: ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A12, GOBOARD7: 12;

      (j + 1) <= (j + 2) by XREAL_1: 6;

      then

       A14: (j + 1) <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),i,(j + 1)))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) by A13, XBOOLE_1: 70;

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A16: (j + 1) < ( width ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),i,(j + 1))))) \/ {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A16, A12, GOBOARD6: 64, XBOOLE_1: 63;

      then 1 <= (j + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 1)))))} by A15, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A17: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),(j + 1))))) = ( LSeg (f,k0)) by A6, A7, A10, A14, 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, A10, A11, A16, A12, A17, A4, A5, GOBOARD7: 59;

    end;

    theorem :: GOBOARD8:5

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= i & (i + 2) <= ( len ( GoB f)) & 1 <= j & (j + 2) <= ( width ( GoB 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 + 2))) or (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),(j + 2)))) holds ( LSeg (((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= i and

       A7: (i + 2) <= ( len ( GoB f)) and

       A8: 1 <= j and

       A9: (j + 2) <= ( width ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * (i,(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) or (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),(j + 2)));

      

       A12: ((i + 1) + 1) = (i + (1 + 1));

      then

       A13: (i + 1) < ( len ( GoB f)) by A7, NAT_1: 13;

      j < (j + 2) by XREAL_1: 29;

      then j < ( width ( GoB f)) by A9, XXREAL_0: 2;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),j))) by A13, GOBOARD7: 12;

      (j + 1) <= (j + 2) by XREAL_1: 6;

      then

       A15: (j + 1) <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),(j + 1)))) by A13, GOBOARD7: 12;

      then

       A16: ( L~ f) misses (( Int ( cell (( GoB f),(i + 1),j))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) by A14, XBOOLE_1: 70;

      

       A17: 1 <= (j + 1) by NAT_1: 11;

      

       A18: ((j + 1) + 1) = (j + (1 + 1));

      then

       A19: (j + 1) < ( width ( GoB f)) by A9, NAT_1: 13;

      

       A20: 1 <= (i + 1) by NAT_1: 11;

      assume ( LSeg (((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),(i + 1),j))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 1)))))}) by A8, A12, A13, A19, A20, GOBOARD6: 64, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 1)))))} by A16, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A21: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 2),(j + 1))))) = ( LSeg (f,k0)) by A7, A10, A17, A15, A12, A20, GOBOARD7: 40, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A10, A11, A17, A13, A18, A19, A21, A4, A5, GOBOARD7: 61;

    end;

    theorem :: GOBOARD8:6

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= i & (i + 2) <= ( len ( GoB f)) & 1 <= j & (j + 2) <= ( width ( GoB 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 + 2)) = (( GoB f) * (i,(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),j))) holds ( LSeg (((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= i and

       A7: (i + 2) <= ( len ( GoB f)) and

       A8: 1 <= j and

       A9: (j + 2) <= ( width ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * (i,(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) or (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) & (f /. k) = (( GoB f) * ((i + 1),j));

      

       A12: ((i + 1) + 1) = (i + (1 + 1));

      then

       A13: (i + 1) < ( len ( GoB f)) by A7, NAT_1: 13;

      (j + 1) <= (j + 2) by XREAL_1: 6;

      then

       A14: (j + 1) <= ( width ( GoB f)) by A9, XXREAL_0: 2;

      then

       A15: ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),(j + 1)))) by A13, GOBOARD7: 12;

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A16: (j + 1) < ( width ( GoB f)) by A9, NAT_1: 13;

      

       A17: 1 <= (i + 1) by NAT_1: 11;

      j < (j + 2) by XREAL_1: 29;

      then

       A18: j < ( width ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),j))) by A13, GOBOARD7: 12;

      then

       A19: ( L~ f) misses (( Int ( cell (( GoB f),(i + 1),j))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) by A15, XBOOLE_1: 70;

      assume ( LSeg (((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),(i + 1),j))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 1)))))}) by A8, A12, A13, A16, A17, GOBOARD6: 64, XBOOLE_1: 63;

      then 1 <= (j + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 1)))))} by A19, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A20: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 2),(j + 1))))) = ( LSeg (f,k0)) by A7, A10, A14, A12, A17, 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, A10, A11, A18, A13, A20, A4, A5, GOBOARD7: 62;

    end;

    theorem :: GOBOARD8:7

    for k st 1 <= k & (k + 2) <= ( len f) holds for i st 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),1)) & ((f /. k) = (( GoB f) * ((i + 2),1)) & (f /. (k + 2)) = (( GoB f) * ((i + 1),2)) or (f /. (k + 2)) = (( GoB f) * ((i + 2),1)) & (f /. k) = (( GoB f) * ((i + 1),2))) holds ( LSeg ((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),2)))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len f);

      

       A3: ((k + 1) + 1) = (k + (1 + 1));

      then (k + 1) < ( len f) by A2, NAT_1: 13;

      then

       A4: ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by A1, TOPREAL1:def 3;

      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;

      

       A6: 1 < ( width ( GoB f)) by GOBOARD7: 33;

      let i such that

       A7: 1 <= i and

       A8: (i + 2) <= ( len ( GoB f)) and

       A9: (f /. (k + 1)) = (( GoB f) * ((i + 1),1)) and

       A10: (f /. k) = (( GoB f) * ((i + 2),1)) & (f /. (k + 2)) = (( GoB f) * ((i + 1),2)) or (f /. (k + 2)) = (( GoB f) * ((i + 2),1)) & (f /. k) = (( GoB f) * ((i + 1),2));

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A11: (i + 1) < ( len ( GoB f)) by A8, NAT_1: 13;

      then

       A12: i < ( len ( GoB f)) by NAT_1: 13;

      ( width ( GoB f)) <> 0 by MATRIX_0:def 10;

      then

       A13: ( 0 + 1) <= ( width ( GoB f)) by NAT_1: 14;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),i,1))) by A12, GOBOARD7: 12;

       0 < ( width ( GoB f)) by A13;

      then ( L~ f) misses ( Int ( cell (( GoB f),i, 0 ))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f),i, 0 ))) \/ ( Int ( cell (( GoB f),i,1)))) by A14, XBOOLE_1: 70;

      assume ( LSeg ((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|),((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),2)))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i, 0 ))) \/ ( Int ( cell (( GoB f),i,1)))) \/ {((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1))))}) by A7, A6, A12, GOBOARD6: 66, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1))))} by A15, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A16: ( LSeg ((f /. (k + 1)),(( GoB f) * (i,1)))) = ( LSeg (f,k0)) by A7, A9, A13, A11, GOBOARD7: 40, ZFMISC_1: 50;

      

       A17: ( LSeg (f,(k + 1))) c= ( L~ f) & (1 + 1) = 2 by TOPREAL3: 19;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A7, A9, A10, A11, A6, A16, A17, A4, A5, GOBOARD7: 61;

    end;

    theorem :: GOBOARD8:8

    for k st 1 <= k & (k + 2) <= ( len f) holds for i 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)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len f);

      

       A3: ((k + 1) + 1) = (k + (1 + 1));

      then (k + 1) < ( len f) by A2, NAT_1: 13;

      then

       A4: ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by A1, TOPREAL1:def 3;

      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;

      

       A6: 1 < ( width ( GoB f)) by GOBOARD7: 33;

      let i such that

       A7: 1 <= i and

       A8: (i + 2) <= ( len ( GoB f)) and

       A9: (f /. (k + 1)) = (( GoB f) * ((i + 1),1)) and

       A10: (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));

      

       A11: ((i + 1) + 1) = (i + (1 + 1));

      then

       A12: (i + 1) < ( len ( GoB f)) by A8, NAT_1: 13;

      ( width ( GoB f)) <> 0 by MATRIX_0:def 10;

      then

       A13: ( 0 + 1) <= ( width ( GoB f)) by NAT_1: 14;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),1))) by A12, GOBOARD7: 12;

       0 < ( width ( GoB f)) by A13;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1), 0 ))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f),(i + 1), 0 ))) \/ ( Int ( cell (( GoB f),(i + 1),1)))) by A14, XBOOLE_1: 70;

      

       A16: 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);

      then ( 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 A11, A12, A6, A16, GOBOARD6: 66, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),1)) + (( GoB f) * ((i + 2),1))))} by A15, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A17: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 2),1)))) = ( LSeg (f,k0)) by A8, A9, A13, A11, A16, GOBOARD7: 40, ZFMISC_1: 50;

      

       A18: ( LSeg (f,(k + 1))) c= ( L~ f) & (1 + 1) = 2 by TOPREAL3: 19;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A7, A9, A10, A12, A6, A17, A4, A18, A5, GOBOARD7: 61;

    end;

    theorem :: GOBOARD8:9

    for k st 1 <= k & (k + 2) <= ( len f) holds for i 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)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 such 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)));

      ((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);

      

       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 be 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;

    end;

    theorem :: GOBOARD8:10

    for k st 1 <= k & (k + 2) <= ( len f) holds for i st 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),( width ( GoB f)))) & ((f /. k) = (( GoB f) * (i,( width ( GoB f)))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),(( width ( GoB f)) -' 1))) or (f /. (k + 2)) = (( GoB f) * (i,( width ( GoB f)))) & (f /. k) = (( GoB f) * ((i + 1),(( width ( GoB f)) -' 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * ((i + 1),(( width ( GoB f)) -' 1))) + (( GoB f) * ((i + 2),( width ( GoB f)))))),(((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 such 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,( width ( GoB f)))) & (f /. (k + 2)) = (( GoB f) * ((i + 1),(( width ( GoB f)) -' 1))) or (f /. (k + 2)) = (( GoB f) * (i,( width ( GoB f)))) & (f /. k) = (( GoB f) * ((i + 1),(( width ( GoB f)) -' 1)));

      

       A10: ((i + 1) + 1) = (i + (1 + 1));

      then

       A11: (i + 1) < ( len ( GoB f)) by A7, NAT_1: 13;

      then

       A12: ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),( width ( GoB f))))) by GOBOARD7: 12;

      

       A13: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      then

       A14: ((( width ( GoB f)) -' 1) + 1) = ( width ( GoB f)) by XREAL_1: 235;

      then

       A15: (( width ( GoB f)) -' 1) < ( width ( GoB f)) by NAT_1: 13;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),(( width ( GoB f)) -' 1)))) by A11, GOBOARD7: 12;

      then

       A16: ( L~ f) misses (( Int ( cell (( GoB f),(i + 1),(( width ( GoB f)) -' 1)))) \/ ( Int ( cell (( GoB f),(i + 1),( width ( GoB f)))))) by A12, XBOOLE_1: 70;

      assume

       A17: ( LSeg (((1 / 2) * ((( GoB f) * ((i + 1),(( width ( GoB f)) -' 1))) + (( GoB f) * ((i + 2),( width ( GoB f)))))),(((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|))) meets ( L~ f);

      

       A18: 1 <= (i + 1) by NAT_1: 11;

      

       A19: 1 < ( width ( GoB f)) by GOBOARD7: 33;

      then

       A20: 1 <= (( width ( GoB f)) -' 1) by A14, NAT_1: 13;

      then ((1 / 2) * ((( GoB f) * ((i + 1),(( width ( GoB f)) -' 1))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) = ((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),(( width ( GoB f)) -' 1))))) by A7, A14, A10, A18, GOBOARD7: 9;

      then ( L~ f) meets ((( Int ( cell (( GoB f),(i + 1),(( width ( GoB f)) -' 1)))) \/ ( Int ( cell (( GoB f),(i + 1),( width ( GoB f)))))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f))))))}) by A19, A10, A11, A18, A17, GOBOARD6: 67, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f))))))} by A16, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A21: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 2),( width ( GoB f)))))) = ( LSeg (f,k0)) by A7, A8, A13, A10, A18, 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, A14, A20, A15, A11, A21, A4, A5, GOBOARD7: 62;

    end;

    theorem :: GOBOARD8:11

    for k st 1 <= k & (k + 2) <= ( len f) holds for i, j st 1 <= j & (j + 1) <= ( width ( GoB f)) & 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * (i,(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) or (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) & (f /. k) = (( GoB f) * ((i + 2),(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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, j such that

       A6: 1 <= j and

       A7: (j + 1) <= ( width ( GoB f)) and

       A8: 1 <= i and

       A9: (i + 2) <= ( len ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * (i,(j + 1))) & (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) or (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) & (f /. k) = (( GoB f) * ((i + 2),(j + 1)));

      

       A12: j < ( width ( GoB f)) by A7, NAT_1: 13;

      i < (i + 2) by XREAL_1: 29;

      then i <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then

       A13: ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A12, GOBOARD7: 12;

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A14: (i + 1) <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),j))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) by A13, XBOOLE_1: 70;

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A16: (i + 1) < ( len ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A16, A12, GOBOARD6: 65, XBOOLE_1: 63;

      then 1 <= (i + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))} by A15, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A17: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),j)))) = ( LSeg (f,k0)) by A6, A7, A10, A14, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A8, A10, A11, A16, A12, A17, A4, A5, GOBOARD7: 62;

    end;

    theorem :: GOBOARD8:12

    for k st 1 <= k & (k + 2) <= ( len f) holds for j, i st 1 <= j & (j + 2) <= ( width ( GoB f)) & 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * ((i + 1),(j + 2))) & (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) & (f /. k) = (( GoB f) * ((i + 2),(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j, i such that

       A6: 1 <= j and

       A7: (j + 2) <= ( width ( GoB f)) and

       A8: 1 <= i and

       A9: (i + 2) <= ( len ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 1),(j + 2))) & (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) & (f /. k) = (( GoB f) * ((i + 2),(j + 1)));

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A12: (j + 1) < ( width ( GoB f)) by A7, NAT_1: 13;

      then

       A13: j < ( width ( GoB f)) by NAT_1: 13;

      i < (i + 2) by XREAL_1: 29;

      then i < ( len ( GoB f)) by A9, XXREAL_0: 2;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A13, GOBOARD7: 12;

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A15: (i + 1) <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),j))) by A13, GOBOARD7: 12;

      then

       A16: ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) by A14, XBOOLE_1: 70;

      

       A17: 1 <= (i + 1) by NAT_1: 11;

      

       A18: ((i + 1) + 1) = (i + (1 + 1));

      then

       A19: (i + 1) < ( len ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A19, A13, GOBOARD6: 65, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))} by A16, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A20: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),j)))) = ( LSeg (f,k0)) by A6, A10, A17, A15, A12, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A10, A11, A17, A12, A18, A19, A20, A4, A5, GOBOARD7: 59;

    end;

    theorem :: GOBOARD8:13

    for k st 1 <= k & (k + 2) <= ( len f) holds for j, i st 1 <= j & (j + 2) <= ( width ( GoB f)) & 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * ((i + 1),(j + 2))) & (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) & (f /. k) = (( GoB f) * (i,(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j, i such that

       A6: 1 <= j and

       A7: (j + 2) <= ( width ( GoB f)) and

       A8: 1 <= i and

       A9: (i + 2) <= ( len ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 1),(j + 2))) & (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),(j + 2))) & (f /. k) = (( GoB f) * (i,(j + 1)));

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A12: (j + 1) < ( width ( GoB f)) by A7, NAT_1: 13;

      then

       A13: j < ( width ( GoB f)) by NAT_1: 13;

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A14: (i + 1) <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then

       A15: ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),j))) by A13, GOBOARD7: 12;

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A16: (i + 1) < ( len ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) meets ( L~ f);

      then

       A17: ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A16, A13, GOBOARD6: 65, XBOOLE_1: 63;

      i < (i + 2) by XREAL_1: 29;

      then

       A18: i < ( len ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A13, GOBOARD7: 12;

      then ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) by A15, XBOOLE_1: 70;

      then 1 <= (i + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))} by A17, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A19: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),j)))) = ( LSeg (f,k0)) by A6, A10, A14, A12, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A8, A10, A11, A18, A12, A19, A4, A5, GOBOARD7: 60;

    end;

    theorem :: GOBOARD8:14

    for k st 1 <= k & (k + 2) <= ( len f) holds for j, i st 1 <= j & (j + 1) <= ( width ( GoB f)) & 1 <= i & (i + 2) <= ( len ( GoB 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 + 2)) = (( GoB f) * (i,j)) & (f /. k) = (( GoB f) * ((i + 2),j))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j, i such that

       A6: 1 <= j and

       A7: (j + 1) <= ( width ( GoB f)) and

       A8: 1 <= i and

       A9: (i + 2) <= ( len ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),j)) and

       A11: (f /. k) = (( GoB f) * (i,j)) & (f /. (k + 2)) = (( GoB f) * ((i + 2),j)) or (f /. (k + 2)) = (( GoB f) * (i,j)) & (f /. k) = (( GoB f) * ((i + 2),j));

      

       A12: j < ( width ( GoB f)) by A7, NAT_1: 13;

      i < (i + 2) by XREAL_1: 29;

      then i <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then

       A13: ( L~ f) misses ( Int ( cell (( GoB f),i,j))) by A12, GOBOARD7: 12;

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A14: (i + 1) <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),j))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) by A13, XBOOLE_1: 70;

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A16: (i + 1) < ( len ( GoB f)) by A9, NAT_1: 13;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,j)) + (( GoB f) * ((i + 1),(j + 1))))),((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 2),(j + 1))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,j))) \/ ( Int ( cell (( GoB f),(i + 1),j)))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))}) by A6, A8, A16, A12, GOBOARD6: 65, XBOOLE_1: 63;

      then 1 <= (i + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),j)) + (( GoB f) * ((i + 1),(j + 1)))))} by A15, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A17: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),(j + 1))))) = ( LSeg (f,k0)) by A6, A7, A10, A14, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A8, A10, A11, A16, A12, A17, A4, A5, GOBOARD7: 61;

    end;

    theorem :: GOBOARD8:15

    for k st 1 <= k & (k + 2) <= ( len f) holds for j, i st 1 <= j & (j + 2) <= ( width ( GoB f)) & 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * ((i + 1),j)) & (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) & (f /. k) = (( GoB f) * ((i + 2),(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j, i such that

       A6: 1 <= j and

       A7: (j + 2) <= ( width ( GoB f)) and

       A8: 1 <= i and

       A9: (i + 2) <= ( len ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 1),j)) & (f /. (k + 2)) = (( GoB f) * ((i + 2),(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) & (f /. k) = (( GoB f) * ((i + 2),(j + 1)));

      

       A12: ((j + 1) + 1) = (j + (1 + 1));

      then

       A13: (j + 1) < ( width ( GoB f)) by A7, NAT_1: 13;

      i < (i + 2) by XREAL_1: 29;

      then i < ( len ( GoB f)) by A9, XXREAL_0: 2;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),i,(j + 1)))) by A13, GOBOARD7: 12;

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A15: (i + 1) <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),(j + 1)))) by A13, GOBOARD7: 12;

      then

       A16: ( L~ f) misses (( Int ( cell (( GoB f),i,(j + 1)))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) by A14, XBOOLE_1: 70;

      

       A17: 1 <= (i + 1) by NAT_1: 11;

      

       A18: ((i + 1) + 1) = (i + (1 + 1));

      then

       A19: (i + 1) < ( len ( GoB f)) by A9, NAT_1: 13;

      

       A20: 1 <= (j + 1) by NAT_1: 11;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,(j + 1)))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 1),(j + 2)))))}) by A8, A12, A13, A19, A20, GOBOARD6: 65, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 1),(j + 2)))))} by A16, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A21: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),(j + 2))))) = ( LSeg (f,k0)) by A7, A10, A17, A15, A12, A20, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A10, A11, A17, A13, A18, A19, A21, A4, A5, GOBOARD7: 59;

    end;

    theorem :: GOBOARD8:16

    for k st 1 <= k & (k + 2) <= ( len f) holds for j, i st 1 <= j & (j + 2) <= ( width ( GoB f)) & 1 <= i & (i + 2) <= ( len ( GoB f)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) & ((f /. k) = (( GoB f) * ((i + 1),j)) & (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) & (f /. k) = (( GoB f) * (i,(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j, i such that

       A6: 1 <= j and

       A7: (j + 2) <= ( width ( GoB f)) and

       A8: 1 <= i and

       A9: (i + 2) <= ( len ( GoB f)) and

       A10: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) and

       A11: (f /. k) = (( GoB f) * ((i + 1),j)) & (f /. (k + 2)) = (( GoB f) * (i,(j + 1))) or (f /. (k + 2)) = (( GoB f) * ((i + 1),j)) & (f /. k) = (( GoB f) * (i,(j + 1)));

      

       A12: ((j + 1) + 1) = (j + (1 + 1));

      then

       A13: (j + 1) < ( width ( GoB f)) by A7, NAT_1: 13;

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A14: (i + 1) <= ( len ( GoB f)) by A9, XXREAL_0: 2;

      then

       A15: ( L~ f) misses ( Int ( cell (( GoB f),(i + 1),(j + 1)))) by A13, GOBOARD7: 12;

      ((i + 1) + 1) = (i + (1 + 1));

      then

       A16: (i + 1) < ( len ( GoB f)) by A9, NAT_1: 13;

      

       A17: 1 <= (j + 1) by NAT_1: 11;

      i < (i + 2) by XREAL_1: 29;

      then

       A18: i < ( len ( GoB f)) by A9, XXREAL_0: 2;

      then ( L~ f) misses ( Int ( cell (( GoB f),i,(j + 1)))) by A13, GOBOARD7: 12;

      then

       A19: ( L~ f) misses (( Int ( cell (( GoB f),i,(j + 1)))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) by A15, XBOOLE_1: 70;

      assume ( LSeg (((1 / 2) * ((( GoB f) * (i,(j + 1))) + (( GoB f) * ((i + 1),(j + 2))))),((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 2),(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f),i,(j + 1)))) \/ ( Int ( cell (( GoB f),(i + 1),(j + 1))))) \/ {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 1),(j + 2)))))}) by A8, A12, A13, A16, A17, GOBOARD6: 65, XBOOLE_1: 63;

      then 1 <= (i + 1) & ( L~ f) meets {((1 / 2) * ((( GoB f) * ((i + 1),(j + 1))) + (( GoB f) * ((i + 1),(j + 2)))))} by A19, NAT_1: 11, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A20: ( LSeg ((f /. (k + 1)),(( GoB f) * ((i + 1),(j + 2))))) = ( LSeg (f,k0)) by A7, A10, A14, A12, A17, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A8, A10, A11, A18, A13, A20, A4, A5, GOBOARD7: 60;

    end;

    theorem :: GOBOARD8:17

    for k st 1 <= k & (k + 2) <= ( len f) holds for j st 1 <= j & (j + 2) <= ( width ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (1,(j + 1))) & ((f /. k) = (( GoB f) * (1,(j + 2))) & (f /. (k + 2)) = (( GoB f) * (2,(j + 1))) or (f /. (k + 2)) = (( GoB f) * (1,(j + 2))) & (f /. k) = (( GoB f) * (2,(j + 1)))) holds ( LSeg ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (2,(j + 1))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len f);

      

       A3: ((k + 1) + 1) = (k + (1 + 1));

      then (k + 1) < ( len f) by A2, NAT_1: 13;

      then

       A4: ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by A1, TOPREAL1:def 3;

      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;

      

       A6: 1 < ( len ( GoB f)) by GOBOARD7: 32;

      let j such that

       A7: 1 <= j and

       A8: (j + 2) <= ( width ( GoB f)) and

       A9: (f /. (k + 1)) = (( GoB f) * (1,(j + 1))) and

       A10: (f /. k) = (( GoB f) * (1,(j + 2))) & (f /. (k + 2)) = (( GoB f) * (2,(j + 1))) or (f /. (k + 2)) = (( GoB f) * (1,(j + 2))) & (f /. k) = (( GoB f) * (2,(j + 1)));

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A11: (j + 1) < ( width ( GoB f)) by A8, NAT_1: 13;

      then

       A12: j < ( width ( GoB f)) by NAT_1: 13;

      ( len ( GoB f)) <> 0 by MATRIX_0:def 10;

      then

       A13: ( 0 + 1) <= ( len ( GoB f)) by NAT_1: 14;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),1,j))) by A12, GOBOARD7: 12;

       0 < ( len ( GoB f)) by A13;

      then ( L~ f) misses ( Int ( cell (( GoB f), 0 ,j))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f), 0 ,j))) \/ ( Int ( cell (( GoB f),1,j)))) by A14, XBOOLE_1: 70;

      assume ( LSeg ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (2,(j + 1))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f), 0 ,j))) \/ ( Int ( cell (( GoB f),1,j)))) \/ {((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1)))))}) by A7, A6, A12, GOBOARD6: 68, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1)))))} by A15, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A16: ( LSeg ((f /. (k + 1)),(( GoB f) * (1,j)))) = ( LSeg (f,k0)) by A7, A9, A13, A11, GOBOARD7: 39, ZFMISC_1: 50;

      

       A17: ( LSeg (f,(k + 1))) c= ( L~ f) & (1 + 1) = 2 by TOPREAL3: 19;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A7, A9, A10, A11, A6, A16, A17, A4, A5, GOBOARD7: 59;

    end;

    theorem :: GOBOARD8:18

    for k st 1 <= k & (k + 2) <= ( len f) holds for j st 1 <= j & (j + 2) <= ( width ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (1,(j + 1))) & ((f /. k) = (( GoB f) * (1,j)) & (f /. (k + 2)) = (( GoB f) * (2,(j + 1))) or (f /. (k + 2)) = (( GoB f) * (1,j)) & (f /. k) = (( GoB f) * (2,(j + 1)))) holds ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (2,(j + 2))))))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len f);

      

       A3: ((k + 1) + 1) = (k + (1 + 1));

      then (k + 1) < ( len f) by A2, NAT_1: 13;

      then

       A4: ( LSeg (f,k)) = ( LSeg ((f /. k),(f /. (k + 1)))) by A1, TOPREAL1:def 3;

      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;

      

       A6: 1 < ( len ( GoB f)) by GOBOARD7: 32;

      let j such that

       A7: 1 <= j and

       A8: (j + 2) <= ( width ( GoB f)) and

       A9: (f /. (k + 1)) = (( GoB f) * (1,(j + 1))) and

       A10: (f /. k) = (( GoB f) * (1,j)) & (f /. (k + 2)) = (( GoB f) * (2,(j + 1))) or (f /. (k + 2)) = (( GoB f) * (1,j)) & (f /. k) = (( GoB f) * (2,(j + 1)));

      

       A11: ((j + 1) + 1) = (j + (1 + 1));

      then

       A12: (j + 1) < ( width ( GoB f)) by A8, NAT_1: 13;

      ( len ( GoB f)) <> 0 by MATRIX_0:def 10;

      then

       A13: ( 0 + 1) <= ( len ( GoB f)) by NAT_1: 14;

      then

       A14: ( L~ f) misses ( Int ( cell (( GoB f),1,(j + 1)))) by A12, GOBOARD7: 12;

       0 < ( len ( GoB f)) by A13;

      then ( L~ f) misses ( Int ( cell (( GoB f), 0 ,(j + 1)))) by A12, GOBOARD7: 12;

      then

       A15: ( L~ f) misses (( Int ( cell (( GoB f), 0 ,(j + 1)))) \/ ( Int ( cell (( GoB f),1,(j + 1))))) by A14, XBOOLE_1: 70;

      

       A16: 1 <= (j + 1) by NAT_1: 11;

      assume ( LSeg ((((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|),((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (2,(j + 2))))))) meets ( L~ f);

      then ( L~ f) meets ((( Int ( cell (( GoB f), 0 ,(j + 1)))) \/ ( Int ( cell (( GoB f),1,(j + 1))))) \/ {((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2)))))}) by A11, A12, A6, A16, GOBOARD6: 68, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2)))))} by A15, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A17: ( LSeg ((f /. (k + 1)),(( GoB f) * (1,(j + 2))))) = ( LSeg (f,k0)) by A8, A9, A13, A11, A16, GOBOARD7: 39, ZFMISC_1: 50;

      

       A18: ( LSeg (f,(k + 1))) c= ( L~ f) & (1 + 1) = 2 by TOPREAL3: 19;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A7, A9, A10, A12, A6, A17, A4, A18, A5, GOBOARD7: 59;

    end;

    theorem :: GOBOARD8:19

    for k st 1 <= k & (k + 2) <= ( len f) holds for j st 1 <= j & (j + 2) <= ( width ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (( len ( GoB f)),(j + 1))) & ((f /. k) = (( GoB f) * (( len ( GoB f)),(j + 2))) & (f /. (k + 2)) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) or (f /. (k + 2)) = (( GoB f) * (( len ( GoB f)),(j + 2))) & (f /. k) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j such that

       A6: 1 <= j and

       A7: (j + 2) <= ( width ( GoB f)) and

       A8: (f /. (k + 1)) = (( GoB f) * (( len ( GoB f)),(j + 1))) and

       A9: (f /. k) = (( GoB f) * (( len ( GoB f)),(j + 2))) & (f /. (k + 2)) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) or (f /. (k + 2)) = (( GoB f) * (( len ( GoB f)),(j + 2))) & (f /. k) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1)));

      ((j + 1) + 1) = (j + (1 + 1));

      then

       A10: (j + 1) < ( width ( GoB f)) by A7, NAT_1: 13;

      then

       A11: j < ( width ( GoB f)) by NAT_1: 13;

      then

       A12: ( L~ f) misses ( Int ( cell (( GoB f),( len ( GoB f)),j))) by GOBOARD7: 12;

      assume

       A13: ( LSeg (((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|))) meets ( L~ f);

      

       A14: 1 < ( len ( GoB f)) by GOBOARD7: 32;

      then

       A15: ((( len ( GoB f)) -' 1) + 1) = ( len ( GoB f)) by XREAL_1: 235;

      then

       A16: (( len ( GoB f)) -' 1) < ( len ( GoB f)) by NAT_1: 13;

      then ( L~ f) misses ( Int ( cell (( GoB f),(( len ( GoB f)) -' 1),j))) by A11, GOBOARD7: 12;

      then

       A17: ( L~ f) misses (( Int ( cell (( GoB f),(( len ( GoB f)) -' 1),j))) \/ ( Int ( cell (( GoB f),( len ( GoB f)),j)))) by A12, XBOOLE_1: 70;

      

       A18: 1 <= (( len ( GoB f)) -' 1) by A14, A15, NAT_1: 13;

      then ((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) = ((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) + (( GoB f) * (( len ( GoB f)),j)))) by A6, A15, A10, GOBOARD7: 9;

      then ( L~ f) meets ((( Int ( cell (( GoB f),(( len ( GoB f)) -' 1),j))) \/ ( Int ( cell (( GoB f),( len ( GoB f)),j)))) \/ {((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1)))))}) by A6, A14, A11, A13, GOBOARD6: 69, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1)))))} by A17, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A19: ( LSeg ((f /. (k + 1)),(( GoB f) * (( len ( GoB f)),j)))) = ( LSeg (f,k0)) by A6, A8, A14, A10, GOBOARD7: 39, 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: 60;

    end;

    theorem :: GOBOARD8:20

    for k st 1 <= k & (k + 2) <= ( len f) holds for j st 1 <= j & (j + 2) <= ( width ( GoB f)) & (f /. (k + 1)) = (( GoB f) * (( len ( GoB f)),(j + 1))) & ((f /. k) = (( GoB f) * (( len ( GoB f)),j)) & (f /. (k + 2)) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) or (f /. (k + 2)) = (( GoB f) * (( len ( GoB f)),j)) & (f /. k) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1)))) holds ( LSeg (((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|))) misses ( L~ f)

    proof

      let k such that

       A1: k >= 1 and

       A2: (k + 2) <= ( len 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 j such that

       A6: 1 <= j and

       A7: (j + 2) <= ( width ( GoB f)) and

       A8: (f /. (k + 1)) = (( GoB f) * (( len ( GoB f)),(j + 1))) and

       A9: (f /. k) = (( GoB f) * (( len ( GoB f)),j)) & (f /. (k + 2)) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) or (f /. (k + 2)) = (( GoB f) * (( len ( GoB f)),j)) & (f /. k) = (( GoB f) * ((( len ( GoB f)) -' 1),(j + 1)));

      

       A10: ((j + 1) + 1) = (j + (1 + 1));

      then

       A11: (j + 1) < ( width ( GoB f)) by A7, NAT_1: 13;

      then

       A12: ( L~ f) misses ( Int ( cell (( GoB f),( len ( GoB f)),(j + 1)))) by GOBOARD7: 12;

      

       A13: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      then

       A14: ((( len ( GoB f)) -' 1) + 1) = ( len ( GoB f)) by XREAL_1: 235;

      then

       A15: (( len ( GoB f)) -' 1) < ( len ( GoB f)) by NAT_1: 13;

      then ( L~ f) misses ( Int ( cell (( GoB f),(( len ( GoB f)) -' 1),(j + 1)))) by A11, GOBOARD7: 12;

      then

       A16: ( L~ f) misses (( Int ( cell (( GoB f),(( len ( GoB f)) -' 1),(j + 1)))) \/ ( Int ( cell (( GoB f),( len ( GoB f)),(j + 1))))) by A12, XBOOLE_1: 70;

      assume

       A17: ( LSeg (((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|))) meets ( L~ f);

      

       A18: 1 <= (j + 1) by NAT_1: 11;

      

       A19: 1 < ( len ( GoB f)) by GOBOARD7: 32;

      then

       A20: 1 <= (( len ( GoB f)) -' 1) by A14, NAT_1: 13;

      then ((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) = ((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * ((( len ( GoB f)) -' 1),(j + 2))))) by A7, A14, A10, A18, GOBOARD7: 9;

      then ( L~ f) meets ((( Int ( cell (( GoB f),(( len ( GoB f)) -' 1),(j + 1)))) \/ ( Int ( cell (( GoB f),( len ( GoB f)),(j + 1))))) \/ {((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2)))))}) by A19, A10, A11, A18, A17, GOBOARD6: 69, XBOOLE_1: 63;

      then ( L~ f) meets {((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2)))))} by A16, XBOOLE_1: 70;

      then

      consider k0 be Nat such that 1 <= k0 and (k0 + 1) <= ( len f) and

       A21: ( LSeg ((f /. (k + 1)),(( GoB f) * (( len ( GoB f)),(j + 2))))) = ( LSeg (f,k0)) by A7, A8, A13, A10, A18, GOBOARD7: 39, ZFMISC_1: 50;

      ( LSeg (f,k0)) c= ( L~ f) & ( LSeg (f,k)) c= ( L~ f) by TOPREAL3: 19;

      hence contradiction by A6, A8, A9, A14, A20, A15, A11, A21, A4, A5, GOBOARD7: 60;

    end;

    reserve P for Subset of ( TOP-REAL 2);

    theorem :: GOBOARD8:21

    

     Th21: (for p st p in P holds (p `1 ) < ((( GoB f) * (1,1)) `1 )) implies P misses ( L~ f)

    proof

      assume

       A1: for p st p in P holds (p `1 ) < ((( GoB f) * (1,1)) `1 );

      assume P meets ( L~ f);

      then

      consider x be object such that

       A2: x in P and

       A3: x in ( L~ f) by XBOOLE_0: 3;

      reconsider x as Point of ( TOP-REAL 2) by A2;

      

       A4: (x `1 ) < ((( GoB f) * (1,1)) `1 ) by A1, A2;

      

       A5: 1 < ( width ( GoB f)) by GOBOARD7: 33;

      

       A6: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      consider i such that

       A7: 1 <= i and

       A8: (i + 1) <= ( len f) and

       A9: x in ( LSeg ((f /. i),(f /. (i + 1)))) by A3, SPPOL_2: 14;

      per cases ;

        suppose ((f /. i) `1 ) <= ((f /. (i + 1)) `1 );

        then

         A10: ((f /. i) `1 ) <= (x `1 ) by A9, TOPREAL1: 3;

        i <= ( len f) by A8, NAT_1: 13;

        then i in ( dom f) by A7, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A11: [i1, j1] in ( Indices ( GoB f)) and

         A12: (f /. i) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A13: 1 <= i1 by A11, MATRIX_0: 32;

        

         A14: i1 <= ( len ( GoB f)) by A11, MATRIX_0: 32;

        1 <= j1 & j1 <= ( width ( GoB f)) by A11, MATRIX_0: 32;

        then

         A15: ((f /. i) `1 ) = ((( GoB f) * (i1,1)) `1 ) by A12, A13, A14, GOBOARD5: 2;

        then 1 < i1 by A4, A10, A13, XXREAL_0: 1;

        then ((( GoB f) * (1,1)) `1 ) < ((f /. i) `1 ) by A5, A14, A15, GOBOARD5: 3;

        hence contradiction by A1, A2, A10, XXREAL_0: 2;

      end;

        suppose ((f /. i) `1 ) >= ((f /. (i + 1)) `1 );

        then

         A16: ((f /. (i + 1)) `1 ) <= (x `1 ) by A9, TOPREAL1: 3;

        1 <= (i + 1) by NAT_1: 11;

        then (i + 1) in ( dom f) by A8, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A17: [i1, j1] in ( Indices ( GoB f)) and

         A18: (f /. (i + 1)) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A19: 1 <= i1 by A17, MATRIX_0: 32;

        

         A20: i1 <= ( len ( GoB f)) by A17, MATRIX_0: 32;

        1 <= j1 & j1 <= ( width ( GoB f)) by A17, MATRIX_0: 32;

        then

         A21: ((f /. (i + 1)) `1 ) = ((( GoB f) * (i1,1)) `1 ) by A18, A19, A20, GOBOARD5: 2;

        then 1 < i1 by A4, A16, A19, XXREAL_0: 1;

        then ((( GoB f) * (1,1)) `1 ) < ((f /. (i + 1)) `1 ) by A5, A20, A21, GOBOARD5: 3;

        hence contradiction by A1, A2, A16, XXREAL_0: 2;

      end;

    end;

    theorem :: GOBOARD8:22

    

     Th22: (for p st p in P holds (p `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 )) implies P misses ( L~ f)

    proof

      assume

       A1: for p st p in P holds (p `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 );

      assume P meets ( L~ f);

      then

      consider x be object such that

       A2: x in P and

       A3: x in ( L~ f) by XBOOLE_0: 3;

      reconsider x as Point of ( TOP-REAL 2) by A2;

      

       A4: (x `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A1, A2;

      

       A5: 1 < ( width ( GoB f)) by GOBOARD7: 33;

      

       A6: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      consider i such that

       A7: 1 <= i and

       A8: (i + 1) <= ( len f) and

       A9: x in ( LSeg ((f /. i),(f /. (i + 1)))) by A3, SPPOL_2: 14;

      per cases ;

        suppose ((f /. i) `1 ) >= ((f /. (i + 1)) `1 );

        then

         A10: ((f /. i) `1 ) >= (x `1 ) by A9, TOPREAL1: 3;

        i <= ( len f) by A8, NAT_1: 13;

        then i in ( dom f) by A7, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A11: [i1, j1] in ( Indices ( GoB f)) and

         A12: (f /. i) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A13: 1 <= i1 by A11, MATRIX_0: 32;

        

         A14: i1 <= ( len ( GoB f)) by A11, MATRIX_0: 32;

        1 <= j1 & j1 <= ( width ( GoB f)) by A11, MATRIX_0: 32;

        then

         A15: ((f /. i) `1 ) = ((( GoB f) * (i1,1)) `1 ) by A12, A13, A14, GOBOARD5: 2;

        then i1 < ( len ( GoB f)) by A4, A10, A14, XXREAL_0: 1;

        then ((( GoB f) * (( len ( GoB f)),1)) `1 ) > ((f /. i) `1 ) by A5, A13, A15, GOBOARD5: 3;

        hence contradiction by A1, A2, A10, XXREAL_0: 2;

      end;

        suppose ((f /. i) `1 ) <= ((f /. (i + 1)) `1 );

        then

         A16: ((f /. (i + 1)) `1 ) >= (x `1 ) by A9, TOPREAL1: 3;

        1 <= (i + 1) by NAT_1: 11;

        then (i + 1) in ( dom f) by A8, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A17: [i1, j1] in ( Indices ( GoB f)) and

         A18: (f /. (i + 1)) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A19: 1 <= i1 by A17, MATRIX_0: 32;

        

         A20: i1 <= ( len ( GoB f)) by A17, MATRIX_0: 32;

        1 <= j1 & j1 <= ( width ( GoB f)) by A17, MATRIX_0: 32;

        then

         A21: ((f /. (i + 1)) `1 ) = ((( GoB f) * (i1,1)) `1 ) by A18, A19, A20, GOBOARD5: 2;

        then i1 < ( len ( GoB f)) by A4, A16, A20, XXREAL_0: 1;

        then ((( GoB f) * (( len ( GoB f)),1)) `1 ) > ((f /. (i + 1)) `1 ) by A5, A19, A21, GOBOARD5: 3;

        hence contradiction by A1, A2, A16, XXREAL_0: 2;

      end;

    end;

    theorem :: GOBOARD8:23

    

     Th23: (for p st p in P holds (p `2 ) < ((( GoB f) * (1,1)) `2 )) implies P misses ( L~ f)

    proof

      assume

       A1: for p st p in P holds (p `2 ) < ((( GoB f) * (1,1)) `2 );

      assume P meets ( L~ f);

      then

      consider x be object such that

       A2: x in P and

       A3: x in ( L~ f) by XBOOLE_0: 3;

      reconsider x as Point of ( TOP-REAL 2) by A2;

      

       A4: (x `2 ) < ((( GoB f) * (1,1)) `2 ) by A1, A2;

      

       A5: 1 < ( len ( GoB f)) by GOBOARD7: 32;

      

       A6: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      consider j such that

       A7: 1 <= j and

       A8: (j + 1) <= ( len f) and

       A9: x in ( LSeg ((f /. j),(f /. (j + 1)))) by A3, SPPOL_2: 14;

      per cases ;

        suppose ((f /. j) `2 ) <= ((f /. (j + 1)) `2 );

        then

         A10: ((f /. j) `2 ) <= (x `2 ) by A9, TOPREAL1: 4;

        j <= ( len f) by A8, NAT_1: 13;

        then j in ( dom f) by A7, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A11: [i1, j1] in ( Indices ( GoB f)) and

         A12: (f /. j) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A13: 1 <= j1 by A11, MATRIX_0: 32;

        

         A14: j1 <= ( width ( GoB f)) by A11, MATRIX_0: 32;

        1 <= i1 & i1 <= ( len ( GoB f)) by A11, MATRIX_0: 32;

        then

         A15: ((f /. j) `2 ) = ((( GoB f) * (1,j1)) `2 ) by A12, A13, A14, GOBOARD5: 1;

        then 1 < j1 by A4, A10, A13, XXREAL_0: 1;

        then ((( GoB f) * (1,1)) `2 ) < ((f /. j) `2 ) by A5, A14, A15, GOBOARD5: 4;

        hence contradiction by A1, A2, A10, XXREAL_0: 2;

      end;

        suppose ((f /. j) `2 ) >= ((f /. (j + 1)) `2 );

        then

         A16: ((f /. (j + 1)) `2 ) <= (x `2 ) by A9, TOPREAL1: 4;

        1 <= (j + 1) by NAT_1: 11;

        then (j + 1) in ( dom f) by A8, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A17: [i1, j1] in ( Indices ( GoB f)) and

         A18: (f /. (j + 1)) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A19: 1 <= j1 by A17, MATRIX_0: 32;

        

         A20: j1 <= ( width ( GoB f)) by A17, MATRIX_0: 32;

        1 <= i1 & i1 <= ( len ( GoB f)) by A17, MATRIX_0: 32;

        then

         A21: ((f /. (j + 1)) `2 ) = ((( GoB f) * (1,j1)) `2 ) by A18, A19, A20, GOBOARD5: 1;

        then 1 < j1 by A4, A16, A19, XXREAL_0: 1;

        then ((( GoB f) * (1,1)) `2 ) < ((f /. (j + 1)) `2 ) by A5, A20, A21, GOBOARD5: 4;

        hence contradiction by A1, A2, A16, XXREAL_0: 2;

      end;

    end;

    theorem :: GOBOARD8:24

    

     Th24: (for p st p in P holds (p `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 )) implies P misses ( L~ f)

    proof

      assume

       A1: for p st p in P holds (p `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 );

      assume P meets ( L~ f);

      then

      consider x be object such that

       A2: x in P and

       A3: x in ( L~ f) by XBOOLE_0: 3;

      reconsider x as Point of ( TOP-REAL 2) by A2;

      

       A4: (x `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A1, A2;

      

       A5: 1 < ( len ( GoB f)) by GOBOARD7: 32;

      

       A6: f is_sequence_on ( GoB f) by GOBOARD5:def 5;

      consider j such that

       A7: 1 <= j and

       A8: (j + 1) <= ( len f) and

       A9: x in ( LSeg ((f /. j),(f /. (j + 1)))) by A3, SPPOL_2: 14;

      per cases ;

        suppose ((f /. j) `2 ) >= ((f /. (j + 1)) `2 );

        then

         A10: ((f /. j) `2 ) >= (x `2 ) by A9, TOPREAL1: 4;

        j <= ( len f) by A8, NAT_1: 13;

        then j in ( dom f) by A7, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A11: [i1, j1] in ( Indices ( GoB f)) and

         A12: (f /. j) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A13: 1 <= j1 by A11, MATRIX_0: 32;

        

         A14: j1 <= ( width ( GoB f)) by A11, MATRIX_0: 32;

        1 <= i1 & i1 <= ( len ( GoB f)) by A11, MATRIX_0: 32;

        then

         A15: ((f /. j) `2 ) = ((( GoB f) * (1,j1)) `2 ) by A12, A13, A14, GOBOARD5: 1;

        then j1 < ( width ( GoB f)) by A4, A10, A14, XXREAL_0: 1;

        then ((( GoB f) * (1,( width ( GoB f)))) `2 ) > ((f /. j) `2 ) by A5, A13, A15, GOBOARD5: 4;

        hence contradiction by A1, A2, A10, XXREAL_0: 2;

      end;

        suppose ((f /. j) `2 ) <= ((f /. (j + 1)) `2 );

        then

         A16: ((f /. (j + 1)) `2 ) >= (x `2 ) by A9, TOPREAL1: 4;

        1 <= (j + 1) by NAT_1: 11;

        then (j + 1) in ( dom f) by A8, FINSEQ_3: 25;

        then

        consider i1, j1 such that

         A17: [i1, j1] in ( Indices ( GoB f)) and

         A18: (f /. (j + 1)) = (( GoB f) * (i1,j1)) by A6, GOBOARD1:def 9;

        

         A19: 1 <= j1 by A17, MATRIX_0: 32;

        

         A20: j1 <= ( width ( GoB f)) by A17, MATRIX_0: 32;

        1 <= i1 & i1 <= ( len ( GoB f)) by A17, MATRIX_0: 32;

        then

         A21: ((f /. (j + 1)) `2 ) = ((( GoB f) * (1,j1)) `2 ) by A18, A19, A20, GOBOARD5: 1;

        then j1 < ( width ( GoB f)) by A4, A16, A20, XXREAL_0: 1;

        then ((( GoB f) * (1,( width ( GoB f)))) `2 ) > ((f /. (j + 1)) `2 ) by A5, A19, A21, GOBOARD5: 4;

        hence contradiction by A1, A2, A16, XXREAL_0: 2;

      end;

    end;

    theorem :: GOBOARD8:25

    for i st 1 <= i & (i + 2) <= ( len ( GoB f)) holds ( LSeg ((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i + 1),1)) + (( GoB f) * ((i + 2),1)))) - |[ 0 , 1]|))) misses ( L~ f)

    proof

      let i such that

       A1: 1 <= i and

       A2: (i + 2) <= ( len ( GoB f));

      

       A3: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      now

        

         A4: i <= (i + 2) by NAT_1: 11;

        then i <= ( len ( GoB f)) by A2, XXREAL_0: 2;

        then

         A5: ((( GoB f) * (i,1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A1, A3, GOBOARD5: 1;

        (i + 1) <= (i + 2) by XREAL_1: 6;

        then 1 <= (i + 1) & (i + 1) <= ( len ( GoB f)) by A2, NAT_1: 11, XXREAL_0: 2;

        then

         A6: ((( GoB f) * ((i + 1),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A3, GOBOARD5: 1;

        1 <= (i + 2) by A1, A4, XXREAL_0: 2;

        then

         A7: ((( GoB f) * ((i + 2),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A2, A3, GOBOARD5: 1;

        ((((1 / 2) * ((( GoB f) * ((i + 1),1)) + (( GoB f) * ((i + 2),1)))) - |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * ((i + 1),1)) + (( GoB f) * ((i + 2),1)))) `2 ) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * ((i + 1),1)) + (( GoB f) * ((i + 2),1))) `2 )) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `2 ) + ((( GoB f) * (1,1)) `2 ))) - ( |[ 0 , 1]| `2 )) by A6, A7, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `2 )) - 1) by EUCLID: 52;

        then

         A8: (((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),1)))) - |[ 0 , 1]|) `1 ), (((( GoB f) * (1,1)) `2 ) - 1)]| by EUCLID: 53;

        ((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) `2 ) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1))) `2 )) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `2 ) + ((( GoB f) * (1,1)) `2 ))) - ( |[ 0 , 1]| `2 )) by A5, A6, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `2 )) - 1) by EUCLID: 52;

        then

         A9: (((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|) `1 ), (((( GoB f) * (1,1)) `2 ) - 1)]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * (i,1)) + (( GoB f) * ((i + 1),1)))) - |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i + 1),1)) + (( GoB f) * ((i + 2),1)))) - |[ 0 , 1]|)));

        then (p `2 ) = (((( GoB f) * (1,1)) `2 ) - 1) by A9, A8, TOPREAL3: 12;

        hence (p `2 ) < ((( GoB f) * (1,1)) `2 ) by XREAL_1: 44;

      end;

      hence thesis by Th23;

    end;

    theorem :: GOBOARD8:26

    ( LSeg (((( GoB f) * (1,1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,1)))) - |[ 0 , 1]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      now

        1 < ( len ( GoB f)) by GOBOARD7: 32;

        then (1 + 1) <= ( len ( GoB f)) by NAT_1: 13;

        then

         A2: ((( GoB f) * (2,1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A1, GOBOARD5: 1;

        ((((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,1)))) - |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,1)))) `2 ) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * (1,1)) + (( GoB f) * (2,1))) `2 )) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `2 ) + ((( GoB f) * (1,1)) `2 ))) - ( |[ 0 , 1]| `2 )) by A2, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `2 )) - 1) by EUCLID: 52;

        then

         A3: (((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,1)))) - |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,1)))) - |[ 0 , 1]|) `1 ), (((( GoB f) * (1,1)) `2 ) - 1)]| by EUCLID: 53;

        (((( GoB f) * (1,1)) - |[1, 1]|) `2 ) = (((( GoB f) * (1,1)) `2 ) - ( |[1, 1]| `2 )) by TOPREAL3: 3

        .= (((( GoB f) * (1,1)) `2 ) - 1) by EUCLID: 52;

        then

         A4: ((( GoB f) * (1,1)) - |[1, 1]|) = |[(((( GoB f) * (1,1)) - |[1, 1]|) `1 ), (((( GoB f) * (1,1)) `2 ) - 1)]| by EUCLID: 53;

        let p;

        assume p in ( LSeg (((( GoB f) * (1,1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (2,1)))) - |[ 0 , 1]|)));

        then (p `2 ) = (((( GoB f) * (1,1)) `2 ) - 1) by A4, A3, TOPREAL3: 12;

        hence (p `2 ) < ((( GoB f) * (1,1)) `2 ) by XREAL_1: 44;

      end;

      hence thesis by Th23;

    end;

    theorem :: GOBOARD8:27

    ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      now

        

         A2: 1 < ( len ( GoB f)) by GOBOARD7: 32;

        then

         A3: ((( len ( GoB f)) -' 1) + 1) = ( len ( GoB f)) by XREAL_1: 235;

        then

         A4: (( len ( GoB f)) -' 1) <= ( len ( GoB f)) by NAT_1: 11;

        

         A5: ((( GoB f) * (( len ( GoB f)),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A1, A2, GOBOARD5: 1;

        

        then (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|) `2 ) = (((( GoB f) * (1,1)) `2 ) + ( |[1, ( - 1)]| `2 )) by TOPREAL3: 2

        .= (((( GoB f) * (1,1)) `2 ) + ( - 1)) by EUCLID: 52

        .= (((( GoB f) * (1,1)) `2 ) - 1);

        then

         A6: ((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|) = |[(((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|) `1 ), (((( GoB f) * (1,1)) `2 ) - 1)]| by EUCLID: 53;

        1 <= (( len ( GoB f)) -' 1) by A2, A3, NAT_1: 13;

        then

         A7: ((( GoB f) * ((( len ( GoB f)) -' 1),1)) `2 ) = ((( GoB f) * (1,1)) `2 ) by A1, A4, GOBOARD5: 1;

        ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) `2 ) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1))) `2 )) - ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `2 ) + ((( GoB f) * (1,1)) `2 ))) - ( |[ 0 , 1]| `2 )) by A7, A5, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `2 )) - 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|) `1 ), (((( GoB f) * (1,1)) `2 ) - 1)]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),1)) + (( GoB f) * (( len ( GoB f)),1)))) - |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|)));

        then (p `2 ) = (((( GoB f) * (1,1)) `2 ) - 1) by A8, A6, TOPREAL3: 12;

        hence (p `2 ) < ((( GoB f) * (1,1)) `2 ) by XREAL_1: 44;

      end;

      hence thesis by Th23;

    end;

    theorem :: GOBOARD8:28

    for i st 1 <= i & (i + 2) <= ( len ( GoB f)) holds ( LSeg ((((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|))) misses ( L~ f)

    proof

      let i such that

       A1: 1 <= i and

       A2: (i + 2) <= ( len ( GoB f));

      

       A3: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      now

        

         A4: i <= (i + 2) by NAT_1: 11;

        then i <= ( len ( GoB f)) by A2, XXREAL_0: 2;

        then

         A5: ((( GoB f) * (i,( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A1, A3, GOBOARD5: 1;

        (i + 1) <= (i + 2) by XREAL_1: 6;

        then 1 <= (i + 1) & (i + 1) <= ( len ( GoB f)) by A2, NAT_1: 11, XXREAL_0: 2;

        then

         A6: ((( GoB f) * ((i + 1),( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A3, GOBOARD5: 1;

        1 <= (i + 2) by A1, A4, XXREAL_0: 2;

        then

         A7: ((( GoB f) * ((i + 2),( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A2, A3, GOBOARD5: 1;

        ((((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) `2 ) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f))))) `2 )) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,( width ( GoB f)))) `2 ) + ((( GoB f) * (1,( width ( GoB f)))) `2 ))) + ( |[ 0 , 1]| `2 )) by A6, A7, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,( width ( GoB f)))) `2 )) + 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|) `1 ), (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1)]| by EUCLID: 53;

        ((((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) + |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) `2 ) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f))))) `2 )) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,( width ( GoB f)))) `2 ) + ((( GoB f) * (1,( width ( GoB f)))) `2 ))) + ( |[ 0 , 1]| `2 )) by A5, A6, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,( width ( GoB f)))) `2 )) + 1) by EUCLID: 52;

        then

         A9: (((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) + |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) + |[ 0 , 1]|) `1 ), (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1)]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * (i,( width ( GoB f)))) + (( GoB f) * ((i + 1),( width ( GoB f)))))) + |[ 0 , 1]|),(((1 / 2) * ((( GoB f) * ((i + 1),( width ( GoB f)))) + (( GoB f) * ((i + 2),( width ( GoB f)))))) + |[ 0 , 1]|)));

        then (p `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by A9, A8, TOPREAL3: 12;

        hence (p `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 ) by XREAL_1: 29;

      end;

      hence thesis by Th24;

    end;

    theorem :: GOBOARD8:29

    ( LSeg (((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|),(((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f)))))) + |[ 0 , 1]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      now

        1 < ( len ( GoB f)) by GOBOARD7: 32;

        then (1 + 1) <= ( len ( GoB f)) by NAT_1: 13;

        then

         A2: ((( GoB f) * (2,( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A1, GOBOARD5: 1;

        ((((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f)))))) + |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f)))))) `2 ) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f))))) `2 )) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,( width ( GoB f)))) `2 ) + ((( GoB f) * (1,( width ( GoB f)))) `2 ))) + ( |[ 0 , 1]| `2 )) by A2, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,( width ( GoB f)))) `2 )) + 1) by EUCLID: 52;

        then

         A3: (((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f)))))) + |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f)))))) + |[ 0 , 1]|) `1 ), (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1)]| by EUCLID: 53;

        (((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|) `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + ( |[( - 1), 1]| `2 )) by TOPREAL3: 2

        .= (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by EUCLID: 52;

        then

         A4: ((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|) = |[(((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|) `1 ), (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1)]| by EUCLID: 53;

        let p;

        assume p in ( LSeg (((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|),(((1 / 2) * ((( GoB f) * (1,( width ( GoB f)))) + (( GoB f) * (2,( width ( GoB f)))))) + |[ 0 , 1]|)));

        then (p `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by A4, A3, TOPREAL3: 12;

        hence (p `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 ) by XREAL_1: 29;

      end;

      hence thesis by Th24;

    end;

    theorem :: GOBOARD8:30

    ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( width ( GoB f)) by GOBOARD7: 33;

      now

        

         A2: 1 < ( len ( GoB f)) by GOBOARD7: 32;

        then

         A3: ((( len ( GoB f)) -' 1) + 1) = ( len ( GoB f)) by XREAL_1: 235;

        then

         A4: (( len ( GoB f)) -' 1) <= ( len ( GoB f)) by NAT_1: 11;

        

         A5: ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A1, A2, GOBOARD5: 1;

        

        then (((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|) `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + ( |[1, 1]| `2 )) by TOPREAL3: 2

        .= (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by EUCLID: 52;

        then

         A6: ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|) = |[(((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|) `1 ), (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1)]| by EUCLID: 53;

        1 <= (( len ( GoB f)) -' 1) by A2, A3, NAT_1: 13;

        then

         A7: ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) `2 ) = ((( GoB f) * (1,( width ( GoB f)))) `2 ) by A1, A4, GOBOARD5: 1;

        ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[ 0 , 1]|) `2 ) = ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) `2 ) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f))))) `2 )) + ( |[ 0 , 1]| `2 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,( width ( GoB f)))) `2 ) + ((( GoB f) * (1,( width ( GoB f)))) `2 ))) + ( |[ 0 , 1]| `2 )) by A7, A5, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,( width ( GoB f)))) `2 )) + 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[ 0 , 1]|) = |[((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[ 0 , 1]|) `1 ), (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1)]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * ((( len ( GoB f)) -' 1),( width ( GoB f)))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[ 0 , 1]|),((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|)));

        then (p `2 ) = (((( GoB f) * (1,( width ( GoB f)))) `2 ) + 1) by A8, A6, TOPREAL3: 12;

        hence (p `2 ) > ((( GoB f) * (1,( width ( GoB f)))) `2 ) by XREAL_1: 29;

      end;

      hence thesis by Th24;

    end;

    theorem :: GOBOARD8:31

    for j st 1 <= j & (j + 2) <= ( width ( GoB f)) holds ( LSeg ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|))) misses ( L~ f)

    proof

      let j such that

       A1: 1 <= j and

       A2: (j + 2) <= ( width ( GoB f));

      

       A3: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      now

        

         A4: j <= (j + 2) by NAT_1: 11;

        then j <= ( width ( GoB f)) by A2, XXREAL_0: 2;

        then

         A5: ((( GoB f) * (1,j)) `1 ) = ((( GoB f) * (1,1)) `1 ) by A1, A3, GOBOARD5: 2;

        (j + 1) <= (j + 2) by XREAL_1: 6;

        then 1 <= (j + 1) & (j + 1) <= ( width ( GoB f)) by A2, NAT_1: 11, XXREAL_0: 2;

        then

         A6: ((( GoB f) * (1,(j + 1))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A3, GOBOARD5: 2;

        1 <= (j + 2) by A1, A4, XXREAL_0: 2;

        then

         A7: ((( GoB f) * (1,(j + 2))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A2, A3, GOBOARD5: 2;

        ((((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) `1 ) - ( |[1, 0 ]| `1 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2)))) `1 )) - ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `1 ) + ((( GoB f) * (1,1)) `1 ))) - ( |[1, 0 ]| `1 )) by A6, A7, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `1 )) - 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|) = |[(((( GoB f) * (1,1)) `1 ) - 1), ((((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|) `2 )]| by EUCLID: 53;

        ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) `1 ) - ( |[1, 0 ]| `1 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1)))) `1 )) - ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `1 ) + ((( GoB f) * (1,1)) `1 ))) - ( |[1, 0 ]| `1 )) by A5, A6, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `1 )) - 1) by EUCLID: 52;

        then

         A9: (((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|) = |[(((( GoB f) * (1,1)) `1 ) - 1), ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|) `2 )]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * (1,j)) + (( GoB f) * (1,(j + 1))))) - |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (1,(j + 1))) + (( GoB f) * (1,(j + 2))))) - |[1, 0 ]|)));

        then (p `1 ) = (((( GoB f) * (1,1)) `1 ) - 1) by A9, A8, TOPREAL3: 11;

        hence (p `1 ) < ((( GoB f) * (1,1)) `1 ) by XREAL_1: 44;

      end;

      hence thesis by Th21;

    end;

    theorem :: GOBOARD8:32

    ( LSeg (((( GoB f) * (1,1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (1,2)))) - |[1, 0 ]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      now

        1 < ( width ( GoB f)) by GOBOARD7: 33;

        then (1 + 1) <= ( width ( GoB f)) by NAT_1: 13;

        then

         A2: ((( GoB f) * (1,2)) `1 ) = ((( GoB f) * (1,1)) `1 ) by A1, GOBOARD5: 2;

        ((((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (1,2)))) - |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (1,2)))) `1 ) - ( |[1, 0 ]| `1 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * (1,1)) + (( GoB f) * (1,2))) `1 )) - ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `1 ) + ((( GoB f) * (1,1)) `1 ))) - ( |[1, 0 ]| `1 )) by A2, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `1 )) - 1) by EUCLID: 52;

        then

         A3: (((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (1,2)))) - |[1, 0 ]|) = |[(((( GoB f) * (1,1)) `1 ) - 1), ((((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (1,2)))) - |[1, 0 ]|) `2 )]| by EUCLID: 53;

        (((( GoB f) * (1,1)) - |[1, 1]|) `1 ) = (((( GoB f) * (1,1)) `1 ) - ( |[1, 1]| `1 )) by TOPREAL3: 3

        .= (((( GoB f) * (1,1)) `1 ) - 1) by EUCLID: 52;

        then

         A4: ((( GoB f) * (1,1)) - |[1, 1]|) = |[(((( GoB f) * (1,1)) `1 ) - 1), (((( GoB f) * (1,1)) - |[1, 1]|) `2 )]| by EUCLID: 53;

        let p;

        assume p in ( LSeg (((( GoB f) * (1,1)) - |[1, 1]|),(((1 / 2) * ((( GoB f) * (1,1)) + (( GoB f) * (1,2)))) - |[1, 0 ]|)));

        then (p `1 ) = (((( GoB f) * (1,1)) `1 ) - 1) by A4, A3, TOPREAL3: 11;

        hence (p `1 ) < ((( GoB f) * (1,1)) `1 ) by XREAL_1: 44;

      end;

      hence thesis by Th21;

    end;

    theorem :: GOBOARD8:33

    ( LSeg ((((1 / 2) * ((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f)))))) - |[1, 0 ]|),((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      now

        

         A2: 1 < ( width ( GoB f)) by GOBOARD7: 33;

        then

         A3: ((( width ( GoB f)) -' 1) + 1) = ( width ( GoB f)) by XREAL_1: 235;

        then

         A4: (( width ( GoB f)) -' 1) <= ( width ( GoB f)) by NAT_1: 11;

        

         A5: ((( GoB f) * (1,( width ( GoB f)))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A1, A2, GOBOARD5: 2;

        

        then (((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|) `1 ) = (((( GoB f) * (1,1)) `1 ) + ( |[( - 1), 1]| `1 )) by TOPREAL3: 2

        .= (((( GoB f) * (1,1)) `1 ) + ( - 1)) by EUCLID: 52

        .= (((( GoB f) * (1,1)) `1 ) - 1);

        then

         A6: ((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|) = |[(((( GoB f) * (1,1)) `1 ) - 1), (((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|) `2 )]| by EUCLID: 53;

        1 <= (( width ( GoB f)) -' 1) by A2, A3, NAT_1: 13;

        then

         A7: ((( GoB f) * (1,(( width ( GoB f)) -' 1))) `1 ) = ((( GoB f) * (1,1)) `1 ) by A1, A4, GOBOARD5: 2;

        ((((1 / 2) * ((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f)))))) - |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f)))))) `1 ) - ( |[1, 0 ]| `1 )) by TOPREAL3: 3

        .= (((1 / 2) * (((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f))))) `1 )) - ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (1,1)) `1 ) + ((( GoB f) * (1,1)) `1 ))) - ( |[1, 0 ]| `1 )) by A7, A5, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (1,1)) `1 )) - 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f)))))) - |[1, 0 ]|) = |[(((( GoB f) * (1,1)) `1 ) - 1), ((((1 / 2) * ((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f)))))) - |[1, 0 ]|) `2 )]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * (1,(( width ( GoB f)) -' 1))) + (( GoB f) * (1,( width ( GoB f)))))) - |[1, 0 ]|),((( GoB f) * (1,( width ( GoB f)))) + |[( - 1), 1]|)));

        then (p `1 ) = (((( GoB f) * (1,1)) `1 ) - 1) by A8, A6, TOPREAL3: 11;

        hence (p `1 ) < ((( GoB f) * (1,1)) `1 ) by XREAL_1: 44;

      end;

      hence thesis by Th21;

    end;

    theorem :: GOBOARD8:34

    for j st 1 <= j & (j + 2) <= ( width ( GoB f)) holds ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|))) misses ( L~ f)

    proof

      let j such that

       A1: 1 <= j and

       A2: (j + 2) <= ( width ( GoB f));

      

       A3: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      now

        

         A4: j <= (j + 2) by NAT_1: 11;

        then j <= ( width ( GoB f)) by A2, XXREAL_0: 2;

        then

         A5: ((( GoB f) * (( len ( GoB f)),j)) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A1, A3, GOBOARD5: 2;

        (j + 1) <= (j + 2) by XREAL_1: 6;

        then 1 <= (j + 1) & (j + 1) <= ( width ( GoB f)) by A2, NAT_1: 11, XXREAL_0: 2;

        then

         A6: ((( GoB f) * (( len ( GoB f)),(j + 1))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A3, GOBOARD5: 2;

        1 <= (j + 2) by A1, A4, XXREAL_0: 2;

        then

         A7: ((( GoB f) * (( len ( GoB f)),(j + 2))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A2, A3, GOBOARD5: 2;

        ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) `1 ) + ( |[1, 0 ]| `1 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2)))) `1 )) + ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),1)) `1 ) + ((( GoB f) * (( len ( GoB f)),1)) `1 ))) + ( |[1, 0 ]| `1 )) by A6, A7, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (( len ( GoB f)),1)) `1 )) + 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|) = |[(((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1), ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|) `2 )]| by EUCLID: 53;

        ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) `1 ) + ( |[1, 0 ]| `1 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1)))) `1 )) + ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),1)) `1 ) + ((( GoB f) * (( len ( GoB f)),1)) `1 ))) + ( |[1, 0 ]| `1 )) by A5, A6, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (( len ( GoB f)),1)) `1 )) + 1) by EUCLID: 52;

        then

         A9: (((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|) = |[(((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1), ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|) `2 )]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),j)) + (( GoB f) * (( len ( GoB f)),(j + 1))))) + |[1, 0 ]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),(j + 1))) + (( GoB f) * (( len ( GoB f)),(j + 2))))) + |[1, 0 ]|)));

        then (p `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by A9, A8, TOPREAL3: 11;

        hence (p `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 ) by XREAL_1: 29;

      end;

      hence thesis by Th22;

    end;

    theorem :: GOBOARD8:35

    ( LSeg (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      now

        1 < ( width ( GoB f)) by GOBOARD7: 33;

        then (1 + 1) <= ( width ( GoB f)) by NAT_1: 13;

        then

         A2: ((( GoB f) * (( len ( GoB f)),2)) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A1, GOBOARD5: 2;

        ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) `1 ) + ( |[1, 0 ]| `1 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2))) `1 )) + ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),1)) `1 ) + ((( GoB f) * (( len ( GoB f)),1)) `1 ))) + ( |[1, 0 ]| `1 )) by A2, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (( len ( GoB f)),1)) `1 )) + 1) by EUCLID: 52;

        then

         A3: (((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|) = |[(((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1), ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|) `2 )]| by EUCLID: 53;

        (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|) `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + ( |[1, ( - 1)]| `1 )) by TOPREAL3: 2

        .= (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by EUCLID: 52;

        then

         A4: ((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|) = |[(((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1), (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|) `2 )]| by EUCLID: 53;

        let p;

        assume p in ( LSeg (((( GoB f) * (( len ( GoB f)),1)) + |[1, ( - 1)]|),(((1 / 2) * ((( GoB f) * (( len ( GoB f)),1)) + (( GoB f) * (( len ( GoB f)),2)))) + |[1, 0 ]|)));

        then (p `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by A4, A3, TOPREAL3: 11;

        hence (p `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 ) by XREAL_1: 29;

      end;

      hence thesis by Th22;

    end;

    theorem :: GOBOARD8:36

    ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[1, 0 ]|),((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|))) misses ( L~ f)

    proof

      

       A1: 1 <= ( len ( GoB f)) by GOBOARD7: 32;

      now

        

         A2: 1 < ( width ( GoB f)) by GOBOARD7: 33;

        then

         A3: ((( width ( GoB f)) -' 1) + 1) = ( width ( GoB f)) by XREAL_1: 235;

        then

         A4: (( width ( GoB f)) -' 1) <= ( width ( GoB f)) by NAT_1: 11;

        

         A5: ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A1, A2, GOBOARD5: 2;

        

        then (((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|) `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + ( |[1, 1]| `1 )) by TOPREAL3: 2

        .= (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by EUCLID: 52;

        then

         A6: ((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|) = |[(((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1), (((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|) `2 )]| by EUCLID: 53;

        1 <= (( width ( GoB f)) -' 1) by A2, A3, NAT_1: 13;

        then

         A7: ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) `1 ) = ((( GoB f) * (( len ( GoB f)),1)) `1 ) by A1, A4, GOBOARD5: 2;

        ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[1, 0 ]|) `1 ) = ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) `1 ) + ( |[1, 0 ]| `1 )) by TOPREAL3: 2

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f))))) `1 )) + ( |[1, 0 ]| `1 )) by TOPREAL3: 4

        .= (((1 / 2) * (((( GoB f) * (( len ( GoB f)),1)) `1 ) + ((( GoB f) * (( len ( GoB f)),1)) `1 ))) + ( |[1, 0 ]| `1 )) by A7, A5, TOPREAL3: 2

        .= ((1 * ((( GoB f) * (( len ( GoB f)),1)) `1 )) + 1) by EUCLID: 52;

        then

         A8: (((1 / 2) * ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[1, 0 ]|) = |[(((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1), ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[1, 0 ]|) `2 )]| by EUCLID: 53;

        let p;

        assume p in ( LSeg ((((1 / 2) * ((( GoB f) * (( len ( GoB f)),(( width ( GoB f)) -' 1))) + (( GoB f) * (( len ( GoB f)),( width ( GoB f)))))) + |[1, 0 ]|),((( GoB f) * (( len ( GoB f)),( width ( GoB f)))) + |[1, 1]|)));

        then (p `1 ) = (((( GoB f) * (( len ( GoB f)),1)) `1 ) + 1) by A8, A6, TOPREAL3: 11;

        hence (p `1 ) > ((( GoB f) * (( len ( GoB f)),1)) `1 ) by XREAL_1: 29;

      end;

      hence thesis by Th22;

    end;

    theorem :: GOBOARD8:37

    1 <= k & (k + 1) <= ( len f) implies ( Int ( left_cell (f,k))) misses ( L~ f)

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f);

      k <= (k + 1) by NAT_1: 11;

      then k <= ( len f) by A2, XXREAL_0: 2;

      then

       A3: k in ( dom f) by A1, FINSEQ_3: 25;

      then

      consider i1,j1 be Nat such that

       A4: [i1, j1] in ( Indices ( GoB f)) and

       A5: (f /. k) = (( GoB f) * (i1,j1)) by GOBOARD2: 14;

      

       A6: i1 <= ( len ( GoB f)) by A4, MATRIX_0: 32;

      j1 <> 0 by A4, MATRIX_0: 32;

      then

      consider j be Nat such that

       A7: j1 = (j + 1) by NAT_1: 6;

      i1 <> 0 by A4, MATRIX_0: 32;

      then

      consider i be Nat such that

       A8: i1 = (i + 1) by NAT_1: 6;

      i <= i1 by A8, NAT_1: 11;

      then

       A9: i <= ( len ( GoB f)) by A6, XXREAL_0: 2;

      

       A10: j1 <= ( width ( GoB f)) by A4, MATRIX_0: 32;

      (k + 1) >= 1 by NAT_1: 11;

      then

       A11: (k + 1) in ( dom f) by A2, FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A12: [i2, j2] in ( Indices ( GoB f)) and

       A13: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by GOBOARD2: 14;

      reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;

      ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A4, A5, A11, A12, A13, GOBOARD5: 12;

      then

       A14: |.(i19 - i29).| = 1 & j1 = j2 or |.(j19 - j29).| = 1 & i1 = i2 by SEQM_3: 42;

      reconsider i, j as Nat;

      

       A15: i1 = (i + 1) by A8;

      

       A16: j1 = (j + 1) by A7;

      

       A17: j2 <= ( width ( GoB f)) by A12, MATRIX_0: 32;

      

       A18: i2 <= ( len ( GoB f)) by A12, MATRIX_0: 32;

      j <= j1 by A7, NAT_1: 11;

      then

       A19: j <= ( width ( GoB f)) by A10, XXREAL_0: 2;

      per cases by A14, SEQM_3: 41;

        suppose i1 = i2 & (j1 + 1) = j2;

        then ( left_cell (f,k)) = ( cell (( GoB f),i,j1)) by A1, A2, A4, A5, A8, A12, A13, GOBOARD5: 27;

        hence thesis by A10, A9, GOBOARD7: 12;

      end;

        suppose (i1 + 1) = i2 & j1 = j2;

        then ( left_cell (f,k)) = ( cell (( GoB f),i1,j1)) by A1, A2, A4, A5, A16, A12, A13, GOBOARD5: 28;

        hence thesis by A6, A10, GOBOARD7: 12;

      end;

        suppose i1 = (i2 + 1) & j1 = j2;

        then ( left_cell (f,k)) = ( cell (( GoB f),i2,j)) by A1, A2, A4, A5, A7, A12, A13, GOBOARD5: 29;

        hence thesis by A19, A18, GOBOARD7: 12;

      end;

        suppose i1 = i2 & j1 = (j2 + 1);

        then ( left_cell (f,k)) = ( cell (( GoB f),i1,j2)) by A1, A2, A4, A5, A15, A12, A13, GOBOARD5: 30;

        hence thesis by A6, A17, GOBOARD7: 12;

      end;

    end;

    theorem :: GOBOARD8:38

    1 <= k & (k + 1) <= ( len f) implies ( Int ( right_cell (f,k))) misses ( L~ f)

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f);

      k <= (k + 1) by NAT_1: 11;

      then k <= ( len f) by A2, XXREAL_0: 2;

      then

       A3: k in ( dom f) by A1, FINSEQ_3: 25;

      then

      consider i1,j1 be Nat such that

       A4: [i1, j1] in ( Indices ( GoB f)) and

       A5: (f /. k) = (( GoB f) * (i1,j1)) by GOBOARD2: 14;

      

       A6: i1 <= ( len ( GoB f)) by A4, MATRIX_0: 32;

      j1 <> 0 by A4, MATRIX_0: 32;

      then

      consider j be Nat such that

       A7: j1 = (j + 1) by NAT_1: 6;

      i1 <> 0 by A4, MATRIX_0: 32;

      then

      consider i be Nat such that

       A8: i1 = (i + 1) by NAT_1: 6;

      i <= i1 by A8, NAT_1: 11;

      then

       A9: i <= ( len ( GoB f)) by A6, XXREAL_0: 2;

      

       A10: j1 <= ( width ( GoB f)) by A4, MATRIX_0: 32;

      (k + 1) >= 1 by NAT_1: 11;

      then

       A11: (k + 1) in ( dom f) by A2, FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A12: [i2, j2] in ( Indices ( GoB f)) and

       A13: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by GOBOARD2: 14;

      reconsider i19 = i1, i29 = i2, j19 = j1, j29 = j2 as Element of REAL by XREAL_0:def 1;

      ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A4, A5, A11, A12, A13, GOBOARD5: 12;

      then

       A14: |.(i19 - i29).| = 1 & j1 = j2 or |.(j19 - j29).| = 1 & i1 = i2 by SEQM_3: 42;

      reconsider i, j as Nat;

      

       A15: i1 = (i + 1) by A8;

      

       A16: j1 = (j + 1) by A7;

      

       A17: j2 <= ( width ( GoB f)) by A12, MATRIX_0: 32;

      

       A18: i2 <= ( len ( GoB f)) by A12, MATRIX_0: 32;

      j <= j1 by A7, NAT_1: 11;

      then

       A19: j <= ( width ( GoB f)) by A10, XXREAL_0: 2;

      per cases by A14, SEQM_3: 41;

        suppose i1 = i2 & (j1 + 1) = j2;

        then ( right_cell (f,k)) = ( cell (( GoB f),i1,j1)) by A1, A2, A4, A5, A15, A12, A13, GOBOARD5: 27;

        hence thesis by A6, A10, GOBOARD7: 12;

      end;

        suppose (i1 + 1) = i2 & j1 = j2;

        then ( right_cell (f,k)) = ( cell (( GoB f),i1,j)) by A1, A2, A4, A5, A7, A12, A13, GOBOARD5: 28;

        hence thesis by A6, A19, GOBOARD7: 12;

      end;

        suppose i1 = (i2 + 1) & j1 = j2;

        then ( right_cell (f,k)) = ( cell (( GoB f),i2,j1)) by A1, A2, A4, A5, A16, A12, A13, GOBOARD5: 29;

        hence thesis by A10, A18, GOBOARD7: 12;

      end;

        suppose i1 = i2 & j1 = (j2 + 1);

        then ( right_cell (f,k)) = ( cell (( GoB f),i,j2)) by A1, A2, A4, A5, A8, A12, A13, GOBOARD5: 30;

        hence thesis by A9, A17, GOBOARD7: 12;

      end;

    end;