:: Some Properties of Cells on Go Board :: by Czes{\l}aw Byli\'nski :: :: Received April 23, 1999 :: Copyright (c) 1999-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, XBOOLE_0, FINSEQ_1, EUCLID, FUNCT_1, RELAT_1, TARSKI, NAT_1, MATRIX_1, TREES_1, XXREAL_0, CARD_1, GOBOARD1, PARTFUN1, ARYTM_3, MCART_1, ARYTM_1, GOBOARD5, GOBOARD2, PRE_TOPC, RLTOPSP1, COMPLEX1, RCOMP_1, RFINSEQ, ORDINAL4, GOBRD13; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, COMPLEX1, NAT_D, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, RFINSEQ, XXREAL_0, SEQ_4, STRUCT_0, MATRIX_0, MATRIX_1, PRE_TOPC, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5; constructors RFINSEQ, NAT_D, GOBOARD2, GOBOARD5, REAL_1, GOBOARD1, RELSET_1, SEQ_4, RVSUM_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, GOBOARD5, VALUED_0, SEQ_4, NAT_1, MATRIX_0; requirements NUMERALS, REAL, SUBSET, ARITHM; 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; ::$CT 7 theorem :: GOBRD13:8 for G being Matrix of TOP-REAL 2 holds f is_sequence_on G implies rng f c= Values G; theorem :: GOBRD13:9 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: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*(len G2,j2) holds i1 = len G1; theorem :: GOBRD13:11 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: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,width G2) holds j1 = width G1; theorem :: GOBRD13:13 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:14 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:15 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:16 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:17 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: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-' 1,j2) c= cell(G1,i1-'1,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, j2-'1) c= cell(G1,i1,j1-'1); theorem :: GOBRD13:20 for f being standard special_circular_sequence st f is_sequence_on G holds Values GoB f c= Values G; definition ::$CD let f, G, k; assume 1 <= k & k+1 <= len f & 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:21 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: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 right_cell(f,k,G) = cell(G,i,j); theorem :: GOBRD13:23 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: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 right_cell(f,k,G) = cell(G,i,j-'1); 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+1,j) & f/.(k+1) = G*(i,j) implies left_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 right_cell(f,k,G) = cell(G,i,j); theorem :: GOBRD13:27 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: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 right_cell(f,k,G) = cell(G,i-'1,j); 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); theorem :: GOBRD13:30 1 <= k & k+1 <= len f & f is_sequence_on G implies right_cell(f,k,G) is closed; 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) ; 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); theorem :: GOBRD13:33 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 1 <= k & k+1 <= len f & 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: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); 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); 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); 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); 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); 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); 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); 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); 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); 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:43 1 <= k & k+2 <= n & f|n turns_right k,G implies f turns_right k,G; theorem :: GOBRD13:44 1 <= k & k+2 <= n & f|n turns_left k,G implies f turns_left k,G; theorem :: GOBRD13:45 1 <= k & k+2 <= n & f|n goes_straight k,G implies f goes_straight k,G; 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 ); 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); 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);