:: Some Remarks on Finite Sequences on Go-boards
:: by Adam Naumowicz
::
:: Received August 29, 2001
:: Copyright (c) 2001-2016 Association of Mizar Users

environ

vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD1, RLTOPSP1, RELAT_1, XBOOLE_0, TOPREAL1, MATRIX_1, XXREAL_0, MCART_1, RCOMP_1, PSCOMP_1, PRE_TOPC, TREES_1, TARSKI, ARYTM_3, PARTFUN1, COMPLEX1, ARYTM_1, CARD_1, SPPOL_1, JORDAN1E, JORDAN9, FINSEQ_6, FINSEQ_5, FINSEQ_4, JORDAN6, TOPREAL2, RELAT_2, JORDAN8, ORDINAL4, FUNCT_1, NAT_1, RFINSEQ, JORDAN1A, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1, FINSEQ_4, FINSEQ_5, FINSEQ_6, MATRIX_0, SEQ_4, STRUCT_0, PRE_TOPC, COMPTS_1, CONNSP_1, RFINSEQ, RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, SPPOL_1, PSCOMP_1, JORDAN6, JORDAN8, JORDAN9, JORDAN1A, JORDAN1E;
definitions TARSKI;
theorems JORDAN8, NAT_1, GOBOARD7, GOBOARD5, SPRECT_3, ABSVALUE, GOBOARD1, JORDAN6, PSCOMP_1, TARSKI, TOPREAL3, SPRECT_2, FINSEQ_6, RELAT_1, FINSEQ_5, TOPREAL1, PRE_TOPC, JORDAN5B, FINSEQ_1, JORDAN1E, JORDAN1A, REVROT_1, JORDAN9, JORDAN1B, FINSEQ_3, UNIFORM1, FINSEQ_4, JORDAN1D, SPRECT_5, RFINSEQ, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, EUCLID, PARTFUN1, MATRIX_0, XREAL_0;
schemes ;
registrations XBOOLE_0, RELSET_1, XREAL_0, NAT_1, MEMBERED, FINSEQ_6, STRUCT_0, SPPOL_2, SPRECT_1, SPRECT_2, TOPREAL6, JORDAN8, JORDAN1A, JORDAN1E, FUNCT_1, EUCLID, PSCOMP_1, ORDINAL1;
constructors HIDDEN, REAL_1, FINSEQ_4, NEWTON, RFINSEQ, FINSEQ_5, CONNSP_1, JORDAN5C, JORDAN6, JORDAN8, GOBRD13, JORDAN9, JORDAN1A, JORDAN1E, NAT_D, SEQ_4, RELSET_1, PSCOMP_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities STRUCT_0, PSCOMP_1;
expansions ;


theorem Th1: :: JORDAN1F:1
for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (i,n)) `2 = lower_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
proof end;

theorem :: JORDAN1F:2
for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (i,j)),(G * (i,k))) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (i,n)) `2 = upper_bound (proj2 .: ((LSeg ((G * (i,j)),(G * (i,k)))) /\ (L~ f))) )
proof end;

theorem :: JORDAN1F:3
for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (n,i)) `1 = lower_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
proof end;

theorem :: JORDAN1F:4
for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg ((G * (j,i)),(G * (k,i))) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * (n,i)) `1 = upper_bound (proj1 .: ((LSeg ((G * (j,i)),(G * (k,i)))) /\ (L~ f))) )
proof end;

theorem Th5: :: JORDAN1F:5
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n)))
proof end;

theorem Th6: :: JORDAN1F:6
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Lower_Seq (C,n)) /. 1 = E-max (L~ (Cage (C,n)))
proof end;

theorem Th7: :: JORDAN1F:7
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
proof end;

theorem Th8: :: JORDAN1F:8
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = W-min (L~ (Cage (C,n)))
proof end;

theorem Th9: :: JORDAN1F:9
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( ( L~ (Upper_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) ) or ( L~ (Upper_Seq (C,n)) = Lower_Arc (L~ (Cage (C,n))) & L~ (Lower_Seq (C,n)) = Upper_Arc (L~ (Cage (C,n))) ) )
proof end;

theorem Th10: :: JORDAN1F:10
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Upper_Seq (C,n) is_sequence_on Gauge (C,n)
proof end;

theorem Th11: :: JORDAN1F:11
for G being Go-board
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st
( [i,j] in Indices G & p = G * (i,j) ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * (i1,j1) & f /. 1 = G * (i2,j2) holds
|.(i2 - i1).| + |.(j2 - j1).| = 1 ) holds
<*p*> ^ f is_sequence_on G
proof end;

theorem Th12: :: JORDAN1F:12
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
proof end;

theorem :: JORDAN1F:13
for i being Nat
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,1)) * ((Center (Gauge (C,1))),(width (Gauge (C,1))))))) /\ (Upper_Arc (L~ (Cage (C,(i + 1))))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,(i + 1))) & p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),j) )
proof end;