:: More on the Finite Sequences on the Plane
:: by Andrzej Trybulec
::
:: Received October 25, 2001
:: Copyright (c) 2001-2021 Association of Mizar Users

theorem Th1: :: TOPREAL8:1

for A, x, y being set st A c= {x,y} & x in A & not y in A holds
A = {x}

proof end;

registration

cluster trivial V7() Function-like for set ;

existence
ex b₁ being Function st b₁ is trivial

proof end;

end;

registration

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

existence
not for b₁ being FinSequence holds b₁ is constant

proof end;

end;

theorem Th2: :: TOPREAL8:2

for f being non trivial FinSequence holds 1 < len f

proof end;

theorem Th3: :: TOPREAL8:3

for D being non trivial set
for f being V25() circular FinSequence of D holds len f > 2

proof end;

theorem Th4: :: TOPREAL8:4

for f being FinSequence
for x being set holds
( x in rng f or x .. f = 0 )

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

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

proof end;

theorem Th7: :: TOPREAL8:7

for f, g being FinSequence holds len f <= len (f ^' g)

proof end;

theorem Th8: :: TOPREAL8:8

for f, g being FinSequence
for x being set st x in rng f holds
x .. f = x .. (f ^' g)

proof end;

theorem :: TOPREAL8:9

for f being non empty FinSequence
for g being FinSequence holds len g <= len (f ^' g)

proof end;

theorem Th10: :: TOPREAL8:10

for f, g being FinSequence holds rng f c= rng (f ^' g)

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

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

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

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

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

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

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

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

proof end;

theorem Th19: :: TOPREAL8:19

for f being non trivial FinSequence of (TOP-REAL 2) holds LSeg (f,1) = L~ (f | 2)

proof end;

theorem Th20: :: TOPREAL8:20

for f being s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st n < len f holds
f | n is s.n.c.

proof end;

theorem Th21: :: TOPREAL8:21

for f being s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st 1 <= n holds
f /^ n is s.n.c.

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

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

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

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

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

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

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)

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

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)

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

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

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.

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

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)

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 )

proof end;