:: Introduction to Go-Board - Part II. Go-Board Determined by Finite Sequence of point from ${\calE}^2_{\rm T}$ :: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura :: :: Received August 24, 1992 :: Copyright (c) 1992-2012 Association of Mizar Users begin theorem :: GOBOARD2:1 for f being FinSequence of (TOP-REAL 2) st ( for n, m being Element of NAT st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds LSeg (f,n) misses LSeg (f,m) ) holds f is s.n.c. proofend; theorem :: GOBOARD2:2 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg (f,i) & i in dom f & i + 1 in dom f holds i + 1 = len f proofend; theorem Th3: :: GOBOARD2:3 for f being FinSequence of (TOP-REAL 2) for k being Element of NAT st k <> 0 & len f = k + 1 holds L~ f = (L~ (f | k)) \/ (LSeg (f,k)) proofend; theorem :: GOBOARD2:4 for f being FinSequence of (TOP-REAL 2) for k being Element of NAT st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds (L~ (f | k)) /\ (LSeg (f,k)) = {(f /. k)} proofend; theorem :: GOBOARD2:5 for f1, f2 being FinSequence of (TOP-REAL 2) for n, m being Element of NAT st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds LSeg ((f1 ^ f2),n) = LSeg (f2,m) proofend; theorem Th6: :: GOBOARD2:6 for f, g being FinSequence of (TOP-REAL 2) holds L~ f c= L~ (f ^ g) proofend; theorem :: GOBOARD2:7 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st f is s.n.c. holds f | i is s.n.c. proofend; theorem :: GOBOARD2:8 for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) holds f1 ^ f2 is special proofend; theorem Th9: :: GOBOARD2:9 for f being FinSequence of (TOP-REAL 2) st f <> {} holds X_axis f <> {} proofend; theorem Th10: :: GOBOARD2:10 for f being FinSequence of (TOP-REAL 2) st f <> {} holds Y_axis f <> {} proofend; registration let f be non empty FinSequence of (TOP-REAL 2); cluster X_axis f -> non empty ; coherence not X_axis f is empty by Th9; cluster Y_axis f -> non empty ; coherence not Y_axis f is empty by Th10; end; theorem Th11: :: GOBOARD2:11 for f being FinSequence of (TOP-REAL 2) for G being Go-board st f is special holds for n being Element of NAT st n in dom f & n + 1 in dom f holds for i, j, m, k being Element of NAT st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * (i,j) & f /. (n + 1) = G * (m,k) & not i = m holds k = j proofend; theorem :: GOBOARD2:12 for f being FinSequence of (TOP-REAL 2) for G being Go-board st ( for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being Element of NAT st n in dom f & n + 1 in dom f holds f /. n <> f /. (n + 1) ) holds ex g being FinSequence of (TOP-REAL 2) st ( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g ) proofend; definition let v1, v2 be FinSequence of REAL ; assume A1: v1 <> {} ; func GoB (v1,v2) -> Matrix of (TOP-REAL 2) means :Def1: :: GOBOARD2:def 1 ( len it = len v1 & width it = len v2 & ( for n, m being Element of NAT st [n,m] in Indices it holds it * (n,m) = |[(v1 . n),(v2 . m)]| ) ); existence ex b1 being Matrix of (TOP-REAL 2) st ( len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) ) proofend; uniqueness for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds b1 * (n,m) = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b2 holds b2 * (n,m) = |[(v1 . n),(v2 . m)]| ) holds b1 = b2 proofend; end; :: deftheorem Def1 defines GoB GOBOARD2:def_1_:_ for v1, v2 being FinSequence of REAL st v1 <> {} holds for b3 being Matrix of (TOP-REAL 2) holds ( b3 = GoB (v1,v2) iff ( len b3 = len v1 & width b3 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b3 holds b3 * (n,m) = |[(v1 . n),(v2 . m)]| ) ) ); registration let v1, v2 be non empty FinSequence of REAL ; cluster GoB (v1,v2) -> V3() X_equal-in-line Y_equal-in-column ; coherence ( not GoB (v1,v2) is empty-yielding & GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column ) proofend; end; registration let v1, v2 be non empty increasing FinSequence of REAL ; cluster GoB (v1,v2) -> Y_increasing-in-line X_increasing-in-column ; coherence ( GoB (v1,v2) is Y_increasing-in-line & GoB (v1,v2) is X_increasing-in-column ) proofend; end; definition let f be non empty FinSequence of (TOP-REAL 2); func GoB f -> Matrix of (TOP-REAL 2) equals :: GOBOARD2:def 2 GoB ((Incr (X_axis f)),(Incr (Y_axis f))); correctness coherence GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Matrix of (TOP-REAL 2); ; end; :: deftheorem defines GoB GOBOARD2:def_2_:_ for f being non empty FinSequence of (TOP-REAL 2) holds GoB f = GoB ((Incr (X_axis f)),(Incr (Y_axis f))); registration let f be non empty FinSequence of (TOP-REAL 2); cluster GoB f -> V3() X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ; coherence ( not GoB f is empty-yielding & GoB f is X_equal-in-line & GoB f is Y_equal-in-column & GoB f is Y_increasing-in-line & GoB f is X_increasing-in-column ) ; end; theorem Th13: :: GOBOARD2:13 for f being non empty FinSequence of (TOP-REAL 2) holds ( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) ) proofend; theorem :: GOBOARD2:14 for f being non empty FinSequence of (TOP-REAL 2) for n being Element of NAT st n in dom f holds ex i, j being Element of NAT st ( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) ) proofend; theorem :: GOBOARD2:15 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . n <= (X_axis f) . m ) holds f /. n in rng (Line ((GoB f),1)) proofend; theorem :: GOBOARD2:16 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (X_axis f) . m <= (X_axis f) . n ) holds f /. n in rng (Line ((GoB f),(len (GoB f)))) proofend; theorem :: GOBOARD2:17 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . n <= (Y_axis f) . m ) holds f /. n in rng (Col ((GoB f),1)) proofend; theorem :: GOBOARD2:18 for n being Element of NAT for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Element of NAT st m in dom f holds (Y_axis f) . m <= (Y_axis f) . n ) holds f /. n in rng (Col ((GoB f),(width (GoB f)))) proofend;