environ vocabulary PRE_TOPC, SEQM_3, GOBOARD5, ARYTM_3, EUCLID, MCART_1, RELAT_1, SUBSET_1, TOPREAL1, FINSEQ_1, GOBOARD2, TREES_1, TOPS_1, BOOLE, CONNSP_3, RELAT_2, GOBOARD9, CONNSP_1, TARSKI, MATRIX_1, ARYTM_1, GOBRD10, FUNCT_1, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, TOPREAL1, GOBOARD1, NUMBERS, XREAL_0, STRUCT_0, REAL_1, NAT_1, BINARITH, PRE_TOPC, FUNCT_1, FINSEQ_1, FINSEQ_4, MATRIX_1, TOPS_1, CONNSP_1, EUCLID, GOBOARD2, GOBOARD5, GOBOARD9, CONNSP_3, GOBRD10; constructors REAL_1, BINARITH, TOPS_1, CONNSP_1, GOBOARD2, GOBOARD9, CONNSP_3, GOBRD10, FINSEQ_4, MEMBERED; clusters SUBSET_1, GOBOARD5, RELSET_1, PRE_TOPC, GOBOARD2, EUCLID, XREAL_0, GOBRD11, NAT_1, MEMBERED; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin reserve i,j,k,k1,k2,i1,i2,j1,j2 for Nat, r,s for Real, x for set, f for non constant standard special_circular_sequence; canceled; theorem :: GOBRD12:2 for i,j st i<=len GoB f & j<=width GoB f holds Int cell(GoB f,i,j)c=(L~f)`; theorem :: GOBRD12:3 for i,j st i<=len GoB f & j<=width GoB f holds Cl Down(Int cell(GoB f,i,j),(L~f)`)=cell(GoB f,i,j)/\((L~f)`); theorem :: GOBRD12:4 for i,j st i<=len GoB f & j<=width GoB f holds Cl Down(Int cell(GoB f,i,j),(L~f)`) is connected & Down(Int cell(GoB f,i,j),(L~f)`)=Int cell(GoB f,i,j); theorem :: GOBRD12:5 (L~f)`=union {Cl Down(Int cell(GoB f,i,j),(L~f)`): i<=len GoB f & j<=width GoB f}; theorem :: GOBRD12:6 Down(LeftComp f,(L~f)`) \/ Down(RightComp f,(L~f)`) is a_union_of_components of (TOP-REAL 2)|((L~f)`) & Down(LeftComp f,(L~f)`)=LeftComp f & Down(RightComp f,(L~f)`)=RightComp f; theorem :: GOBRD12:7 for i1,j1,i2,j2 st i1<=len GoB f & j1<=width GoB f & i2<=len GoB f & j2<=width GoB f & i1,j1,i2,j2 are_adjacent2 holds Int cell(GoB f,i1,j1) c= LeftComp f \/ RightComp f iff Int cell(GoB f,i2,j2) c= LeftComp f \/ RightComp f; theorem :: GOBRD12:8 for F1,F2 being FinSequence of NAT st len F1=len F2 & (ex i st i in dom F1 & Int cell(GoB f,F1/.i,F2/.i) c=LeftComp f \/ RightComp f)& (for i st 1<=i & i<len F1 holds F1/.i,F2/.i,F1/.(i+1),F2/.(i+1) are_adjacent2)& (for i,k1,k2 st i in dom F1 & k1=F1.i & k2=F2.i holds k1<=len GoB f & k2<=width GoB f) holds (for i st i in dom F1 holds Int cell(GoB f,F1/.i,F2/.i)c=LeftComp f \/ RightComp f); theorem :: GOBRD12:9 ex i,j st i<=len GoB f & j<=width GoB f & Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f; theorem :: GOBRD12:10 for i,j st i<=len GoB f & j<=width GoB f holds Int cell(GoB f,i,j) c= LeftComp f \/ RightComp f; theorem :: GOBRD12:11 (L~f)`=LeftComp f \/ RightComp f;