Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Some Properties of Cells on Go Board

**by****Czeslaw Bylinski**- Received April 23, 1999
- MML identifier: GOBRD13

- [ Mizar article, MML identifier index ]

environ vocabulary FINSEQ_1, FINSEQ_2, EUCLID, FUNCT_1, PROB_1, FUNCT_6, RELAT_1, MATRLIN, PRALG_1, TARSKI, FINSET_1, MATRIX_1, TREES_1, CARD_1, CARD_2, GOBOARD1, MCART_1, ARYTM_1, GOBOARD5, GOBOARD2, PRE_TOPC, BOOLE, TOPREAL1, ABSVALUE, RFINSEQ, GOBRD13, FINSEQ_4; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, REAL_1, NAT_1, BINARITH, ABSVALUE, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, CARD_1, CARD_2, FINSEQ_1, FINSEQ_2, MATRLIN, PRALG_1, FINSEQ_4, FINSET_1, PROB_1, FUNCT_6, RFINSEQ, MATRIX_1, PRE_TOPC, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5; constructors REAL_1, ABSVALUE, RFINSEQ, SEQM_3, BINARITH, CARD_2, GOBOARD2, GOBOARD5, PRALG_1, MATRLIN, WELLORD2, PROB_1, MEMBERED; clusters STRUCT_0, RELSET_1, EUCLID, GOBOARD2, GOBOARD5, FINSEQ_1, CARD_1, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; begin reserve i,i1,i2,i',i1',j,j1,j2,j',j1',k,k1,k2,l,m,n for Nat; reserve r,s,r',s' for Real; reserve D for non empty set, f for FinSequence of D; definition let E be non empty set; let S be FinSequence-DOMAIN of the carrier of TOP-REAL 2; let F be Function of E,S; let e be Element of E; redefine func F.e -> FinSequence of TOP-REAL 2; end; definition let F be Function; func Values F -> set equals :: GOBRD13:def 1 Union rngs F; end; theorem :: GOBRD13:1 for M being FinSequence of D* holds M.i is FinSequence of D; definition let D be set; cluster -> FinSequence-yielding FinSequence of D*; end; definition cluster FinSequence-yielding -> Function-yielding Function; end; canceled; theorem :: GOBRD13:3 for M being FinSequence of D* holds Values M = union {rng f where f is Element of D*: f in rng M}; definition let D be non empty set, M be FinSequence of D*; cluster Values M -> finite; end; theorem :: GOBRD13:4 for M being Matrix of D st i in dom M & M.i = f holds len f = width M; theorem :: GOBRD13:5 for M being Matrix of D st i in dom M & M.i = f & j in dom f holds [i,j] in Indices M; theorem :: GOBRD13:6 for M being Matrix of D st [i,j] in Indices M & M.i = f holds len f = width M & j in dom f; theorem :: GOBRD13:7 for M being Matrix of D holds Values M = { M*(i,j): [i,j] in Indices M }; theorem :: GOBRD13:8 for D being non empty set, M being Matrix of D holds card Values M <= (len M)*(width M); reserve f for FinSequence of TOP-REAL 2, G for Go-board; theorem :: GOBRD13:9 for G being Matrix of TOP-REAL 2 holds f is_sequence_on G implies rng f c= Values G; theorem :: GOBRD13:10 for G1,G2 being 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; theorem :: GOBRD13:11 for G1,G2 being 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; theorem :: GOBRD13:12 for G1,G2 being 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; theorem :: GOBRD13:13 for G1,G2 being 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; theorem :: GOBRD13:14 for G1,G2 being 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; theorem :: GOBRD13:15 for G1,G2 being 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; theorem :: GOBRD13:16 for G1,G2 being 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; theorem :: GOBRD13:17 for G1,G2 being 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; theorem :: GOBRD13:18 for G1,G2 being 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); theorem :: GOBRD13:19 for G1,G2 being 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); theorem :: GOBRD13:20 for G1,G2 being 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); theorem :: GOBRD13:21 for f being standard special_circular_sequence st f is_sequence_on G holds Values GoB f c= Values G; definition let f, G, k; assume that 1 <= k & k+1 <= len f and f is_sequence_on G; func right_cell(f,k,G) -> Subset of TOP-REAL 2 means :: GOBRD13:def 2 for i1,j1,i2,j2 being 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); func left_cell(f,k,G) -> Subset of TOP-REAL 2 means :: GOBRD13:def 3 for i1,j1,i2,j2 being 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); end; theorem :: GOBRD13:22 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); theorem :: GOBRD13:23 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); theorem :: GOBRD13:24 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); theorem :: GOBRD13:25 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); theorem :: GOBRD13:26 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); theorem :: GOBRD13:27 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); theorem :: GOBRD13:28 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); theorem :: GOBRD13:29 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); theorem :: GOBRD13:30 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); theorem :: GOBRD13:31 1 <= k & k+1 <= len f & f is_sequence_on G implies right_cell(f,k,G) is closed; theorem :: GOBRD13:32 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); theorem :: GOBRD13:33 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); theorem :: GOBRD13:34 for G being Go-board, f being 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); definition let f,G,k; assume that 1 <= k & k+1 <= len f and f is_sequence_on G; func front_right_cell(f,k,G) -> Subset of TOP-REAL 2 means :: GOBRD13:def 4 for i1,j1,i2,j2 being 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); func front_left_cell(f,k,G) -> Subset of TOP-REAL 2 means :: GOBRD13:def 5 for i1,j1,i2,j2 being 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); 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_left_cell(f,k,G) = cell(G,i-'1,j+1); theorem :: GOBRD13:36 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); 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_left_cell(f,k,G) = cell(G,i+1,j); 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,j) & f/.(k+1) = G*(i+1,j) implies front_right_cell(f,k,G) = cell(G,i+1,j-'1); 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_left_cell(f,k,G) = cell(G,i-'1,j-'1); theorem :: GOBRD13:40 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); 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_left_cell(f,k,G) = cell(G,i,j-'1); theorem :: GOBRD13:42 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); theorem :: GOBRD13:43 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); definition let D be set; let f be FinSequence of D, G be (Matrix of D), k; pred f turns_right k,G means :: GOBRD13:def 6 for i1,j1,i2,j2 being 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); pred f turns_left k,G means :: GOBRD13:def 7 for i1,j1,i2,j2 being 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); pred f goes_straight k,G means :: GOBRD13:def 8 for i1,j1,i2,j2 being 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:44 1 <= k & k+2 <= len f & k+2 <= n & f|n turns_right k,G implies f turns_right k,G; theorem :: GOBRD13:45 1 <= k & k+2 <= len f & k+2 <= n & f|n turns_left k,G implies f turns_left k,G; theorem :: GOBRD13:46 1 <= k & k+2 <= len f & k+2 <= n & f|n goes_straight k,G implies f goes_straight k,G; theorem :: GOBRD13:47 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); theorem :: GOBRD13:48 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); theorem :: GOBRD13:49 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); theorem :: GOBRD13:50 for D being non empty set, M being Matrix of D st 1 <= i & i <= len M & 1 <= j & j <= width M holds M*(i,j) in Values M;

Back to top