Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
The abstract of the Mizar article:
-
- 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