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;