Volume 13, 2001

University of Bialystok

Copyright (c) 2001 Association of Mizar Users

### The abstract of the Mizar article:

### More on the Finite Sequences on the Plane

**by****Andrzej Trybulec**- Received October 25, 2001
- MML identifier: TOPREAL8

- [ Mizar article, MML identifier index ]

environ vocabulary GOBOARD5, GOBOARD1, BOOLE, JORDAN1E, FINSEQ_5, RFINSEQ, FINSEQ_1, RELAT_1, GRAPH_2, REALSET1, FINSEQ_4, FINSEQ_6, MATRIX_1, FUNCT_1, TOPREAL1, EUCLID, SEQM_3, RLSUB_2, ARYTM_1, PRE_TOPC, ABSVALUE, COMPTS_1, SPPOL_1, MCART_1, TARSKI, SETFAM_1; notation TARSKI, XBOOLE_0, XCMPLX_0, XREAL_0, NAT_1, ABSVALUE, BINARITH, SEQM_3, SETFAM_1, FUNCT_1, FINSEQ_1, FINSEQ_5, FINSEQ_6, RFINSEQ, GRAPH_2, MATRIX_1, RELSET_1, REALSET1, STRUCT_0, PRE_TOPC, COMPTS_1, EUCLID, SPPOL_1, TOPREAL1, GOBOARD1, GOBOARD5, JORDAN1E, FINSEQ_4; constructors REAL_1, GOBOARD1, GRAPH_2, FINSEQ_4, ABSVALUE, REALSET1, JORDAN1E, SPRECT_1, BINARITH, RFINSEQ, INT_1, GOBOARD9, MEMBERED; clusters RELSET_1, FINSEQ_6, FINSEQ_5, JORDAN1E, GOBOARD9, INT_1, REVROT_1, SPRECT_1, SPRECT_3, FINSEQ_1, SPPOL_2, REALSET1, MEMBERED, NUMBERS, ORDINAL2; 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}; definition cluster trivial Function; end; begin :: FinSequences reserve G for Go-board, i,j,k,m,n for Nat; definition cluster non constant 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}; definition cluster one-to-one special unfolded s.n.c. non empty FinSequence of TOP-REAL 2; end; 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 st n in dom f ex i,j 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;

Back to top