goboard5.miz



    begin

    reserve p,q for Point of ( TOP-REAL 2),

i,i1,i2,j,j1,j2,k for Nat,

r,s for Real,

G for Matrix of ( TOP-REAL 2);

    definition

      let G be Matrix of ( TOP-REAL 2);

      let i be Nat;

      :: GOBOARD5:def1

      func v_strip (G,i) -> Subset of ( TOP-REAL 2) equals

      : Def1: { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) } if 1 <= i & i < ( len G),

{ |[r, s]| : ((G * (i,1)) `1 ) <= r } if i >= ( len G)

      otherwise { |[r, s]| : r <= ((G * ((i + 1),1)) `1 ) };

      coherence

      proof

        hereby

          assume that 1 <= i and i < ( len G);

          set A = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) };

          A c= the carrier of ( TOP-REAL 2)

          proof

            let x be object;

            assume x in A;

            then ex r, s st x = |[r, s]| & ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 );

            hence thesis;

          end;

          hence A is Subset of ( TOP-REAL 2);

        end;

        hereby

          assume i >= ( len G);

          set A = { |[r, s]| : ((G * (i,1)) `1 ) <= r };

          A c= the carrier of ( TOP-REAL 2)

          proof

            let x be object;

            assume x in A;

            then ex r, s st x = |[r, s]| & ((G * (i,1)) `1 ) <= r;

            hence thesis;

          end;

          hence A is Subset of ( TOP-REAL 2);

        end;

        assume that not (1 <= i & i < ( len G)) and i < ( len G);

        set A = { |[r, s]| : r <= ((G * ((i + 1),1)) `1 ) };

        A c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in A;

          then ex r, s st x = |[r, s]| & r <= ((G * ((i + 1),1)) `1 );

          hence thesis;

        end;

        hence thesis;

      end;

      correctness ;

      :: GOBOARD5:def2

      func h_strip (G,i) -> Subset of ( TOP-REAL 2) equals

      : Def2: { |[r, s]| : ((G * (1,i)) `2 ) <= s & s <= ((G * (1,(i + 1))) `2 ) } if 1 <= i & i < ( width G),

{ |[r, s]| : ((G * (1,i)) `2 ) <= s } if i >= ( width G)

      otherwise { |[r, s]| : s <= ((G * (1,(i + 1))) `2 ) };

      coherence

      proof

        hereby

          assume that 1 <= i and i < ( width G);

          set A = { |[r, s]| : ((G * (1,i)) `2 ) <= s & s <= ((G * (1,(i + 1))) `2 ) };

          A c= the carrier of ( TOP-REAL 2)

          proof

            let x be object;

            assume x in A;

            then ex r, s st x = |[r, s]| & ((G * (1,i)) `2 ) <= s & s <= ((G * (1,(i + 1))) `2 );

            hence thesis;

          end;

          hence A is Subset of ( TOP-REAL 2);

        end;

        hereby

          assume i >= ( width G);

          set A = { |[r, s]| : ((G * (1,i)) `2 ) <= s };

          A c= the carrier of ( TOP-REAL 2)

          proof

            let x be object;

            assume x in A;

            then ex r, s st x = |[r, s]| & ((G * (1,i)) `2 ) <= s;

            hence thesis;

          end;

          hence A is Subset of ( TOP-REAL 2);

        end;

        assume that not (1 <= i & i < ( width G)) and i < ( width G);

        set A = { |[r, s]| : s <= ((G * (1,(i + 1))) `2 ) };

        A c= the carrier of ( TOP-REAL 2)

        proof

          let x be object;

          assume x in A;

          then ex r, s st x = |[r, s]| & s <= ((G * (1,(i + 1))) `2 );

          hence thesis;

        end;

        hence thesis;

      end;

      correctness ;

    end

    theorem :: GOBOARD5:1

    

     Th1: G is Y_equal-in-column & 1 <= j & j <= ( width G) & 1 <= i & i <= ( len G) implies ((G * (i,j)) `2 ) = ((G * (1,j)) `2 )

    proof

      assume that

       A1: G is Y_equal-in-column and

       A2: 1 <= j and

       A3: j <= ( width G) and

       A4: 1 <= i and

       A5: i <= ( len G);

      j in ( Seg ( width G)) by A2, A3, FINSEQ_1: 1;

      then

       A6: ( Y_axis ( Col (G,j))) is constant by A1;

      reconsider c = ( Col (G,j)) as FinSequence of ( TOP-REAL 2);

      

       A7: i in ( dom G) by A4, A5, FINSEQ_3: 25;

      

       A8: 1 <= ( len G) by A4, A5, XXREAL_0: 2;

      then

       A9: 1 in ( dom G) by FINSEQ_3: 25;

      

       A10: ( len c) = ( len G) by MATRIX_0:def 8;

      then 1 in ( dom c) by A8, FINSEQ_3: 25;

      then

       A11: (c /. 1) = (c . 1) by PARTFUN1:def 6;

      i in ( dom c) by A4, A5, A10, FINSEQ_3: 25;

      then

       A12: (c /. i) = (c . i) by PARTFUN1:def 6;

      

       A13: ( len ( Y_axis ( Col (G,j)))) = ( len c) by GOBOARD1:def 2;

      then

       A14: 1 in ( dom ( Y_axis ( Col (G,j)))) by A8, A10, FINSEQ_3: 25;

      

       A15: i in ( dom ( Y_axis ( Col (G,j)))) by A4, A5, A10, A13, FINSEQ_3: 25;

      

      thus ((G * (i,j)) `2 ) = ((c /. i) `2 ) by A7, A12, MATRIX_0:def 8

      .= (( Y_axis ( Col (G,j))) . i) by A15, GOBOARD1:def 2

      .= (( Y_axis ( Col (G,j))) . 1) by A6, A14, A15

      .= ((c /. 1) `2 ) by A14, GOBOARD1:def 2

      .= ((G * (1,j)) `2 ) by A9, A11, MATRIX_0:def 8;

    end;

    theorem :: GOBOARD5:2

    

     Th2: G is X_equal-in-line & 1 <= j & j <= ( width G) & 1 <= i & i <= ( len G) implies ((G * (i,j)) `1 ) = ((G * (i,1)) `1 )

    proof

      assume that

       A1: G is X_equal-in-line and

       A2: 1 <= j and

       A3: j <= ( width G) and

       A4: 1 <= i and

       A5: i <= ( len G);

      i in ( dom G) by A4, A5, FINSEQ_3: 25;

      then

       A6: ( X_axis ( Line (G,i))) is constant by A1;

      reconsider c = ( Line (G,i)) as FinSequence of ( TOP-REAL 2);

      

       A7: j in ( Seg ( width G)) by A2, A3, FINSEQ_1: 1;

      

       A8: 1 <= ( width G) by A2, A3, XXREAL_0: 2;

      then

       A9: 1 in ( Seg ( width G)) by FINSEQ_1: 1;

      

       A10: ( len c) = ( width G) by MATRIX_0:def 7;

      then 1 in ( dom c) by A8, FINSEQ_3: 25;

      then

       A11: (c /. 1) = (c . 1) by PARTFUN1:def 6;

      j in ( dom c) by A2, A3, A10, FINSEQ_3: 25;

      then

       A12: (c /. j) = (c . j) by PARTFUN1:def 6;

      

       A13: ( len ( X_axis ( Line (G,i)))) = ( len c) by GOBOARD1:def 1;

      then

       A14: 1 in ( dom ( X_axis ( Line (G,i)))) by A8, A10, FINSEQ_3: 25;

      

       A15: j in ( dom ( X_axis ( Line (G,i)))) by A2, A3, A10, A13, FINSEQ_3: 25;

      

      thus ((G * (i,j)) `1 ) = ((c /. j) `1 ) by A7, A12, MATRIX_0:def 7

      .= (( X_axis ( Line (G,i))) . j) by A15, GOBOARD1:def 1

      .= (( X_axis ( Line (G,i))) . 1) by A6, A14, A15

      .= ((c /. 1) `1 ) by A14, GOBOARD1:def 1

      .= ((G * (i,1)) `1 ) by A9, A11, MATRIX_0:def 7;

    end;

    theorem :: GOBOARD5:3

    

     Th3: G is X_increasing-in-column & 1 <= j & j <= ( width G) & 1 <= i1 & i1 < i2 & i2 <= ( len G) implies ((G * (i1,j)) `1 ) < ((G * (i2,j)) `1 )

    proof

      assume that

       A1: G is X_increasing-in-column and

       A2: 1 <= j and

       A3: j <= ( width G) and

       A4: 1 <= i1 and

       A5: i1 < i2 and

       A6: i2 <= ( len G);

      j in ( Seg ( width G)) by A2, A3, FINSEQ_1: 1;

      then

       A7: ( X_axis ( Col (G,j))) is increasing by A1;

      reconsider c = ( Col (G,j)) as FinSequence of ( TOP-REAL 2);

      

       A8: i1 <= ( len G) by A5, A6, XXREAL_0: 2;

      then

       A9: i1 in ( dom G) by A4, FINSEQ_3: 25;

      

       A10: 1 <= i2 by A4, A5, XXREAL_0: 2;

      then

       A11: i2 in ( dom G) by A6, FINSEQ_3: 25;

      

       A12: ( len c) = ( len G) by MATRIX_0:def 8;

      then i1 in ( dom c) by A4, A8, FINSEQ_3: 25;

      then

       A13: (c /. i1) = (c . i1) by PARTFUN1:def 6;

      i2 in ( dom c) by A6, A10, A12, FINSEQ_3: 25;

      then

       A14: (c /. i2) = (c . i2) by PARTFUN1:def 6;

      

       A15: ( len ( X_axis ( Col (G,j)))) = ( len c) by GOBOARD1:def 1;

      then

       A16: i1 in ( dom ( X_axis ( Col (G,j)))) by A4, A8, A12, FINSEQ_3: 25;

      

       A17: ((G * (i1,j)) `1 ) = ((c /. i1) `1 ) by A9, A13, MATRIX_0:def 8

      .= (( X_axis ( Col (G,j))) . i1) by A16, GOBOARD1:def 1;

      

       A18: i2 in ( dom ( X_axis ( Col (G,j)))) by A6, A10, A12, A15, FINSEQ_3: 25;

      

      then (( X_axis ( Col (G,j))) . i2) = ((c /. i2) `1 ) by GOBOARD1:def 1

      .= ((G * (i2,j)) `1 ) by A11, A14, MATRIX_0:def 8;

      hence thesis by A5, A7, A16, A17, A18;

    end;

    theorem :: GOBOARD5:4

    

     Th4: G is Y_increasing-in-line & 1 <= j1 & j1 < j2 & j2 <= ( width G) & 1 <= i & i <= ( len G) implies ((G * (i,j1)) `2 ) < ((G * (i,j2)) `2 )

    proof

      assume that

       A1: G is Y_increasing-in-line and

       A2: 1 <= j1 and

       A3: j1 < j2 and

       A4: j2 <= ( width G) and

       A5: 1 <= i and

       A6: i <= ( len G);

      i in ( dom G) by A5, A6, FINSEQ_3: 25;

      then

       A7: ( Y_axis ( Line (G,i))) is increasing by A1;

      reconsider c = ( Line (G,i)) as FinSequence of ( TOP-REAL 2);

      

       A8: j1 <= ( width G) by A3, A4, XXREAL_0: 2;

      then

       A9: j1 in ( Seg ( width G)) by A2, FINSEQ_1: 1;

      

       A10: 1 <= j2 by A2, A3, XXREAL_0: 2;

      then

       A11: j2 in ( Seg ( width G)) by A4, FINSEQ_1: 1;

      

       A12: ( len c) = ( width G) by MATRIX_0:def 7;

      then j1 in ( dom c) by A2, A8, FINSEQ_3: 25;

      then

       A13: (c /. j1) = (c . j1) by PARTFUN1:def 6;

      j2 in ( dom c) by A4, A10, A12, FINSEQ_3: 25;

      then

       A14: (c /. j2) = (c . j2) by PARTFUN1:def 6;

      

       A15: ( len ( Y_axis ( Line (G,i)))) = ( len c) by GOBOARD1:def 2;

      then

       A16: j1 in ( dom ( Y_axis ( Line (G,i)))) by A2, A8, A12, FINSEQ_3: 25;

      

       A17: ((G * (i,j1)) `2 ) = ((c /. j1) `2 ) by A9, A13, MATRIX_0:def 7

      .= (( Y_axis ( Line (G,i))) . j1) by A16, GOBOARD1:def 2;

      

       A18: j2 in ( dom ( Y_axis ( Line (G,i)))) by A4, A10, A12, A15, FINSEQ_3: 25;

      

      then (( Y_axis ( Line (G,i))) . j2) = ((c /. j2) `2 ) by GOBOARD1:def 2

      .= ((G * (i,j2)) `2 ) by A11, A14, MATRIX_0:def 7;

      hence thesis by A3, A7, A16, A17, A18;

    end;

    theorem :: GOBOARD5:5

    

     Th5: G is Y_equal-in-column & 1 <= j & j < ( width G) & 1 <= i & i <= ( len G) implies ( h_strip (G,j)) = { |[r, s]| : ((G * (i,j)) `2 ) <= s & s <= ((G * (i,(j + 1))) `2 ) }

    proof

      assume that

       A1: G is Y_equal-in-column and

       A2: 1 <= j and

       A3: j < ( width G) and

       A4: 1 <= i and

       A5: i <= ( len G);

      

       A6: 1 <= (j + 1) by A2, NAT_1: 13;

      

       A7: (j + 1) <= ( width G) by A3, NAT_1: 13;

      

       A8: ((G * (i,j)) `2 ) = ((G * (1,j)) `2 ) by A1, A2, A3, A4, A5, Th1;

      ((G * (i,(j + 1))) `2 ) = ((G * (1,(j + 1))) `2 ) by A1, A4, A5, A6, A7, Th1;

      hence thesis by A2, A3, A8, Def2;

    end;

    theorem :: GOBOARD5:6

    

     Th6: G is non empty-yielding Y_equal-in-column & 1 <= i & i <= ( len G) implies ( h_strip (G,( width G))) = { |[r, s]| : ((G * (i,( width G))) `2 ) <= s }

    proof

      assume that

       A1: G is non empty-yielding Y_equal-in-column and

       A2: 1 <= i and

       A3: i <= ( len G);

      ( width G) <> 0 by A1, MATRIX_0:def 10;

      then 1 <= ( width G) by NAT_1: 14;

      then ((G * (i,( width G))) `2 ) = ((G * (1,( width G))) `2 ) by A1, A2, A3, Th1;

      hence thesis by Def2;

    end;

    theorem :: GOBOARD5:7

    

     Th7: G is non empty-yielding Y_equal-in-column & 1 <= i & i <= ( len G) implies ( h_strip (G, 0 )) = { |[r, s]| : s <= ((G * (i,1)) `2 ) }

    proof

      assume that

       A1: G is non empty-yielding Y_equal-in-column and

       A2: 1 <= i and

       A3: i <= ( len G);

      set A = { |[r, s]| : ((G * (i,1)) `2 ) >= s };

      

       A4: 0 <> ( width G) by A1, MATRIX_0:def 10;

      then

       A5: 0 < ( width G);

      1 <= ( width G) by A4, NAT_1: 14;

      then ((G * (i,1)) `2 ) = ((G * (1,1)) `2 ) by A1, A2, A3, Th1;

      then A = { |[r, s]| : ((G * (1,(1 + 0 ))) `2 ) >= s };

      hence thesis by A5, Def2;

    end;

    theorem :: GOBOARD5:8

    

     Th8: G is X_equal-in-line & 1 <= i & i < ( len G) & 1 <= j & j <= ( width G) implies ( v_strip (G,i)) = { |[r, s]| : ((G * (i,j)) `1 ) <= r & r <= ((G * ((i + 1),j)) `1 ) }

    proof

      assume that

       A1: G is X_equal-in-line and

       A2: 1 <= i and

       A3: i < ( len G) and

       A4: 1 <= j and

       A5: j <= ( width G);

      

       A6: 1 <= (i + 1) by A2, NAT_1: 13;

      

       A7: (i + 1) <= ( len G) by A3, NAT_1: 13;

      

       A8: ((G * (i,j)) `1 ) = ((G * (i,1)) `1 ) by A1, A2, A3, A4, A5, Th2;

      ((G * ((i + 1),j)) `1 ) = ((G * ((i + 1),1)) `1 ) by A1, A4, A5, A6, A7, Th2;

      hence thesis by A2, A3, A8, Def1;

    end;

    theorem :: GOBOARD5:9

    

     Th9: G is non empty-yielding X_equal-in-line & 1 <= j & j <= ( width G) implies ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),j)) `1 ) <= r }

    proof

      assume that

       A1: G is non empty-yielding X_equal-in-line and

       A2: 1 <= j and

       A3: j <= ( width G);

      ( len G) <> 0 by A1, MATRIX_0:def 10;

      then 1 <= ( len G) by NAT_1: 14;

      then ((G * (( len G),j)) `1 ) = ((G * (( len G),1)) `1 ) by A1, A2, A3, Th2;

      hence thesis by Def1;

    end;

    theorem :: GOBOARD5:10

    

     Th10: G is non empty-yielding X_equal-in-line & 1 <= j & j <= ( width G) implies ( v_strip (G, 0 )) = { |[r, s]| : r <= ((G * (1,j)) `1 ) }

    proof

      assume that

       A1: G is non empty-yielding X_equal-in-line and

       A2: 1 <= j and

       A3: j <= ( width G);

      set A = { |[r, s]| : ((G * (1,j)) `1 ) >= r };

      

       A4: 0 <> ( len G) by A1, MATRIX_0:def 10;

      then

       A5: 0 < ( len G);

      1 <= ( len G) by A4, NAT_1: 14;

      then ((G * (1,j)) `1 ) = ((G * (1,1)) `1 ) by A1, A2, A3, Th2;

      then A = { |[r, s]| : ((G * (1,(1 + 0 ))) `1 ) >= r };

      hence thesis by A5, Def1;

    end;

    definition

      let G be Matrix of ( TOP-REAL 2);

      let i,j be Nat;

      :: GOBOARD5:def3

      func cell (G,i,j) -> Subset of ( TOP-REAL 2) equals (( v_strip (G,i)) /\ ( h_strip (G,j)));

      correctness ;

    end

    definition

      let IT be FinSequence of ( TOP-REAL 2);

      :: GOBOARD5:def4

      attr IT is s.c.c. means for i,j be Nat st (i + 1) < j & (i > 1 & j < ( len IT) or (j + 1) < ( len IT)) holds ( LSeg (IT,i)) misses ( LSeg (IT,j));

    end

    definition

      let IT be non empty FinSequence of ( TOP-REAL 2);

      :: GOBOARD5:def5

      attr IT is standard means

      : Def5: IT is_sequence_on ( GoB IT);

    end

    reconsider jj = 1, zz = 0 as Element of REAL by XREAL_0:def 1;

    registration

      cluster non constant special unfolded circular s.c.c. standard for non empty FinSequence of ( TOP-REAL 2);

      existence

      proof

        set f1 = <* |[ 0 , 0 ]|, |[ 0 , 1]|, |[1, 1]|*>, f2 = <* |[1, 0 ]|, |[ 0 , 0 ]|*>;

        

         A1: ( len f1) = 3 by FINSEQ_1: 45;

        

         A2: ( len f2) = 2 by FINSEQ_1: 44;

        then

         A3: ( len (f1 ^ f2)) = (3 + 2) by A1, FINSEQ_1: 22;

        reconsider f = (f1 ^ f2) as non empty FinSequence of ( TOP-REAL 2);

        take f;

        

         A4: 1 in ( dom f1) by A1, FINSEQ_3: 25;

        

        then

         A5: (f /. 1) = (f1 /. 1) by FINSEQ_4: 68

        .= |[ 0 , 0 ]| by FINSEQ_4: 18;

        

         A6: 2 in ( dom f1) by A1, FINSEQ_3: 25;

        

        then

         A7: (f /. 2) = (f1 /. 2) by FINSEQ_4: 68

        .= |[ 0 , 1]| by FINSEQ_4: 18;

        

         A8: ( dom f1) c= ( dom f) by FINSEQ_1: 26;

        then

         A9: (f . 1) = (f /. 1) by A4, PARTFUN1:def 6;

        (f . 2) = (f /. 2) by A6, A8, PARTFUN1:def 6;

        then (f . 1) <> (f . 2) by A5, A7, A9, SPPOL_2: 1;

        hence f is non constant by A4, A6, A8;

        3 in ( dom f1) by A1, FINSEQ_3: 25;

        

        then

         A10: (f /. 3) = (f1 /. 3) by FINSEQ_4: 68

        .= |[1, 1]| by FINSEQ_4: 18;

        1 in ( dom f2) by A2, FINSEQ_3: 25;

        

        then

         A11: (f /. (3 + 1)) = (f2 /. 1) by A1, FINSEQ_4: 69

        .= |[1, 0 ]| by FINSEQ_4: 17;

        2 in ( dom f2) by A2, FINSEQ_3: 25;

        

        then

         A12: (f /. (3 + 2)) = (f2 /. 2) by A1, FINSEQ_4: 69

        .= |[ 0 , 0 ]| by FINSEQ_4: 17;

        (1 + 1) = 2;

        then

         A13: ( LSeg (f,1)) = ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|)) by A3, A5, A7, TOPREAL1:def 3;

        (2 + 1) = 3;

        then

         A14: ( LSeg (f,2)) = ( LSeg ( |[ 0 , 1]|, |[1, 1]|)) by A3, A7, A10, TOPREAL1:def 3;

        

         A15: ( LSeg (f,3)) = ( LSeg ( |[1, 1]|, |[1, 0 ]|)) by A3, A10, A11, TOPREAL1:def 3;

        (4 + 1) = 5;

        then

         A16: ( LSeg (f,4)) = ( LSeg ( |[1, 0 ]|, |[ 0 , 0 ]|)) by A3, A11, A12, TOPREAL1:def 3;

        thus f is special

        proof

          let i be Nat;

          assume 1 <= i;

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

          then

           A17: 1 < (i + 1) by XXREAL_0: 2;

          assume (i + 1) <= ( len f);

          then

           A18: (i + 1) = 0 or ... or (i + 1) = 5 by A3;

          per cases by A17, A18;

            suppose

             A19: i = 1;

            ((f /. 1) `1 ) = 0 by A5, EUCLID: 52

            .= ((f /. (1 + 1)) `1 ) by A7, EUCLID: 52;

            hence thesis by A19;

          end;

            suppose

             A20: i = 2;

            ((f /. 2) `2 ) = 1 by A7, EUCLID: 52

            .= ((f /. (2 + 1)) `2 ) by A10, EUCLID: 52;

            hence thesis by A20;

          end;

            suppose

             A21: i = 3;

            ((f /. 3) `1 ) = 1 by A10, EUCLID: 52

            .= ((f /. (3 + 1)) `1 ) by A11, EUCLID: 52;

            hence thesis by A21;

          end;

            suppose

             A22: i = 4;

            ((f /. 4) `2 ) = 0 by A11, EUCLID: 52

            .= ((f /. (4 + 1)) `2 ) by A12, EUCLID: 52;

            hence thesis by A22;

          end;

        end;

        thus f is unfolded

        proof

          let i be Nat;

          assume 1 <= i;

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

          then

           A23: 2 < (i + 2) by XXREAL_0: 2;

          assume (i + 2) <= ( len f);

          then

           A24: (i + 2) = 0 or ... or (i + 2) = 5 by A3;

          per cases by A23, A24;

            suppose i = 1;

            hence thesis by A3, A5, A7, A14, TOPREAL1: 15, TOPREAL1:def 3;

          end;

            suppose i = 2;

            hence thesis by A3, A7, A10, A15, TOPREAL1: 18, TOPREAL1:def 3;

          end;

            suppose i = 3;

            hence thesis by A3, A10, A11, A16, TOPREAL1: 16, TOPREAL1:def 3;

          end;

        end;

        thus (f /. 1) = (f /. ( len f)) by A1, A2, A5, A12, FINSEQ_1: 22;

        thus f is s.c.c.

        proof

          let i,j be Nat;

          assume that

           A25: (i + 1) < j and

           A26: i > 1 & j < ( len f) or (j + 1) < ( len f);

          

           A27: (i + 1) >= 1 by NAT_1: 11;

          (j + 1) <= 5 by A3, A26, NAT_1: 13;

          then

           A28: (j + 1) = 0 or ... or (j + 1) = 5;

          

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

          then

           A30: (i + 2) <= j by A25, NAT_1: 13;

          

           A31: (i + 2) <> ( 0 + 1) by A29;

           A32:

          now

            per cases by A25, A27, A28;

              case j = 2;

              then (i + 2) = 0 or ... or (i + 2) = 2 by A30;

              hence i = 0 by A25;

            end;

              case j = 3;

              then (i + 2) = 0 or ... or (i + 2) = 3 by A30;

              hence i = 0 or i = 1 by A25;

            end;

              case

               A33: j = 4;

              then (i + 2) = 0 or ... or (i + 2) = 4 by A30;

              hence i = 0 or i = 2 by A3, A26, A31, A33;

            end;

          end;

          per cases by A32;

            suppose i = 0 ;

            then ( LSeg (f,i)) = {} by TOPREAL1:def 3;

            hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} ;

          end;

            suppose i = 1 & j = 3;

            hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} by A13, A15, TOPREAL1: 20;

          end;

            suppose i = 2 & j = 4;

            hence (( LSeg (f,i)) /\ ( LSeg (f,j))) = {} by A14, A16, TOPREAL1: 19;

          end;

        end;

        set Xf1 = <*zz, zz, jj*>, Xf2 = <*jj, zz*>;

        reconsider Xf = (Xf1 ^ Xf2) as FinSequence of REAL ;

        

         A34: ( len Xf1) = 3 by FINSEQ_1: 45;

        

         A35: ( len Xf2) = 2 by FINSEQ_1: 44;

        then

         A36: ( len Xf) = (3 + 2) by A34, FINSEQ_1: 22;

        1 in ( dom Xf1) by A34, FINSEQ_3: 25;

        

        then

         A37: (Xf . 1) = (Xf1 . 1) by FINSEQ_1:def 7

        .= 0 by FINSEQ_1: 45;

        2 in ( dom Xf1) by A34, FINSEQ_3: 25;

        

        then

         A38: (Xf . 2) = (Xf1 . 2) by FINSEQ_1:def 7

        .= 0 by FINSEQ_1: 45;

        3 in ( dom Xf1) by A34, FINSEQ_3: 25;

        

        then

         A39: (Xf . 3) = (Xf1 . 3) by FINSEQ_1:def 7

        .= 1 by FINSEQ_1: 45;

        1 in ( dom Xf2) by A35, FINSEQ_3: 25;

        

        then

         A40: (Xf . (3 + 1)) = (Xf2 . 1) by A34, FINSEQ_1:def 7

        .= 1 by FINSEQ_1: 44;

        2 in ( dom Xf2) by A35, FINSEQ_3: 25;

        

        then

         A41: (Xf . (3 + 2)) = (Xf2 . 2) by A34, FINSEQ_1:def 7

        .= 0 by FINSEQ_1: 44;

        now

          let n be Nat;

          assume

           A42: n in ( dom Xf);

          then

           A43: n <> 0 by FINSEQ_3: 25;

          n <= 5 by A36, A42, FINSEQ_3: 25;

          then n = 0 or ... or n = 5;

          per cases by A43;

            suppose n = 1;

            hence (Xf . n) = ((f /. n) `1 ) by A5, A37, EUCLID: 52;

          end;

            suppose n = 2;

            hence (Xf . n) = ((f /. n) `1 ) by A7, A38, EUCLID: 52;

          end;

            suppose n = 3;

            hence (Xf . n) = ((f /. n) `1 ) by A10, A39, EUCLID: 52;

          end;

            suppose n = 4;

            hence (Xf . n) = ((f /. n) `1 ) by A11, A40, EUCLID: 52;

          end;

            suppose n = 5;

            hence (Xf . n) = ((f /. n) `1 ) by A12, A41, EUCLID: 52;

          end;

        end;

        then

         A44: Xf = ( X_axis f) by A3, A36, GOBOARD1:def 1;

        

         A45: ( rng Xf1) = { 0 , 0 , 1} by FINSEQ_2: 128

        .= { 0 , 1} by ENUMSET1: 30;

        ( rng Xf2) = { 0 , 1} by FINSEQ_2: 127;

        

        then

         A46: ( rng Xf) = ( { 0 , 1} \/ { 0 , 1}) by A45, FINSEQ_1: 31

        .= { 0 , 1};

        then

         A47: ( rng <*zz, jj*>) = ( rng Xf) by FINSEQ_2: 127;

        

         A48: ( len <*zz, jj*>) = 2 by FINSEQ_1: 44

        .= ( card ( rng Xf)) by A46, CARD_2: 57;

         <*zz, jj*> is increasing

        proof

          let n,m be Nat;

          ( len <*zz, jj*>) = 2 by FINSEQ_1: 44;

          then

           A49: ( dom <*zz, jj*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

          assume that

           A50: n in ( dom <*zz, jj*>) and

           A51: m in ( dom <*zz, jj*>);

          

           A52: n = 1 or n = 2 by A49, A50, TARSKI:def 2;

          

           A53: m = 1 or m = 2 by A49, A51, TARSKI:def 2;

          assume

           A54: n < m;

          then

           A55: ( <* 0 , jj*> . n) = 0 by A52, A53, FINSEQ_1: 44;

          ( <* 0 , jj*> . m) = 1 by A52, A53, A54, FINSEQ_1: 44;

          hence ( <*zz, jj*> . n) < ( <*zz, jj*> . m) by A55;

        end;

        then

         A56: <* 0 , jj*> = ( Incr ( X_axis f)) by A44, A47, A48, SEQ_4:def 21;

        set Yf1 = <*zz, jj, jj*>, Yf2 = <*zz, zz*>;

        reconsider Yf = (Yf1 ^ Yf2) as FinSequence of REAL ;

        

         A57: ( len Yf1) = 3 by FINSEQ_1: 45;

        

         A58: ( len Yf2) = 2 by FINSEQ_1: 44;

        then

         A59: ( len Yf) = (3 + 2) by A57, FINSEQ_1: 22;

        1 in ( dom Yf1) by A57, FINSEQ_3: 25;

        

        then

         A60: (Yf . 1) = (Yf1 . 1) by FINSEQ_1:def 7

        .= 0 by FINSEQ_1: 45;

        2 in ( dom Yf1) by A57, FINSEQ_3: 25;

        

        then

         A61: (Yf . 2) = (Yf1 . 2) by FINSEQ_1:def 7

        .= 1 by FINSEQ_1: 45;

        3 in ( dom Yf1) by A57, FINSEQ_3: 25;

        

        then

         A62: (Yf . 3) = (Yf1 . 3) by FINSEQ_1:def 7

        .= 1 by FINSEQ_1: 45;

        1 in ( dom Yf2) by A58, FINSEQ_3: 25;

        

        then

         A63: (Yf . (3 + 1)) = (Yf2 . 1) by A57, FINSEQ_1:def 7

        .= 0 by FINSEQ_1: 44;

        2 in ( dom Yf2) by A58, FINSEQ_3: 25;

        

        then

         A64: (Yf . (3 + 2)) = (Yf2 . 2) by A57, FINSEQ_1:def 7

        .= 0 by FINSEQ_1: 44;

        now

          let n be Nat;

          assume

           A65: n in ( dom Yf);

          then

           A66: n <> 0 by FINSEQ_3: 25;

          n <= 5 by A59, A65, FINSEQ_3: 25;

          then n = 0 or ... or n = 5;

          per cases by A66;

            suppose n = 1;

            hence (Yf . n) = ((f /. n) `2 ) by A5, A60, EUCLID: 52;

          end;

            suppose n = 2;

            hence (Yf . n) = ((f /. n) `2 ) by A7, A61, EUCLID: 52;

          end;

            suppose n = 3;

            hence (Yf . n) = ((f /. n) `2 ) by A10, A62, EUCLID: 52;

          end;

            suppose n = 4;

            hence (Yf . n) = ((f /. n) `2 ) by A11, A63, EUCLID: 52;

          end;

            suppose n = 5;

            hence (Yf . n) = ((f /. n) `2 ) by A12, A64, EUCLID: 52;

          end;

        end;

        then

         A67: Yf = ( Y_axis f) by A3, A59, GOBOARD1:def 2;

        

         A68: ( rng Yf1) = { 0 , 1, 1} by FINSEQ_2: 128

        .= {1, 1, 0 } by ENUMSET1: 59

        .= { 0 , 1} by ENUMSET1: 30;

        ( rng Yf2) = { 0 , 0 } by FINSEQ_2: 127

        .= { 0 } by ENUMSET1: 29;

        

        then

         A69: ( rng Yf) = ( { 0 , 1} \/ { 0 }) by A68, FINSEQ_1: 31

        .= { 0 , 0 , 1} by ENUMSET1: 2

        .= { 0 , 1} by ENUMSET1: 30;

        then

         A70: ( rng <* 0 , jj*>) = ( rng Yf) by FINSEQ_2: 127;

        

         A71: ( len <* 0 , jj*>) = 2 by FINSEQ_1: 44

        .= ( card ( rng Yf)) by A69, CARD_2: 57;

         <*( In ( 0 , REAL )), jj*> is increasing

        proof

          let n,m be Nat;

          ( len <* 0 , jj*>) = 2 by FINSEQ_1: 44;

          then

           A72: ( dom <* 0 , jj*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

          assume that

           A73: n in ( dom <*( In ( 0 , REAL )), jj*>) and

           A74: m in ( dom <*( In ( 0 , REAL )), jj*>);

          

           A75: n = 1 or n = 2 by A72, A73, TARSKI:def 2;

          

           A76: m = 1 or m = 2 by A72, A74, TARSKI:def 2;

          assume

           A77: n < m;

          then

           A78: ( <* 0 , jj*> . n) = 0 by A75, A76, FINSEQ_1: 44;

          ( <* 0 , jj*> . m) = 1 by A75, A76, A77, FINSEQ_1: 44;

          hence ( <*( In ( 0 , REAL )), jj*> . n) < ( <*( In ( 0 , REAL )), jj*> . m) by A78;

        end;

        then

         A79: <* 0 , jj*> = ( Incr ( Y_axis f)) by A67, A70, A71, SEQ_4:def 21;

        set M = (( |[ 0 , 0 ]|, |[ 0 , 1]|) ][ ( |[1, 0 ]|, |[1, 1]|));

        

         A80: ( len M) = 2 by MATRIX_0: 47

        .= ( len ( Incr ( X_axis f))) by A56, FINSEQ_1: 44;

        

         A81: ( width M) = 2 by MATRIX_0: 47

        .= ( len ( Incr ( Y_axis f))) by A79, FINSEQ_1: 44;

        for n,m be Nat st [n, m] in ( Indices M) holds (M * (n,m)) = |[(( Incr ( X_axis f)) . n), (( Incr ( Y_axis f)) . m)]|

        proof

          let n,m be Nat;

          assume [n, m] in ( Indices M);

          then [n, m] in [: {1, 2}, {1, 2}:] by FINSEQ_1: 2, MATRIX_0: 47;

          then

           A82: [n, m] in { [1, 1], [1, 2], [2, 1], [2, 2]} by MCART_1: 23;

          

           A83: ( <* 0 , jj*> . 1) = 0 by FINSEQ_1: 44;

          

           A84: ( <* 0 , jj*> . 2) = 1 by FINSEQ_1: 44;

          per cases by A82, ENUMSET1:def 2;

            suppose

             A85: [n, m] = [1, 1];

            then

             A86: n = 1 by XTUPLE_0: 1;

            m = 1 by A85, XTUPLE_0: 1;

            hence thesis by A56, A79, A83, A86, MATRIX_0: 50;

          end;

            suppose

             A87: [n, m] = [1, 2];

            then

             A88: n = 1 by XTUPLE_0: 1;

            m = 2 by A87, XTUPLE_0: 1;

            hence thesis by A56, A79, A83, A84, A88, MATRIX_0: 50;

          end;

            suppose

             A89: [n, m] = [2, 1];

            then

             A90: n = 2 by XTUPLE_0: 1;

            m = 1 by A89, XTUPLE_0: 1;

            hence thesis by A56, A79, A83, A84, A90, MATRIX_0: 50;

          end;

            suppose

             A91: [n, m] = [2, 2];

            then

             A92: n = 2 by XTUPLE_0: 1;

            m = 2 by A91, XTUPLE_0: 1;

            hence thesis by A56, A79, A84, A92, MATRIX_0: 50;

          end;

        end;

        

        then

         A93: (( |[ 0 , 0 ]|, |[ 0 , 1]|) ][ ( |[1, 0 ]|, |[1, 1]|)) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by A80, A81, GOBOARD2:def 1

        .= ( GoB f) by GOBOARD2:def 2;

        then

         A94: (f /. 1) = (( GoB f) * (1,1)) by A5, MATRIX_0: 50;

        

         A95: (f /. 2) = (( GoB f) * (1,2)) by A7, A93, MATRIX_0: 50;

        

         A96: (f /. 3) = (( GoB f) * (2,2)) by A10, A93, MATRIX_0: 50;

        

         A97: (f /. 4) = (( GoB f) * (2,1)) by A11, A93, MATRIX_0: 50;

        thus for k st k in ( dom f) holds ex i, j st [i, j] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i,j))

        proof

          let k;

          assume

           A98: k in ( dom f);

          then

           A99: k <= 5 by A3, FINSEQ_3: 25;

          

           A100: k <> 0 by A98, FINSEQ_3: 25;

          k = 0 or ... or k = 5 by A99;

          per cases by A100;

            suppose

             A101: k = 1;

            take 1, 1;

            thus [1, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

            thus thesis by A5, A93, A101, MATRIX_0: 50;

          end;

            suppose

             A102: k = 2;

            take 1, 2;

            thus [1, 2] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

            thus thesis by A7, A93, A102, MATRIX_0: 50;

          end;

            suppose

             A103: k = 3;

            take 2, 2;

            thus [2, 2] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

            thus thesis by A10, A93, A103, MATRIX_0: 50;

          end;

            suppose

             A104: k = 4;

            take 2, 1;

            thus [2, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

            thus thesis by A11, A93, A104, MATRIX_0: 50;

          end;

            suppose

             A105: k = 5;

            take 1, 1;

            thus [1, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

            thus thesis by A12, A93, A105, MATRIX_0: 50;

          end;

        end;

        let n be Nat such that

         A106: n in ( dom f) and

         A107: (n + 1) in ( dom f);

        let m,k,i,j be Nat such that

         A108: [m, k] in ( Indices ( GoB f)) and

         A109: [i, j] in ( Indices ( GoB f)) and

         A110: (f /. n) = (( GoB f) * (m,k)) and

         A111: (f /. (n + 1)) = (( GoB f) * (i,j));

        

         A112: n <> 0 by A106, FINSEQ_3: 25;

        (n + 1) <= (4 + 1) by A3, A107, FINSEQ_3: 25;

        then n = 0 or ... or n = 4 by NAT_1: 60, XREAL_1: 6;

        per cases by A112;

          suppose

           A113: n = 1;

          

           A114: [1, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A115: m = 1 by A94, A108, A110, A113, GOBOARD1: 5;

          

           A116: k = 1 by A94, A108, A110, A113, A114, GOBOARD1: 5;

          

           A117: [1, 2] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A118: i = 1 by A95, A109, A111, A113, GOBOARD1: 5;

          j = (1 + 1) by A95, A109, A111, A113, A117, GOBOARD1: 5;

          then |.(k - j).| = 1 by A116, SEQM_3: 41;

          hence thesis by A115, A118, SEQM_3: 42;

        end;

          suppose

           A119: n = 2;

          

           A120: [1, 2] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A121: m = 1 by A95, A108, A110, A119, GOBOARD1: 5;

          

           A122: k = 2 by A95, A108, A110, A119, A120, GOBOARD1: 5;

          

           A123: [2, 2] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A124: i = (1 + 1) by A96, A109, A111, A119, GOBOARD1: 5;

          

           A125: j = 2 by A96, A109, A111, A119, A123, GOBOARD1: 5;

           |.(m - i).| = 1 by A121, A124, SEQM_3: 41;

          hence thesis by A122, A125, SEQM_3: 42;

        end;

          suppose

           A126: n = 3;

          

           A127: [2, 2] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A128: m = 2 by A96, A108, A110, A126, GOBOARD1: 5;

          

           A129: k = (1 + 1) by A96, A108, A110, A126, A127, GOBOARD1: 5;

          

           A130: [2, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A131: i = 2 by A97, A109, A111, A126, GOBOARD1: 5;

          j = 1 by A97, A109, A111, A126, A130, GOBOARD1: 5;

          then |.(k - j).| = 1 by A129, SEQM_3: 41;

          hence thesis by A128, A131, SEQM_3: 42;

        end;

          suppose

           A132: n = 4;

          

           A133: [2, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A134: m = (1 + 1) by A97, A108, A110, A132, GOBOARD1: 5;

          

           A135: k = 1 by A97, A108, A110, A132, A133, GOBOARD1: 5;

          

           A136: [1, 1] in ( Indices ( GoB f)) by A93, MATRIX_0: 48;

          then

           A137: i = 1 by A5, A12, A94, A109, A111, A132, GOBOARD1: 5;

          

           A138: j = 1 by A5, A12, A94, A109, A111, A132, A136, GOBOARD1: 5;

           |.(m - i).| = 1 by A134, A137, SEQM_3: 41;

          hence thesis by A135, A138, SEQM_3: 42;

        end;

      end;

    end

    

     Lm1: for f be FinSequence of ( TOP-REAL 2) holds ( dom ( X_axis f)) = ( dom f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      ( len ( X_axis f)) = ( len f) by GOBOARD1:def 1;

      hence thesis by FINSEQ_3: 29;

    end;

    

     Lm2: for f be FinSequence of ( TOP-REAL 2) holds ( dom ( Y_axis f)) = ( dom f)

    proof

      let f be FinSequence of ( TOP-REAL 2);

      ( len ( Y_axis f)) = ( len f) by GOBOARD1:def 2;

      hence thesis by FINSEQ_3: 29;

    end;

    theorem :: GOBOARD5:11

    

     Th11: for f be non empty FinSequence of ( TOP-REAL 2) holds for n be Nat st n in ( dom f) holds ex i, j st [i, j] in ( Indices ( GoB f)) & (f /. n) = (( GoB f) * (i,j))

    proof

      let f be non empty FinSequence of ( TOP-REAL 2);

      let n be Nat such that

       A1: n in ( dom f);

      

       A2: ( GoB f) = ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))) by GOBOARD2:def 2;

      set x = ((f /. n) `1 ), y = ((f /. n) `2 );

      

       A3: n in ( dom ( X_axis f)) by A1, Lm1;

      then (( X_axis f) . n) = x by GOBOARD1:def 1;

      then x in ( rng ( X_axis f)) by A3, FUNCT_1:def 3;

      then x in ( rng ( Incr ( X_axis f))) by SEQ_4:def 21;

      then

      consider i be Nat such that

       A4: i in ( dom ( Incr ( X_axis f))) and

       A5: (( Incr ( X_axis f)) . i) = x by FINSEQ_2: 10;

      

       A6: n in ( dom ( Y_axis f)) by A1, Lm2;

      then (( Y_axis f) . n) = y by GOBOARD1:def 2;

      then y in ( rng ( Y_axis f)) by A6, FUNCT_1:def 3;

      then y in ( rng ( Incr ( Y_axis f))) by SEQ_4:def 21;

      then

      consider j be Nat such that

       A7: j in ( dom ( Incr ( Y_axis f))) and

       A8: (( Incr ( Y_axis f)) . j) = y by FINSEQ_2: 10;

      reconsider i, j as Nat;

      take i, j;

      i in ( Seg ( len ( Incr ( X_axis f)))) by A4, FINSEQ_1:def 3;

      then i in ( Seg ( len ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))))) by GOBOARD2:def 1;

      then

       A9: i in ( dom ( GoB f)) by A2, FINSEQ_1:def 3;

      j in ( Seg ( len ( Incr ( Y_axis f)))) by A7, FINSEQ_1:def 3;

      then j in ( Seg ( width ( GoB (( Incr ( X_axis f)),( Incr ( Y_axis f)))))) by GOBOARD2:def 1;

      then [i, j] in [:( dom ( GoB f)), ( Seg ( width ( GoB f))):] by A2, A9, ZFMISC_1: 87;

      hence

       A10: [i, j] in ( Indices ( GoB f)) by MATRIX_0:def 4;

      

      thus (f /. n) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A5, A8, EUCLID: 53

      .= (( GoB f) * (i,j)) by A2, A10, GOBOARD2:def 1;

    end;

    theorem :: GOBOARD5:12

    

     Th12: for f be standard non empty FinSequence of ( TOP-REAL 2), n be Nat st n in ( dom f) & (n + 1) in ( dom f) holds for m,k,i,j be Nat st [m, k] in ( Indices ( GoB f)) & [i, j] in ( Indices ( GoB f)) & (f /. n) = (( GoB f) * (m,k)) & (f /. (n + 1)) = (( GoB f) * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1

    proof

      let f be standard non empty FinSequence of ( TOP-REAL 2), n be Nat such that

       A1: n in ( dom f) and

       A2: (n + 1) in ( dom f);

      f is_sequence_on ( GoB f) by Def5;

      hence thesis by A1, A2;

    end;

    definition

      mode special_circular_sequence is special unfolded circular s.c.c. non empty FinSequence of ( TOP-REAL 2);

    end

    reserve f for standard special_circular_sequence;

    definition

      let f, k;

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

      

       A6: (k + 1) in ( dom f) by A2, FINSEQ_3: 25, NAT_1: 11;

      then

      consider i2,j2 be Nat such that

       A7: [i2, j2] in ( Indices ( GoB f)) and

       A8: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by Th11;

      

       A9: ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A4, A5, A6, A7, A8, Th12;

       A10:

      now

        per cases by A9, SEQM_3: 42;

          case that

           A11: |.(i1 - i2).| = 1 and

           A12: j1 = j2;

          (i1 - i2) = 1 or ( - (i1 - i2)) = 1 by A11, ABSVALUE:def 1;

          hence i1 = (i2 + 1) or (i1 + 1) = i2;

          thus j1 = j2 by A12;

        end;

          case that

           A13: i1 = i2 and

           A14: |.(j1 - j2).| = 1;

          (j1 - j2) = 1 or ( - (j1 - j2)) = 1 by A14, ABSVALUE:def 1;

          hence j1 = (j2 + 1) or (j1 + 1) = j2;

          thus i1 = i2 by A13;

        end;

      end;

      :: GOBOARD5:def6

      func right_cell (f,k) -> Subset of ( TOP-REAL 2) means

      : Def6: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB f)) & [i2, j2] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & it = ( cell (( GoB f),i1,j1)) or (i1 + 1) = i2 & j1 = j2 & it = ( cell (( GoB f),i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & it = ( cell (( GoB f),i2,j2)) or i1 = i2 & j1 = (j2 + 1) & it = ( cell (( GoB f),(i1 -' 1),j2));

      existence

      proof

        per cases by A10;

          suppose

           A15: i1 = i2 & (j1 + 1) = j2;

          take ( cell (( GoB f),i1,j1));

          let i19,j19,i29,j29 be Nat;

          assume that

           A16: [i19, j19] in ( Indices ( GoB f)) and

           A17: [i29, j29] in ( Indices ( GoB f)) and

           A18: (f /. k) = (( GoB f) * (i19,j19)) and

           A19: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A20: i1 = i19 by A4, A5, A16, A18, GOBOARD1: 5;

          j1 = j19 by A4, A5, A16, A18, GOBOARD1: 5;

          hence thesis by A7, A8, A15, A17, A19, A20, GOBOARD1: 5;

        end;

          suppose

           A21: (i1 + 1) = i2 & j1 = j2;

          take ( cell (( GoB f),i1,(j1 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume that

           A22: [i19, j19] in ( Indices ( GoB f)) and

           A23: [i29, j29] in ( Indices ( GoB f)) and

           A24: (f /. k) = (( GoB f) * (i19,j19)) and

           A25: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A26: i1 = i19 by A4, A5, A22, A24, GOBOARD1: 5;

          j1 = j19 by A4, A5, A22, A24, GOBOARD1: 5;

          hence thesis by A7, A8, A21, A23, A25, A26, GOBOARD1: 5;

        end;

          suppose

           A27: i1 = (i2 + 1) & j1 = j2;

          take ( cell (( GoB f),i2,j2));

          let i19,j19,i29,j29 be Nat;

          assume that

           A28: [i19, j19] in ( Indices ( GoB f)) and

           A29: [i29, j29] in ( Indices ( GoB f)) and

           A30: (f /. k) = (( GoB f) * (i19,j19)) and

           A31: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A32: i2 = i29 by A7, A8, A29, A31, GOBOARD1: 5;

          j1 = j19 by A4, A5, A28, A30, GOBOARD1: 5;

          hence thesis by A4, A5, A7, A8, A27, A28, A29, A30, A31, A32, GOBOARD1: 5;

        end;

          suppose

           A33: i1 = i2 & j1 = (j2 + 1);

          take ( cell (( GoB f),(i1 -' 1),j2));

          let i19,j19,i29,j29 be Nat;

          assume that

           A34: [i19, j19] in ( Indices ( GoB f)) and

           A35: [i29, j29] in ( Indices ( GoB f)) and

           A36: (f /. k) = (( GoB f) * (i19,j19)) and

           A37: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A38: i1 = i19 by A4, A5, A34, A36, GOBOARD1: 5;

          j1 = j19 by A4, A5, A34, A36, GOBOARD1: 5;

          hence thesis by A7, A8, A33, A35, A37, A38, GOBOARD1: 5;

        end;

      end;

      uniqueness

      proof

        let P1,P2 be Subset of ( TOP-REAL 2) such that

         A39: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB f)) & [i2, j2] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & P1 = ( cell (( GoB f),i1,j1)) or (i1 + 1) = i2 & j1 = j2 & P1 = ( cell (( GoB f),i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & P1 = ( cell (( GoB f),i2,j2)) or i1 = i2 & j1 = (j2 + 1) & P1 = ( cell (( GoB f),(i1 -' 1),j2)) and

         A40: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB f)) & [i2, j2] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & P2 = ( cell (( GoB f),i1,j1)) or (i1 + 1) = i2 & j1 = j2 & P2 = ( cell (( GoB f),i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & P2 = ( cell (( GoB f),i2,j2)) or i1 = i2 & j1 = (j2 + 1) & P2 = ( cell (( GoB f),(i1 -' 1),j2));

        per cases by A10;

          suppose i1 = i2 & (j1 + 1) = j2;

          then

           A41: j1 < j2 by XREAL_1: 29;

          

           A42: j2 <= (j2 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),i1,j1)) by A4, A5, A7, A8, A39, A41

          .= P2 by A4, A5, A7, A8, A40, A41, A42;

        end;

          suppose (i1 + 1) = i2 & j1 = j2;

          then

           A43: i1 < i2 by XREAL_1: 29;

          

           A44: i2 <= (i2 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),i1,(j1 -' 1))) by A4, A5, A7, A8, A39, A43

          .= P2 by A4, A5, A7, A8, A40, A43, A44;

        end;

          suppose i1 = (i2 + 1) & j1 = j2;

          then

           A45: i2 < i1 by XREAL_1: 29;

          

           A46: i1 <= (i1 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),i2,j2)) by A4, A5, A7, A8, A39, A45

          .= P2 by A4, A5, A7, A8, A40, A45, A46;

        end;

          suppose i1 = i2 & j1 = (j2 + 1);

          then

           A47: j2 < j1 by XREAL_1: 29;

          

           A48: j1 <= (j1 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),(i1 -' 1),j2)) by A4, A5, A7, A8, A39, A47

          .= P2 by A4, A5, A7, A8, A40, A47, A48;

        end;

      end;

      :: GOBOARD5:def7

      func left_cell (f,k) -> Subset of ( TOP-REAL 2) means

      : Def7: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB f)) & [i2, j2] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & it = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & it = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & it = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & it = ( cell (( GoB f),i1,j2));

      existence

      proof

        per cases by A10;

          suppose

           A49: i1 = i2 & (j1 + 1) = j2;

          take ( cell (( GoB f),(i1 -' 1),j1));

          let i19,j19,i29,j29 be Nat;

          assume that

           A50: [i19, j19] in ( Indices ( GoB f)) and

           A51: [i29, j29] in ( Indices ( GoB f)) and

           A52: (f /. k) = (( GoB f) * (i19,j19)) and

           A53: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A54: i1 = i19 by A4, A5, A50, A52, GOBOARD1: 5;

          j1 = j19 by A4, A5, A50, A52, GOBOARD1: 5;

          hence thesis by A7, A8, A49, A51, A53, A54, GOBOARD1: 5;

        end;

          suppose

           A55: (i1 + 1) = i2 & j1 = j2;

          take ( cell (( GoB f),i1,j1));

          let i19,j19,i29,j29 be Nat;

          assume that

           A56: [i19, j19] in ( Indices ( GoB f)) and

           A57: [i29, j29] in ( Indices ( GoB f)) and

           A58: (f /. k) = (( GoB f) * (i19,j19)) and

           A59: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A60: i1 = i19 by A4, A5, A56, A58, GOBOARD1: 5;

          j1 = j19 by A4, A5, A56, A58, GOBOARD1: 5;

          hence thesis by A7, A8, A55, A57, A59, A60, GOBOARD1: 5;

        end;

          suppose

           A61: i1 = (i2 + 1) & j1 = j2;

          take ( cell (( GoB f),i2,(j2 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume that

           A62: [i19, j19] in ( Indices ( GoB f)) and

           A63: [i29, j29] in ( Indices ( GoB f)) and

           A64: (f /. k) = (( GoB f) * (i19,j19)) and

           A65: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A66: i2 = i29 by A7, A8, A63, A65, GOBOARD1: 5;

          j1 = j19 by A4, A5, A62, A64, GOBOARD1: 5;

          hence thesis by A4, A5, A7, A8, A61, A62, A63, A64, A65, A66, GOBOARD1: 5;

        end;

          suppose

           A67: i1 = i2 & j1 = (j2 + 1);

          take ( cell (( GoB f),i1,j2));

          let i19,j19,i29,j29 be Nat;

          assume that

           A68: [i19, j19] in ( Indices ( GoB f)) and

           A69: [i29, j29] in ( Indices ( GoB f)) and

           A70: (f /. k) = (( GoB f) * (i19,j19)) and

           A71: (f /. (k + 1)) = (( GoB f) * (i29,j29));

          

           A72: i1 = i19 by A4, A5, A68, A70, GOBOARD1: 5;

          j1 = j19 by A4, A5, A68, A70, GOBOARD1: 5;

          hence thesis by A7, A8, A67, A69, A71, A72, GOBOARD1: 5;

        end;

      end;

      uniqueness

      proof

        let P1,P2 be Subset of ( TOP-REAL 2) such that

         A73: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB f)) & [i2, j2] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & P1 = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & P1 = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & P1 = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & P1 = ( cell (( GoB f),i1,j2)) and

         A74: for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices ( GoB f)) & [i2, j2] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i1,j1)) & (f /. (k + 1)) = (( GoB f) * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & P2 = ( cell (( GoB f),(i1 -' 1),j1)) or (i1 + 1) = i2 & j1 = j2 & P2 = ( cell (( GoB f),i1,j1)) or i1 = (i2 + 1) & j1 = j2 & P2 = ( cell (( GoB f),i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & P2 = ( cell (( GoB f),i1,j2));

        per cases by A10;

          suppose i1 = i2 & (j1 + 1) = j2;

          then

           A75: j1 < j2 by XREAL_1: 29;

          

           A76: j2 <= (j2 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),(i1 -' 1),j1)) by A4, A5, A7, A8, A73, A75

          .= P2 by A4, A5, A7, A8, A74, A75, A76;

        end;

          suppose (i1 + 1) = i2 & j1 = j2;

          then

           A77: i1 < i2 by XREAL_1: 29;

          

           A78: i2 <= (i2 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),i1,j1)) by A4, A5, A7, A8, A73, A77

          .= P2 by A4, A5, A7, A8, A74, A77, A78;

        end;

          suppose i1 = (i2 + 1) & j1 = j2;

          then

           A79: i2 < i1 by XREAL_1: 29;

          

           A80: i1 <= (i1 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),i2,(j2 -' 1))) by A4, A5, A7, A8, A73, A79

          .= P2 by A4, A5, A7, A8, A74, A79, A80;

        end;

          suppose i1 = i2 & j1 = (j2 + 1);

          then

           A81: j2 < j1 by XREAL_1: 29;

          

           A82: j1 <= (j1 + 1) by NAT_1: 11;

          

          hence P1 = ( cell (( GoB f),i1,j2)) by A4, A5, A7, A8, A73, A81

          .= P2 by A4, A5, A7, A8, A74, A81, A82;

        end;

      end;

    end

    theorem :: GOBOARD5:13

    

     Th13: G is non empty-yielding X_equal-in-line X_increasing-in-column & i < ( len G) & 1 <= j & j < ( width G) implies ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) c= ( v_strip (G,i))

    proof

      assume that

       A1: G is non empty-yielding and

       A2: G is X_equal-in-line and

       A3: G is X_increasing-in-column and

       A4: i < ( len G) and

       A5: 1 <= j and

       A6: j < ( width G);

      

       A7: 1 <= (j + 1) by A5, NAT_1: 13;

      

       A8: (j + 1) <= ( width G) by A6, NAT_1: 13;

      let x be object;

      assume

       A9: x in ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))));

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A10: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

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

      

       A12: (i + 1) <= ( len G) by A4, NAT_1: 13;

      

      then

       A13: ((G * ((i + 1),j)) `1 ) = ((G * ((i + 1),1)) `1 ) by A2, A5, A6, A11, Th2

      .= ((G * ((i + 1),(j + 1))) `1 ) by A2, A7, A8, A11, A12, Th2;

      now

        per cases ;

          suppose

           A14: i = 0 ;

          then (p `1 ) <= ((G * (1,j)) `1 ) by A9, A13, TOPREAL1: 3;

          then p in { |[r, s]| : r <= ((G * (1,j)) `1 ) } by A10;

          hence thesis by A1, A2, A5, A6, A14, Th10;

        end;

          suppose i > 0 ;

          then

           A15: ( 0 + 1) <= i by NAT_1: 13;

          

           A16: ((G * ((i + 1),j)) `1 ) <= (p `1 ) by A9, A13, TOPREAL1: 3;

          

           A17: (p `1 ) <= ((G * ((i + 1),j)) `1 ) by A9, A13, TOPREAL1: 3;

          then

           A18: (p `1 ) = ((G * ((i + 1),j)) `1 ) by A16, XXREAL_0: 1;

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

          then ((G * (i,j)) `1 ) < (p `1 ) by A3, A5, A6, A12, A15, A18, Th3;

          then p in { |[r, s]| : ((G * (i,j)) `1 ) <= r & r <= ((G * ((i + 1),j)) `1 ) } by A10, A17;

          hence thesis by A2, A4, A5, A6, A15, Th8;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD5:14

    

     Th14: G is non empty-yielding X_equal-in-line X_increasing-in-column & 1 <= i & i <= ( len G) & 1 <= j & j < ( width G) implies ( LSeg ((G * (i,j)),(G * (i,(j + 1))))) c= ( v_strip (G,i))

    proof

      assume that

       A1: G is non empty-yielding and

       A2: G is X_equal-in-line and

       A3: G is X_increasing-in-column and

       A4: 1 <= i and

       A5: i <= ( len G) and

       A6: 1 <= j and

       A7: j < ( width G);

      

       A8: 1 <= (j + 1) by A6, NAT_1: 13;

      

       A9: (j + 1) <= ( width G) by A7, NAT_1: 13;

      let x be object;

      assume

       A10: x in ( LSeg ((G * (i,j)),(G * (i,(j + 1)))));

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A11: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A12: ((G * (i,j)) `1 ) = ((G * (i,1)) `1 ) by A2, A4, A5, A6, A7, Th2

      .= ((G * (i,(j + 1))) `1 ) by A2, A4, A5, A8, A9, Th2;

      now

        per cases by A5, XXREAL_0: 1;

          suppose

           A13: i = ( len G);

          then ((G * (( len G),j)) `1 ) <= (p `1 ) by A10, A12, TOPREAL1: 3;

          then p in { |[r, s]| : ((G * (( len G),j)) `1 ) <= r } by A11;

          hence thesis by A1, A2, A6, A7, A13, Th9;

        end;

          suppose

           A14: i < ( len G);

          then

           A15: (i + 1) <= ( len G) by NAT_1: 13;

          

           A16: ((G * (i,j)) `1 ) <= (p `1 ) by A10, A12, TOPREAL1: 3;

          (p `1 ) <= ((G * (i,j)) `1 ) by A10, A12, TOPREAL1: 3;

          then

           A17: (p `1 ) = ((G * (i,j)) `1 ) by A16, XXREAL_0: 1;

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

          then (p `1 ) < ((G * ((i + 1),j)) `1 ) by A3, A4, A6, A7, A15, A17, Th3;

          then p in { |[r, s]| : ((G * (i,j)) `1 ) <= r & r <= ((G * ((i + 1),j)) `1 ) } by A11, A16;

          hence thesis by A2, A4, A6, A7, A14, Th8;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD5:15

    

     Th15: G is non empty-yielding Y_equal-in-column Y_increasing-in-line & j < ( width G) & 1 <= i & i < ( len G) implies ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))) c= ( h_strip (G,j))

    proof

      assume that

       A1: G is non empty-yielding and

       A2: G is Y_equal-in-column and

       A3: G is Y_increasing-in-line and

       A4: j < ( width G) and

       A5: 1 <= i and

       A6: i < ( len G);

      

       A7: 1 <= (i + 1) by A5, NAT_1: 13;

      

       A8: (i + 1) <= ( len G) by A6, NAT_1: 13;

      let x be object;

      assume

       A9: x in ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))));

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A10: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

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

      

       A12: (j + 1) <= ( width G) by A4, NAT_1: 13;

      

      then

       A13: ((G * (i,(j + 1))) `2 ) = ((G * (1,(j + 1))) `2 ) by A2, A5, A6, A11, Th1

      .= ((G * ((i + 1),(j + 1))) `2 ) by A2, A7, A8, A11, A12, Th1;

      now

        per cases ;

          suppose

           A14: j = 0 ;

          then (p `2 ) <= ((G * (i,1)) `2 ) by A9, A13, TOPREAL1: 4;

          then p in { |[r, s]| : s <= ((G * (i,1)) `2 ) } by A10;

          hence thesis by A1, A2, A5, A6, A14, Th7;

        end;

          suppose j > 0 ;

          then

           A15: ( 0 + 1) <= j by NAT_1: 13;

          

           A16: ((G * (i,(j + 1))) `2 ) <= (p `2 ) by A9, A13, TOPREAL1: 4;

          

           A17: (p `2 ) <= ((G * (i,(j + 1))) `2 ) by A9, A13, TOPREAL1: 4;

          then

           A18: (p `2 ) = ((G * (i,(j + 1))) `2 ) by A16, XXREAL_0: 1;

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

          then ((G * (i,j)) `2 ) < (p `2 ) by A3, A5, A6, A12, A15, A18, Th4;

          then p in { |[r, s]| : ((G * (i,j)) `2 ) <= s & s <= ((G * (i,(j + 1))) `2 ) } by A10, A17;

          hence thesis by A2, A4, A5, A6, A15, Th5;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD5:16

    

     Th16: G is non empty-yielding Y_equal-in-column Y_increasing-in-line & 1 <= j & j <= ( width G) & 1 <= i & i < ( len G) implies ( LSeg ((G * (i,j)),(G * ((i + 1),j)))) c= ( h_strip (G,j))

    proof

      assume that

       A1: G is non empty-yielding and

       A2: G is Y_equal-in-column and

       A3: G is Y_increasing-in-line and

       A4: 1 <= j and

       A5: j <= ( width G) and

       A6: 1 <= i and

       A7: i < ( len G);

      

       A8: 1 <= (i + 1) by A6, NAT_1: 13;

      

       A9: (i + 1) <= ( len G) by A7, NAT_1: 13;

      let x be object;

      assume

       A10: x in ( LSeg ((G * (i,j)),(G * ((i + 1),j))));

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A11: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A12: ((G * (i,j)) `2 ) = ((G * (1,j)) `2 ) by A2, A4, A5, A6, A7, Th1

      .= ((G * ((i + 1),j)) `2 ) by A2, A4, A5, A8, A9, Th1;

      now

        per cases by A5, XXREAL_0: 1;

          suppose

           A13: j = ( width G);

          then ((G * (i,( width G))) `2 ) <= (p `2 ) by A10, A12, TOPREAL1: 4;

          then p in { |[r, s]| : ((G * (i,( width G))) `2 ) <= s } by A11;

          hence thesis by A1, A2, A6, A7, A13, Th6;

        end;

          suppose

           A14: j < ( width G);

          then

           A15: (j + 1) <= ( width G) by NAT_1: 13;

          

           A16: ((G * (i,j)) `2 ) <= (p `2 ) by A10, A12, TOPREAL1: 4;

          (p `2 ) <= ((G * (i,j)) `2 ) by A10, A12, TOPREAL1: 4;

          then

           A17: (p `2 ) = ((G * (i,j)) `2 ) by A16, XXREAL_0: 1;

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

          then (p `2 ) < ((G * (i,(j + 1))) `2 ) by A3, A4, A6, A7, A15, A17, Th4;

          then p in { |[r, s]| : ((G * (i,j)) `2 ) <= s & s <= ((G * (i,(j + 1))) `2 ) } by A11, A16;

          hence thesis by A2, A4, A6, A7, A14, Th5;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD5:17

    

     Th17: G is Y_equal-in-column Y_increasing-in-line & 1 <= i & i <= ( len G) & 1 <= j & (j + 1) <= ( width G) implies ( LSeg ((G * (i,j)),(G * (i,(j + 1))))) c= ( h_strip (G,j))

    proof

      assume that

       A1: G is Y_equal-in-column and

       A2: G is Y_increasing-in-line and

       A3: 1 <= i and

       A4: i <= ( len G) and

       A5: 1 <= j and

       A6: (j + 1) <= ( width G);

      let x be object;

      assume

       A7: x in ( LSeg ((G * (i,j)),(G * (i,(j + 1)))));

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A8: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A9: j < ( width G) by A6, NAT_1: 13;

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

      then

       A10: ((G * (i,j)) `2 ) < ((G * (i,(j + 1))) `2 ) by A2, A3, A4, A5, A6, Th4;

      then

       A11: ((G * (i,j)) `2 ) <= (p `2 ) by A7, TOPREAL1: 4;

      (p `2 ) <= ((G * (i,(j + 1))) `2 ) by A7, A10, TOPREAL1: 4;

      then p in { |[r, s]| : ((G * (i,j)) `2 ) <= s & s <= ((G * (i,(j + 1))) `2 ) } by A8, A11;

      hence thesis by A1, A3, A4, A5, A9, Th5;

    end;

    theorem :: GOBOARD5:18

    

     Th18: for G be Go-board holds i < ( len G) & 1 <= j & j < ( width G) implies ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) c= ( cell (G,i,j))

    proof

      let G be Go-board;

      assume that

       A1: i < ( len G) and

       A2: 1 <= j and

       A3: j < ( width G);

      

       A4: ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) c= ( v_strip (G,i)) by A1, A2, A3, Th13;

      

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

      

       A6: (i + 1) <= ( len G) by A1, NAT_1: 13;

      (j + 1) <= ( width G) by A3, NAT_1: 13;

      then ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) c= ( h_strip (G,j)) by A2, A5, A6, Th17;

      hence thesis by A4, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:19

    

     Th19: for G be Go-board holds 1 <= i & i <= ( len G) & 1 <= j & j < ( width G) implies ( LSeg ((G * (i,j)),(G * (i,(j + 1))))) c= ( cell (G,i,j))

    proof

      let G be Go-board;

      assume that

       A1: 1 <= i and

       A2: i <= ( len G) and

       A3: 1 <= j and

       A4: j < ( width G);

      

       A5: ( LSeg ((G * (i,j)),(G * (i,(j + 1))))) c= ( v_strip (G,i)) by A1, A2, A3, A4, Th14;

      (j + 1) <= ( width G) by A4, NAT_1: 13;

      then ( LSeg ((G * (i,j)),(G * (i,(j + 1))))) c= ( h_strip (G,j)) by A1, A2, A3, Th17;

      hence thesis by A5, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:20

    

     Th20: G is X_equal-in-line X_increasing-in-column & 1 <= j & j <= ( width G) & 1 <= i & (i + 1) <= ( len G) implies ( LSeg ((G * (i,j)),(G * ((i + 1),j)))) c= ( v_strip (G,i))

    proof

      assume that

       A1: G is X_equal-in-line and

       A2: G is X_increasing-in-column and

       A3: 1 <= j and

       A4: j <= ( width G) and

       A5: 1 <= i and

       A6: (i + 1) <= ( len G);

      let x be object;

      assume

       A7: x in ( LSeg ((G * (i,j)),(G * ((i + 1),j))));

      then

      reconsider p = x as Point of ( TOP-REAL 2);

      

       A8: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

      

       A9: i < ( len G) by A6, NAT_1: 13;

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

      then

       A10: ((G * (i,j)) `1 ) < ((G * ((i + 1),j)) `1 ) by A2, A3, A4, A5, A6, Th3;

      then

       A11: ((G * (i,j)) `1 ) <= (p `1 ) by A7, TOPREAL1: 3;

      (p `1 ) <= ((G * ((i + 1),j)) `1 ) by A7, A10, TOPREAL1: 3;

      then p in { |[r, s]| : ((G * (i,j)) `1 ) <= r & r <= ((G * ((i + 1),j)) `1 ) } by A8, A11;

      hence thesis by A1, A3, A4, A5, A9, Th8;

    end;

    theorem :: GOBOARD5:21

    

     Th21: for G be Go-board holds j < ( width G) & 1 <= i & i < ( len G) implies ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))) c= ( cell (G,i,j))

    proof

      let G be Go-board;

      assume that

       A1: j < ( width G) and

       A2: 1 <= i and

       A3: i < ( len G);

      

       A4: ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))) c= ( h_strip (G,j)) by A1, A2, A3, Th15;

      

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

      

       A6: (i + 1) <= ( len G) by A3, NAT_1: 13;

      (j + 1) <= ( width G) by A1, NAT_1: 13;

      then ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))) c= ( v_strip (G,i)) by A2, A5, A6, Th20;

      hence thesis by A4, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:22

    

     Th22: for G be Go-board holds 1 <= i & i < ( len G) & 1 <= j & j <= ( width G) implies ( LSeg ((G * (i,j)),(G * ((i + 1),j)))) c= ( cell (G,i,j))

    proof

      let G be Go-board;

      assume that

       A1: 1 <= i and

       A2: i < ( len G) and

       A3: 1 <= j and

       A4: j <= ( width G);

      

       A5: ( LSeg ((G * (i,j)),(G * ((i + 1),j)))) c= ( h_strip (G,j)) by A1, A2, A3, A4, Th16;

      (i + 1) <= ( len G) by A2, NAT_1: 13;

      then ( LSeg ((G * (i,j)),(G * ((i + 1),j)))) c= ( v_strip (G,i)) by A1, A3, A4, Th20;

      hence thesis by A5, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:23

    

     Th23: G is non empty-yielding X_equal-in-line X_increasing-in-column & (i + 1) <= ( len G) implies (( v_strip (G,i)) /\ ( v_strip (G,(i + 1)))) = { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) }

    proof

      assume that

       A1: G is non empty-yielding X_equal-in-line and

       A2: G is X_increasing-in-column and

       A3: (i + 1) <= ( len G);

      ( width G) <> 0 by A1, MATRIX_0:def 10;

      then

       A4: 1 <= ( width G) by NAT_1: 14;

      

       A5: i < ( len G) by A3, NAT_1: 13;

      thus (( v_strip (G,i)) /\ ( v_strip (G,(i + 1)))) c= { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) }

      proof

        let x be object;

        assume

         A6: x in (( v_strip (G,i)) /\ ( v_strip (G,(i + 1))));

        then

         A7: x in ( v_strip (G,i)) by XBOOLE_0:def 4;

        

         A8: x in ( v_strip (G,(i + 1))) by A6, XBOOLE_0:def 4;

        reconsider p = x as Point of ( TOP-REAL 2) by A6;

        per cases ;

          suppose that

           A9: i = 0 and

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

          ( v_strip (G,i)) = { |[r, s]| : r <= ((G * (( 0 + 1),1)) `1 ) } by A1, A4, A9, Th10;

          then

          consider r1,s1 be Real such that

           A11: x = |[r1, s1]| and

           A12: r1 <= ((G * (1,1)) `1 ) by A7;

          ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r } by A1, A4, Th9;

          then

          consider r2,s2 be Real such that

           A13: x = |[r2, s2]| and

           A14: ((G * ((i + 1),1)) `1 ) <= r2 by A8, A10;

          r1 = ( |[r2, s2]| `1 ) by A11, A13, EUCLID: 52

          .= r2 by EUCLID: 52;

          then ((G * ((i + 1),1)) `1 ) = r1 by A9, A12, A14, XXREAL_0: 1;

          then ((G * ((i + 1),1)) `1 ) = (p `1 ) by A11, EUCLID: 52;

          hence thesis;

        end;

          suppose that

           A15: i = 0 and

           A16: (i + 1) <> ( len G);

          ( v_strip (G,i)) = { |[r, s]| : r <= ((G * (( 0 + 1),1)) `1 ) } by A1, A4, A15, Th10;

          then

          consider r1,s1 be Real such that

           A17: x = |[r1, s1]| and

           A18: r1 <= ((G * (1,1)) `1 ) by A7;

          (i + 1) < ( len G) by A3, A16, XXREAL_0: 1;

          then ( v_strip (G,(i + 1))) = { |[r, s]| : ((G * (( 0 + 1),1)) `1 ) <= r & r <= ((G * ((( 0 + 1) + 1),1)) `1 ) } by A1, A4, A15, Th8;

          then

          consider r2,s2 be Real such that

           A19: x = |[r2, s2]| and

           A20: ((G * (1,1)) `1 ) <= r2 and r2 <= ((G * ((1 + 1),1)) `1 ) by A8;

          r1 = ( |[r2, s2]| `1 ) by A17, A19, EUCLID: 52

          .= r2 by EUCLID: 52;

          then ((G * (1,1)) `1 ) = r1 by A18, A20, XXREAL_0: 1;

          then ((G * (1,1)) `1 ) = (p `1 ) by A17, EUCLID: 52;

          hence thesis by A15;

        end;

          suppose that

           A21: i <> 0 and

           A22: (i + 1) = ( len G);

          

           A23: 1 <= i by A21, NAT_1: 14;

          ( v_strip (G,i)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) } by A1, A4, A23, Th8, A3, NAT_1: 13;

          then

          consider r1,s1 be Real such that

           A24: x = |[r1, s1]| and ((G * (i,1)) `1 ) <= r1 and

           A25: r1 <= ((G * ((i + 1),1)) `1 ) by A7;

          ( v_strip (G,( len G))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r } by A1, A4, Th9;

          then

          consider r2,s2 be Real such that

           A26: x = |[r2, s2]| and

           A27: ((G * ((i + 1),1)) `1 ) <= r2 by A8, A22;

          r1 = ( |[r2, s2]| `1 ) by A24, A26, EUCLID: 52

          .= r2 by EUCLID: 52;

          then ((G * ((i + 1),1)) `1 ) = r1 by A25, A27, XXREAL_0: 1;

          then ((G * ((i + 1),1)) `1 ) = (p `1 ) by A24, EUCLID: 52;

          hence thesis;

        end;

          suppose that

           A28: i <> 0 and

           A29: (i + 1) <> ( len G);

          

           A30: 1 <= i by A28, NAT_1: 14;

          ( v_strip (G,i)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) } by A1, A4, A30, Th8, A3, NAT_1: 13;

          then

          consider r1,s1 be Real such that

           A31: x = |[r1, s1]| and ((G * (i,1)) `1 ) <= r1 and

           A32: r1 <= ((G * ((i + 1),1)) `1 ) by A7;

          

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

          (i + 1) < ( len G) by A3, A29, XXREAL_0: 1;

          then ( v_strip (G,(i + 1))) = { |[r, s]| : ((G * ((i + 1),1)) `1 ) <= r & r <= ((G * (((i + 1) + 1),1)) `1 ) } by A1, A4, A33, Th8;

          then

          consider r2,s2 be Real such that

           A34: x = |[r2, s2]| and

           A35: ((G * ((i + 1),1)) `1 ) <= r2 and r2 <= ((G * (((i + 1) + 1),1)) `1 ) by A8;

          r1 = ( |[r2, s2]| `1 ) by A31, A34, EUCLID: 52

          .= r2 by EUCLID: 52;

          then ((G * ((i + 1),1)) `1 ) = r1 by A32, A35, XXREAL_0: 1;

          then ((G * ((i + 1),1)) `1 ) = (p `1 ) by A31, EUCLID: 52;

          hence thesis;

        end;

      end;

      

       A36: { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) } c= ( v_strip (G,i))

      proof

        let x be object;

        assume x in { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) };

        then

        consider p such that

         A37: p = x and

         A38: (p `1 ) = ((G * ((i + 1),1)) `1 );

        

         A39: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

        per cases by NAT_1: 14;

          suppose

           A40: i = 0 ;

          then ( v_strip (G,i)) = { |[r, s]| : r <= ((G * (1,1)) `1 ) } by A1, A4, Th10;

          hence thesis by A37, A38, A39, A40;

        end;

          suppose

           A41: i >= 1;

          then

           A42: ( v_strip (G,i)) = { |[r, s]| : ((G * (i,1)) `1 ) <= r & r <= ((G * ((i + 1),1)) `1 ) } by A1, A4, A5, Th8;

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

          then ((G * (i,1)) `1 ) < (p `1 ) by A2, A3, A4, A38, A41, Th3;

          hence thesis by A37, A38, A39, A42;

        end;

      end;

      { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) } c= ( v_strip (G,(i + 1)))

      proof

        let x be object;

        assume x in { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) };

        then

        consider p such that

         A43: p = x and

         A44: (p `1 ) = ((G * ((i + 1),1)) `1 );

        

         A45: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

        

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

        per cases by A3, XXREAL_0: 1;

          suppose

           A47: (i + 1) = ( len G);

          then ( v_strip (G,(i + 1))) = { |[r, s]| : ((G * (( len G),1)) `1 ) <= r } by A1, A4, Th9;

          hence thesis by A43, A44, A45, A47;

        end;

          suppose

           A48: (i + 1) < ( len G);

          then

           A49: ( v_strip (G,(i + 1))) = { |[r, s]| : ((G * ((i + 1),1)) `1 ) <= r & r <= ((G * (((i + 1) + 1),1)) `1 ) } by A1, A4, A46, Th8;

          

           A50: (i + 1) < ((i + 1) + 1) by NAT_1: 13;

          ((i + 1) + 1) <= ( len G) by A48, NAT_1: 13;

          then (p `1 ) < ((G * (((i + 1) + 1),1)) `1 ) by A2, A4, A44, A46, A50, Th3;

          hence thesis by A43, A44, A45, A49;

        end;

      end;

      hence thesis by A36, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:24

    

     Th24: G is non empty-yielding Y_equal-in-column Y_increasing-in-line & (j + 1) <= ( width G) implies (( h_strip (G,j)) /\ ( h_strip (G,(j + 1)))) = { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) }

    proof

      assume that

       A1: G is non empty-yielding Y_equal-in-column and

       A2: G is Y_increasing-in-line and

       A3: (j + 1) <= ( width G);

      ( len G) <> 0 by A1, MATRIX_0:def 10;

      then

       A4: 1 <= ( len G) by NAT_1: 14;

      

       A5: j < ( width G) by A3, NAT_1: 13;

      thus (( h_strip (G,j)) /\ ( h_strip (G,(j + 1)))) c= { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) }

      proof

        let x be object;

        assume

         A6: x in (( h_strip (G,j)) /\ ( h_strip (G,(j + 1))));

        then

         A7: x in ( h_strip (G,j)) by XBOOLE_0:def 4;

        

         A8: x in ( h_strip (G,(j + 1))) by A6, XBOOLE_0:def 4;

        reconsider p = x as Point of ( TOP-REAL 2) by A6;

        per cases ;

          suppose that

           A9: j = 0 and

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

          ( h_strip (G,j)) = { |[r, s]| : s <= ((G * (1,( 0 + 1))) `2 ) } by A1, A4, A9, Th7;

          then

          consider r1,s1 be Real such that

           A11: x = |[r1, s1]| and

           A12: s1 <= ((G * (1,1)) `2 ) by A7;

          ( h_strip (G,( width G))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s } by A1, A4, Th6;

          then

          consider r2,s2 be Real such that

           A13: x = |[r2, s2]| and

           A14: ((G * (1,(j + 1))) `2 ) <= s2 by A8, A10;

          s1 = ( |[r2, s2]| `2 ) by A11, A13, EUCLID: 52

          .= s2 by EUCLID: 52;

          then ((G * (1,(j + 1))) `2 ) = s1 by A9, A12, A14, XXREAL_0: 1;

          then ((G * (1,(j + 1))) `2 ) = (p `2 ) by A11, EUCLID: 52;

          hence thesis;

        end;

          suppose that

           A15: j = 0 and

           A16: (j + 1) <> ( width G);

          ( h_strip (G,j)) = { |[r, s]| : s <= ((G * (1,( 0 + 1))) `2 ) } by A1, A4, A15, Th7;

          then

          consider r1,s1 be Real such that

           A17: x = |[r1, s1]| and

           A18: s1 <= ((G * (1,1)) `2 ) by A7;

          (j + 1) < ( width G) by A3, A16, XXREAL_0: 1;

          then ( h_strip (G,(j + 1))) = { |[r, s]| : ((G * (1,( 0 + 1))) `2 ) <= s & s <= ((G * (1,(( 0 + 1) + 1))) `2 ) } by A1, A4, A15, Th5;

          then

          consider r2,s2 be Real such that

           A19: x = |[r2, s2]| and

           A20: ((G * (1,1)) `2 ) <= s2 and s2 <= ((G * (1,(1 + 1))) `2 ) by A8;

          s1 = ( |[r2, s2]| `2 ) by A17, A19, EUCLID: 52

          .= s2 by EUCLID: 52;

          then ((G * (1,1)) `2 ) = s1 by A18, A20, XXREAL_0: 1;

          then ((G * (1,1)) `2 ) = (p `2 ) by A17, EUCLID: 52;

          hence thesis by A15;

        end;

          suppose that

           A21: j <> 0 and

           A22: (j + 1) = ( width G);

          

           A23: 1 <= j by A21, NAT_1: 14;

          ( h_strip (G,j)) = { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A1, A4, A23, Th5, A3, NAT_1: 13;

          then

          consider r1,s1 be Real such that

           A24: x = |[r1, s1]| and ((G * (1,j)) `2 ) <= s1 and

           A25: s1 <= ((G * (1,(j + 1))) `2 ) by A7;

          ( h_strip (G,( width G))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s } by A1, A4, Th6;

          then

          consider r2,s2 be Real such that

           A26: x = |[r2, s2]| and

           A27: ((G * (1,(j + 1))) `2 ) <= s2 by A8, A22;

          s1 = ( |[r2, s2]| `2 ) by A24, A26, EUCLID: 52

          .= s2 by EUCLID: 52;

          then ((G * (1,(j + 1))) `2 ) = s1 by A25, A27, XXREAL_0: 1;

          then ((G * (1,(j + 1))) `2 ) = (p `2 ) by A24, EUCLID: 52;

          hence thesis;

        end;

          suppose that

           A28: j <> 0 and

           A29: (j + 1) <> ( width G);

          

           A30: 1 <= j by A28, NAT_1: 14;

          ( h_strip (G,j)) = { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A1, A4, A30, Th5, A3, NAT_1: 13;

          then

          consider r1,s1 be Real such that

           A31: x = |[r1, s1]| and ((G * (1,j)) `2 ) <= s1 and

           A32: s1 <= ((G * (1,(j + 1))) `2 ) by A7;

          

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

          (j + 1) < ( width G) by A3, A29, XXREAL_0: 1;

          then ( h_strip (G,(j + 1))) = { |[r, s]| : ((G * (1,(j + 1))) `2 ) <= s & s <= ((G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A33, Th5;

          then

          consider r2,s2 be Real such that

           A34: x = |[r2, s2]| and

           A35: ((G * (1,(j + 1))) `2 ) <= s2 and s2 <= ((G * (1,((j + 1) + 1))) `2 ) by A8;

          s1 = ( |[r2, s2]| `2 ) by A31, A34, EUCLID: 52

          .= s2 by EUCLID: 52;

          then ((G * (1,(j + 1))) `2 ) = s1 by A32, A35, XXREAL_0: 1;

          then ((G * (1,(j + 1))) `2 ) = (p `2 ) by A31, EUCLID: 52;

          hence thesis;

        end;

      end;

      

       A36: { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) } c= ( h_strip (G,j))

      proof

        let x be object;

        assume x in { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) };

        then

        consider p such that

         A37: p = x and

         A38: (p `2 ) = ((G * (1,(j + 1))) `2 );

        

         A39: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

        per cases by NAT_1: 14;

          suppose

           A40: j = 0 ;

          then ( h_strip (G,j)) = { |[r, s]| : s <= ((G * (1,1)) `2 ) } by A1, A4, Th7;

          hence thesis by A37, A38, A39, A40;

        end;

          suppose

           A41: j >= 1;

          then

           A42: ( h_strip (G,j)) = { |[r, s]| : ((G * (1,j)) `2 ) <= s & s <= ((G * (1,(j + 1))) `2 ) } by A1, A4, A5, Th5;

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

          then ((G * (1,j)) `2 ) < (p `2 ) by A2, A3, A4, A38, A41, Th4;

          hence thesis by A37, A38, A39, A42;

        end;

      end;

      { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) } c= ( h_strip (G,(j + 1)))

      proof

        let x be object;

        assume x in { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) };

        then

        consider p such that

         A43: p = x and

         A44: (p `2 ) = ((G * (1,(j + 1))) `2 );

        

         A45: p = |[(p `1 ), (p `2 )]| by EUCLID: 53;

        

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

        per cases by A3, XXREAL_0: 1;

          suppose

           A47: (j + 1) = ( width G);

          then ( h_strip (G,(j + 1))) = { |[r, s]| : ((G * (1,( width G))) `2 ) <= s } by A1, A4, Th6;

          hence thesis by A43, A44, A45, A47;

        end;

          suppose

           A48: (j + 1) < ( width G);

          then

           A49: ( h_strip (G,(j + 1))) = { |[r, s]| : ((G * (1,(j + 1))) `2 ) <= s & s <= ((G * (1,((j + 1) + 1))) `2 ) } by A1, A4, A46, Th5;

          

           A50: (j + 1) < ((j + 1) + 1) by NAT_1: 13;

          ((j + 1) + 1) <= ( width G) by A48, NAT_1: 13;

          then (p `2 ) < ((G * (1,((j + 1) + 1))) `2 ) by A2, A4, A44, A46, A50, Th4;

          hence thesis by A43, A44, A45, A49;

        end;

      end;

      hence thesis by A36, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:25

    

     Th25: for G be Go-board holds i < ( len G) & 1 <= j & j < ( width G) implies (( cell (G,i,j)) /\ ( cell (G,(i + 1),j))) = ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))))

    proof

      let G be Go-board;

      assume that

       A1: i < ( len G) and

       A2: 1 <= j and

       A3: j < ( width G);

      

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

      

       A5: (i + 1) <= ( len G) by A1, NAT_1: 13;

      thus (( cell (G,i,j)) /\ ( cell (G,(i + 1),j))) c= ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))))

      proof

        let x be object;

        

         A6: (( cell (G,i,j)) /\ ( cell (G,(i + 1),j))) = (( v_strip (G,i)) /\ ((( v_strip (G,(i + 1))) /\ ( h_strip (G,j))) /\ ( h_strip (G,j)))) by XBOOLE_1: 16

        .= (( v_strip (G,i)) /\ (( v_strip (G,(i + 1))) /\ (( h_strip (G,j)) /\ ( h_strip (G,j))))) by XBOOLE_1: 16

        .= ((( v_strip (G,i)) /\ ( v_strip (G,(i + 1)))) /\ ( h_strip (G,j))) by XBOOLE_1: 16;

        assume

         A7: x in (( cell (G,i,j)) /\ ( cell (G,(i + 1),j)));

        then

         A8: x in (( v_strip (G,i)) /\ ( v_strip (G,(i + 1)))) by A6, XBOOLE_0:def 4;

        

         A9: x in ( h_strip (G,j)) by A6, A7, XBOOLE_0:def 4;

        

         A10: j < (j + 1) by NAT_1: 13;

        

         A11: (j + 1) <= ( width G) by A3, NAT_1: 13;

        then

         A12: ((G * ((i + 1),j)) `2 ) < ((G * ((i + 1),(j + 1))) `2 ) by A2, A4, A5, A10, Th4;

        

         A13: (G * ((i + 1),j)) = |[((G * ((i + 1),j)) `1 ), ((G * ((i + 1),j)) `2 )]| by EUCLID: 53;

        

         A14: (j + 1) >= 1 by NAT_1: 11;

        ((G * ((i + 1),j)) `1 ) = ((G * ((i + 1),1)) `1 ) by A2, A3, A4, A5, Th2

        .= ((G * ((i + 1),(j + 1))) `1 ) by A4, A5, A11, A14, Th2;

        then

         A15: (G * ((i + 1),(j + 1))) = |[((G * ((i + 1),j)) `1 ), ((G * ((i + 1),(j + 1))) `2 )]| by EUCLID: 53;

        reconsider p = x as Point of ( TOP-REAL 2) by A7;

        (i + 1) <= ( len G) by A1, NAT_1: 13;

        then p in { q : (q `1 ) = ((G * ((i + 1),1)) `1 ) } by A8, Th23;

        then ex q st q = p & (q `1 ) = ((G * ((i + 1),1)) `1 );

        then

         A16: (p `1 ) = ((G * ((i + 1),j)) `1 ) by A2, A3, A4, A5, Th2;

        p in { |[r, s]| : ((G * ((i + 1),j)) `2 ) <= s & s <= ((G * ((i + 1),(j + 1))) `2 ) } by A2, A3, A4, A5, A9, Th5;

        then

         A17: ex r, s st (p = |[r, s]|) & (((G * ((i + 1),j)) `2 ) <= s) & (s <= ((G * ((i + 1),(j + 1))) `2 ));

        then

         A18: ((G * ((i + 1),j)) `2 ) <= (p `2 ) by EUCLID: 52;

        (p `2 ) <= ((G * ((i + 1),(j + 1))) `2 ) by A17, EUCLID: 52;

        then p in { q : (q `1 ) = ((G * ((i + 1),j)) `1 ) & ((G * ((i + 1),j)) `2 ) <= (q `2 ) & (q `2 ) <= ((G * ((i + 1),(j + 1))) `2 ) } by A16, A18;

        hence thesis by A12, A13, A15, TOPREAL3: 9;

      end;

      

       A19: ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) c= ( cell (G,i,j)) by A1, A2, A3, Th18;

      ( LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1))))) c= ( cell (G,(i + 1),j)) by A2, A3, A4, A5, Th19;

      hence thesis by A19, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:26

    

     Th26: for G be Go-board holds j < ( width G) & 1 <= i & i < ( len G) implies (( cell (G,i,j)) /\ ( cell (G,i,(j + 1)))) = ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))))

    proof

      let G be Go-board;

      assume that

       A1: j < ( width G) and

       A2: 1 <= i and

       A3: i < ( len G);

      

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

      

       A5: (j + 1) <= ( width G) by A1, NAT_1: 13;

      thus (( cell (G,i,j)) /\ ( cell (G,i,(j + 1)))) c= ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1)))))

      proof

        let x be object;

        

         A6: (( cell (G,i,j)) /\ ( cell (G,i,(j + 1)))) = (( h_strip (G,j)) /\ ((( h_strip (G,(j + 1))) /\ ( v_strip (G,i))) /\ ( v_strip (G,i)))) by XBOOLE_1: 16

        .= (( h_strip (G,j)) /\ (( h_strip (G,(j + 1))) /\ (( v_strip (G,i)) /\ ( v_strip (G,i))))) by XBOOLE_1: 16

        .= ((( h_strip (G,j)) /\ ( h_strip (G,(j + 1)))) /\ ( v_strip (G,i))) by XBOOLE_1: 16;

        assume

         A7: x in (( cell (G,i,j)) /\ ( cell (G,i,(j + 1))));

        then

         A8: x in (( h_strip (G,j)) /\ ( h_strip (G,(j + 1)))) by A6, XBOOLE_0:def 4;

        

         A9: x in ( v_strip (G,i)) by A6, A7, XBOOLE_0:def 4;

        

         A10: i < (i + 1) by NAT_1: 13;

        

         A11: (i + 1) <= ( len G) by A3, NAT_1: 13;

        then

         A12: ((G * (i,(j + 1))) `1 ) < ((G * ((i + 1),(j + 1))) `1 ) by A2, A4, A5, A10, Th3;

        

         A13: (G * (i,(j + 1))) = |[((G * (i,(j + 1))) `1 ), ((G * (i,(j + 1))) `2 )]| by EUCLID: 53;

        

         A14: (i + 1) >= 1 by NAT_1: 11;

        ((G * (i,(j + 1))) `2 ) = ((G * (1,(j + 1))) `2 ) by A2, A3, A4, A5, Th1

        .= ((G * ((i + 1),(j + 1))) `2 ) by A4, A5, A11, A14, Th1;

        then

         A15: (G * ((i + 1),(j + 1))) = |[((G * ((i + 1),(j + 1))) `1 ), ((G * (i,(j + 1))) `2 )]| by EUCLID: 53;

        reconsider p = x as Point of ( TOP-REAL 2) by A7;

        (j + 1) <= ( width G) by A1, NAT_1: 13;

        then p in { q : (q `2 ) = ((G * (1,(j + 1))) `2 ) } by A8, Th24;

        then ex q st q = p & (q `2 ) = ((G * (1,(j + 1))) `2 );

        then

         A16: (p `2 ) = ((G * (i,(j + 1))) `2 ) by A2, A3, A4, A5, Th1;

        p in { |[r, s]| : ((G * (i,(j + 1))) `1 ) <= r & r <= ((G * ((i + 1),(j + 1))) `1 ) } by A2, A3, A4, A5, A9, Th8;

        then

         A17: ex r, s st (p = |[r, s]|) & (((G * (i,(j + 1))) `1 ) <= r) & (r <= ((G * ((i + 1),(j + 1))) `1 ));

        then

         A18: ((G * (i,(j + 1))) `1 ) <= (p `1 ) by EUCLID: 52;

        (p `1 ) <= ((G * ((i + 1),(j + 1))) `1 ) by A17, EUCLID: 52;

        then p in { q : (q `2 ) = ((G * (i,(j + 1))) `2 ) & ((G * (i,(j + 1))) `1 ) <= (q `1 ) & (q `1 ) <= ((G * ((i + 1),(j + 1))) `1 ) } by A16, A18;

        hence thesis by A12, A13, A15, TOPREAL3: 10;

      end;

      

       A19: ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))) c= ( cell (G,i,j)) by A1, A2, A3, Th21;

      ( LSeg ((G * (i,(j + 1))),(G * ((i + 1),(j + 1))))) c= ( cell (G,i,(j + 1))) by A2, A3, A4, A5, Th22;

      hence thesis by A19, XBOOLE_1: 19;

    end;

    theorem :: GOBOARD5:27

    

     Th27: 1 <= k & (k + 1) <= ( len f) & [(i + 1), j] in ( Indices ( GoB f)) & [(i + 1), (j + 1)] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * ((i + 1),j)) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) implies ( left_cell (f,k)) = ( cell (( GoB f),i,j)) & ( right_cell (f,k)) = ( cell (( GoB f),(i + 1),j))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: [(i + 1), j] in ( Indices ( GoB f)) and

       A4: [(i + 1), (j + 1)] in ( Indices ( GoB f)) and

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

       A6: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1)));

      

       A7: j < (j + 1) by XREAL_1: 29;

      

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

      

      hence ( left_cell (f,k)) = ( cell (( GoB f),((i + 1) -' 1),j)) by A1, A2, A3, A4, A5, A6, A7, Def7

      .= ( cell (( GoB f),i,j)) by NAT_D: 34;

      thus thesis by A1, A2, A3, A4, A5, A6, A7, A8, Def6;

    end;

    theorem :: GOBOARD5:28

    

     Th28: 1 <= k & (k + 1) <= ( len f) & [i, (j + 1)] in ( Indices ( GoB f)) & [(i + 1), (j + 1)] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * (i,(j + 1))) & (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1))) implies ( left_cell (f,k)) = ( cell (( GoB f),i,(j + 1))) & ( right_cell (f,k)) = ( cell (( GoB f),i,j))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: [i, (j + 1)] in ( Indices ( GoB f)) and

       A4: [(i + 1), (j + 1)] in ( Indices ( GoB f)) and

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

       A6: (f /. (k + 1)) = (( GoB f) * ((i + 1),(j + 1)));

      

       A7: i < (i + 1) by XREAL_1: 29;

      

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

      hence ( left_cell (f,k)) = ( cell (( GoB f),i,(j + 1))) by A1, A2, A3, A4, A5, A6, A7, Def7;

      

      thus ( right_cell (f,k)) = ( cell (( GoB f),i,((j + 1) -' 1))) by A1, A2, A3, A4, A5, A6, A7, A8, Def6

      .= ( cell (( GoB f),i,j)) by NAT_D: 34;

    end;

    theorem :: GOBOARD5:29

    

     Th29: 1 <= k & (k + 1) <= ( len f) & [i, (j + 1)] in ( Indices ( GoB f)) & [(i + 1), (j + 1)] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * ((i + 1),(j + 1))) & (f /. (k + 1)) = (( GoB f) * (i,(j + 1))) implies ( left_cell (f,k)) = ( cell (( GoB f),i,j)) & ( right_cell (f,k)) = ( cell (( GoB f),i,(j + 1)))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: [i, (j + 1)] in ( Indices ( GoB f)) and

       A4: [(i + 1), (j + 1)] in ( Indices ( GoB f)) and

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

       A6: (f /. (k + 1)) = (( GoB f) * (i,(j + 1)));

      

       A7: i < (i + 1) by XREAL_1: 29;

      

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

      

      hence ( left_cell (f,k)) = ( cell (( GoB f),i,((j + 1) -' 1))) by A1, A2, A3, A4, A5, A6, A7, Def7

      .= ( cell (( GoB f),i,j)) by NAT_D: 34;

      thus thesis by A1, A2, A3, A4, A5, A6, A7, A8, Def6;

    end;

    theorem :: GOBOARD5:30

    

     Th30: 1 <= k & (k + 1) <= ( len f) & [(i + 1), (j + 1)] in ( Indices ( GoB f)) & [(i + 1), j] in ( Indices ( GoB f)) & (f /. k) = (( GoB f) * ((i + 1),(j + 1))) & (f /. (k + 1)) = (( GoB f) * ((i + 1),j)) implies ( left_cell (f,k)) = ( cell (( GoB f),(i + 1),j)) & ( right_cell (f,k)) = ( cell (( GoB f),i,j))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: [(i + 1), (j + 1)] in ( Indices ( GoB f)) and

       A4: [(i + 1), j] in ( Indices ( GoB f)) and

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

       A6: (f /. (k + 1)) = (( GoB f) * ((i + 1),j));

      

       A7: j < (j + 1) by XREAL_1: 29;

      

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

      hence ( left_cell (f,k)) = ( cell (( GoB f),(i + 1),j)) by A1, A2, A3, A4, A5, A6, A7, Def7;

      

      thus ( right_cell (f,k)) = ( cell (( GoB f),((i + 1) -' 1),j)) by A1, A2, A3, A4, A5, A6, A7, A8, Def6

      .= ( cell (( GoB f),i,j)) by NAT_D: 34;

    end;

    theorem :: GOBOARD5:31

    1 <= k & (k + 1) <= ( len f) implies (( left_cell (f,k)) /\ ( right_cell (f,k))) = ( LSeg (f,k))

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

      

       A6: (k + 1) in ( dom f) by A2, FINSEQ_3: 25, NAT_1: 11;

      then

      consider i2,j2 be Nat such that

       A7: [i2, j2] in ( Indices ( GoB f)) and

       A8: (f /. (k + 1)) = (( GoB f) * (i2,j2)) by Th11;

      

       A9: ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A4, A5, A6, A7, A8, Th12;

       A10:

      now

        per cases by A9, SEQM_3: 42;

          case that

           A11: |.(i1 - i2).| = 1 and

           A12: j1 = j2;

          (i1 - i2) = 1 or ( - (i1 - i2)) = 1 by A11, ABSVALUE:def 1;

          hence i1 = (i2 + 1) or (i1 + 1) = i2;

          thus j1 = j2 by A12;

        end;

          case that

           A13: i1 = i2 and

           A14: |.(j1 - j2).| = 1;

          (j1 - j2) = 1 or ( - (j1 - j2)) = 1 by A14, ABSVALUE:def 1;

          hence j1 = (j2 + 1) or (j1 + 1) = j2;

          thus i1 = i2 by A13;

        end;

      end;

      

       A15: ( 0 + 1) <= j1 by A4, MATRIX_0: 32;

      

       A16: j1 <= ( width ( GoB f)) by A4, MATRIX_0: 32;

      

       A17: 1 <= j2 by A7, MATRIX_0: 32;

      

       A18: j2 <= ( width ( GoB f)) by A7, MATRIX_0: 32;

      

       A19: ( 0 + 1) <= i1 by A4, MATRIX_0: 32;

      

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

      

       A21: 1 <= i2 by A7, MATRIX_0: 32;

      

       A22: i2 <= ( len ( GoB f)) by A7, MATRIX_0: 32;

      i1 > 0 by A19;

      then

      consider i be Nat such that

       A23: (i + 1) = i1 by NAT_1: 6;

      reconsider i as Nat;

      

       A24: (i + 1) = i1 by A23;

      

       A25: i < ( len ( GoB f)) by A20, A23, NAT_1: 13;

      j1 > 0 by A15;

      then

      consider j be Nat such that

       A26: (j + 1) = j1 by NAT_1: 6;

      reconsider j as Nat;

      

       A27: (j + 1) = j1 by A26;

      

       A28: j < ( width ( GoB f)) by A16, A26, NAT_1: 13;

      per cases by A10;

        suppose

         A29: i1 = i2 & (j1 + 1) = j2;

        then

         A30: j1 < ( width ( GoB f)) by A18, NAT_1: 13;

        

         A31: ( left_cell (f,k)) = ( cell (( GoB f),i,j1)) by A1, A2, A4, A5, A7, A8, A23, A29, Th27;

        ( right_cell (f,k)) = ( cell (( GoB f),i1,j1)) by A1, A2, A4, A5, A7, A8, A24, A29, Th27;

        

        hence (( left_cell (f,k)) /\ ( right_cell (f,k))) = ( LSeg ((( GoB f) * (i1,j1)),(( GoB f) * (i1,(j1 + 1))))) by A15, A23, A25, A30, A31, Th25

        .= ( LSeg (f,k)) by A1, A2, A5, A8, A29, TOPREAL1:def 3;

      end;

        suppose

         A32: (i1 + 1) = i2 & j1 = j2;

        then

         A33: i1 < ( len ( GoB f)) by A22, NAT_1: 13;

        

         A34: ( left_cell (f,k)) = ( cell (( GoB f),i1,j1)) by A1, A2, A4, A5, A7, A8, A27, A32, Th28;

        ( right_cell (f,k)) = ( cell (( GoB f),i1,j)) by A1, A2, A4, A5, A7, A8, A26, A32, Th28;

        

        hence (( left_cell (f,k)) /\ ( right_cell (f,k))) = ( LSeg ((( GoB f) * (i1,j1)),(( GoB f) * ((i1 + 1),j1)))) by A19, A26, A28, A33, A34, Th26

        .= ( LSeg (f,k)) by A1, A2, A5, A8, A32, TOPREAL1:def 3;

      end;

        suppose

         A35: i1 = (i2 + 1) & j1 = j2;

        then

         A36: i2 < ( len ( GoB f)) by A20, NAT_1: 13;

        

         A37: ( left_cell (f,k)) = ( cell (( GoB f),i2,j)) by A1, A2, A4, A5, A7, A8, A26, A35, Th29;

        ( right_cell (f,k)) = ( cell (( GoB f),i2,j1)) by A1, A2, A4, A5, A7, A8, A27, A35, Th29;

        

        hence (( left_cell (f,k)) /\ ( right_cell (f,k))) = ( LSeg ((( GoB f) * ((i2 + 1),j1)),(( GoB f) * (i2,j1)))) by A21, A26, A28, A36, A37, Th26

        .= ( LSeg (f,k)) by A1, A2, A5, A8, A35, TOPREAL1:def 3;

      end;

        suppose

         A38: i1 = i2 & j1 = (j2 + 1);

        then

         A39: j2 < ( width ( GoB f)) by A16, NAT_1: 13;

        

         A40: ( left_cell (f,k)) = ( cell (( GoB f),i1,j2)) by A1, A2, A4, A5, A7, A8, A24, A38, Th30;

        ( right_cell (f,k)) = ( cell (( GoB f),i,j2)) by A1, A2, A4, A5, A7, A8, A23, A38, Th30;

        

        hence (( left_cell (f,k)) /\ ( right_cell (f,k))) = ( LSeg ((( GoB f) * (i1,(j2 + 1))),(( GoB f) * (i1,j2)))) by A17, A23, A25, A39, A40, Th25

        .= ( LSeg (f,k)) by A1, A2, A5, A8, A38, TOPREAL1:def 3;

      end;

    end;