:: by Andrzej Trybulec

::

:: Received October 25, 2001

:: Copyright (c) 2001-2019 Association of Mizar Users

registration

not for b_{1} being FinSequence holds b_{1} is constant
end;

cluster V7() V10( NAT ) Function-like non constant V31() FinSequence-like FinSubsequence-like for set ;

existence not for b

proof end;

theorem Th5: :: TOPREAL8:5

for p being set

for 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

for 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

proof end;

theorem Th6: :: 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

for f being non empty one-to-one FinSequence of D holds (f /. (len f)) .. f = len f

proof end;

theorem Th11: :: 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

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

proof end;

theorem Th12: :: 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

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

proof end;

Lm1: for p being FinSequence

for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds

( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds

((m,n) -cut p) . (i + 1) = p . (m + i) ) )

proof end;

theorem Th13: :: TOPREAL8:13

for k being Nat

for D being set

for f being FinSequence of D st 1 <= k holds

((k + 1),(len f)) -cut f = f /^ k

for D being set

for f being FinSequence of D st 1 <= k holds

((k + 1),(len f)) -cut f = f /^ k

proof end;

theorem Th14: :: TOPREAL8:14

for k being Nat

for D being set

for f being FinSequence of D st k <= len f holds

(1,k) -cut f = f | k

for D being set

for f being FinSequence of D st k <= len f holds

(1,k) -cut f = f | k

proof end;

theorem Th15: :: TOPREAL8:15

for p being set

for 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

for 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

proof end;

theorem Th16: :: 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

for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds

(f ^' g) :- (g /. 1) = g

proof end;

theorem Th17: :: 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

for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds

(f ^' g) -: (g /. 1) = f

proof end;

theorem Th18: :: 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 being Nat st 1 <= i & i < len f holds

f /. i <> g /. 1 ) holds

Rotate ((f ^' g),(g /. 1)) = g ^' f

for f being non empty FinSequence of D

for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Nat st 1 <= i & i < len f holds

f /. i <> g /. 1 ) holds

Rotate ((f ^' g),(g /. 1)) = g ^' f

proof end;

theorem Th22: :: TOPREAL8:22

for f being circular s.c.c. FinSequence of (TOP-REAL 2)

for n being Nat st n < len f & len f > 4 holds

f | n is one-to-one

for n being Nat st n < len f & len f > 4 holds

f | n is one-to-one

proof end;

theorem Th23: :: TOPREAL8:23

for f being circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds

for i, j being Nat st 1 < i & i < j & j <= len f holds

f /. i <> f /. j

for i, j being Nat st 1 < i & i < j & j <= len f holds

f /. i <> f /. j

proof end;

theorem Th24: :: TOPREAL8:24

for f being circular s.c.c. FinSequence of (TOP-REAL 2)

for n being Nat st 1 <= n & len f > 4 holds

f /^ n is one-to-one

for n being Nat st 1 <= n & len f > 4 holds

f /^ n is one-to-one

proof end;

theorem Th25: :: TOPREAL8:25

for m, n being Nat

for f being non empty special FinSequence of (TOP-REAL 2) holds (m,n) -cut f is special

for f being non empty special FinSequence of (TOP-REAL 2) holds (m,n) -cut f is special

proof end;

theorem Th26: :: TOPREAL8:26

for f being non empty special FinSequence of (TOP-REAL 2)

for g being non trivial special FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds

f ^' g is special

for g being non trivial special FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds

f ^' g is special

proof end;

theorem Th27: :: 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)}

(LSeg (f,1)) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}

proof end;

theorem Th28: :: TOPREAL8:28

for j being Nat

for f, g being FinSequence of (TOP-REAL 2) st j < len f holds

LSeg ((f ^' g),j) = LSeg (f,j)

for f, g being FinSequence of (TOP-REAL 2) st j < len f holds

LSeg ((f ^' g),j) = LSeg (f,j)

proof end;

theorem Th29: :: TOPREAL8:29

for j being Nat

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))

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))

proof end;

theorem Th30: :: 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)

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)

proof end;

theorem Th31: :: TOPREAL8:31

for j being Nat

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))

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))

proof end;

theorem Th32: :: TOPREAL8:32

for f being non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)

for i being Nat st 1 <= i & i < len f holds

(LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}

for i being Nat st 1 <= i & i < len f holds

(LSeg (f,i)) /\ (rng f) = {(f /. i),(f /. (i + 1))}

proof end;

Lm2: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)

for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)

for i, j being Nat st i < len f & 1 < i holds

for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds

x <> f /. 1

proof end;

Lm3: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)

for g being non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)

for i, j being Nat st j > len f & j + 1 < len (f ^' g) holds

for x being Point of (TOP-REAL 2) st x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) holds

x <> g /. (len g)

proof end;

theorem Th33: :: TOPREAL8:33

for f, g being non trivial one-to-one unfolded s.n.c. 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.

f ^' g is s.c.c.

proof end;

theorem Th34: :: TOPREAL8:34

for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & g is unfolded & f /. (len f) = g /. 1 & (LSeg (f,((len f) -' 1))) /\ (LSeg (g,1)) = {(f /. (len f))} holds

f ^' g is unfolded

f ^' g is unfolded

proof end;

theorem Th35: :: TOPREAL8:35

for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is trivial & f /. (len f) = g /. 1 holds

L~ (f ^' g) = (L~ f) \/ (L~ g)

L~ (f ^' g) = (L~ f) \/ (L~ g)

proof end;

theorem :: TOPREAL8:36

for G being Go-board

for f being FinSequence of (TOP-REAL 2) st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is V25() & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )

for f being FinSequence of (TOP-REAL 2) st ( for n being Nat st n in dom f holds

ex i, j being Nat st

( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is V25() & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds

ex g being FinSequence of (TOP-REAL 2) st

( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )

proof end;