:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura

::

:: Received August 24, 1992

:: Copyright (c) 1992-2017 Association of Mizar Users

theorem :: GOBOARD2:1

for f being FinSequence of (TOP-REAL 2) st ( for n, m being 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.

LSeg (f,n) misses LSeg (f,m) ) holds

f is s.n.c.

proof end;

theorem :: GOBOARD2:2

for f being FinSequence of (TOP-REAL 2)

for i being 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

for i being 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

proof end;

theorem Th3: :: GOBOARD2:3

for f being FinSequence of (TOP-REAL 2)

for k being Nat st k <> 0 & len f = k + 1 holds

L~ f = (L~ (f | k)) \/ (LSeg (f,k))

for k being Nat st k <> 0 & len f = k + 1 holds

L~ f = (L~ (f | k)) \/ (LSeg (f,k))

proof end;

theorem :: GOBOARD2:4

for f being FinSequence of (TOP-REAL 2)

for k being 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)}

for k being 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)}

proof end;

theorem :: GOBOARD2:5

for f1, f2 being FinSequence of (TOP-REAL 2)

for n, m being Nat st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds

LSeg ((f1 ^ f2),n) = LSeg (f2,m)

for n, m being Nat st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds

LSeg ((f1 ^ f2),n) = LSeg (f2,m)

proof end;

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

f1 ^ f2 is special

proof end;

registration

let f be non empty FinSequence of (TOP-REAL 2);

coherence

not X_axis f is empty by Th9;

coherence

not Y_axis f is empty by Th10;

end;
coherence

not X_axis f is empty by Th9;

coherence

not Y_axis f is empty by Th10;

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 Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being 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

for G being Go-board st f is special holds

for n being Nat st n in dom f & n + 1 in dom f holds

for i, j, m, k being 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

proof end;

theorem :: GOBOARD2:12

for f being FinSequence of (TOP-REAL 2)

for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being 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 )

for G being Go-board st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is special & ( for n being 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 )

proof end;

definition

let v1, v2 be FinSequence of REAL ;

assume A1: v1 <> {} ;

ex b_{1} being Matrix of (TOP-REAL 2) st

( len b_{1} = len v1 & width b_{1} = len v2 & ( for n, m being Nat st [n,m] in Indices b_{1} holds

b_{1} * (n,m) = |[(v1 . n),(v2 . m)]| ) )

for b_{1}, b_{2} being Matrix of (TOP-REAL 2) st len b_{1} = len v1 & width b_{1} = len v2 & ( for n, m being Nat st [n,m] in Indices b_{1} holds

b_{1} * (n,m) = |[(v1 . n),(v2 . m)]| ) & len b_{2} = len v1 & width b_{2} = len v2 & ( for n, m being Nat st [n,m] in Indices b_{2} holds

b_{2} * (n,m) = |[(v1 . n),(v2 . m)]| ) holds

b_{1} = b_{2}

end;
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 Nat st [n,m] in Indices it holds

it * (n,m) = |[(v1 . n),(v2 . m)]| ) );

existence ( len it = len v1 & width it = len v2 & ( for n, m being Nat st [n,m] in Indices it holds

it * (n,m) = |[(v1 . n),(v2 . m)]| ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines GoB GOBOARD2:def 1 :

for v1, v2 being FinSequence of REAL st v1 <> {} holds

for b_{3} being Matrix of (TOP-REAL 2) holds

( b_{3} = GoB (v1,v2) iff ( len b_{3} = len v1 & width b_{3} = len v2 & ( for n, m being Nat st [n,m] in Indices b_{3} holds

b_{3} * (n,m) = |[(v1 . n),(v2 . m)]| ) ) );

for v1, v2 being FinSequence of REAL st v1 <> {} holds

for b

( b

b

registration

let v1, v2 be non empty FinSequence of REAL ;

coherence

( not GoB (v1,v2) is empty-yielding & GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column )

end;
coherence

( not GoB (v1,v2) is empty-yielding & GoB (v1,v2) is X_equal-in-line & GoB (v1,v2) is Y_equal-in-column )

proof end;

registration

let v1, v2 be non empty increasing FinSequence of REAL ;

coherence

( GoB (v1,v2) is Y_increasing-in-line & GoB (v1,v2) is X_increasing-in-column )

end;
coherence

( GoB (v1,v2) is Y_increasing-in-line & GoB (v1,v2) is X_increasing-in-column )

proof end;

definition

let f be non empty FinSequence of (TOP-REAL 2);

coherence

GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Matrix of (TOP-REAL 2);

;

end;
func GoB f -> Matrix of (TOP-REAL 2) equals :: GOBOARD2:def 2

GoB ((Incr (X_axis f)),(Incr (Y_axis f)));

correctness GoB ((Incr (X_axis f)),(Incr (Y_axis f)));

coherence

GoB ((Incr (X_axis f)),(Incr (Y_axis f))) is Matrix of (TOP-REAL 2);

;

:: 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)));

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);

( 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;
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 ) ;

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)) )

( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) )

proof end;

theorem :: GOBOARD2:14

for f being non empty FinSequence of (TOP-REAL 2)

for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices (GoB f) & f /. n = (GoB f) * (i,j) )

proof end;

theorem :: GOBOARD2:15

for n being Nat

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds

(X_axis f) . n <= (X_axis f) . m ) holds

f /. n in rng (Line ((GoB f),1))

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds

(X_axis f) . n <= (X_axis f) . m ) holds

f /. n in rng (Line ((GoB f),1))

proof end;

theorem :: GOBOARD2:16

for n being Nat

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being 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))))

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being 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))))

proof end;

theorem :: GOBOARD2:17

for n being Nat

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds

(Y_axis f) . n <= (Y_axis f) . m ) holds

f /. n in rng (Col ((GoB f),1))

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds

(Y_axis f) . n <= (Y_axis f) . m ) holds

f /. n in rng (Col ((GoB f),1))

proof end;

theorem :: GOBOARD2:18

for n being Nat

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being 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))))

for f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being 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))))

proof end;