:: More on the Finite Sequences on the Plane
:: by Andrzej Trybulec
::
:: Copyright (c) 2001-2019 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
existence
ex b1 being Function st b1 is trivial
proof end;
end;

registration
existence
not for b1 being FinSequence holds b1 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 () holds LSeg (f,1) = L~ (f | 2)
proof end;

theorem Th20: :: TOPREAL8:20
for f being s.c.c. FinSequence of ()
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 ()
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 ()
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 () 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 ()
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 () holds (m,n) -cut f is special
proof end;

theorem Th26: :: TOPREAL8:26
for f being non empty special FinSequence of ()
for g being non trivial special FinSequence of () 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 () 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 () 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 () 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 ()
for g being non trivial FinSequence of () 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 ()
for g being non trivial FinSequence of () 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 ()
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 ()
for g being non trivial one-to-one unfolded s.n.c. FinSequence of ()
for i, j being Nat st i < len f & 1 < i holds
for x being Point of () 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 ()
for g being non trivial one-to-one unfolded s.n.c. FinSequence of ()
for i, j being Nat st j > len f & j + 1 < len (f ^' g) holds
for x being Point of () 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 () 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 () 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 () 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 () 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 () 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;