:: Go-Board Theorem :: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura :: :: Received August 24, 1992 :: Copyright (c) 1992-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, PRE_TOPC, EUCLID, SUBSET_1, FINSEQ_1, GOBOARD1, XXREAL_0, PARTFUN1, RELAT_1, INCSP_1, MATRIX_1, TREES_1, XBOOLE_0, CARD_1, ARYTM_3, NAT_1, TARSKI, FUNCT_1, ARYTM_1, ZFMISC_1, COMPLEX1, ORDINAL4, TOPREAL1, REAL_1, XXREAL_1, GOBOARD2, MCART_1, TOPREAL4, GOBOARD4; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, REAL_1, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, MATRIX_0, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, TOPREAL4, GOBOARD1, GOBOARD2; constructors XXREAL_1, COMPLEX1, FINSEQ_3, TOPREAL1, TOPREAL4, GOBOARD2, GOBOARD1, RELSET_1, REAL_1, MATRIX_1; registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0, EUCLID, GOBOARD2, VALUED_0, CARD_1, GOBOARD1, NAT_1, INT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve p,p1,p2,q1,q2 for Point of TOP-REAL 2, P1,P2 for Subset of TOP-REAL 2, f,f1,f2,g1,g2 for FinSequence of TOP-REAL 2, n,m,i,j,k for Nat, G,G1 for Go-board, x,y for set; theorem :: GOBOARD4:1 for G,f1,f2 st 1<=len f1 & 1<=len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) & f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds rng f1 meets rng f2; theorem :: GOBOARD4:2 for G,f1,f2 st 2<=len f1 & 2<=len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) & f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds L~f1 meets L~f2; theorem :: GOBOARD4:3 for G,f1,f2 st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2 is_sequence_on G & f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) & f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds L~f1 meets L~f2; definition let f be Relation, r,s be Real; pred f lies_between r,s means :: GOBOARD4:def 1 rng f c= [. r,s .]; end; definition let f be FinSequence of REAL, r,s be Real; redefine pred f lies_between r,s means :: GOBOARD4:def 2 for n st n in dom f holds r <= f.n & f.n <= s; end; theorem :: GOBOARD4:4 for f1,f2 being FinSequence of TOP-REAL 2 st 2<=len f1 & 2<=len f2 & f1 is special & f2 is special & (for n st n in dom f1 & n+1 in dom f1 holds f1/.n <> f1/.(n+1)) & (for n st n in dom f2 & n+1 in dom f2 holds f2/.n <> f2/.(n+1)) & X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) & Y_axis(f2) lies_between ( Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds L~f1 meets L~f2; theorem :: GOBOARD4:5 for f1,f2 being FinSequence of TOP-REAL 2 st f1 is one-to-one special & 2 <= len f1 & f2 is one-to-one special & 2 <= len f2 & X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & X_axis(f2) lies_between ( X_axis(f1)).1, (X_axis(f1)).(len f1) & Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) & Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).( len f2) holds L~f1 meets L~f2; theorem :: GOBOARD4:6 for P1,P2,p1,p2,q1,q2 st P1 is_S-P_arc_joining p1,q1 & P2 is_S-P_arc_joining p2,q2 & (for p st p in P1 \/ P2 holds p1`1<=p`1 & p`1<=q1`1) & (for p st p in P1 \/ P2 holds p2`2<=p`2 & p`2<=q2`2) holds P1 meets P2;