:: More on the Finite Sequences on the Plane
::  by Andrzej Trybulec
::
:: Received October 25, 2001
:: Copyright (c) 2001-2021 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;