:: More on the Finite Sequences on the Plane
:: by Andrzej Trybulec
::
:: Received October 25, 2001
:: Copyright (c) 2001-2018 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, TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, GOBOARD1, SUBSET_1,
FINSEQ_1, ARYTM_3, XXREAL_0, FINSEQ_6, RELAT_1, PARTFUN1, FINSEQ_4,
CARD_1, ORDINAL4, RFINSEQ, NAT_1, GRAPH_2, MATRIX_1, ARYTM_1, FINSEQ_5,
EUCLID, RLTOPSP1, TOPREAL1, GOBOARD5, STRUCT_0, MCART_1, SETFAM_1,
PRE_TOPC;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1,
NAT_D, SETFAM_1, FUNCT_1, PARTFUN1, FINSEQ_5, FINSEQ_6, RFINSEQ, GRAPH_2,
MATRIX_0, RELSET_1, FINSEQ_1, ZFMISC_1, STRUCT_0, PRE_TOPC, RLTOPSP1,
EUCLID, TOPREAL1, GOBOARD1, GOBOARD5, FINSEQ_4, XXREAL_0;
constructors SETFAM_1, REAL_1, FINSEQ_4, RFINSEQ, NAT_D, FINSEQ_5, REALSET2,
GOBOARD1, GOBOARD5, GRAPH_2, SPRECT_1, RELSET_1;
registrations XBOOLE_0, ORDINAL1, XXREAL_0, XREAL_0, NAT_1, INT_1, FINSEQ_1,
FINSEQ_5, FINSEQ_6, STRUCT_0, SPPOL_2, GOBOARD9, SPRECT_1, REVROT_1,
CARD_1, FUNCT_1, RELAT_1, EUCLID;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
theorem :: TOPREAL8:1
for A,x,y being set st A c= {x,y} & x in A & not y in A holds A = {x};
registration
cluster trivial for Function;
end;
begin :: FinSequences
reserve G for Go-board,
i,j,k,m,n for Nat;
registration
cluster non constant for FinSequence;
end;
theorem :: TOPREAL8:2
for f being non trivial FinSequence holds 1 < len f;
theorem :: TOPREAL8:3
for D being non trivial set for f being non constant circular
FinSequence of D holds len f > 2;
theorem :: TOPREAL8:4
for f being FinSequence, x being set holds x in rng f or x..f = 0;
theorem :: TOPREAL8:5
for p being set, D being non empty set for f being non empty
FinSequence of D for g being FinSequence of D st p..f = len f holds (f^g)|--p =
g;
theorem :: TOPREAL8:6
for D being non empty set for f being non empty one-to-one
FinSequence of D holds f/.len f..f = len f;
theorem :: TOPREAL8:7
for f,g being FinSequence holds len f <= len(f^'g);
theorem :: TOPREAL8:8
for f,g being FinSequence for x being set st x in rng f holds x..
f = x..(f^'g);
theorem :: TOPREAL8:9
for f being non empty FinSequence for g being FinSequence holds len g
<= len(f^'g);
theorem :: TOPREAL8:10
for f,g being FinSequence holds rng f c= rng(f^'g);
theorem :: TOPREAL8:11
for D being non empty set for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g/.len g = f/.1 holds f^'g is
circular;
theorem :: TOPREAL8:12
for D being non empty set for M being Matrix of D for f being
FinSequence of D for g being non empty FinSequence of D st f/.len f = g/.1 & f
is_sequence_on M & g is_sequence_on M holds f^'g is_sequence_on M;
theorem :: TOPREAL8:13
for D being set, f being FinSequence of D st 1 <= k holds (k+1,
len f)-cut f = f/^k;
theorem :: TOPREAL8:14
for D being set, f being FinSequence of D st k <= len f holds (1
, k)-cut f = f|k;
theorem :: TOPREAL8:15
for p being set, D being non empty set for f being non empty
FinSequence of D for g being FinSequence of D st p..f = len f holds (f^g)-|p =
(1,len f -' 1)-cut f;
theorem :: TOPREAL8:16
for D being non empty set for f,g being non empty FinSequence of
D st g/.1..f = len f holds (f^'g:-g/.1) = g;
theorem :: TOPREAL8:17
for D being non empty set for f,g being non empty FinSequence of
D st g/.1..f = len f holds (f^'g-:g/.1) = f;
theorem :: TOPREAL8:18
for D being non trivial set for f being non empty FinSequence of
D for g being non trivial FinSequence of D st g/.1 = f/.len f & for i st 1 <= i
& i < len f holds f/.i <> g/.1 holds Rotate(f^'g,g/.1) = g^'f;
begin :: TOP-REAL
theorem :: TOPREAL8:19
for f being non trivial FinSequence of TOP-REAL 2 holds LSeg(f,1 ) = L~(f|2);
theorem :: TOPREAL8:20
for f being s.c.c. FinSequence of TOP-REAL 2, n st n < len f
holds f|n is s.n.c.;
theorem :: TOPREAL8:21
for f being s.c.c. FinSequence of TOP-REAL 2, n st 1 <= n holds
f/^n is s.n.c.;
theorem :: TOPREAL8:22
for f being circular s.c.c. FinSequence of TOP-REAL 2, n st n <
len f & len f > 4 holds f|n is one-to-one;
theorem :: TOPREAL8:23
for f being circular s.c.c. FinSequence of TOP-REAL 2 st len f >
4 for i,j being Nat st 1 < i & i < j & j <= len f holds f/.i <> f/.j;
theorem :: TOPREAL8:24
for f being circular s.c.c. FinSequence of TOP-REAL 2, n st 1 <=
n & len f > 4 holds f/^n is one-to-one;
theorem :: TOPREAL8:25
for f being special non empty FinSequence of TOP-REAL 2 holds (m
,n)-cut f is special;
theorem :: TOPREAL8:26
for f being special non empty FinSequence of TOP-REAL 2 for g
being special non trivial FinSequence of TOP-REAL 2 st f/.len f = g/.1 holds f
^'g is special;
theorem :: TOPREAL8:27
for f being circular unfolded s.c.c. FinSequence of TOP-REAL 2
st len f > 4 holds LSeg(f,1) /\ L~(f/^1) = {f/.1,f/.2};
theorem :: TOPREAL8:28
for f,g being FinSequence of TOP-REAL 2 st j < len f holds LSeg(
f^'g,j) = LSeg(f,j);
theorem :: TOPREAL8:29
for f,g being non empty FinSequence of TOP-REAL 2 st 1 <= j & j+
1 < len g holds LSeg(f^'g,len f+j) = LSeg(g,j+1);
theorem :: TOPREAL8:30
for f being non empty FinSequence of TOP-REAL 2 for g being non
trivial FinSequence of TOP-REAL 2 st f/.len f = g/.1 holds LSeg(f^'g,len f) =
LSeg(g,1);
theorem :: TOPREAL8:31
for f being non empty FinSequence of TOP-REAL 2 for g being non
trivial FinSequence of TOP-REAL 2 st j+1 < len g & f/.len f = g/.1 holds LSeg(f
^'g,len f+j) = LSeg(g,j+1);
theorem :: TOPREAL8:32
for f being non empty s.n.c. unfolded FinSequence of TOP-REAL 2,
i st 1 <= i & i < len f holds LSeg(f,i) /\ rng f = {f/.i,f/.(i+1)};
theorem :: TOPREAL8:33
for f,g being non trivial s.n.c. one-to-one unfolded FinSequence
of TOP-REAL 2 st L~f /\ L~g = {f/.1,g/.1} & f/.1 = g/.len g & g/.1 = f/.len f
holds f ^' g is s.c.c.;
reserve f,g,g1,g2 for FinSequence of TOP-REAL 2;
theorem :: TOPREAL8:34
f is unfolded & g is unfolded & f/.len f = g/.1 & LSeg(f,len f
-' 1) /\ LSeg(g,1) = { f/.len f } implies f^'g is unfolded;
theorem :: TOPREAL8:35
f is non empty & g is non trivial & f/.len f = g/.1 implies L~(f
^'g) = L~f \/ L~g;
theorem :: TOPREAL8:36
(for n be Nat st n in dom f ex i,j be Nat st [i,j] in Indices G & f/.n
=G*(i,j)) & f is non constant circular unfolded s.c.c. special & len f > 4
implies ex g st g is_sequence_on G & g is unfolded s.c.c. special & L~f = L~g &
f/.1 = g/.1 & f/.len f = g/.len g & len f <= len g;