gobrd13.miz



    begin

    reserve i,i1,i2,i9,i19,j,j1,j2,j9,j19,k,k1,k2,l,m,n for Nat;

    reserve r,s,r9,s9 for Real;

    reserve D for non empty set,

f for FinSequence of D;

    reserve f for FinSequence of ( TOP-REAL 2),

G for Go-board;

    ::$Canceled

    theorem :: GOBRD13:8

    for G be Matrix of ( TOP-REAL 2) holds f is_sequence_on G implies ( rng f) c= ( Values G)

    proof

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

      assume

       A1: f is_sequence_on G;

      let y be object;

      assume y in ( rng f);

      then

      consider n be Element of NAT such that

       A2: n in ( dom f) and

       A3: (f /. n) = y by PARTFUN2: 2;

      ex i, j st [i, j] in ( Indices G) & (f /. n) = (G * (i,j)) by A1, A2, GOBOARD1:def 9;

      then y in { (G * (i,j)) : [i, j] in ( Indices G) } by A3;

      hence thesis by MATRIX_0: 39;

    end;

    theorem :: GOBRD13:9

    

     Th2: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & 1 <= j2 & j2 <= ( width G2) & (G1 * (i1,j1)) = (G2 * (1,j2)) holds i1 = 1

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: 1 <= j2 & j2 <= ( width G2) and

       A4: (G1 * (i1,j1)) = (G2 * (1,j2));

      set p = (G1 * (1,j1));

      

       A5: 1 <= j1 & j1 <= ( width G1) by A2, MATRIX_0: 32;

      assume

       A6: i1 <> 1;

      1 <= i1 by A2, MATRIX_0: 32;

      then

       A7: 1 < i1 by A6, XXREAL_0: 1;

      i1 <= ( len G1) by A2, MATRIX_0: 32;

      then

       A8: (p `1 ) < ((G1 * (i1,j1)) `1 ) by A5, A7, GOBOARD5: 3;

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

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

      then [1, j1] in ( Indices G1) by A5, MATRIX_0: 30;

      then p in { (G1 * (i,j)) : [i, j] in ( Indices G1) };

      then p in ( Values G1) by MATRIX_0: 39;

      then p in ( Values G2) by A1;

      then p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by MATRIX_0: 39;

      then

      consider i, j such that

       A9: p = (G2 * (i,j)) and

       A10: [i, j] in ( Indices G2);

      

       A11: 1 <= j & j <= ( width G2) by A10, MATRIX_0: 32;

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

      then

       A12: 1 <= ( len G2) by NAT_1: 14;

      

      then

       A13: ((G2 * (1,j)) `1 ) = ((G2 * (1,1)) `1 ) by A11, GOBOARD5: 2

      .= ((G2 * (1,j2)) `1 ) by A3, A12, GOBOARD5: 2;

      

       A14: i <= ( len G2) by A10, MATRIX_0: 32;

      1 <= i by A10, MATRIX_0: 32;

      then 1 < i by A4, A8, A9, A13, XXREAL_0: 1;

      hence contradiction by A4, A8, A9, A14, A11, A13, GOBOARD5: 3;

    end;

    theorem :: GOBRD13:10

    

     Th3: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & 1 <= j2 & j2 <= ( width G2) & (G1 * (i1,j1)) = (G2 * (( len G2),j2)) holds i1 = ( len G1)

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: 1 <= j2 & j2 <= ( width G2) and

       A4: (G1 * (i1,j1)) = (G2 * (( len G2),j2));

      set p = (G1 * (( len G1),j1));

      

       A5: 1 <= j1 & j1 <= ( width G1) by A2, MATRIX_0: 32;

      assume

       A6: i1 <> ( len G1);

      i1 <= ( len G1) by A2, MATRIX_0: 32;

      then

       A7: i1 < ( len G1) by A6, XXREAL_0: 1;

      1 <= i1 by A2, MATRIX_0: 32;

      then

       A8: ((G1 * (i1,j1)) `1 ) < (p `1 ) by A5, A7, GOBOARD5: 3;

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

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

      then [( len G1), j1] in ( Indices G1) by A5, MATRIX_0: 30;

      then p in { (G1 * (i,j)) : [i, j] in ( Indices G1) };

      then p in ( Values G1) by MATRIX_0: 39;

      then p in ( Values G2) by A1;

      then p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by MATRIX_0: 39;

      then

      consider i, j such that

       A9: p = (G2 * (i,j)) and

       A10: [i, j] in ( Indices G2);

      

       A11: 1 <= j & j <= ( width G2) by A10, MATRIX_0: 32;

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

      then

       A12: 1 <= ( len G2) by NAT_1: 14;

      

      then

       A13: ((G2 * (( len G2),j)) `1 ) = ((G2 * (( len G2),1)) `1 ) by A11, GOBOARD5: 2

      .= ((G2 * (( len G2),j2)) `1 ) by A3, A12, GOBOARD5: 2;

      

       A14: 1 <= i by A10, MATRIX_0: 32;

      i <= ( len G2) by A10, MATRIX_0: 32;

      then i < ( len G2) by A4, A8, A9, A13, XXREAL_0: 1;

      hence contradiction by A4, A8, A9, A14, A11, A13, GOBOARD5: 3;

    end;

    theorem :: GOBRD13:11

    

     Th4: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & 1 <= i2 & i2 <= ( len G2) & (G1 * (i1,j1)) = (G2 * (i2,1)) holds j1 = 1

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: 1 <= i2 & i2 <= ( len G2) and

       A4: (G1 * (i1,j1)) = (G2 * (i2,1));

      set p = (G1 * (i1,1));

      

       A5: 1 <= i1 & i1 <= ( len G1) by A2, MATRIX_0: 32;

      assume

       A6: j1 <> 1;

      1 <= j1 by A2, MATRIX_0: 32;

      then

       A7: 1 < j1 by A6, XXREAL_0: 1;

      j1 <= ( width G1) by A2, MATRIX_0: 32;

      then

       A8: (p `2 ) < ((G1 * (i1,j1)) `2 ) by A5, A7, GOBOARD5: 4;

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

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

      then [i1, 1] in ( Indices G1) by A5, MATRIX_0: 30;

      then p in { (G1 * (i,j)) : [i, j] in ( Indices G1) };

      then p in ( Values G1) by MATRIX_0: 39;

      then p in ( Values G2) by A1;

      then p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by MATRIX_0: 39;

      then

      consider i, j such that

       A9: p = (G2 * (i,j)) and

       A10: [i, j] in ( Indices G2);

      

       A11: 1 <= i & i <= ( len G2) by A10, MATRIX_0: 32;

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

      then

       A12: 1 <= ( width G2) by NAT_1: 14;

      

      then

       A13: ((G2 * (i,1)) `2 ) = ((G2 * (1,1)) `2 ) by A11, GOBOARD5: 1

      .= ((G2 * (i2,1)) `2 ) by A3, A12, GOBOARD5: 1;

      

       A14: j <= ( width G2) by A10, MATRIX_0: 32;

      1 <= j by A10, MATRIX_0: 32;

      then 1 < j by A4, A8, A9, A13, XXREAL_0: 1;

      hence contradiction by A4, A8, A9, A11, A14, A13, GOBOARD5: 4;

    end;

    theorem :: GOBRD13:12

    

     Th5: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & 1 <= i2 & i2 <= ( len G2) & (G1 * (i1,j1)) = (G2 * (i2,( width G2))) holds j1 = ( width G1)

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: 1 <= i2 & i2 <= ( len G2) and

       A4: (G1 * (i1,j1)) = (G2 * (i2,( width G2)));

      set p = (G1 * (i1,( width G1)));

      

       A5: 1 <= i1 & i1 <= ( len G1) by A2, MATRIX_0: 32;

      assume

       A6: j1 <> ( width G1);

      j1 <= ( width G1) by A2, MATRIX_0: 32;

      then

       A7: j1 < ( width G1) by A6, XXREAL_0: 1;

      1 <= j1 by A2, MATRIX_0: 32;

      then

       A8: ((G1 * (i1,j1)) `2 ) < (p `2 ) by A5, A7, GOBOARD5: 4;

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

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

      then [i1, ( width G1)] in ( Indices G1) by A5, MATRIX_0: 30;

      then p in { (G1 * (i,j)) : [i, j] in ( Indices G1) };

      then p in ( Values G1) by MATRIX_0: 39;

      then p in ( Values G2) by A1;

      then p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by MATRIX_0: 39;

      then

      consider i, j such that

       A9: p = (G2 * (i,j)) and

       A10: [i, j] in ( Indices G2);

      

       A11: 1 <= i & i <= ( len G2) by A10, MATRIX_0: 32;

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

      then

       A12: 1 <= ( width G2) by NAT_1: 14;

      

      then

       A13: ((G2 * (i,( width G2))) `2 ) = ((G2 * (1,( width G2))) `2 ) by A11, GOBOARD5: 1

      .= ((G2 * (i2,( width G2))) `2 ) by A3, A12, GOBOARD5: 1;

      

       A14: 1 <= j by A10, MATRIX_0: 32;

      j <= ( width G2) by A10, MATRIX_0: 32;

      then j < ( width G2) by A4, A8, A9, A13, XXREAL_0: 1;

      hence contradiction by A4, A8, A9, A11, A14, A13, GOBOARD5: 4;

    end;

    theorem :: GOBRD13:13

    

     Th6: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & 1 <= i1 & i1 < ( len G1) & 1 <= j1 & j1 <= ( width G1) & 1 <= i2 & i2 < ( len G2) & 1 <= j2 & j2 <= ( width G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ((G2 * ((i2 + 1),j2)) `1 ) <= ((G1 * ((i1 + 1),j1)) `1 )

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: 1 <= i1 and

       A3: i1 < ( len G1) and

       A4: 1 <= j1 & j1 <= ( width G1) and

       A5: 1 <= i2 and

       A6: i2 < ( len G2) and

       A7: 1 <= j2 & j2 <= ( width G2) and

       A8: (G1 * (i1,j1)) = (G2 * (i2,j2));

      set p = (G1 * ((i1 + 1),j1));

      

       A9: (i1 + 1) <= ( len G1) by A3, NAT_1: 13;

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

      then [(i1 + 1), j1] in ( Indices G1) by A4, A9, MATRIX_0: 30;

      then p in { (G1 * (i,j)) : [i, j] in ( Indices G1) };

      then p in ( Values G1) by MATRIX_0: 39;

      then p in ( Values G2) by A1;

      then p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by MATRIX_0: 39;

      then

      consider i, j such that

       A10: p = (G2 * (i,j)) and

       A11: [i, j] in ( Indices G2);

      

       A12: 1 <= i by A11, MATRIX_0: 32;

      

       A13: i <= ( len G2) by A11, MATRIX_0: 32;

      1 <= j & j <= ( width G2) by A11, MATRIX_0: 32;

      

      then

       A14: ((G2 * (i,j)) `1 ) = ((G2 * (i,1)) `1 ) by A12, A13, GOBOARD5: 2

      .= ((G2 * (i,j2)) `1 ) by A7, A12, A13, GOBOARD5: 2;

      i1 < (i1 + 1) by NAT_1: 13;

      then

       A15: ((G2 * (i2,j2)) `1 ) < ((G2 * (i,j2)) `1 ) by A2, A4, A8, A9, A10, A14, GOBOARD5: 3;

       A16:

      now

        assume i <= i2;

        then i = i2 or i < i2 by XXREAL_0: 1;

        hence contradiction by A6, A7, A12, A15, GOBOARD5: 3;

      end;

      assume

       A17: (p `1 ) < ((G2 * ((i2 + 1),j2)) `1 );

      

       A18: 1 <= (i2 + 1) by A5, NAT_1: 13;

      now

        assume (i2 + 1) <= i;

        then (i2 + 1) = i or (i2 + 1) < i by XXREAL_0: 1;

        hence contradiction by A7, A17, A10, A13, A14, A18, GOBOARD5: 3;

      end;

      hence contradiction by A16, NAT_1: 13;

    end;

    theorem :: GOBRD13:14

    

     Th7: for G1,G2 be Go-board st (G1 * ((i1 -' 1),j1)) in ( Values G2) & 1 < i1 & i1 <= ( len G1) & 1 <= j1 & j1 <= ( width G1) & 1 < i2 & i2 <= ( len G2) & 1 <= j2 & j2 <= ( width G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ((G1 * ((i1 -' 1),j1)) `1 ) <= ((G2 * ((i2 -' 1),j2)) `1 )

    proof

      let G1,G2 be Go-board such that

       A1: (G1 * ((i1 -' 1),j1)) in ( Values G2) and

       A2: 1 < i1 and

       A3: i1 <= ( len G1) & 1 <= j1 & j1 <= ( width G1) and

       A4: 1 < i2 and

       A5: i2 <= ( len G2) and

       A6: 1 <= j2 & j2 <= ( width G2) and

       A7: (G1 * (i1,j1)) = (G2 * (i2,j2));

      set p = (G1 * ((i1 -' 1),j1));

      

       A8: p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by A1, MATRIX_0: 39;

      1 <= (i2 -' 1) by A4, NAT_D: 49;

      then (i2 -' 1) < i2 by NAT_D: 51;

      then

       A9: (i2 -' 1) < ( len G2) by A5, XXREAL_0: 2;

      consider i, j such that

       A10: p = (G2 * (i,j)) and

       A11: [i, j] in ( Indices G2) by A8;

      

       A12: 1 <= i by A11, MATRIX_0: 32;

      

       A13: i <= ( len G2) by A11, MATRIX_0: 32;

      1 <= j & j <= ( width G2) by A11, MATRIX_0: 32;

      

      then

       A14: ((G2 * (i,j)) `1 ) = ((G2 * (i,1)) `1 ) by A12, A13, GOBOARD5: 2

      .= ((G2 * (i,j2)) `1 ) by A6, A12, A13, GOBOARD5: 2;

      

       A15: 1 <= (i1 -' 1) by A2, NAT_D: 49;

      then (i1 -' 1) < i1 by NAT_D: 51;

      then

       A16: ((G2 * (i,j2)) `1 ) < ((G2 * (i2,j2)) `1 ) by A3, A7, A15, A10, A14, GOBOARD5: 3;

       A17:

      now

        assume i2 <= i;

        then i = i2 or i2 < i by XXREAL_0: 1;

        hence contradiction by A4, A6, A13, A16, GOBOARD5: 3;

      end;

      assume

       A18: ((G2 * ((i2 -' 1),j2)) `1 ) < (p `1 );

      now

        assume i <= (i2 -' 1);

        then (i2 -' 1) = i or i < (i2 -' 1) by XXREAL_0: 1;

        hence contradiction by A6, A18, A10, A12, A14, A9, GOBOARD5: 3;

      end;

      hence contradiction by A17, NAT_D: 49;

    end;

    theorem :: GOBRD13:15

    

     Th8: for G1,G2 be Go-board st (G1 * (i1,(j1 + 1))) in ( Values G2) & 1 <= i1 & i1 <= ( len G1) & 1 <= j1 & j1 < ( width G1) & 1 <= i2 & i2 <= ( len G2) & 1 <= j2 & j2 < ( width G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ((G2 * (i2,(j2 + 1))) `2 ) <= ((G1 * (i1,(j1 + 1))) `2 )

    proof

      let G1,G2 be Go-board such that

       A1: (G1 * (i1,(j1 + 1))) in ( Values G2) and

       A2: 1 <= i1 & i1 <= ( len G1) & 1 <= j1 and

       A3: j1 < ( width G1) and

       A4: 1 <= i2 & i2 <= ( len G2) and

       A5: 1 <= j2 and

       A6: j2 < ( width G2) and

       A7: (G1 * (i1,j1)) = (G2 * (i2,j2));

      set p = (G1 * (i1,(j1 + 1)));

      p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by A1, MATRIX_0: 39;

      then

      consider i, j such that

       A8: p = (G2 * (i,j)) and

       A9: [i, j] in ( Indices G2);

      

       A10: 1 <= j by A9, MATRIX_0: 32;

      

       A11: j <= ( width G2) by A9, MATRIX_0: 32;

      1 <= i & i <= ( len G2) by A9, MATRIX_0: 32;

      

      then

       A12: ((G2 * (i,j)) `2 ) = ((G2 * (1,j)) `2 ) by A10, A11, GOBOARD5: 1

      .= ((G2 * (i2,j)) `2 ) by A4, A10, A11, GOBOARD5: 1;

      j1 < (j1 + 1) & (j1 + 1) <= ( width G1) by A3, NAT_1: 13;

      then

       A13: ((G2 * (i2,j2)) `2 ) < ((G2 * (i2,j)) `2 ) by A2, A7, A8, A12, GOBOARD5: 4;

       A14:

      now

        assume j <= j2;

        then j = j2 or j < j2 by XXREAL_0: 1;

        hence contradiction by A4, A6, A10, A13, GOBOARD5: 4;

      end;

      assume

       A15: (p `2 ) < ((G2 * (i2,(j2 + 1))) `2 );

      

       A16: 1 <= (j2 + 1) by A5, NAT_1: 13;

      now

        assume (j2 + 1) <= j;

        then (j2 + 1) = j or (j2 + 1) < j by XXREAL_0: 1;

        hence contradiction by A4, A15, A8, A11, A12, A16, GOBOARD5: 4;

      end;

      hence contradiction by A14, NAT_1: 13;

    end;

    theorem :: GOBRD13:16

    

     Th9: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & 1 <= i1 & i1 <= ( len G1) & 1 < j1 & j1 <= ( width G1) & 1 <= i2 & i2 <= ( len G2) & 1 < j2 & j2 <= ( width G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ((G1 * (i1,(j1 -' 1))) `2 ) <= ((G2 * (i2,(j2 -' 1))) `2 )

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: 1 <= i1 & i1 <= ( len G1) and

       A3: 1 < j1 and

       A4: j1 <= ( width G1) and

       A5: 1 <= i2 & i2 <= ( len G2) and

       A6: 1 < j2 and

       A7: j2 <= ( width G2) and

       A8: (G1 * (i1,j1)) = (G2 * (i2,j2));

      set p = (G1 * (i1,(j1 -' 1)));

      

       A9: 1 <= (j1 -' 1) by A3, NAT_D: 49;

      then

       A10: (j1 -' 1) < j1 by NAT_D: 51;

      then (j1 -' 1) < ( width G1) by A4, XXREAL_0: 2;

      then [i1, (j1 -' 1)] in ( Indices G1) by A2, A9, MATRIX_0: 30;

      then p in { (G1 * (i,j)) : [i, j] in ( Indices G1) };

      then p in ( Values G1) by MATRIX_0: 39;

      then p in ( Values G2) by A1;

      then p in { (G2 * (i,j)) : [i, j] in ( Indices G2) } by MATRIX_0: 39;

      then

      consider i, j such that

       A11: p = (G2 * (i,j)) and

       A12: [i, j] in ( Indices G2);

      

       A13: 1 <= j by A12, MATRIX_0: 32;

      

       A14: j <= ( width G2) by A12, MATRIX_0: 32;

      1 <= i & i <= ( len G2) by A12, MATRIX_0: 32;

      

      then

       A15: ((G2 * (i,j)) `2 ) = ((G2 * (1,j)) `2 ) by A13, A14, GOBOARD5: 1

      .= ((G2 * (i2,j)) `2 ) by A5, A13, A14, GOBOARD5: 1;

      then

       A16: ((G2 * (i2,j)) `2 ) < ((G2 * (i2,j2)) `2 ) by A2, A4, A8, A9, A10, A11, GOBOARD5: 4;

       A17:

      now

        assume j2 <= j;

        then j = j2 or j2 < j by XXREAL_0: 1;

        hence contradiction by A5, A6, A14, A16, GOBOARD5: 4;

      end;

      1 <= (j2 -' 1) by A6, NAT_D: 49;

      then (j2 -' 1) < j2 by NAT_D: 51;

      then

       A18: (j2 -' 1) < ( width G2) by A7, XXREAL_0: 2;

      assume

       A19: ((G2 * (i2,(j2 -' 1))) `2 ) < (p `2 );

      now

        assume j <= (j2 -' 1);

        then (j2 -' 1) = j or j < (j2 -' 1) by XXREAL_0: 1;

        hence contradiction by A5, A19, A11, A13, A15, A18, GOBOARD5: 4;

      end;

      hence contradiction by A17, NAT_D: 49;

    end;

    theorem :: GOBRD13:17

    

     Th10: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & [i2, j2] in ( Indices G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ( cell (G2,i2,j2)) c= ( cell (G1,i1,j1))

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: [i2, j2] in ( Indices G2) and

       A4: (G1 * (i1,j1)) = (G2 * (i2,j2));

      

       A5: 1 <= i1 by A2, MATRIX_0: 32;

      

       A6: j1 <= ( width G1) by A2, MATRIX_0: 32;

      let p be object such that

       A7: p in ( cell (G2,i2,j2));

      

       A8: 1 <= i2 by A3, MATRIX_0: 32;

      

       A9: j2 <= ( width G2) by A3, MATRIX_0: 32;

      

       A10: 1 <= j2 by A3, MATRIX_0: 32;

      

       A11: i2 <= ( len G2) by A3, MATRIX_0: 32;

      then

       A12: ((G2 * (i2,j2)) `1 ) = ((G2 * (i2,1)) `1 ) & ((G2 * (i2,j2)) `2 ) = ((G2 * (1,j2)) `2 ) by A8, A10, A9, GOBOARD5: 1, GOBOARD5: 2;

      

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

      

       A14: i1 <= ( len G1) by A2, MATRIX_0: 32;

      then

       A15: ((G1 * (i1,j1)) `1 ) = ((G1 * (i1,1)) `1 ) & ((G1 * (i1,j1)) `2 ) = ((G1 * (1,j1)) `2 ) by A5, A13, A6, GOBOARD5: 1, GOBOARD5: 2;

      per cases by A11, A9, XXREAL_0: 1;

        suppose

         A16: i2 = ( len G2) & j2 = ( width G2);

        then

         A17: p in { |[r, s]| : ((G2 * (i2,j2)) `1 ) <= r & ((G2 * (i2,j2)) `2 ) <= s } by A7, A12, GOBRD11: 28;

        i1 = ( len G1) & j1 = ( width G1) by A1, A2, A4, A8, A10, A16, Th3, Th5;

        hence thesis by A4, A15, A17, GOBRD11: 28;

      end;

        suppose

         A18: i2 = ( len G2) & j2 < ( width G2);

        then p in { |[r, s]| : ((G2 * (i2,j2)) `1 ) <= r & ((G2 * (i2,j2)) `2 ) <= s & s <= ((G2 * (1,(j2 + 1))) `2 ) } by A7, A10, A12, GOBRD11: 29;

        then

        consider r9, s9 such that

         A19: p = |[r9, s9]| & ((G2 * (i2,j2)) `1 ) <= r9 & ((G2 * (i2,j2)) `2 ) <= s9 and

         A20: s9 <= ((G2 * (1,(j2 + 1))) `2 );

        

         A21: i1 = ( len G1) by A1, A2, A4, A10, A18, Th3;

        now

          per cases by A6, XXREAL_0: 1;

            suppose

             A22: j1 = ( width G1);

            p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & ((G1 * (i1,j1)) `2 ) <= s } by A4, A19;

            hence thesis by A15, A21, A22, GOBRD11: 28;

          end;

            suppose

             A23: j1 < ( width G1);

            1 <= (j2 + 1) & (j2 + 1) <= ( width G2) by A18, NAT_1: 12, NAT_1: 13;

            then

             A24: ((G2 * (i2,(j2 + 1))) `2 ) = ((G2 * (1,(j2 + 1))) `2 ) by A8, A11, GOBOARD5: 1;

            1 <= (j1 + 1) & (j1 + 1) <= ( width G1) by A23, NAT_1: 12, NAT_1: 13;

            then (G1 * (i1,(j1 + 1))) in ( Values G1) & ((G1 * (i1,(j1 + 1))) `2 ) = ((G1 * (1,(j1 + 1))) `2 ) by A5, A14, GOBOARD5: 1, MATRIX_0: 41;

            then ((G2 * (1,(j2 + 1))) `2 ) <= ((G1 * (1,(j1 + 1))) `2 ) by A1, A4, A5, A14, A13, A8, A10, A18, A23, A24, Th8;

            then s9 <= ((G1 * (1,(j1 + 1))) `2 ) by A20, XXREAL_0: 2;

            then p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & ((G1 * (i1,j1)) `2 ) <= s & s <= ((G1 * (1,(j1 + 1))) `2 ) } by A4, A19;

            hence thesis by A13, A15, A21, A23, GOBRD11: 29;

          end;

        end;

        hence thesis;

      end;

        suppose

         A25: i2 < ( len G2) & j2 = ( width G2);

        then p in { |[r, s]| : ((G2 * (i2,j2)) `1 ) <= r & r <= ((G2 * ((i2 + 1),1)) `1 ) & ((G2 * (i2,j2)) `2 ) <= s } by A7, A8, A12, GOBRD11: 31;

        then

        consider r9, s9 such that

         A26: p = |[r9, s9]| & ((G2 * (i2,j2)) `1 ) <= r9 and

         A27: r9 <= ((G2 * ((i2 + 1),1)) `1 ) and

         A28: ((G2 * (i2,j2)) `2 ) <= s9;

        

         A29: j1 = ( width G1) by A1, A2, A4, A8, A25, Th5;

        now

          per cases by A14, XXREAL_0: 1;

            suppose

             A30: i1 = ( len G1);

            p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & ((G1 * (i1,j1)) `2 ) <= s } by A4, A26, A28;

            hence thesis by A15, A29, A30, GOBRD11: 28;

          end;

            suppose

             A31: i1 < ( len G1);

            1 <= (i2 + 1) & (i2 + 1) <= ( len G2) by A25, NAT_1: 12, NAT_1: 13;

            then

             A32: ((G2 * ((i2 + 1),j2)) `1 ) = ((G2 * ((i2 + 1),1)) `1 ) by A10, A9, GOBOARD5: 2;

            1 <= (i1 + 1) & (i1 + 1) <= ( len G1) by A31, NAT_1: 12, NAT_1: 13;

            then ((G1 * ((i1 + 1),j1)) `1 ) = ((G1 * ((i1 + 1),1)) `1 ) by A13, A6, GOBOARD5: 2;

            then ((G2 * ((i2 + 1),1)) `1 ) <= ((G1 * ((i1 + 1),1)) `1 ) by A1, A4, A5, A13, A6, A8, A10, A25, A31, A32, Th6;

            then r9 <= ((G1 * ((i1 + 1),1)) `1 ) by A27, XXREAL_0: 2;

            then p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & r <= ((G1 * ((i1 + 1),1)) `1 ) & ((G1 * (i1,j1)) `2 ) <= s } by A4, A26, A28;

            hence thesis by A5, A15, A29, A31, GOBRD11: 31;

          end;

        end;

        hence thesis;

      end;

        suppose

         A33: i2 < ( len G2) & j2 < ( width G2);

        then 1 <= (j2 + 1) & (j2 + 1) <= ( width G2) by NAT_1: 12, NAT_1: 13;

        then

         A34: ((G2 * (i2,(j2 + 1))) `2 ) = ((G2 * (1,(j2 + 1))) `2 ) by A8, A11, GOBOARD5: 1;

        1 <= (i2 + 1) & (i2 + 1) <= ( len G2) by A33, NAT_1: 12, NAT_1: 13;

        then ((G2 * ((i2 + 1),j2)) `1 ) = ((G2 * ((i2 + 1),1)) `1 ) by A10, A9, GOBOARD5: 2;

        then p in { |[r, s]| : ((G2 * (i2,j2)) `1 ) <= r & r <= ((G2 * ((i2 + 1),j2)) `1 ) & ((G2 * (i2,j2)) `2 ) <= s & s <= ((G2 * (i2,(j2 + 1))) `2 ) } by A7, A8, A10, A12, A33, A34, GOBRD11: 32;

        then

        consider r9, s9 such that

         A35: p = |[r9, s9]| & ((G2 * (i2,j2)) `1 ) <= r9 and

         A36: r9 <= ((G2 * ((i2 + 1),j2)) `1 ) and

         A37: ((G2 * (i2,j2)) `2 ) <= s9 and

         A38: s9 <= ((G2 * (i2,(j2 + 1))) `2 );

        now

          per cases by A14, A6, XXREAL_0: 1;

            suppose

             A39: i1 = ( len G1) & j1 = ( width G1);

            p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & ((G1 * (i1,j1)) `2 ) <= s } by A4, A35, A37;

            hence thesis by A15, A39, GOBRD11: 28;

          end;

            suppose

             A40: i1 = ( len G1) & j1 < ( width G1);

            then 1 <= (j1 + 1) & (j1 + 1) <= ( width G1) by NAT_1: 12, NAT_1: 13;

            then (G1 * (i1,(j1 + 1))) in ( Values G1) & ((G1 * (i1,(j1 + 1))) `2 ) = ((G1 * (1,(j1 + 1))) `2 ) by A5, A14, GOBOARD5: 1, MATRIX_0: 41;

            then ((G2 * (i2,(j2 + 1))) `2 ) <= ((G1 * (1,(j1 + 1))) `2 ) by A1, A4, A5, A13, A8, A10, A33, A40, Th8;

            then s9 <= ((G1 * (1,(j1 + 1))) `2 ) by A38, XXREAL_0: 2;

            then p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & ((G1 * (i1,j1)) `2 ) <= s & s <= ((G1 * (1,(j1 + 1))) `2 ) } by A4, A35, A37;

            hence thesis by A13, A15, A40, GOBRD11: 29;

          end;

            suppose

             A41: i1 < ( len G1) & j1 = ( width G1);

            then 1 <= (i1 + 1) & (i1 + 1) <= ( len G1) by NAT_1: 12, NAT_1: 13;

            then ((G1 * ((i1 + 1),j1)) `1 ) = ((G1 * ((i1 + 1),1)) `1 ) by A13, A6, GOBOARD5: 2;

            then ((G2 * ((i2 + 1),j2)) `1 ) <= ((G1 * ((i1 + 1),1)) `1 ) by A1, A4, A5, A13, A8, A10, A33, A41, Th6;

            then r9 <= ((G1 * ((i1 + 1),1)) `1 ) by A36, XXREAL_0: 2;

            then p in { |[r, s]| : ((G1 * (i1,j1)) `1 ) <= r & r <= ((G1 * ((i1 + 1),1)) `1 ) & ((G1 * (i1,j1)) `2 ) <= s } by A4, A35, A37;

            hence thesis by A5, A15, A41, GOBRD11: 31;

          end;

            suppose

             A42: i1 < ( len G1) & j1 < ( width G1);

            then 1 <= (i1 + 1) & (i1 + 1) <= ( len G1) by NAT_1: 12, NAT_1: 13;

            then ((G1 * ((i1 + 1),j1)) `1 ) = ((G1 * ((i1 + 1),1)) `1 ) by A13, A6, GOBOARD5: 2;

            then ((G2 * ((i2 + 1),j2)) `1 ) <= ((G1 * ((i1 + 1),1)) `1 ) by A1, A4, A5, A13, A8, A10, A33, A42, Th6;

            then

             A43: r9 <= ((G1 * ((i1 + 1),1)) `1 ) by A36, XXREAL_0: 2;

            1 <= (j1 + 1) & (j1 + 1) <= ( width G1) by A42, NAT_1: 12, NAT_1: 13;

            then (G1 * (i1,(j1 + 1))) in ( Values G1) & ((G1 * (i1,(j1 + 1))) `2 ) = ((G1 * (1,(j1 + 1))) `2 ) by A5, A14, GOBOARD5: 1, MATRIX_0: 41;

            then ((G2 * (i2,(j2 + 1))) `2 ) <= ((G1 * (1,(j1 + 1))) `2 ) by A1, A4, A5, A13, A8, A10, A33, A42, Th8;

            then s9 <= ((G1 * (1,(j1 + 1))) `2 ) by A38, XXREAL_0: 2;

            then p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & r <= ((G1 * ((i1 + 1),1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s & s <= ((G1 * (1,(j1 + 1))) `2 ) } by A4, A15, A35, A37, A43;

            hence thesis by A5, A13, A42, GOBRD11: 32;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: GOBRD13:18

    

     Th11: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & [i2, j2] in ( Indices G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ( cell (G2,(i2 -' 1),j2)) c= ( cell (G1,(i1 -' 1),j1))

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: [i2, j2] in ( Indices G2) and

       A4: (G1 * (i1,j1)) = (G2 * (i2,j2));

      

       A5: i2 <= ( len G2) by A3, MATRIX_0: 32;

      

       A6: j1 <= ( width G1) by A2, MATRIX_0: 32;

      

       A7: 1 <= j1 by A2, MATRIX_0: 32;

      

       A8: j2 <= ( width G2) by A3, MATRIX_0: 32;

      

       A9: 1 <= j2 by A3, MATRIX_0: 32;

      

       A10: 1 <= i2 by A3, MATRIX_0: 32;

      then

       A11: ((G2 * (i2,j2)) `1 ) = ((G2 * (i2,1)) `1 ) by A5, A9, A8, GOBOARD5: 2;

      

       A12: ((G2 * (i2,j2)) `2 ) = ((G2 * (1,j2)) `2 ) by A10, A5, A9, A8, GOBOARD5: 1;

      let p be object such that

       A13: p in ( cell (G2,(i2 -' 1),j2));

      

       A14: 1 <= i1 by A2, MATRIX_0: 32;

      

       A15: i1 <= ( len G1) by A2, MATRIX_0: 32;

      per cases by A14, A10, XXREAL_0: 1;

        suppose

         A16: i1 = 1 & i2 = 1;

        then

         A17: (i1 -' 1) = 0 by XREAL_1: 232;

        

         A18: (i2 -' 1) = 0 by A16, XREAL_1: 232;

        now

          per cases by A8, XXREAL_0: 1;

            suppose

             A19: j2 = ( width G2);

            then

             A20: j1 = ( width G1) by A1, A2, A4, A10, A5, Th5;

            p in { |[r, s]| : r <= ((G2 * (1,1)) `1 ) & ((G2 * (1,( width G2))) `2 ) <= s } by A13, A18, A19, GOBRD11: 25;

            then

            consider r9, s9 such that

             A21: p = |[r9, s9]| and

             A22: r9 <= ((G2 * (1,1)) `1 ) and

             A23: ((G2 * (1,( width G2))) `2 ) <= s9;

            ((G2 * (1,1)) `1 ) = ((G2 * (i1,j2)) `1 ) by A5, A9, A8, A16, GOBOARD5: 2;

            then r9 <= ((G1 * (1,1)) `1 ) by A4, A15, A7, A6, A16, A22, GOBOARD5: 2;

            then p in { |[r, s]| : r <= ((G1 * (1,1)) `1 ) & ((G1 * (1,( width G1))) `2 ) <= s } by A4, A16, A19, A21, A23, A20;

            hence thesis by A17, A20, GOBRD11: 25;

          end;

            suppose

             A24: j2 < ( width G2);

            then p in { |[r, s]| : r <= ((G2 * (1,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s & s <= ((G2 * (1,(j2 + 1))) `2 ) } by A13, A9, A18, GOBRD11: 26;

            then

            consider r9, s9 such that

             A25: p = |[r9, s9]| and

             A26: r9 <= ((G2 * (1,1)) `1 ) and

             A27: ((G2 * (1,j2)) `2 ) <= s9 and

             A28: s9 <= ((G2 * (1,(j2 + 1))) `2 );

            ((G2 * (1,1)) `1 ) = ((G2 * (i1,j2)) `1 ) by A5, A9, A8, A16, GOBOARD5: 2;

            then

             A29: r9 <= ((G1 * (1,1)) `1 ) by A4, A15, A7, A6, A16, A26, GOBOARD5: 2;

            now

              per cases by A6, XXREAL_0: 1;

                suppose

                 A30: j1 = ( width G1);

                then p in { |[r, s]| : r <= ((G1 * (1,1)) `1 ) & ((G1 * (1,( width G1))) `2 ) <= s } by A4, A16, A25, A27, A29;

                hence thesis by A17, A30, GOBRD11: 25;

              end;

                suppose

                 A31: j1 < ( width G1);

                then 1 <= (j1 + 1) & (j1 + 1) <= ( width G1) by NAT_1: 11, NAT_1: 13;

                then (G1 * (i1,(j1 + 1))) in ( Values G1) by A14, A15, MATRIX_0: 41;

                then ((G2 * (1,(j2 + 1))) `2 ) <= ((G1 * (1,(j1 + 1))) `2 ) by A1, A4, A15, A7, A5, A9, A16, A24, A31, Th8;

                then s9 <= ((G1 * (1,(j1 + 1))) `2 ) by A28, XXREAL_0: 2;

                then p in { |[r, s]| : r <= ((G1 * (1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s & s <= ((G1 * (1,(j1 + 1))) `2 ) } by A4, A16, A25, A27, A29;

                hence thesis by A7, A17, A31, GOBRD11: 26;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A32: i1 = 1 and

         A33: 1 < i2;

        

         A34: (i1 -' 1) = 0 by A32, XREAL_1: 232;

        

         A35: 1 <= (i2 -' 1) by A33, NAT_D: 49;

        then (i2 -' 1) < i2 by NAT_D: 51;

        then

         A36: (i2 -' 1) < ( len G2) by A5, XXREAL_0: 2;

        

         A37: ((i2 -' 1) + 1) = i2 by A33, XREAL_1: 235;

        now

          per cases by A8, XXREAL_0: 1;

            suppose

             A38: j2 = ( width G2);

            then p in { |[r, s]| : ((G2 * ((i2 -' 1),1)) `1 ) <= r & r <= ((G2 * (i2,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s } by A13, A35, A36, A37, GOBRD11: 31;

            then

            consider r9, s9 such that

             A39: p = |[r9, s9]| and ((G2 * ((i2 -' 1),1)) `1 ) <= r9 and

             A40: r9 <= ((G2 * (i2,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s9;

            r9 <= ((G1 * (1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s9 by A4, A15, A7, A6, A11, A12, A32, A40, GOBOARD5: 2;

            then

             A41: p in { |[r, s]| : r <= ((G1 * (1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s } by A39;

            j1 = ( width G1) by A1, A2, A4, A10, A5, A38, Th5;

            hence thesis by A34, A41, GOBRD11: 25;

          end;

            suppose

             A42: j2 < ( width G2);

            then p in { |[r, s]| : ((G2 * ((i2 -' 1),1)) `1 ) <= r & r <= ((G2 * (i2,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s & s <= ((G2 * (1,(j2 + 1))) `2 ) } by A13, A9, A35, A36, A37, GOBRD11: 32;

            then

            consider r9, s9 such that

             A43: p = |[r9, s9]| and ((G2 * ((i2 -' 1),1)) `1 ) <= r9 and

             A44: r9 <= ((G2 * (i2,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s9 and

             A45: s9 <= ((G2 * (1,(j2 + 1))) `2 );

            

             A46: r9 <= ((G1 * (1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s9 by A4, A15, A7, A6, A11, A12, A32, A44, GOBOARD5: 2;

            now

              per cases by A6, XXREAL_0: 1;

                suppose

                 A47: j1 = ( width G1);

                then p in { |[r, s]| : r <= ((G1 * (1,1)) `1 ) & ((G1 * (1,( width G1))) `2 ) <= s } by A43, A46;

                hence thesis by A34, A47, GOBRD11: 25;

              end;

                suppose

                 A48: j1 < ( width G1);

                1 <= (j2 + 1) & (j2 + 1) <= ( width G2) by A42, NAT_1: 12, NAT_1: 13;

                then

                 A49: ((G2 * (i2,(j2 + 1))) `2 ) = ((G2 * (1,(j2 + 1))) `2 ) by A10, A5, GOBOARD5: 1;

                1 <= (j1 + 1) & (j1 + 1) <= ( width G1) by A48, NAT_1: 12, NAT_1: 13;

                then (G1 * (i1,(j1 + 1))) in ( Values G1) & ((G1 * (i1,(j1 + 1))) `2 ) = ((G1 * (1,(j1 + 1))) `2 ) by A14, A15, GOBOARD5: 1, MATRIX_0: 41;

                then ((G2 * (1,(j2 + 1))) `2 ) <= ((G1 * (1,(j1 + 1))) `2 ) by A1, A4, A14, A15, A7, A10, A5, A9, A42, A48, A49, Th8;

                then s9 <= ((G1 * (1,(j1 + 1))) `2 ) by A45, XXREAL_0: 2;

                then p in { |[r, s]| : r <= ((G1 * (1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s & s <= ((G1 * (1,(j1 + 1))) `2 ) } by A43, A46;

                hence thesis by A7, A34, A48, GOBRD11: 26;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose 1 < i1 & i2 = 1;

        hence thesis by A1, A2, A4, A9, A8, Th2;

      end;

        suppose

         A50: 1 < i1 & 1 < i2;

        then

         A51: 1 <= (i2 -' 1) by NAT_D: 49;

        then

         A52: ((i2 -' 1) + 1) = i2 by NAT_D: 43;

        (i2 -' 1) < i2 by A51, NAT_D: 51;

        then

         A53: (i2 -' 1) < ( len G2) by A5, XXREAL_0: 2;

        then

         A54: ((G2 * ((i2 -' 1),1)) `1 ) = ((G2 * ((i2 -' 1),j2)) `1 ) by A9, A8, A51, GOBOARD5: 2;

        

         A55: 1 <= (i1 -' 1) by A50, NAT_D: 49;

        then

         A56: ((i1 -' 1) + 1) = i1 by NAT_D: 43;

        (i1 -' 1) < i1 by A55, NAT_D: 51;

        then

         A57: (i1 -' 1) < ( len G1) by A15, XXREAL_0: 2;

        then (G1 * ((i1 -' 1),j1)) in ( Values G1) & ((G1 * ((i1 -' 1),1)) `1 ) = ((G1 * ((i1 -' 1),j1)) `1 ) by A7, A6, A55, GOBOARD5: 2, MATRIX_0: 41;

        then

         A58: ((G1 * ((i1 -' 1),1)) `1 ) <= ((G2 * ((i2 -' 1),1)) `1 ) by A1, A4, A15, A7, A6, A5, A9, A8, A50, A54, Th7;

        now

          per cases by A8, XXREAL_0: 1;

            suppose

             A59: j2 = ( width G2);

            then p in { |[r, s]| : ((G2 * ((i2 -' 1),1)) `1 ) <= r & r <= ((G2 * (i2,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s } by A13, A51, A53, A52, GOBRD11: 31;

            then

            consider r9, s9 such that

             A60: p = |[r9, s9]| and

             A61: ((G2 * ((i2 -' 1),1)) `1 ) <= r9 & r9 <= ((G2 * (i2,1)) `1 ) and

             A62: ((G2 * (1,j2)) `2 ) <= s9;

            

             A63: ((G1 * (1,j1)) `2 ) <= s9 by A4, A14, A15, A7, A6, A12, A62, GOBOARD5: 1;

            ((G1 * ((i1 -' 1),1)) `1 ) <= r9 & r9 <= ((G1 * (i1,1)) `1 ) by A4, A14, A15, A7, A6, A11, A58, A61, GOBOARD5: 2, XXREAL_0: 2;

            then

             A64: p in { |[r, s]| : ((G1 * ((i1 -' 1),1)) `1 ) <= r & r <= ((G1 * (i1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s } by A60, A63;

            j1 = ( width G1) by A1, A2, A4, A10, A5, A59, Th5;

            hence thesis by A55, A57, A56, A64, GOBRD11: 31;

          end;

            suppose

             A65: j2 < ( width G2);

            then p in { |[r, s]| : ((G2 * ((i2 -' 1),1)) `1 ) <= r & r <= ((G2 * (i2,1)) `1 ) & ((G2 * (1,j2)) `2 ) <= s & s <= ((G2 * (1,(j2 + 1))) `2 ) } by A13, A9, A51, A53, A52, GOBRD11: 32;

            then

            consider r9, s9 such that

             A66: p = |[r9, s9]| and

             A67: ((G2 * ((i2 -' 1),1)) `1 ) <= r9 & r9 <= ((G2 * (i2,1)) `1 ) and

             A68: ((G2 * (1,j2)) `2 ) <= s9 and

             A69: s9 <= ((G2 * (1,(j2 + 1))) `2 );

            

             A70: ((G1 * (1,j1)) `2 ) <= s9 by A4, A14, A15, A7, A6, A12, A68, GOBOARD5: 1;

            

             A71: ((G1 * ((i1 -' 1),1)) `1 ) <= r9 & r9 <= ((G1 * (i1,1)) `1 ) by A4, A14, A15, A7, A6, A11, A58, A67, GOBOARD5: 2, XXREAL_0: 2;

            per cases by A6, XXREAL_0: 1;

              suppose

               A72: j1 = ( width G1);

              p in { |[r, s]| : ((G1 * ((i1 -' 1),1)) `1 ) <= r & r <= ((G1 * (i1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s } by A66, A71, A70;

              hence thesis by A55, A57, A56, A72, GOBRD11: 31;

            end;

              suppose

               A73: j1 < ( width G1);

              1 <= (j2 + 1) & (j2 + 1) <= ( width G2) by A65, NAT_1: 12, NAT_1: 13;

              then

               A74: ((G2 * (i2,(j2 + 1))) `2 ) = ((G2 * (1,(j2 + 1))) `2 ) by A10, A5, GOBOARD5: 1;

              1 <= (j1 + 1) & (j1 + 1) <= ( width G1) by A73, NAT_1: 12, NAT_1: 13;

              then (G1 * (i1,(j1 + 1))) in ( Values G1) & ((G1 * (i1,(j1 + 1))) `2 ) = ((G1 * (1,(j1 + 1))) `2 ) by A14, A15, GOBOARD5: 1, MATRIX_0: 41;

              then ((G2 * (1,(j2 + 1))) `2 ) <= ((G1 * (1,(j1 + 1))) `2 ) by A1, A4, A14, A15, A7, A10, A5, A9, A65, A73, A74, Th8;

              then s9 <= ((G1 * (1,(j1 + 1))) `2 ) by A69, XXREAL_0: 2;

              then p in { |[r, s]| : ((G1 * ((i1 -' 1),1)) `1 ) <= r & r <= ((G1 * (i1,1)) `1 ) & ((G1 * (1,j1)) `2 ) <= s & s <= ((G1 * (1,(j1 + 1))) `2 ) } by A66, A71, A70;

              hence thesis by A7, A55, A57, A56, A73, GOBRD11: 32;

            end;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: GOBRD13:19

    

     Th12: for G1,G2 be Go-board st ( Values G1) c= ( Values G2) & [i1, j1] in ( Indices G1) & [i2, j2] in ( Indices G2) & (G1 * (i1,j1)) = (G2 * (i2,j2)) holds ( cell (G2,i2,(j2 -' 1))) c= ( cell (G1,i1,(j1 -' 1)))

    proof

      let G1,G2 be Go-board such that

       A1: ( Values G1) c= ( Values G2) and

       A2: [i1, j1] in ( Indices G1) and

       A3: [i2, j2] in ( Indices G2) and

       A4: (G1 * (i1,j1)) = (G2 * (i2,j2));

      

       A5: 1 <= i1 by A2, MATRIX_0: 32;

      

       A6: 1 <= j2 by A3, MATRIX_0: 32;

      

       A7: 1 <= i2 by A3, MATRIX_0: 32;

      

       A8: j1 <= ( width G1) by A2, MATRIX_0: 32;

      

       A9: j2 <= ( width G2) by A3, MATRIX_0: 32;

      

       A10: i2 <= ( len G2) by A3, MATRIX_0: 32;

      then

       A11: ((G2 * (i2,j2)) `1 ) = ((G2 * (i2,1)) `1 ) by A7, A6, A9, GOBOARD5: 2;

      

       A12: i1 <= ( len G1) by A2, MATRIX_0: 32;

      

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

      then

       A14: ((G1 * (i1,j1)) `2 ) = ((G1 * (1,j1)) `2 ) by A5, A12, A8, GOBOARD5: 1;

      let p be object such that

       A15: p in ( cell (G2,i2,(j2 -' 1)));

      

       A16: ((G2 * (i2,j2)) `2 ) = ((G2 * (1,j2)) `2 ) by A7, A10, A6, A9, GOBOARD5: 1;

      per cases by A13, A6, XXREAL_0: 1;

        suppose

         A17: j1 = 1 & j2 = 1;

        then

         A18: (j1 -' 1) = 0 by XREAL_1: 232;

        

         A19: (j2 -' 1) = 0 by A17, XREAL_1: 232;

        now

          per cases by A10, XXREAL_0: 1;

            suppose

             A20: i2 = ( len G2);

            then p in { |[r, s]| : ((G2 * (( len G2),1)) `1 ) <= r & s <= ((G2 * (1,1)) `2 ) } by A15, A19, GOBRD11: 27;

            then

            consider r9, s9 such that

             A21: p = |[r9, s9]| & ((G2 * (( len G2),1)) `1 ) <= r9 and

             A22: s9 <= ((G2 * (1,1)) `2 );

            

             A23: i1 = ( len G1) by A1, A2, A4, A6, A9, A20, Th3;

            ((G2 * (1,1)) `2 ) = ((G2 * (i2,j2)) `2 ) by A7, A10, A9, A17, GOBOARD5: 1;

            then s9 <= ((G1 * (1,1)) `2 ) by A4, A5, A12, A8, A17, A22, GOBOARD5: 1;

            then p in { |[r, s]| : ((G1 * (( len G1),1)) `1 ) <= r & s <= ((G1 * (1,1)) `2 ) } by A4, A17, A20, A21, A23;

            hence thesis by A18, A23, GOBRD11: 27;

          end;

            suppose

             A24: i2 < ( len G2);

            then p in { |[r, s]| : ((G2 * (i2,1)) `1 ) <= r & r <= ((G2 * ((i2 + 1),1)) `1 ) & s <= ((G2 * (1,1)) `2 ) } by A15, A7, A19, GOBRD11: 30;

            then

            consider r9, s9 such that

             A25: p = |[r9, s9]| & ((G2 * (i2,1)) `1 ) <= r9 and

             A26: r9 <= ((G2 * ((i2 + 1),1)) `1 ) and

             A27: s9 <= ((G2 * (1,1)) `2 );

            ((G2 * (1,1)) `2 ) = ((G2 * (i2,j1)) `2 ) by A7, A10, A9, A17, GOBOARD5: 1;

            then

             A28: s9 <= ((G1 * (1,1)) `2 ) by A4, A5, A12, A8, A17, A27, GOBOARD5: 1;

            now

              per cases by A12, XXREAL_0: 1;

                suppose

                 A29: i1 = ( len G1);

                then p in { |[r, s]| : ((G1 * (( len G1),1)) `1 ) <= r & s <= ((G1 * (1,1)) `2 ) } by A4, A17, A25, A28;

                hence thesis by A18, A29, GOBRD11: 27;

              end;

                suppose

                 A30: i1 < ( len G1);

                then ((G2 * ((i2 + 1),1)) `1 ) <= ((G1 * ((i1 + 1),1)) `1 ) by A1, A4, A5, A8, A7, A9, A17, A24, Th6;

                then r9 <= ((G1 * ((i1 + 1),1)) `1 ) by A26, XXREAL_0: 2;

                then p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & r <= ((G1 * ((i1 + 1),1)) `1 ) & s <= ((G1 * (1,1)) `2 ) } by A4, A17, A25, A28;

                hence thesis by A5, A18, A30, GOBRD11: 30;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose that

         A31: j1 = 1 and

         A32: 1 < j2;

        

         A33: (j1 -' 1) = 0 by A31, XREAL_1: 232;

        

         A34: 1 <= (j2 -' 1) by A32, NAT_D: 49;

        then (j2 -' 1) < j2 by NAT_D: 51;

        then

         A35: (j2 -' 1) < ( width G2) by A9, XXREAL_0: 2;

        

         A36: ((j2 -' 1) + 1) = j2 by A32, XREAL_1: 235;

        now

          per cases by A10, XXREAL_0: 1;

            suppose

             A37: i2 = ( len G2);

            then p in { |[r, s]| : ((G2 * (i2,1)) `1 ) <= r & ((G2 * (1,(j2 -' 1))) `2 ) <= s & s <= ((G2 * (1,j2)) `2 ) } by A15, A34, A35, A36, GOBRD11: 29;

            then ex r9, s9 st p = |[r9, s9]| & ((G2 * (i2,1)) `1 ) <= r9 & ((G2 * (1,(j2 -' 1))) `2 ) <= s9 & s9 <= ((G2 * (1,j2)) `2 );

            then

             A38: p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & s <= ((G1 * (1,1)) `2 ) } by A4, A14, A11, A16, A31;

            i1 = ( len G1) by A1, A2, A4, A6, A9, A37, Th3;

            hence thesis by A33, A38, GOBRD11: 27;

          end;

            suppose

             A39: i2 < ( len G2);

            then p in { |[r, s]| : ((G2 * (i2,1)) `1 ) <= r & r <= ((G2 * ((i2 + 1),1)) `1 ) & ((G2 * (1,(j2 -' 1))) `2 ) <= s & s <= ((G2 * (1,j2)) `2 ) } by A15, A7, A34, A35, A36, GOBRD11: 32;

            then

            consider r9, s9 such that

             A40: p = |[r9, s9]| and

             A41: ((G2 * (i2,1)) `1 ) <= r9 and

             A42: r9 <= ((G2 * ((i2 + 1),1)) `1 ) and ((G2 * (1,(j2 -' 1))) `2 ) <= s9 and

             A43: s9 <= ((G2 * (1,j2)) `2 );

            

             A44: s9 <= ((G1 * (1,1)) `2 ) & ((G1 * (i1,1)) `1 ) <= r9 by A4, A7, A10, A6, A9, A14, A31, A41, A43, GOBOARD5: 1, GOBOARD5: 2;

            now

              per cases by A12, XXREAL_0: 1;

                suppose

                 A45: i1 = ( len G1);

                then p in { |[r, s]| : ((G1 * (( len G1),1)) `1 ) <= r & s <= ((G1 * (1,1)) `2 ) } by A40, A44;

                hence thesis by A33, A45, GOBRD11: 27;

              end;

                suppose

                 A46: i1 < ( len G1);

                1 <= (i2 + 1) & (i2 + 1) <= ( len G2) by A39, NAT_1: 12, NAT_1: 13;

                then

                 A47: ((G2 * ((i2 + 1),j2)) `1 ) = ((G2 * ((i2 + 1),1)) `1 ) by A6, A9, GOBOARD5: 2;

                1 <= (i1 + 1) & (i1 + 1) <= ( len G1) by A46, NAT_1: 12, NAT_1: 13;

                then ((G1 * ((i1 + 1),j1)) `1 ) = ((G1 * ((i1 + 1),1)) `1 ) by A13, A8, GOBOARD5: 2;

                then ((G2 * ((i2 + 1),1)) `1 ) <= ((G1 * ((i1 + 1),1)) `1 ) by A1, A4, A5, A13, A8, A7, A6, A9, A39, A46, A47, Th6;

                then r9 <= ((G1 * ((i1 + 1),1)) `1 ) by A42, XXREAL_0: 2;

                then p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & r <= ((G1 * ((i1 + 1),1)) `1 ) & s <= ((G1 * (1,1)) `2 ) } by A40, A44;

                hence thesis by A5, A33, A46, GOBRD11: 30;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose 1 < j1 & j2 = 1;

        hence thesis by A1, A2, A4, A7, A10, Th4;

      end;

        suppose

         A48: 1 < j1 & 1 < j2;

        then

         A49: 1 <= (j2 -' 1) by NAT_D: 49;

        then

         A50: ((j2 -' 1) + 1) = j2 by NAT_D: 43;

        (j2 -' 1) < j2 by A49, NAT_D: 51;

        then

         A51: (j2 -' 1) < ( width G2) by A9, XXREAL_0: 2;

        then

         A52: ((G2 * (1,(j2 -' 1))) `2 ) = ((G2 * (i2,(j2 -' 1))) `2 ) by A7, A10, A49, GOBOARD5: 1;

        

         A53: 1 <= (j1 -' 1) by A48, NAT_D: 49;

        then

         A54: ((j1 -' 1) + 1) = j1 by NAT_D: 43;

        (j1 -' 1) < j1 by A53, NAT_D: 51;

        then

         A55: (j1 -' 1) < ( width G1) by A8, XXREAL_0: 2;

        then ((G1 * (1,(j1 -' 1))) `2 ) = ((G1 * (i1,(j1 -' 1))) `2 ) by A5, A12, A53, GOBOARD5: 1;

        then

         A56: ((G1 * (1,(j1 -' 1))) `2 ) <= ((G2 * (1,(j2 -' 1))) `2 ) by A1, A4, A5, A12, A8, A7, A10, A9, A48, A52, Th9;

        now

          per cases by A10, XXREAL_0: 1;

            suppose

             A57: i2 = ( len G2);

            then p in { |[r, s]| : ((G2 * (i2,1)) `1 ) <= r & ((G2 * (1,(j2 -' 1))) `2 ) <= s & s <= ((G2 * (1,j2)) `2 ) } by A15, A49, A51, A50, GOBRD11: 29;

            then

            consider r9, s9 such that

             A58: p = |[r9, s9]| and

             A59: ((G2 * (i2,1)) `1 ) <= r9 and

             A60: ((G2 * (1,(j2 -' 1))) `2 ) <= s9 & s9 <= ((G2 * (1,j2)) `2 );

            

             A61: ((G1 * (i1,1)) `1 ) <= r9 by A4, A5, A12, A13, A8, A11, A59, GOBOARD5: 2;

            ((G1 * (1,(j1 -' 1))) `2 ) <= s9 & s9 <= ((G1 * (1,j1)) `2 ) by A4, A5, A12, A13, A8, A16, A56, A60, GOBOARD5: 1, XXREAL_0: 2;

            then

             A62: p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & ((G1 * (1,(j1 -' 1))) `2 ) <= s & s <= ((G1 * (1,j1)) `2 ) } by A58, A61;

            i1 = ( len G1) by A1, A2, A4, A6, A9, A57, Th3;

            hence thesis by A53, A55, A54, A62, GOBRD11: 29;

          end;

            suppose

             A63: i2 < ( len G2);

            then p in { |[r, s]| : ((G2 * (i2,1)) `1 ) <= r & r <= ((G2 * ((i2 + 1),1)) `1 ) & ((G2 * (1,(j2 -' 1))) `2 ) <= s & s <= ((G2 * (1,j2)) `2 ) } by A15, A7, A49, A51, A50, GOBRD11: 32;

            then

            consider r9, s9 such that

             A64: p = |[r9, s9]| and

             A65: ((G2 * (i2,1)) `1 ) <= r9 and

             A66: r9 <= ((G2 * ((i2 + 1),1)) `1 ) and

             A67: ((G2 * (1,(j2 -' 1))) `2 ) <= s9 & s9 <= ((G2 * (1,j2)) `2 );

            

             A68: ((G1 * (i1,1)) `1 ) <= r9 by A4, A5, A12, A13, A8, A11, A65, GOBOARD5: 2;

            

             A69: ((G1 * (1,(j1 -' 1))) `2 ) <= s9 & s9 <= ((G1 * (1,j1)) `2 ) by A4, A5, A12, A13, A8, A16, A56, A67, GOBOARD5: 1, XXREAL_0: 2;

            now

              per cases by A12, XXREAL_0: 1;

                suppose

                 A70: i1 = ( len G1);

                p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & ((G1 * (1,(j1 -' 1))) `2 ) <= s & s <= ((G1 * (1,j1)) `2 ) } by A64, A69, A68;

                hence thesis by A53, A55, A54, A70, GOBRD11: 29;

              end;

                suppose

                 A71: i1 < ( len G1);

                1 <= (i2 + 1) & (i2 + 1) <= ( len G2) by A63, NAT_1: 12, NAT_1: 13;

                then

                 A72: ((G2 * ((i2 + 1),j2)) `1 ) = ((G2 * ((i2 + 1),1)) `1 ) by A6, A9, GOBOARD5: 2;

                1 <= (i1 + 1) & (i1 + 1) <= ( len G1) by A71, NAT_1: 12, NAT_1: 13;

                then ((G1 * ((i1 + 1),j1)) `1 ) = ((G1 * ((i1 + 1),1)) `1 ) by A13, A8, GOBOARD5: 2;

                then ((G2 * ((i2 + 1),1)) `1 ) <= ((G1 * ((i1 + 1),1)) `1 ) by A1, A4, A5, A13, A8, A7, A6, A9, A63, A71, A72, Th6;

                then r9 <= ((G1 * ((i1 + 1),1)) `1 ) by A66, XXREAL_0: 2;

                then p in { |[r, s]| : ((G1 * (i1,1)) `1 ) <= r & r <= ((G1 * ((i1 + 1),1)) `1 ) & ((G1 * (1,(j1 -' 1))) `2 ) <= s & s <= ((G1 * (1,j1)) `2 ) } by A64, A69, A68;

                hence thesis by A5, A53, A55, A54, A71, GOBRD11: 32;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end;

    

     Lm1: for f be non empty FinSequence of ( TOP-REAL 2) st 1 <= i & i <= ( len ( GoB f)) & 1 <= j & j <= ( width ( GoB f)) holds ex k st k in ( dom f) & ((f /. k) `1 ) = ((( GoB f) * (i,j)) `1 )

    proof

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

      assume that

       A1: 1 <= i & i <= ( len ( GoB f)) and

       A2: 1 <= j & j <= ( width ( GoB f));

      

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

      then ( len ( Incr ( X_axis f))) = ( len ( GoB f)) by GOBOARD2:def 1;

      then i in ( dom ( Incr ( X_axis f))) by A1, FINSEQ_3: 25;

      then (( Incr ( X_axis f)) . i) in ( rng ( Incr ( X_axis f))) by FUNCT_1:def 3;

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

      then

      consider k be Nat such that

       A4: k in ( dom ( X_axis f)) and

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

       [i, j] in ( Indices ( GoB f)) by A1, A2, MATRIX_0: 30;

      then

       A6: (( GoB f) * (i,j)) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A3, GOBOARD2:def 1;

      reconsider k as Nat;

      take k;

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

      hence k in ( dom f) by A4, FINSEQ_3: 29;

      

      thus ((f /. k) `1 ) = (( Incr ( X_axis f)) . i) by A4, A5, GOBOARD1:def 1

      .= ((( GoB f) * (i,j)) `1 ) by A6, EUCLID: 52;

    end;

    

     Lm2: for f be non empty FinSequence of ( TOP-REAL 2) st 1 <= i & i <= ( len ( GoB f)) & 1 <= j & j <= ( width ( GoB f)) holds ex k st k in ( dom f) & ((f /. k) `2 ) = ((( GoB f) * (i,j)) `2 )

    proof

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

      assume that

       A1: 1 <= i & i <= ( len ( GoB f)) and

       A2: 1 <= j & j <= ( width ( GoB f));

      

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

      then ( len ( Incr ( Y_axis f))) = ( width ( GoB f)) by GOBOARD2:def 1;

      then j in ( dom ( Incr ( Y_axis f))) by A2, FINSEQ_3: 25;

      then (( Incr ( Y_axis f)) . j) in ( rng ( Incr ( Y_axis f))) by FUNCT_1:def 3;

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

      then

      consider k be Nat such that

       A4: k in ( dom ( Y_axis f)) and

       A5: (( Y_axis f) . k) = (( Incr ( Y_axis f)) . j) by FINSEQ_2: 10;

       [i, j] in ( Indices ( GoB f)) by A1, A2, MATRIX_0: 30;

      then

       A6: (( GoB f) * (i,j)) = |[(( Incr ( X_axis f)) . i), (( Incr ( Y_axis f)) . j)]| by A3, GOBOARD2:def 1;

      reconsider k as Nat;

      take k;

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

      hence k in ( dom f) by A4, FINSEQ_3: 29;

      

      thus ((f /. k) `2 ) = (( Incr ( Y_axis f)) . j) by A4, A5, GOBOARD1:def 2

      .= ((( GoB f) * (i,j)) `2 ) by A6, EUCLID: 52;

    end;

    theorem :: GOBRD13:20

    

     Th13: for f be standard special_circular_sequence st f is_sequence_on G holds ( Values ( GoB f)) c= ( Values G)

    proof

      let f be standard special_circular_sequence such that

       A1: f is_sequence_on G;

      let p be object;

      set F = ( GoB f);

      assume p in ( Values F);

      then p in { (F * (i,j)) : [i, j] in ( Indices F) } by MATRIX_0: 39;

      then

      consider i, j such that

       A2: p = (F * (i,j)) and

       A3: [i, j] in ( Indices F);

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

      

       A4: 1 <= j & j <= ( width F) by A3, MATRIX_0: 32;

      

       A5: 1 <= i & i <= ( len F) by A3, MATRIX_0: 32;

      then

      consider k1 such that

       A6: k1 in ( dom f) and

       A7: (p `1 ) = ((f /. k1) `1 ) by A2, A4, Lm1;

      consider k2 such that

       A8: k2 in ( dom f) and

       A9: (p `2 ) = ((f /. k2) `2 ) by A2, A5, A4, Lm2;

      consider i2, j2 such that

       A10: [i2, j2] in ( Indices G) and

       A11: (f /. k2) = (G * (i2,j2)) by A1, A8, GOBOARD1:def 9;

      

       A12: 1 <= i2 & i2 <= ( len G) by A10, MATRIX_0: 32;

      consider i1, j1 such that

       A13: [i1, j1] in ( Indices G) and

       A14: (f /. k1) = (G * (i1,j1)) by A1, A6, GOBOARD1:def 9;

      

       A15: 1 <= j1 & j1 <= ( width G) by A13, MATRIX_0: 32;

      

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

      

       A17: 1 <= j2 & j2 <= ( width G) by A10, MATRIX_0: 32;

      

       A18: 1 <= i1 & i1 <= ( len G) by A13, MATRIX_0: 32;

      then

       A19: [i1, j2] in ( Indices G) by A17, MATRIX_0: 30;

      

       A20: ((G * (i1,j2)) `2 ) = ((G * (1,j2)) `2 ) by A18, A17, GOBOARD5: 1

      .= ((G * (i2,j2)) `2 ) by A12, A17, GOBOARD5: 1;

      ((G * (i1,j2)) `1 ) = ((G * (i1,1)) `1 ) by A18, A17, GOBOARD5: 2

      .= ((G * (i1,j1)) `1 ) by A18, A15, GOBOARD5: 2;

      then p = (G * (i1,j2)) by A7, A9, A14, A11, A20, A16, EUCLID: 53;

      then p in { (G * (k,l)) : [k, l] in ( Indices G) } by A19;

      hence thesis by MATRIX_0: 39;

    end;

    definition

      ::$Canceled

      let f, G, k;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G;

      then

      consider i1,j1,i2,j2 be Nat such that

       A1: [i1, j1] in ( Indices G) & (f /. k) = (G * (i1,j1)) and

       A2: [i2, j2] in ( Indices G) & (f /. (k + 1)) = (G * (i2,j2)) and

       A3: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by JORDAN8: 3;

      :: GOBRD13:def2

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

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

      existence

      proof

        per cases by A3;

          suppose

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

          take ( cell (G,i1,j1));

          let i19,j19,i29,j29 be Nat;

          assume that

           A5: [i19, j19] in ( Indices G) and

           A6: [i29, j29] in ( Indices G) and

           A7: (f /. k) = (G * (i19,j19)) and

           A8: (f /. (k + 1)) = (G * (i29,j29));

          i1 = i19 & j1 = j19 by A1, A5, A7, GOBOARD1: 5;

          hence thesis by A2, A4, A6, A8, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i1,(j1 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume that

           A10: [i19, j19] in ( Indices G) and

           A11: [i29, j29] in ( Indices G) and

           A12: (f /. k) = (G * (i19,j19)) and

           A13: (f /. (k + 1)) = (G * (i29,j29));

          i1 = i19 & j1 = j19 by A1, A10, A12, GOBOARD1: 5;

          hence thesis by A2, A9, A11, A13, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i2,j2));

          let i19,j19,i29,j29 be Nat;

          assume

           A15: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, A2, GOBOARD1: 5;

          hence thesis by A1, A2, A14, A15, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,(i1 -' 1),j2));

          let i19,j19,i29,j29 be Nat;

          assume that

           A17: [i19, j19] in ( Indices G) and

           A18: [i29, j29] in ( Indices G) and

           A19: (f /. k) = (G * (i19,j19)) and

           A20: (f /. (k + 1)) = (G * (i29,j29));

          i1 = i19 & j1 = j19 by A1, A17, A19, GOBOARD1: 5;

          hence thesis by A2, A16, A18, A20, GOBOARD1: 5;

        end;

      end;

      uniqueness

      proof

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

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

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

        per cases by A3;

          suppose

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

          

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

          

           A25: j1 < j2 by A23, XREAL_1: 29;

          

          hence P1 = ( cell (G,i1,j1)) by A1, A2, A21, A24

          .= P2 by A1, A2, A22, A25, A24;

        end;

          suppose

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

          

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

          

           A28: i1 < i2 by A26, XREAL_1: 29;

          

          hence P1 = ( cell (G,i1,(j1 -' 1))) by A1, A2, A21, A27

          .= P2 by A1, A2, A22, A28, A27;

        end;

          suppose

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

          

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

          

           A31: i2 < i1 by A29, XREAL_1: 29;

          

          hence P1 = ( cell (G,i2,j2)) by A1, A2, A21, A30

          .= P2 by A1, A2, A22, A31, A30;

        end;

          suppose

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

          

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

          

           A34: j2 < j1 by A32, XREAL_1: 29;

          

          hence P1 = ( cell (G,(i1 -' 1),j2)) by A1, A2, A21, A33

          .= P2 by A1, A2, A22, A34, A33;

        end;

      end;

      :: GOBRD13:def3

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

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

      existence

      proof

        per cases by A3;

          suppose

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

          take ( cell (G,(i1 -' 1),j1));

          let i19,j19,i29,j29 be Nat;

          assume that

           A36: [i19, j19] in ( Indices G) and

           A37: [i29, j29] in ( Indices G) and

           A38: (f /. k) = (G * (i19,j19)) and

           A39: (f /. (k + 1)) = (G * (i29,j29));

          i1 = i19 & j1 = j19 by A1, A36, A38, GOBOARD1: 5;

          hence thesis by A2, A35, A37, A39, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i1,j1));

          let i19,j19,i29,j29 be Nat;

          assume that

           A41: [i19, j19] in ( Indices G) and

           A42: [i29, j29] in ( Indices G) and

           A43: (f /. k) = (G * (i19,j19)) and

           A44: (f /. (k + 1)) = (G * (i29,j29));

          i1 = i19 & j1 = j19 by A1, A41, A43, GOBOARD1: 5;

          hence thesis by A2, A40, A42, A44, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i2,(j2 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume

           A46: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, A2, GOBOARD1: 5;

          hence thesis by A1, A2, A45, A46, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i1,j2));

          let i19,j19,i29,j29 be Nat;

          assume that

           A48: [i19, j19] in ( Indices G) and

           A49: [i29, j29] in ( Indices G) and

           A50: (f /. k) = (G * (i19,j19)) and

           A51: (f /. (k + 1)) = (G * (i29,j29));

          i1 = i19 & j1 = j19 by A1, A48, A50, GOBOARD1: 5;

          hence thesis by A2, A47, A49, A51, GOBOARD1: 5;

        end;

      end;

      uniqueness

      proof

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

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

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

        per cases by A3;

          suppose

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

          

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

          

           A56: j1 < j2 by A54, XREAL_1: 29;

          

          hence P1 = ( cell (G,(i1 -' 1),j1)) by A1, A2, A52, A55

          .= P2 by A1, A2, A53, A56, A55;

        end;

          suppose

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

          

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

          

           A59: i1 < i2 by A57, XREAL_1: 29;

          

          hence P1 = ( cell (G,i1,j1)) by A1, A2, A52, A58

          .= P2 by A1, A2, A53, A59, A58;

        end;

          suppose

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

          

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

          

           A62: i2 < i1 by A60, XREAL_1: 29;

          

          hence P1 = ( cell (G,i2,(j2 -' 1))) by A1, A2, A52, A61

          .= P2 by A1, A2, A53, A62, A61;

        end;

          suppose

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

          

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

          

           A65: j2 < j1 by A63, XREAL_1: 29;

          

          hence P1 = ( cell (G,i1,j2)) by A1, A2, A52, A64

          .= P2 by A1, A2, A53, A65, A64;

        end;

      end;

    end

    theorem :: GOBRD13:21

    

     Th14: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1))) implies ( left_cell (f,k,G)) = ( cell (G,(i -' 1),j))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1)));

      hence thesis by A1, Def2;

    end;

    theorem :: GOBRD13:22

    

     Th15: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1))) implies ( right_cell (f,k,G)) = ( cell (G,i,j))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1)));

      hence thesis by A1, Def1;

    end;

    theorem :: GOBRD13:23

    

     Th16: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j)) implies ( left_cell (f,k,G)) = ( cell (G,i,j))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j));

      hence thesis by A1, Def2;

    end;

    theorem :: GOBRD13:24

    

     Th17: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j)) implies ( right_cell (f,k,G)) = ( cell (G,i,(j -' 1)))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j));

      hence thesis by A1, Def1;

    end;

    theorem :: GOBRD13:25

    

     Th18: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j)) implies ( left_cell (f,k,G)) = ( cell (G,i,(j -' 1)))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def2;

    end;

    theorem :: GOBRD13:26

    

     Th19: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j)) implies ( right_cell (f,k,G)) = ( cell (G,i,j))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def1;

    end;

    theorem :: GOBRD13:27

    

     Th20: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j)) implies ( left_cell (f,k,G)) = ( cell (G,i,j))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def2;

    end;

    theorem :: GOBRD13:28

    

     Th21: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j)) implies ( right_cell (f,k,G)) = ( cell (G,(i -' 1),j))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def1;

    end;

    theorem :: GOBRD13:29

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G implies (( left_cell (f,k,G)) /\ ( right_cell (f,k,G))) = ( LSeg (f,k))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: f is_sequence_on G;

      (k + 1) >= 1 by NAT_1: 11;

      then

       A4: (k + 1) in ( dom f) by A2, FINSEQ_3: 25;

      then

      consider i2,j2 be Nat such that

       A5: [i2, j2] in ( Indices G) and

       A6: (f /. (k + 1)) = (G * (i2,j2)) by A3, GOBOARD1:def 9;

      

       A7: 1 <= j2 by A5, MATRIX_0: 32;

      

       A8: i2 <= ( len G) by A5, MATRIX_0: 32;

      

       A9: 1 <= i2 by A5, MATRIX_0: 32;

      

       A10: j2 <= ( width G) by A5, MATRIX_0: 32;

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

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

      then

       A11: k in ( dom f) by A1, FINSEQ_3: 25;

      then

      consider i1,j1 be Nat such that

       A12: [i1, j1] in ( Indices G) and

       A13: (f /. k) = (G * (i1,j1)) by A3, GOBOARD1:def 9;

      

       A14: ( 0 + 1) <= j1 by A12, MATRIX_0: 32;

      then j1 > 0 ;

      then

      consider j be Nat such that

       A15: (j + 1) = j1 by NAT_1: 6;

      

       A16: ( |.(i1 - i2).| + |.(j1 - j2).|) = 1 by A3, A11, A12, A13, A4, A5, A6, GOBOARD1:def 9;

       A17:

      now

        per cases by A16, SEQM_3: 42;

          case that

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

           A19: j1 = j2;

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

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

          thus j1 = j2 by A19;

        end;

          case that

           A20: i1 = i2 and

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

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

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

          thus i1 = i2 by A20;

        end;

      end;

      

       A22: (j1 -' 1) = j by A15, NAT_D: 34;

      

       A23: j1 <= ( width G) by A12, MATRIX_0: 32;

      then

       A24: j < ( width G) by A15, NAT_1: 13;

      

       A25: ( 0 + 1) <= i1 by A12, MATRIX_0: 32;

      then i1 > 0 ;

      then

      consider i be Nat such that

       A26: (i + 1) = i1 by NAT_1: 6;

      

       A27: i1 <= ( len G) by A12, MATRIX_0: 32;

      then

       A28: i < ( len G) by A26, NAT_1: 13;

      

       A29: (i1 -' 1) = i by A26, NAT_D: 34;

      reconsider i, j as Nat;

      per cases by A17;

        suppose

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

        then

         A31: ( right_cell (f,k,G)) = ( cell (G,i1,j1)) by A1, A2, A3, A12, A13, A5, A6, Th15;

        j1 < ( width G) & ( left_cell (f,k,G)) = ( cell (G,i,j1)) by A1, A2, A3, A12, A13, A5, A6, A10, A29, A30, Th14, NAT_1: 13;

        

        hence (( left_cell (f,k,G)) /\ ( right_cell (f,k,G))) = ( LSeg ((G * (i1,j1)),(G * (i1,(j1 + 1))))) by A14, A26, A28, A31, GOBOARD5: 25

        .= ( LSeg (f,k)) by A1, A2, A13, A6, A30, TOPREAL1:def 3;

      end;

        suppose

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

        then

         A33: ( right_cell (f,k,G)) = ( cell (G,i1,j)) by A1, A2, A3, A12, A13, A5, A6, A22, Th17;

        i1 < ( len G) & ( left_cell (f,k,G)) = ( cell (G,i1,j1)) by A1, A2, A3, A12, A13, A5, A6, A8, A32, Th16, NAT_1: 13;

        

        hence (( left_cell (f,k,G)) /\ ( right_cell (f,k,G))) = ( LSeg ((G * (i1,j1)),(G * ((i1 + 1),j1)))) by A25, A15, A24, A33, GOBOARD5: 26

        .= ( LSeg (f,k)) by A1, A2, A13, A6, A32, TOPREAL1:def 3;

      end;

        suppose

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

        then

         A35: ( right_cell (f,k,G)) = ( cell (G,i2,j1)) by A1, A2, A3, A12, A13, A5, A6, Th19;

        i2 < ( len G) & ( left_cell (f,k,G)) = ( cell (G,i2,j)) by A1, A2, A3, A12, A13, A5, A6, A27, A22, A34, Th18, NAT_1: 13;

        

        hence (( left_cell (f,k,G)) /\ ( right_cell (f,k,G))) = ( LSeg ((G * ((i2 + 1),j1)),(G * (i2,j1)))) by A9, A15, A24, A35, GOBOARD5: 26

        .= ( LSeg (f,k)) by A1, A2, A13, A6, A34, TOPREAL1:def 3;

      end;

        suppose

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

        then

         A37: ( right_cell (f,k,G)) = ( cell (G,i,j2)) by A1, A2, A3, A12, A13, A5, A6, A29, Th21;

        j2 < ( width G) & ( left_cell (f,k,G)) = ( cell (G,i1,j2)) by A1, A2, A3, A12, A13, A5, A6, A23, A36, Th20, NAT_1: 13;

        

        hence (( left_cell (f,k,G)) /\ ( right_cell (f,k,G))) = ( LSeg ((G * (i1,(j2 + 1))),(G * (i1,j2)))) by A7, A26, A28, A37, GOBOARD5: 25

        .= ( LSeg (f,k)) by A1, A2, A13, A6, A36, TOPREAL1:def 3;

      end;

    end;

    theorem :: GOBRD13:30

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G implies ( right_cell (f,k,G)) is closed

    proof

      assume

       A1: 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G;

      then

      consider i1,j1,i2,j2 be Nat such that

       A2: [i1, j1] in ( Indices G) & (f /. k) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f /. (k + 1)) = (G * (i2,j2)) & (i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1)) by JORDAN8: 3;

      i1 = i2 & (j1 + 1) = j2 & ( right_cell (f,k,G)) = ( cell (G,i1,j1)) or (i1 + 1) = i2 & j1 = j2 & ( right_cell (f,k,G)) = ( cell (G,i1,(j1 -' 1))) or i1 = (i2 + 1) & j1 = j2 & ( right_cell (f,k,G)) = ( cell (G,i2,j2)) or i1 = i2 & j1 = (j2 + 1) & ( right_cell (f,k,G)) = ( cell (G,(i1 -' 1),j2)) by A1, A2, Def1;

      hence thesis by GOBRD11: 33;

    end;

    theorem :: GOBRD13:31

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & (k + 1) <= n implies ( left_cell (f,k,G)) = ( left_cell ((f | n),k,G)) & ( right_cell (f,k,G)) = ( right_cell ((f | n),k,G))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: f is_sequence_on G and

       A4: (k + 1) <= n;

      per cases ;

        suppose ( len f) <= n;

        hence thesis by FINSEQ_1: 58;

      end;

        suppose n < ( len f);

        then

         A5: ( len (f | n)) = n by FINSEQ_1: 59;

        then k in ( dom (f | n)) by A1, A4, SEQ_4: 134;

        then

         A6: ((f | n) /. k) = (f /. k) by FINSEQ_4: 70;

        (k + 1) in ( dom (f | n)) by A1, A4, A5, SEQ_4: 134;

        then

         A7: ((f | n) /. (k + 1)) = (f /. (k + 1)) by FINSEQ_4: 70;

        set lf = ( left_cell (f,k,G)), lfn = ( left_cell ((f | n),k,G)), rf = ( right_cell (f,k,G)), rfn = ( right_cell ((f | n),k,G));

        

         A8: (f | n) is_sequence_on G by A3, GOBOARD1: 22;

        consider i1,j1,i2,j2 be Nat such that

         A9: [i1, j1] in ( Indices G) & (f /. k) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f /. (k + 1)) = (G * (i2,j2)) and

         A10: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A2, A3, JORDAN8: 3;

        

         A11: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

        

         A12: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

        now

          per cases by A10;

            suppose

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

            

            hence lf = ( cell (G,(i1 -' 1),j1)) by A1, A2, A3, A9, A11, Def2

            .= lfn by A1, A4, A9, A11, A8, A5, A6, A7, A13, Def2;

            

            thus rf = ( cell (G,i1,j1)) by A1, A2, A3, A9, A11, A13, Def1

            .= rfn by A1, A4, A9, A11, A8, A5, A6, A7, A13, Def1;

          end;

            suppose

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

            

            hence lf = ( cell (G,i1,j1)) by A1, A2, A3, A9, A12, Def2

            .= lfn by A1, A4, A9, A12, A8, A5, A6, A7, A14, Def2;

            

            thus rf = ( cell (G,i1,(j1 -' 1))) by A1, A2, A3, A9, A12, A14, Def1

            .= rfn by A1, A4, A9, A12, A8, A5, A6, A7, A14, Def1;

          end;

            suppose

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

            

            hence lf = ( cell (G,i2,(j2 -' 1))) by A1, A2, A3, A9, A12, Def2

            .= lfn by A1, A4, A9, A12, A8, A5, A6, A7, A15, Def2;

            

            thus rf = ( cell (G,i2,j2)) by A1, A2, A3, A9, A12, A15, Def1

            .= rfn by A1, A4, A9, A12, A8, A5, A6, A7, A15, Def1;

          end;

            suppose

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

            

            hence lf = ( cell (G,i1,j2)) by A1, A2, A3, A9, A11, Def2

            .= lfn by A1, A4, A9, A11, A8, A5, A6, A7, A16, Def2;

            

            thus rf = ( cell (G,(i1 -' 1),j2)) by A1, A2, A3, A9, A11, A16, Def1

            .= rfn by A1, A4, A9, A11, A8, A5, A6, A7, A16, Def1;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: GOBRD13:32

    1 <= k & (k + 1) <= ( len (f /^ n)) & n <= ( len f) & f is_sequence_on G implies ( left_cell (f,(k + n),G)) = ( left_cell ((f /^ n),k,G)) & ( right_cell (f,(k + n),G)) = ( right_cell ((f /^ n),k,G))

    proof

      set g = (f /^ n);

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len g) and

       A3: n <= ( len f) and

       A4: f is_sequence_on G;

      

       A5: ( len g) = (( len f) - n) & ((k + 1) + n) <= (( len g) + n) by A2, A3, RFINSEQ:def 1, XREAL_1: 6;

      k in ( dom g) by A1, A2, SEQ_4: 134;

      then

       A6: (g /. k) = (f /. (k + n)) by FINSEQ_5: 27;

      set lf = ( left_cell (f,(k + n),G)), lfn = ( left_cell (g,k,G)), rf = ( right_cell (f,(k + n),G)), rfn = ( right_cell (g,k,G));

      

       A7: ((k + 1) + n) = ((k + n) + 1) & 1 <= (k + n) by A1, NAT_1: 12;

      (k + 1) in ( dom g) by A1, A2, SEQ_4: 134;

      then

       A8: (g /. (k + 1)) = (f /. ((k + 1) + n)) by FINSEQ_5: 27;

      

       A9: g is_sequence_on G by A4, JORDAN8: 2;

      then

      consider i1,j1,i2,j2 be Nat such that

       A10: [i1, j1] in ( Indices G) & (g /. k) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (g /. (k + 1)) = (G * (i2,j2)) and

       A11: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A2, JORDAN8: 3;

      

       A12: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

      

       A13: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

      now

        per cases by A11;

          suppose

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

          

          hence lf = ( cell (G,(i1 -' 1),j1)) by A4, A10, A12, A6, A8, A5, A7, Def2

          .= lfn by A1, A2, A9, A10, A12, A14, Def2;

          

          thus rf = ( cell (G,i1,j1)) by A4, A10, A12, A6, A8, A5, A7, A14, Def1

          .= rfn by A1, A2, A9, A10, A12, A14, Def1;

        end;

          suppose

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

          

          hence lf = ( cell (G,i1,j1)) by A4, A10, A13, A6, A8, A5, A7, Def2

          .= lfn by A1, A2, A9, A10, A13, A15, Def2;

          

          thus rf = ( cell (G,i1,(j1 -' 1))) by A4, A10, A13, A6, A8, A5, A7, A15, Def1

          .= rfn by A1, A2, A9, A10, A13, A15, Def1;

        end;

          suppose

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

          

          hence lf = ( cell (G,i2,(j2 -' 1))) by A4, A10, A13, A6, A8, A5, A7, Def2

          .= lfn by A1, A2, A9, A10, A13, A16, Def2;

          

          thus rf = ( cell (G,i2,j2)) by A4, A10, A13, A6, A8, A5, A7, A16, Def1

          .= rfn by A1, A2, A9, A10, A13, A16, Def1;

        end;

          suppose

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

          

          hence lf = ( cell (G,i1,j2)) by A4, A10, A12, A6, A8, A5, A7, Def2

          .= lfn by A1, A2, A9, A10, A12, A17, Def2;

          

          thus rf = ( cell (G,(i1 -' 1),j2)) by A4, A10, A12, A6, A8, A5, A7, A17, Def1

          .= rfn by A1, A2, A9, A10, A12, A17, Def1;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBRD13:33

    for G be Go-board, f be standard special_circular_sequence st 1 <= n & (n + 1) <= ( len f) & f is_sequence_on G holds ( left_cell (f,n,G)) c= ( left_cell (f,n)) & ( right_cell (f,n,G)) c= ( right_cell (f,n))

    proof

      let G be Go-board, f be standard special_circular_sequence such that

       A1: 1 <= n & (n + 1) <= ( len f) and

       A2: f is_sequence_on G;

      consider i1, j1, i2, j2 such that

       A3: [i1, j1] in ( Indices G) and

       A4: (f /. n) = (G * (i1,j1)) and

       A5: [i2, j2] in ( Indices G) and

       A6: (f /. (n + 1)) = (G * (i2,j2)) and

       A7: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A2, JORDAN8: 3;

      

       A8: 1 <= j1 by A3, MATRIX_0: 32;

      

       A9: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

      

       A10: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

      

       A11: j2 <= ( width G) by A5, MATRIX_0: 32;

      

       A12: j1 <= ( width G) by A3, MATRIX_0: 32;

      

       A13: i2 <= ( len G) by A5, MATRIX_0: 32;

      

       A14: 1 <= i2 by A5, MATRIX_0: 32;

      then

       A15: ((G * (i2,j1)) `2 ) = ((G * (1,j1)) `2 ) by A8, A12, A13, GOBOARD5: 1;

      

       A16: 1 <= j2 by A5, MATRIX_0: 32;

      then

       A17: ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A14, A13, A11, GOBOARD5: 2;

      

       A18: i1 <= ( len G) by A3, MATRIX_0: 32;

      set F = ( GoB f);

      

       A19: ( Values F) c= ( Values G) by A2, Th13;

      f is_sequence_on F by GOBOARD5:def 5;

      then

      consider m, k, i, j such that

       A20: [m, k] in ( Indices F) and

       A21: (f /. n) = (F * (m,k)) and

       A22: [i, j] in ( Indices F) and

       A23: (f /. (n + 1)) = (F * (i,j)) and m = i & (k + 1) = j or (m + 1) = i & k = j or m = (i + 1) & k = j or m = i & k = (j + 1) by A1, JORDAN8: 3;

      

       A24: 1 <= m by A20, MATRIX_0: 32;

      

       A25: 1 <= i1 by A3, MATRIX_0: 32;

      then

       A26: ((G * (i1,j1)) `1 ) = ((G * (i1,1)) `1 ) by A18, A8, A12, GOBOARD5: 2;

      

       A27: ((G * (i1,j1)) `2 ) = ((G * (1,j1)) `2 ) by A25, A18, A8, A12, GOBOARD5: 1;

      

       A28: m <= ( len F) by A20, MATRIX_0: 32;

      

       A29: (j + 1) > j by NAT_1: 13;

      

       A30: (k + 1) > k by NAT_1: 13;

      

       A31: (k + 1) >= 1 by NAT_1: 12;

      

       A32: (j + 1) >= 1 by NAT_1: 12;

      

       A33: j <= ( width F) by A22, MATRIX_0: 32;

      

       A34: (i + 1) > i by NAT_1: 13;

      

       A35: (m + 1) > m by NAT_1: 13;

      

       A36: i <= ( len F) by A22, MATRIX_0: 32;

      

       A37: (i + 1) >= 1 by NAT_1: 12;

      

       A38: (m + 1) >= 1 by NAT_1: 12;

      

       A39: k <= ( width F) by A20, MATRIX_0: 32;

      

       A40: 1 <= j by A22, MATRIX_0: 32;

      then

       A41: ((F * (m,j)) `2 ) = ((F * (1,j)) `2 ) by A24, A28, A33, GOBOARD5: 1;

      

       A42: 1 <= i by A22, MATRIX_0: 32;

      then

       A43: ((F * (i,j)) `1 ) = ((F * (i,1)) `1 ) by A36, A40, A33, GOBOARD5: 2;

      

       A44: ((F * (i,j)) `2 ) = ((F * (1,j)) `2 ) by A42, A36, A40, A33, GOBOARD5: 1;

      

       A45: 1 <= k by A20, MATRIX_0: 32;

      then

       A46: ((F * (i,k)) `1 ) = ((F * (i,1)) `1 ) by A39, A42, A36, GOBOARD5: 2;

      per cases by A7;

        suppose

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

         A48:

        now

          

           A49: ((G * (i2,j2)) `2 ) = ((G * (1,j2)) `2 ) by A14, A13, A16, A11, GOBOARD5: 1;

          assume

           A50: (k + 1) < j;

          then

           A51: (k + 1) < ( width F) by A33, XXREAL_0: 2;

          then

          consider l, i9 such that

           A52: l in ( dom f) and

           A53: [i9, (k + 1)] in ( Indices F) and

           A54: (f /. l) = (F * (i9,(k + 1))) by JORDAN5D: 8, NAT_1: 12;

          

           A55: ((F * (m,(k + 1))) `2 ) = ((F * (1,(k + 1))) `2 ) by A24, A28, A31, A51, GOBOARD5: 1;

          1 <= i9 & i9 <= ( len F) by A53, MATRIX_0: 32;

          then

           A56: ((F * (i9,(k + 1))) `2 ) = ((F * (1,(k + 1))) `2 ) by A31, A51, GOBOARD5: 1;

          consider i19, j19 such that

           A57: [i19, j19] in ( Indices G) and

           A58: (f /. l) = (G * (i19,j19)) by A2, A52, GOBOARD1:def 9;

          

           A59: 1 <= j19 by A57, MATRIX_0: 32;

          

           A60: 1 <= i19 & i19 <= ( len G) by A57, MATRIX_0: 32;

          then

           A61: ((G * (i19,j1)) `2 ) = ((G * (1,j1)) `2 ) by A8, A12, GOBOARD5: 1;

           A62:

          now

            assume j1 >= j19;

            then ((G * (i19,j19)) `2 ) <= ((G * (i1,j1)) `2 ) by A12, A27, A60, A59, A61, SPRECT_3: 12;

            hence contradiction by A21, A24, A28, A45, A4, A30, A51, A54, A56, A55, A58, GOBOARD5: 4;

          end;

          

           A63: j19 <= ( width G) by A57, MATRIX_0: 32;

          

           A64: ((G * (i19,j2)) `2 ) = ((G * (1,j2)) `2 ) by A16, A11, A60, GOBOARD5: 1;

          now

            assume j2 <= j19;

            then ((G * (i2,j2)) `2 ) <= ((G * (i19,j19)) `2 ) by A16, A60, A63, A49, A64, SPRECT_3: 12;

            hence contradiction by A23, A24, A28, A33, A44, A41, A6, A31, A50, A54, A56, A55, A58, GOBOARD5: 4;

          end;

          hence contradiction by A47, A62, NAT_1: 13;

        end;

        now

          assume j <= k;

          then

           A65: ((F * (i,j)) `2 ) <= ((F * (m,k)) `2 ) by A24, A28, A39, A40, A44, A41, SPRECT_3: 12;

          j1 < j2 by A47, NAT_1: 13;

          hence contradiction by A21, A23, A4, A6, A8, A14, A13, A11, A27, A15, A65, GOBOARD5: 4;

        end;

        then (k + 1) <= j by NAT_1: 13;

        then (k + 1) = j by A48, XXREAL_0: 1;

        then

         A66: ( right_cell (f,n)) = ( cell (F,m,k)) & ( left_cell (f,n)) = ( cell (F,(m -' 1),k)) by A1, A20, A21, A22, A23, A30, A29, GOBOARD5:def 6, GOBOARD5:def 7;

        ( right_cell (f,n,G)) = ( cell (G,i1,j1)) & ( left_cell (f,n,G)) = ( cell (G,(i1 -' 1),j1)) by A1, A2, A3, A4, A5, A6, A9, A47, Def1, Def2;

        hence thesis by A19, A20, A21, A3, A4, A66, Th10, Th11;

      end;

        suppose

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

         A68:

        now

          assume

           A69: (m + 1) < i;

          then

           A70: (m + 1) < ( len F) by A36, XXREAL_0: 2;

          then

          consider l, j9 such that

           A71: l in ( dom f) and

           A72: [(m + 1), j9] in ( Indices F) and

           A73: (f /. l) = (F * ((m + 1),j9)) by JORDAN5D: 7, NAT_1: 12;

          

           A74: ((F * ((m + 1),k)) `1 ) = ((F * ((m + 1),1)) `1 ) by A45, A39, A38, A70, GOBOARD5: 2;

          1 <= j9 & j9 <= ( width F) by A72, MATRIX_0: 32;

          then

           A75: ((F * ((m + 1),j9)) `1 ) = ((F * ((m + 1),1)) `1 ) by A38, A70, GOBOARD5: 2;

          

           A76: 1 <= (m + 1) & ((F * ((m + 1),j)) `1 ) = ((F * ((m + 1),1)) `1 ) by A40, A33, A38, A70, GOBOARD5: 2;

          

           A77: ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A14, A13, A16, A11, GOBOARD5: 2;

          consider i19, j19 such that

           A78: [i19, j19] in ( Indices G) and

           A79: (f /. l) = (G * (i19,j19)) by A2, A71, GOBOARD1:def 9;

          

           A80: i19 <= ( len G) by A78, MATRIX_0: 32;

          

           A81: 1 <= j19 & j19 <= ( width G) by A78, MATRIX_0: 32;

          

           A82: 1 <= i19 by A78, MATRIX_0: 32;

          then

           A83: ((G * (i19,j19)) `1 ) = ((G * (i19,1)) `1 ) by A80, A81, GOBOARD5: 2;

          

           A84: ((G * (i19,j1)) `1 ) = ((G * (i19,1)) `1 ) by A8, A12, A82, A80, GOBOARD5: 2;

           A85:

          now

            assume i1 >= i19;

            then ((G * (i19,j19)) `1 ) <= ((G * (i1,j1)) `1 ) by A18, A8, A12, A82, A83, A84, SPRECT_3: 13;

            hence contradiction by A21, A24, A45, A39, A4, A35, A70, A73, A75, A74, A79, GOBOARD5: 3;

          end;

          

           A86: ((G * (i2,j19)) `1 ) = ((G * (i2,1)) `1 ) by A14, A13, A81, GOBOARD5: 2;

          now

            assume i2 <= i19;

            then ((G * (i2,j2)) `1 ) <= ((G * (i19,j19)) `1 ) by A14, A80, A81, A77, A86, SPRECT_3: 13;

            hence contradiction by A23, A36, A40, A33, A6, A69, A73, A75, A76, A79, GOBOARD5: 3;

          end;

          hence contradiction by A67, A85, NAT_1: 13;

        end;

        now

          assume i <= m;

          then

           A87: ((F * (i,j)) `1 ) <= ((F * (m,k)) `1 ) by A28, A45, A39, A42, A43, A46, SPRECT_3: 13;

          i1 < i2 by A67, NAT_1: 13;

          hence contradiction by A21, A23, A4, A6, A25, A8, A12, A13, A67, A87, GOBOARD5: 3;

        end;

        then (m + 1) <= i by NAT_1: 13;

        then (m + 1) = i by A68, XXREAL_0: 1;

        then

         A88: ( right_cell (f,n)) = ( cell (F,m,(k -' 1))) & ( left_cell (f,n)) = ( cell (F,m,k)) by A1, A20, A21, A22, A23, A35, A34, GOBOARD5:def 6, GOBOARD5:def 7;

        ( right_cell (f,n,G)) = ( cell (G,i1,(j1 -' 1))) & ( left_cell (f,n,G)) = ( cell (G,i1,j1)) by A1, A2, A3, A4, A5, A6, A10, A67, Def1, Def2;

        hence thesis by A19, A20, A21, A3, A4, A88, Th10, Th12;

      end;

        suppose

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

         A90:

        now

          assume

           A91: m > (i + 1);

          then

           A92: (i + 1) < ( len F) by A28, XXREAL_0: 2;

          then

          consider l, j9 such that

           A93: l in ( dom f) and

           A94: [(i + 1), j9] in ( Indices F) and

           A95: (f /. l) = (F * ((i + 1),j9)) by JORDAN5D: 7, NAT_1: 12;

          

           A96: 1 <= (i + 1) & ((F * ((i + 1),k)) `1 ) = ((F * ((i + 1),1)) `1 ) by A45, A39, A37, A92, GOBOARD5: 2;

          1 <= j9 & j9 <= ( width F) by A94, MATRIX_0: 32;

          then

           A97: ((F * ((i + 1),j9)) `1 ) = ((F * ((i + 1),1)) `1 ) by A37, A92, GOBOARD5: 2;

          

           A98: ((F * ((i + 1),j)) `1 ) = ((F * ((i + 1),1)) `1 ) by A40, A33, A37, A92, GOBOARD5: 2;

          

           A99: ((G * (i2,j2)) `1 ) = ((G * (i2,1)) `1 ) by A14, A13, A16, A11, GOBOARD5: 2;

          consider i19, j19 such that

           A100: [i19, j19] in ( Indices G) and

           A101: (f /. l) = (G * (i19,j19)) by A2, A93, GOBOARD1:def 9;

          

           A102: 1 <= i19 by A100, MATRIX_0: 32;

          

           A103: 1 <= j19 & j19 <= ( width G) by A100, MATRIX_0: 32;

          

           A104: i19 <= ( len G) by A100, MATRIX_0: 32;

          then

           A105: ((G * (i19,j19)) `1 ) = ((G * (i19,1)) `1 ) by A102, A103, GOBOARD5: 2;

          

           A106: ((G * (i19,j1)) `1 ) = ((G * (i19,1)) `1 ) by A8, A12, A102, A104, GOBOARD5: 2;

           A107:

          now

            assume i1 <= i19;

            then ((G * (i19,j19)) `1 ) >= ((G * (i1,j1)) `1 ) by A25, A8, A12, A104, A105, A106, SPRECT_3: 13;

            hence contradiction by A21, A28, A45, A39, A4, A91, A95, A97, A96, A101, GOBOARD5: 3;

          end;

          

           A108: ((G * (i2,j19)) `1 ) = ((G * (i2,1)) `1 ) by A14, A13, A103, GOBOARD5: 2;

          now

            assume i2 >= i19;

            then ((G * (i2,j2)) `1 ) >= ((G * (i19,j19)) `1 ) by A13, A102, A103, A99, A108, SPRECT_3: 13;

            hence contradiction by A23, A42, A40, A33, A6, A34, A92, A95, A97, A98, A101, GOBOARD5: 3;

          end;

          hence contradiction by A89, A107, NAT_1: 13;

        end;

        now

          assume m <= i;

          then

           A109: ((F * (i,j)) `1 ) >= ((F * (m,k)) `1 ) by A24, A45, A39, A36, A43, A46, SPRECT_3: 13;

          i1 > i2 by A89, NAT_1: 13;

          hence contradiction by A21, A23, A4, A6, A18, A8, A12, A14, A89, A109, GOBOARD5: 3;

        end;

        then (i + 1) <= m by NAT_1: 13;

        then (i + 1) = m by A90, XXREAL_0: 1;

        then

         A110: ( right_cell (f,n)) = ( cell (F,i,j)) & ( left_cell (f,n)) = ( cell (F,i,(j -' 1))) by A1, A20, A21, A22, A23, A35, A34, GOBOARD5:def 6, GOBOARD5:def 7;

        ( right_cell (f,n,G)) = ( cell (G,i2,j2)) & ( left_cell (f,n,G)) = ( cell (G,i2,(j2 -' 1))) by A1, A2, A3, A4, A5, A6, A10, A89, Def1, Def2;

        hence thesis by A19, A22, A23, A5, A6, A110, Th10, Th12;

      end;

        suppose

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

         A112:

        now

          

           A113: ((G * (i2,j2)) `2 ) = ((G * (1,j2)) `2 ) by A14, A13, A16, A11, GOBOARD5: 1;

          assume

           A114: (j + 1) < k;

          then

           A115: (j + 1) < ( width F) by A39, XXREAL_0: 2;

          then

          consider l, i9 such that

           A116: l in ( dom f) and

           A117: [i9, (j + 1)] in ( Indices F) and

           A118: (f /. l) = (F * (i9,(j + 1))) by JORDAN5D: 8, NAT_1: 12;

          

           A119: ((F * (m,(j + 1))) `2 ) = ((F * (1,(j + 1))) `2 ) by A24, A28, A32, A115, GOBOARD5: 1;

          1 <= i9 & i9 <= ( len F) by A117, MATRIX_0: 32;

          then

           A120: ((F * (i9,(j + 1))) `2 ) = ((F * (1,(j + 1))) `2 ) by A32, A115, GOBOARD5: 1;

          consider i19, j19 such that

           A121: [i19, j19] in ( Indices G) and

           A122: (f /. l) = (G * (i19,j19)) by A2, A116, GOBOARD1:def 9;

          

           A123: j19 <= ( width G) by A121, MATRIX_0: 32;

          

           A124: 1 <= i19 & i19 <= ( len G) by A121, MATRIX_0: 32;

          then

           A125: ((G * (i19,j1)) `2 ) = ((G * (1,j1)) `2 ) by A8, A12, GOBOARD5: 1;

           A126:

          now

            assume j1 <= j19;

            then ((G * (i19,j19)) `2 ) >= ((G * (i1,j1)) `2 ) by A8, A27, A124, A123, A125, SPRECT_3: 12;

            hence contradiction by A21, A24, A28, A39, A4, A32, A114, A118, A120, A119, A122, GOBOARD5: 4;

          end;

          

           A127: ((F * (i,(j + 1))) `2 ) = ((F * (1,(j + 1))) `2 ) by A42, A36, A32, A115, GOBOARD5: 1;

          

           A128: 1 <= j19 by A121, MATRIX_0: 32;

          

           A129: ((G * (i19,j2)) `2 ) = ((G * (1,j2)) `2 ) by A16, A11, A124, GOBOARD5: 1;

          now

            assume j2 >= j19;

            then ((G * (i2,j2)) `2 ) >= ((G * (i19,j19)) `2 ) by A11, A124, A128, A113, A129, SPRECT_3: 12;

            hence contradiction by A23, A42, A36, A40, A6, A29, A115, A118, A120, A127, A122, GOBOARD5: 4;

          end;

          hence contradiction by A111, A126, NAT_1: 13;

        end;

        now

          assume j >= k;

          then

           A130: ((F * (i,j)) `2 ) >= ((F * (m,k)) `2 ) by A24, A28, A45, A33, A44, A41, SPRECT_3: 12;

          j1 > j2 by A111, NAT_1: 13;

          hence contradiction by A21, A23, A4, A6, A12, A14, A13, A16, A27, A15, A130, GOBOARD5: 4;

        end;

        then (j + 1) <= k by NAT_1: 13;

        then (j + 1) = k by A112, XXREAL_0: 1;

        then

         A131: ( right_cell (f,n)) = ( cell (F,(m -' 1),j)) & ( left_cell (f,n)) = ( cell (F,m,j)) by A1, A20, A21, A22, A23, A30, A29, GOBOARD5:def 6, GOBOARD5:def 7;

         A132:

        now

          assume

           A133: m <> i;

          per cases by A133, XXREAL_0: 1;

            suppose m < i;

            hence contradiction by A21, A23, A24, A45, A39, A36, A43, A46, A4, A6, A26, A17, A111, GOBOARD5: 3;

          end;

            suppose m > i;

            hence contradiction by A21, A23, A28, A45, A39, A42, A43, A46, A4, A6, A26, A17, A111, GOBOARD5: 3;

          end;

        end;

        ( right_cell (f,n,G)) = ( cell (G,(i1 -' 1),j2)) & ( left_cell (f,n,G)) = ( cell (G,i1,j2)) by A1, A2, A3, A4, A5, A6, A9, A111, Def1, Def2;

        hence thesis by A19, A22, A23, A5, A6, A111, A132, A131, Th10, Th11;

      end;

    end;

    definition

      let f, G, k;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G;

      then

      consider i1,j1,i2,j2 be Nat such that

       A1: [i1, j1] in ( Indices G) & (f /. k) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f /. (k + 1)) = (G * (i2,j2)) and

       A2: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by JORDAN8: 3;

      :: GOBRD13:def4

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

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

      existence

      proof

        per cases by A2;

          suppose

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

          take ( cell (G,i2,j2));

          let i19,j19,i29,j29 be Nat;

          assume

           A4: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A3, A4, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i2,(j2 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume

           A6: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A5, A6, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,(i2 -' 1),j2));

          let i19,j19,i29,j29 be Nat;

          assume

           A8: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A7, A8, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,(i2 -' 1),(j2 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume

           A10: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A9, A10, GOBOARD1: 5;

        end;

      end;

      uniqueness

      proof

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

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

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

        per cases by A2;

          suppose

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

          

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

          

           A15: j1 < j2 by A13, XREAL_1: 29;

          

          hence P1 = ( cell (G,i2,j2)) by A1, A11, A14

          .= P2 by A1, A12, A15, A14;

        end;

          suppose

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

          

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

          

           A18: i1 < i2 by A16, XREAL_1: 29;

          

          hence P1 = ( cell (G,i2,(j2 -' 1))) by A1, A11, A17

          .= P2 by A1, A12, A18, A17;

        end;

          suppose

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

          

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

          

           A21: i2 < i1 by A19, XREAL_1: 29;

          

          hence P1 = ( cell (G,(i2 -' 1),j2)) by A1, A11, A20

          .= P2 by A1, A12, A21, A20;

        end;

          suppose

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

          

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

          

           A24: j2 < j1 by A22, XREAL_1: 29;

          

          hence P1 = ( cell (G,(i2 -' 1),(j2 -' 1))) by A1, A11, A23

          .= P2 by A1, A12, A24, A23;

        end;

      end;

      :: GOBRD13:def5

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

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

      existence

      proof

        per cases by A2;

          suppose

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

          take ( cell (G,(i2 -' 1),j2));

          let i19,j19,i29,j29 be Nat;

          assume

           A26: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A25, A26, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i2,j2));

          let i19,j19,i29,j29 be Nat;

          assume

           A28: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A27, A28, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,(i2 -' 1),(j2 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume

           A30: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A29, A30, GOBOARD1: 5;

        end;

          suppose

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

          take ( cell (G,i2,(j2 -' 1)));

          let i19,j19,i29,j29 be Nat;

          assume

           A32: [i19, j19] in ( Indices G) & [i29, j29] in ( Indices G) & (f /. k) = (G * (i19,j19)) & (f /. (k + 1)) = (G * (i29,j29));

          then i2 = i29 & j1 = j19 by A1, GOBOARD1: 5;

          hence thesis by A1, A31, A32, GOBOARD1: 5;

        end;

      end;

      uniqueness

      proof

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

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

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

        per cases by A2;

          suppose

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

          

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

          

           A37: j1 < j2 by A35, XREAL_1: 29;

          

          hence P1 = ( cell (G,(i2 -' 1),j2)) by A1, A33, A36

          .= P2 by A1, A34, A37, A36;

        end;

          suppose

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

          

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

          

           A40: i1 < i2 by A38, XREAL_1: 29;

          

          hence P1 = ( cell (G,i2,j2)) by A1, A33, A39

          .= P2 by A1, A34, A40, A39;

        end;

          suppose

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

          

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

          

           A43: i2 < i1 by A41, XREAL_1: 29;

          

          hence P1 = ( cell (G,(i2 -' 1),(j2 -' 1))) by A1, A33, A42

          .= P2 by A1, A34, A43, A42;

        end;

          suppose

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

          

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

          

           A46: j2 < j1 by A44, XREAL_1: 29;

          

          hence P1 = ( cell (G,i2,(j2 -' 1))) by A1, A33, A45

          .= P2 by A1, A34, A46, A45;

        end;

      end;

    end

    theorem :: GOBRD13:34

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1))) implies ( front_left_cell (f,k,G)) = ( cell (G,(i -' 1),(j + 1)))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1)));

      hence thesis by A1, Def4;

    end;

    theorem :: GOBRD13:35

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1))) implies ( front_right_cell (f,k,G)) = ( cell (G,i,(j + 1)))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [i, (j + 1)] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * (i,(j + 1)));

      hence thesis by A1, Def3;

    end;

    theorem :: GOBRD13:36

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j)) implies ( front_left_cell (f,k,G)) = ( cell (G,(i + 1),j))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j));

      hence thesis by A1, Def4;

    end;

    theorem :: GOBRD13:37

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j)) implies ( front_right_cell (f,k,G)) = ( cell (G,(i + 1),(j -' 1)))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * (i,j)) & (f /. (k + 1)) = (G * ((i + 1),j));

      hence thesis by A1, Def3;

    end;

    theorem :: GOBRD13:38

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j)) implies ( front_left_cell (f,k,G)) = ( cell (G,(i -' 1),(j -' 1)))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def4;

    end;

    theorem :: GOBRD13:39

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j)) implies ( front_right_cell (f,k,G)) = ( cell (G,(i -' 1),j))

    proof

      

       A1: i < (i + 1) & (i + 1) <= ((i + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, j] in ( Indices G) & [(i + 1), j] in ( Indices G) & (f /. k) = (G * ((i + 1),j)) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def3;

    end;

    theorem :: GOBRD13:40

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j)) implies ( front_left_cell (f,k,G)) = ( cell (G,i,(j -' 1)))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def4;

    end;

    theorem :: GOBRD13:41

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j)) implies ( front_right_cell (f,k,G)) = ( cell (G,(i -' 1),(j -' 1)))

    proof

      

       A1: j < (j + 1) & (j + 1) <= ((j + 1) + 1) by XREAL_1: 29;

      assume 1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & [i, (j + 1)] in ( Indices G) & [i, j] in ( Indices G) & (f /. k) = (G * (i,(j + 1))) & (f /. (k + 1)) = (G * (i,j));

      hence thesis by A1, Def3;

    end;

    theorem :: GOBRD13:42

    1 <= k & (k + 1) <= ( len f) & f is_sequence_on G & (k + 1) <= n implies ( front_left_cell (f,k,G)) = ( front_left_cell ((f | n),k,G)) & ( front_right_cell (f,k,G)) = ( front_right_cell ((f | n),k,G))

    proof

      assume that

       A1: 1 <= k and

       A2: (k + 1) <= ( len f) and

       A3: f is_sequence_on G and

       A4: (k + 1) <= n;

      per cases ;

        suppose ( len f) <= n;

        hence thesis by FINSEQ_1: 58;

      end;

        suppose n < ( len f);

        then

         A5: ( len (f | n)) = n by FINSEQ_1: 59;

        then k in ( dom (f | n)) by A1, A4, SEQ_4: 134;

        then

         A6: ((f | n) /. k) = (f /. k) by FINSEQ_4: 70;

        (k + 1) in ( dom (f | n)) by A1, A4, A5, SEQ_4: 134;

        then

         A7: ((f | n) /. (k + 1)) = (f /. (k + 1)) by FINSEQ_4: 70;

        set lf = ( front_left_cell (f,k,G)), lfn = ( front_left_cell ((f | n),k,G)), rf = ( front_right_cell (f,k,G)), rfn = ( front_right_cell ((f | n),k,G));

        

         A8: (f | n) is_sequence_on G by A3, GOBOARD1: 22;

        consider i1,j1,i2,j2 be Nat such that

         A9: [i1, j1] in ( Indices G) & (f /. k) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f /. (k + 1)) = (G * (i2,j2)) and

         A10: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A1, A2, A3, JORDAN8: 3;

        

         A11: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

        

         A12: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

        now

          per cases by A10;

            suppose

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

            

            hence lf = ( cell (G,(i2 -' 1),j2)) by A1, A2, A3, A9, A11, Def4

            .= lfn by A1, A4, A9, A11, A8, A5, A6, A7, A13, Def4;

            

            thus rf = ( cell (G,i2,j2)) by A1, A2, A3, A9, A11, A13, Def3

            .= rfn by A1, A4, A9, A11, A8, A5, A6, A7, A13, Def3;

          end;

            suppose

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

            

            hence lf = ( cell (G,i2,j2)) by A1, A2, A3, A9, A12, Def4

            .= lfn by A1, A4, A9, A12, A8, A5, A6, A7, A14, Def4;

            

            thus rf = ( cell (G,i2,(j2 -' 1))) by A1, A2, A3, A9, A12, A14, Def3

            .= rfn by A1, A4, A9, A12, A8, A5, A6, A7, A14, Def3;

          end;

            suppose

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

            

            hence lf = ( cell (G,(i2 -' 1),(j2 -' 1))) by A1, A2, A3, A9, A12, Def4

            .= lfn by A1, A4, A9, A12, A8, A5, A6, A7, A15, Def4;

            

            thus rf = ( cell (G,(i2 -' 1),j2)) by A1, A2, A3, A9, A12, A15, Def3

            .= rfn by A1, A4, A9, A12, A8, A5, A6, A7, A15, Def3;

          end;

            suppose

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

            

            hence lf = ( cell (G,i2,(j2 -' 1))) by A1, A2, A3, A9, A11, Def4

            .= lfn by A1, A4, A9, A11, A8, A5, A6, A7, A16, Def4;

            

            thus rf = ( cell (G,(i2 -' 1),(j2 -' 1))) by A1, A2, A3, A9, A11, A16, Def3

            .= rfn by A1, A4, A9, A11, A8, A5, A6, A7, A16, Def3;

          end;

        end;

        hence thesis;

      end;

    end;

    definition

      let D be set;

      let f be FinSequence of D, G be Matrix of D, k;

      :: GOBRD13:def6

      pred f turns_right k,G means for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & [(i2 + 1), j2] in ( Indices G) & (f /. (k + 2)) = (G * ((i2 + 1),j2)) or (i1 + 1) = i2 & j1 = j2 & [i2, (j2 -' 1)] in ( Indices G) & (f /. (k + 2)) = (G * (i2,(j2 -' 1))) or i1 = (i2 + 1) & j1 = j2 & [i2, (j2 + 1)] in ( Indices G) & (f /. (k + 2)) = (G * (i2,(j2 + 1))) or i1 = i2 & j1 = (j2 + 1) & [(i2 -' 1), j2] in ( Indices G) & (f /. (k + 2)) = (G * ((i2 -' 1),j2));

      :: GOBRD13:def7

      pred f turns_left k,G means for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & [(i2 -' 1), j2] in ( Indices G) & (f /. (k + 2)) = (G * ((i2 -' 1),j2)) or (i1 + 1) = i2 & j1 = j2 & [i2, (j2 + 1)] in ( Indices G) & (f /. (k + 2)) = (G * (i2,(j2 + 1))) or i1 = (i2 + 1) & j1 = j2 & [i2, (j2 -' 1)] in ( Indices G) & (f /. (k + 2)) = (G * (i2,(j2 -' 1))) or i1 = i2 & j1 = (j2 + 1) & [(i2 + 1), j2] in ( Indices G) & (f /. (k + 2)) = (G * ((i2 + 1),j2));

      :: GOBRD13:def8

      pred f goes_straight k,G means for i1,j1,i2,j2 be Nat st [i1, j1] in ( Indices G) & [i2, j2] in ( Indices G) & (f /. k) = (G * (i1,j1)) & (f /. (k + 1)) = (G * (i2,j2)) holds i1 = i2 & (j1 + 1) = j2 & [i2, (j2 + 1)] in ( Indices G) & (f /. (k + 2)) = (G * (i2,(j2 + 1))) or (i1 + 1) = i2 & j1 = j2 & [(i2 + 1), j2] in ( Indices G) & (f /. (k + 2)) = (G * ((i2 + 1),j2)) or i1 = (i2 + 1) & j1 = j2 & [(i2 -' 1), j2] in ( Indices G) & (f /. (k + 2)) = (G * ((i2 -' 1),j2)) or i1 = i2 & j1 = (j2 + 1) & [i2, (j2 -' 1)] in ( Indices G) & (f /. (k + 2)) = (G * (i2,(j2 -' 1)));

    end

    reserve D for set,

f,f1,f2 for FinSequence of D,

G for Matrix of D;

    theorem :: GOBRD13:43

    1 <= k & (k + 2) <= n & (f | n) turns_right (k,G) implies f turns_right (k,G)

    proof

      assume that

       A1: 1 <= k & (k + 2) <= n and

       A2: (f | n) turns_right (k,G);

      per cases ;

        suppose ( len f) <= n;

        hence thesis by A2, FINSEQ_1: 58;

      end;

        suppose

         A3: n < ( len f);

        let i19,j19,i29,j29 be Nat;

        

         A4: ( len (f | n)) = n by A3, FINSEQ_1: 59;

        then (k + 1) in ( dom (f | n)) by A1, SEQ_4: 135;

        then

         A5: ((f | n) /. (k + 1)) = (f /. (k + 1)) by FINSEQ_4: 70;

        (k + 2) in ( dom (f | n)) by A1, A4, SEQ_4: 135;

        then

         A6: ((f | n) /. (k + 2)) = (f /. (k + 2)) by FINSEQ_4: 70;

        k in ( dom (f | n)) by A1, A4, SEQ_4: 135;

        then ((f | n) /. k) = (f /. k) by FINSEQ_4: 70;

        hence thesis by A2, A5, A6;

      end;

    end;

    theorem :: GOBRD13:44

    1 <= k & (k + 2) <= n & (f | n) turns_left (k,G) implies f turns_left (k,G)

    proof

      assume that

       A1: 1 <= k & (k + 2) <= n and

       A2: (f | n) turns_left (k,G);

      per cases ;

        suppose ( len f) <= n;

        hence thesis by A2, FINSEQ_1: 58;

      end;

        suppose

         A3: n < ( len f);

        let i19,j19,i29,j29 be Nat;

        

         A4: ( len (f | n)) = n by A3, FINSEQ_1: 59;

        then (k + 1) in ( dom (f | n)) by A1, SEQ_4: 135;

        then

         A5: ((f | n) /. (k + 1)) = (f /. (k + 1)) by FINSEQ_4: 70;

        (k + 2) in ( dom (f | n)) by A1, A4, SEQ_4: 135;

        then

         A6: ((f | n) /. (k + 2)) = (f /. (k + 2)) by FINSEQ_4: 70;

        k in ( dom (f | n)) by A1, A4, SEQ_4: 135;

        then ((f | n) /. k) = (f /. k) by FINSEQ_4: 70;

        hence thesis by A2, A5, A6;

      end;

    end;

    theorem :: GOBRD13:45

    1 <= k & (k + 2) <= n & (f | n) goes_straight (k,G) implies f goes_straight (k,G)

    proof

      assume that

       A1: 1 <= k & (k + 2) <= n and

       A2: (f | n) goes_straight (k,G);

      per cases ;

        suppose ( len f) <= n;

        hence thesis by A2, FINSEQ_1: 58;

      end;

        suppose

         A3: n < ( len f);

        let i19,j19,i29,j29 be Nat;

        

         A4: ( len (f | n)) = n by A3, FINSEQ_1: 59;

        then (k + 1) in ( dom (f | n)) by A1, SEQ_4: 135;

        then

         A5: ((f | n) /. (k + 1)) = (f /. (k + 1)) by FINSEQ_4: 70;

        (k + 2) in ( dom (f | n)) by A1, A4, SEQ_4: 135;

        then

         A6: ((f | n) /. (k + 2)) = (f /. (k + 2)) by FINSEQ_4: 70;

        k in ( dom (f | n)) by A1, A4, SEQ_4: 135;

        then ((f | n) /. k) = (f /. k) by FINSEQ_4: 70;

        hence thesis by A2, A5, A6;

      end;

    end;

    theorem :: GOBRD13:46

    1 < k & (k + 1) <= ( len f1) & (k + 1) <= ( len f2) & f1 is_sequence_on G & (f1 | k) = (f2 | k) & f1 turns_right ((k -' 1),G) & f2 turns_right ((k -' 1),G) implies (f1 | (k + 1)) = (f2 | (k + 1))

    proof

      assume that

       A1: 1 < k and

       A2: (k + 1) <= ( len f1) and

       A3: (k + 1) <= ( len f2) and

       A4: f1 is_sequence_on G and

       A5: (f1 | k) = (f2 | k) and

       A6: f1 turns_right ((k -' 1),G) and

       A7: f2 turns_right ((k -' 1),G);

      

       A8: 1 <= (k -' 1) by A1, NAT_D: 49;

      

       A9: k <= (k + 1) by NAT_1: 12;

      then k <= ( len (f1 | k)) by A2, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A10: k in ( dom (f1 | k)) by A1, FINSEQ_3: 25;

      then

       A11: (f2 /. k) = ((f2 | k) /. k) by A5, FINSEQ_4: 70;

      (k -' 1) <= k by NAT_D: 35;

      then (k -' 1) <= ( len (f1 | k)) by A2, A9, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A12: (k -' 1) in ( dom (f1 | k)) by A8, FINSEQ_3: 25;

      then

       A13: (f2 /. (k -' 1)) = ((f2 | k) /. (k -' 1)) by A5, FINSEQ_4: 70;

      

       A14: (f1 /. k) = ((f1 | k) /. k) by A10, FINSEQ_4: 70;

      

       A15: (f1 /. (k -' 1)) = ((f1 | k) /. (k -' 1)) by A12, FINSEQ_4: 70;

      

       A16: k = ((k -' 1) + 1) by A1, XREAL_1: 235;

      k <= ( len f1) by A2, A9, XXREAL_0: 2;

      then

      consider i1,j1,i2,j2 be Nat such that

       A17: [i1, j1] in ( Indices G) & (f1 /. (k -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f1 /. k) = (G * (i2,j2)) and

       A18: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A4, A8, A16, JORDAN8: 3;

      

       A19: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

      

       A20: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

      now

        per cases by A18;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * ((i2 + 1),j2)) by A6, A16, A17, A19

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A19, A21;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * (i2,(j2 -' 1))) by A6, A16, A17, A20

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A20, A22;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * (i2,(j2 + 1))) by A6, A16, A17, A20

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A20, A23;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * ((i2 -' 1),j2)) by A6, A16, A17, A19

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A19, A24;

        end;

      end;

      

      hence (f1 | (k + 1)) = ((f2 | k) ^ <*(f2 /. (k + 1))*>) by A2, A5, FINSEQ_5: 82

      .= (f2 | (k + 1)) by A3, FINSEQ_5: 82;

    end;

    theorem :: GOBRD13:47

    1 < k & (k + 1) <= ( len f1) & (k + 1) <= ( len f2) & f1 is_sequence_on G & (f1 | k) = (f2 | k) & f1 turns_left ((k -' 1),G) & f2 turns_left ((k -' 1),G) implies (f1 | (k + 1)) = (f2 | (k + 1))

    proof

      assume that

       A1: 1 < k and

       A2: (k + 1) <= ( len f1) and

       A3: (k + 1) <= ( len f2) and

       A4: f1 is_sequence_on G and

       A5: (f1 | k) = (f2 | k) and

       A6: f1 turns_left ((k -' 1),G) and

       A7: f2 turns_left ((k -' 1),G);

      

       A8: 1 <= (k -' 1) by A1, NAT_D: 49;

      

       A9: k <= (k + 1) by NAT_1: 12;

      then k <= ( len (f1 | k)) by A2, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A10: k in ( dom (f1 | k)) by A1, FINSEQ_3: 25;

      then

       A11: (f2 /. k) = ((f2 | k) /. k) by A5, FINSEQ_4: 70;

      (k -' 1) <= k by NAT_D: 35;

      then (k -' 1) <= ( len (f1 | k)) by A2, A9, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A12: (k -' 1) in ( dom (f1 | k)) by A8, FINSEQ_3: 25;

      then

       A13: (f2 /. (k -' 1)) = ((f2 | k) /. (k -' 1)) by A5, FINSEQ_4: 70;

      

       A14: (f1 /. k) = ((f1 | k) /. k) by A10, FINSEQ_4: 70;

      

       A15: (f1 /. (k -' 1)) = ((f1 | k) /. (k -' 1)) by A12, FINSEQ_4: 70;

      

       A16: k = ((k -' 1) + 1) by A1, XREAL_1: 235;

      k <= ( len f1) by A2, A9, XXREAL_0: 2;

      then

      consider i1,j1,i2,j2 be Nat such that

       A17: [i1, j1] in ( Indices G) & (f1 /. (k -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f1 /. k) = (G * (i2,j2)) and

       A18: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A4, A8, A16, JORDAN8: 3;

      

       A19: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

      

       A20: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

      now

        per cases by A18;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * ((i2 -' 1),j2)) by A6, A16, A17, A19

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A19, A21;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * (i2,(j2 + 1))) by A6, A16, A17, A20

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A20, A22;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * (i2,(j2 -' 1))) by A6, A16, A17, A20

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A20, A23;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * ((i2 + 1),j2)) by A6, A16, A17, A19

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A19, A24;

        end;

      end;

      

      hence (f1 | (k + 1)) = ((f2 | k) ^ <*(f2 /. (k + 1))*>) by A2, A5, FINSEQ_5: 82

      .= (f2 | (k + 1)) by A3, FINSEQ_5: 82;

    end;

    theorem :: GOBRD13:48

    1 < k & (k + 1) <= ( len f1) & (k + 1) <= ( len f2) & f1 is_sequence_on G & (f1 | k) = (f2 | k) & f1 goes_straight ((k -' 1),G) & f2 goes_straight ((k -' 1),G) implies (f1 | (k + 1)) = (f2 | (k + 1))

    proof

      assume that

       A1: 1 < k and

       A2: (k + 1) <= ( len f1) and

       A3: (k + 1) <= ( len f2) and

       A4: f1 is_sequence_on G and

       A5: (f1 | k) = (f2 | k) and

       A6: f1 goes_straight ((k -' 1),G) and

       A7: f2 goes_straight ((k -' 1),G);

      

       A8: 1 <= (k -' 1) by A1, NAT_D: 49;

      

       A9: k <= (k + 1) by NAT_1: 12;

      then k <= ( len (f1 | k)) by A2, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A10: k in ( dom (f1 | k)) by A1, FINSEQ_3: 25;

      then

       A11: (f2 /. k) = ((f2 | k) /. k) by A5, FINSEQ_4: 70;

      (k -' 1) <= k by NAT_D: 35;

      then (k -' 1) <= ( len (f1 | k)) by A2, A9, FINSEQ_1: 59, XXREAL_0: 2;

      then

       A12: (k -' 1) in ( dom (f1 | k)) by A8, FINSEQ_3: 25;

      then

       A13: (f2 /. (k -' 1)) = ((f2 | k) /. (k -' 1)) by A5, FINSEQ_4: 70;

      

       A14: (f1 /. k) = ((f1 | k) /. k) by A10, FINSEQ_4: 70;

      

       A15: (f1 /. (k -' 1)) = ((f1 | k) /. (k -' 1)) by A12, FINSEQ_4: 70;

      

       A16: k = ((k -' 1) + 1) by A1, XREAL_1: 235;

      k <= ( len f1) by A2, A9, XXREAL_0: 2;

      then

      consider i1,j1,i2,j2 be Nat such that

       A17: [i1, j1] in ( Indices G) & (f1 /. (k -' 1)) = (G * (i1,j1)) & [i2, j2] in ( Indices G) & (f1 /. k) = (G * (i2,j2)) and

       A18: i1 = i2 & (j1 + 1) = j2 or (i1 + 1) = i2 & j1 = j2 or i1 = (i2 + 1) & j1 = j2 or i1 = i2 & j1 = (j2 + 1) by A4, A8, A16, JORDAN8: 3;

      

       A19: (j1 + 1) > j1 & (j2 + 1) > j2 by NAT_1: 13;

      

       A20: (i1 + 1) > i1 & (i2 + 1) > i2 by NAT_1: 13;

      now

        per cases by A18;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * (i2,(j2 + 1))) by A6, A16, A17, A19

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A19, A21;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * ((i2 + 1),j2)) by A6, A16, A17, A20

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A20, A22;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * ((i2 -' 1),j2)) by A6, A16, A17, A20

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A20, A23;

        end;

          suppose

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

          

          hence (f1 /. (k + 1)) = (G * (i2,(j2 -' 1))) by A6, A16, A17, A19

          .= (f2 /. (k + 1)) by A5, A7, A16, A15, A14, A13, A11, A17, A19, A24;

        end;

      end;

      

      hence (f1 | (k + 1)) = ((f2 | k) ^ <*(f2 /. (k + 1))*>) by A2, A5, FINSEQ_5: 82

      .= (f2 | (k + 1)) by A3, FINSEQ_5: 82;

    end;