:: Rotating and reversing.(Finite sequences)
:: by Andrzej Trybulec
::
:: Received January 21, 1999
:: Copyright (c) 1999-2017 Association of Mizar Users
definition
let
D
be non
empty
set
;
let
f
be
FinSequence
of
D
;
:: original:
constant
redefine
attr
f
is
constant
means
:
Def1
:
:: REVROT_1:def 1
for
n
,
m
being
Nat
st
n
in
dom
f
&
m
in
dom
f
holds
f
/.
n
=
f
/.
m
;
compatibility
(
f
is
constant
iff for
n
,
m
being
Nat
st
n
in
dom
f
&
m
in
dom
f
holds
f
/.
n
=
f
/.
m
)
proof
end;
end;
::
deftheorem
Def1
defines
constant
REVROT_1:def 1 :
for
D
being non
empty
set
for
f
being
FinSequence
of
D
holds
(
f
is
constant
iff for
n
,
m
being
Nat
st
n
in
dom
f
&
m
in
dom
f
holds
f
/.
n
=
f
/.
m
);
theorem
Th1
:
:: REVROT_1:1
for
D
being non
empty
set
for
f
being
FinSequence
of
D
st
f
just_once_values
f
/.
(
len
f
)
holds
(
f
/.
(
len
f
)
)
..
f
=
len
f
proof
end;
theorem
:: REVROT_1:2
for
D
being non
empty
set
for
f
being
FinSequence
of
D
holds
f
/^
(
len
f
)
=
{}
by
RFINSEQ:27
;
theorem
Th3
:
:: REVROT_1:3
for
D
being non
empty
set
for
f
being non
empty
FinSequence
of
D
holds
f
/.
(
len
f
)
in
rng
f
proof
end;
definition
let
D
be non
empty
set
;
let
f
be
FinSequence
of
D
;
let
y
be
set
;
:: original:
just_once_values
redefine
pred
f
just_once_values
y
means
:: REVROT_1:def 2
ex
x
being
set
st
(
x
in
dom
f
&
y
=
f
/.
x
& ( for
z
being
set
st
z
in
dom
f
&
z
<>
x
holds
f
/.
z
<>
y
) );
compatibility
(
f
just_once_values
y
iff ex
x
being
set
st
(
x
in
dom
f
&
y
=
f
/.
x
& ( for
z
being
set
st
z
in
dom
f
&
z
<>
x
holds
f
/.
z
<>
y
) ) )
proof
end;
end;
::
deftheorem
defines
just_once_values
REVROT_1:def 2 :
for
D
being non
empty
set
for
f
being
FinSequence
of
D
for
y
being
set
holds
(
f
just_once_values
y
iff ex
x
being
set
st
(
x
in
dom
f
&
y
=
f
/.
x
& ( for
z
being
set
st
z
in
dom
f
&
z
<>
x
holds
f
/.
z
<>
y
) ) );
theorem
Th4
:
:: REVROT_1:4
for
D
being non
empty
set
for
f
being
FinSequence
of
D
st
f
just_once_values
f
/.
(
len
f
)
holds
f
-:
(
f
/.
(
len
f
)
)
=
f
proof
end;
theorem
Th5
:
:: REVROT_1:5
for
D
being non
empty
set
for
f
being
FinSequence
of
D
st
f
just_once_values
f
/.
(
len
f
)
holds
f
:-
(
f
/.
(
len
f
)
)
=
<*
(
f
/.
(
len
f
)
)
*>
proof
end;
theorem
Th6
:
:: REVROT_1:6
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
holds 1
<=
len
(
f
:-
p
)
proof
end;
theorem
:: REVROT_1:7
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
st
p
in
rng
f
holds
len
(
f
:-
p
)
<=
len
f
proof
end;
theorem
:: REVROT_1:8
for
D
being non
empty
set
for
f
being non
empty
circular
FinSequence
of
D
holds
Rev
f
is
circular
proof
end;
theorem
Th9
:
:: REVROT_1:9
for
i
being
Nat
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
st
p
in
rng
f
& 1
<=
i
&
i
<=
len
(
f
:-
p
)
holds
(
Rotate
(
f
,
p
)
)
/.
i
=
f
/.
(
(
i
-'
1
)
+
(
p
..
f
)
)
proof
end;
theorem
Th10
:
:: REVROT_1:10
for
i
being
Nat
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
st
p
in
rng
f
&
p
..
f
<=
i
&
i
<=
len
f
holds
f
/.
i
=
(
Rotate
(
f
,
p
)
)
/.
(
(
i
+
1
)
-'
(
p
..
f
)
)
proof
end;
theorem
Th11
:
:: REVROT_1:11
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
st
p
in
rng
f
holds
(
Rotate
(
f
,
p
)
)
/.
(
len
(
f
:-
p
)
)
=
f
/.
(
len
f
)
proof
end;
theorem
Th12
:
:: REVROT_1:12
for
i
being
Nat
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
st
p
in
rng
f
&
len
(
f
:-
p
)
<
i
&
i
<=
len
f
holds
(
Rotate
(
f
,
p
)
)
/.
i
=
f
/.
(
(
i
+
(
p
..
f
)
)
-'
(
len
f
)
)
proof
end;
theorem
:: REVROT_1:13
for
i
being
Nat
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
st
p
in
rng
f
& 1
<
i
&
i
<=
p
..
f
holds
f
/.
i
=
(
Rotate
(
f
,
p
)
)
/.
(
(
i
+
(
len
f
)
)
-'
(
p
..
f
)
)
proof
end;
theorem
Th14
:
:: REVROT_1:14
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
holds
len
(
Rotate
(
f
,
p
)
)
=
len
f
proof
end;
theorem
Th15
:
:: REVROT_1:15
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
FinSequence
of
D
holds
dom
(
Rotate
(
f
,
p
)
)
=
dom
f
proof
end;
theorem
Th16
:
:: REVROT_1:16
for
D
being non
empty
set
for
f
being
circular
FinSequence
of
D
for
p
being
Element
of
D
st ( for
i
being
Nat
st 1
<
i
&
i
<
len
f
holds
f
/.
i
<>
f
/.
1 ) holds
Rotate
(
(
Rotate
(
f
,
p
)
)
,
(
f
/.
1
)
)
=
f
proof
end;
theorem
Th17
:
:: REVROT_1:17
for
i
being
Nat
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
circular
FinSequence
of
D
st
p
in
rng
f
&
len
(
f
:-
p
)
<=
i
&
i
<=
len
f
holds
(
Rotate
(
f
,
p
)
)
/.
i
=
f
/.
(
(
i
+
(
p
..
f
)
)
-'
(
len
f
)
)
proof
end;
theorem
Th18
:
:: REVROT_1:18
for
i
being
Nat
for
D
being non
empty
set
for
p
being
Element
of
D
for
f
being
circular
FinSequence
of
D
st
p
in
rng
f
& 1
<=
i
&
i
<=
p
..
f
holds
f
/.
i
=
(
Rotate
(
f
,
p
)
)
/.
(
(
i
+
(
len
f
)
)
-'
(
p
..
f
)
)
proof
end;
registration
let
D
be non
trivial
set
;
cluster
V1
()
V4
(
NAT
)
V5
(
D
)
Function-like
V8
()
V33
()
FinSequence-like
FinSubsequence-like
circular
for
FinSequence
of
D
;
existence
ex
b
1
being
FinSequence
of
D
st
(
b
1
is
V8
() &
b
1
is
circular
)
proof
end;
end;
registration
let
D
be non
trivial
set
;
let
p
be
Element
of
D
;
let
f
be
V8
()
circular
FinSequence
of
D
;
cluster
Rotate
(
f
,
p
)
->
V8
() ;
coherence
not
Rotate
(
f
,
p
) is
constant
proof
end;
end;
theorem
Th19
:
:: REVROT_1:19
for
n
being non
zero
Nat
holds
0.REAL
n
<>
1.REAL
n
proof
end;
registration
let
n
be non
zero
Nat
;
cluster
TOP-REAL
n
->
non
trivial
;
coherence
not
TOP-REAL
n
is
trivial
proof
end;
end;
theorem
Th20
:
:: REVROT_1:20
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
rng
f
c=
rng
g
holds
rng
(
X_axis
f
)
c=
rng
(
X_axis
g
)
proof
end;
theorem
Th21
:
:: REVROT_1:21
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
rng
f
=
rng
g
holds
rng
(
X_axis
f
)
=
rng
(
X_axis
g
)
by
Th20
;
theorem
Th22
:
:: REVROT_1:22
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
rng
f
c=
rng
g
holds
rng
(
Y_axis
f
)
c=
rng
(
Y_axis
g
)
proof
end;
theorem
Th23
:
:: REVROT_1:23
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
rng
f
=
rng
g
holds
rng
(
Y_axis
f
)
=
rng
(
Y_axis
g
)
by
Th22
;
registration
let
p
be
Point
of
(
TOP-REAL
2
)
;
let
f
be
circular
special
FinSequence
of
(
TOP-REAL
2
)
;
cluster
Rotate
(
f
,
p
)
->
special
;
coherence
Rotate
(
f
,
p
) is
special
proof
end;
end;
theorem
Th24
:
:: REVROT_1:24
for
i
being
Nat
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
p
in
rng
f
& 1
<=
i
&
i
<
len
(
f
:-
p
)
holds
LSeg
(
(
Rotate
(
f
,
p
)
)
,
i
)
=
LSeg
(
f
,
(
(
i
-'
1
)
+
(
p
..
f
)
)
)
proof
end;
theorem
Th25
:
:: REVROT_1:25
for
i
being
Nat
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
p
in
rng
f
&
p
..
f
<=
i
&
i
<
len
f
holds
LSeg
(
f
,
i
)
=
LSeg
(
(
Rotate
(
f
,
p
)
)
,
(
(
i
-'
(
p
..
f
)
)
+
1
)
)
proof
end;
theorem
Th26
:
:: REVROT_1:26
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
circular
FinSequence
of
(
TOP-REAL
2
)
holds
Incr
(
X_axis
f
)
=
Incr
(
X_axis
(
Rotate
(
f
,
p
)
)
)
proof
end;
theorem
Th27
:
:: REVROT_1:27
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
circular
FinSequence
of
(
TOP-REAL
2
)
holds
Incr
(
Y_axis
f
)
=
Incr
(
Y_axis
(
Rotate
(
f
,
p
)
)
)
proof
end;
theorem
Th28
:
:: REVROT_1:28
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being non
empty
circular
FinSequence
of
(
TOP-REAL
2
)
holds
GoB
(
Rotate
(
f
,
p
)
)
=
GoB
f
proof
end;
theorem
Th29
:
:: REVROT_1:29
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
V8
()
standard
special_circular_sequence
holds
Rev
(
Rotate
(
f
,
p
)
)
=
Rotate
(
(
Rev
f
)
,
p
)
proof
end;
theorem
Th30
:
:: REVROT_1:30
for
f
being
circular
s.c.c.
FinSequence
of
(
TOP-REAL
2
)
st
len
f
>
4 holds
(
LSeg
(
f
,
(
(
len
f
)
-'
1
)
)
)
/\
(
LSeg
(
f
,1)
)
=
{
(
f
/.
1
)
}
proof
end;
theorem
Th31
:
:: REVROT_1:31
for
i
being
Nat
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
circular
FinSequence
of
(
TOP-REAL
2
)
st
p
in
rng
f
&
len
(
f
:-
p
)
<=
i
&
i
<
len
f
holds
LSeg
(
(
Rotate
(
f
,
p
)
)
,
i
)
=
LSeg
(
f
,
(
(
i
+
(
p
..
f
)
)
-'
(
len
f
)
)
)
proof
end;
registration
let
p
be
Point
of
(
TOP-REAL
2
)
;
let
f
be
circular
s.c.c.
FinSequence
of
(
TOP-REAL
2
)
;
cluster
Rotate
(
f
,
p
)
->
s.c.c.
;
coherence
Rotate
(
f
,
p
) is
s.c.c.
proof
end;
end;
registration
let
p
be
Point
of
(
TOP-REAL
2
)
;
let
f
be
V8
()
standard
special_circular_sequence
;
cluster
Rotate
(
f
,
p
)
->
unfolded
;
coherence
Rotate
(
f
,
p
) is
unfolded
proof
end;
end;
theorem
Th32
:
:: REVROT_1:32
for
i
being
Nat
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
circular
FinSequence
of
(
TOP-REAL
2
)
st
p
in
rng
f
& 1
<=
i
&
i
<
p
..
f
holds
LSeg
(
f
,
i
)
=
LSeg
(
(
Rotate
(
f
,
p
)
)
,
(
(
i
+
(
len
f
)
)
-'
(
p
..
f
)
)
)
proof
end;
theorem
Th33
:
:: REVROT_1:33
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
circular
FinSequence
of
(
TOP-REAL
2
)
holds
L~
(
Rotate
(
f
,
p
)
)
=
L~
f
proof
end;
theorem
Th34
:
:: REVROT_1:34
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
circular
FinSequence
of
(
TOP-REAL
2
)
for
G
being
Go-board
holds
(
f
is_sequence_on
G
iff
Rotate
(
f
,
p
)
is_sequence_on
G
)
proof
end;
registration
let
p
be
Point
of
(
TOP-REAL
2
)
;
let
f
be non
empty
circular
standard
FinSequence
of
(
TOP-REAL
2
)
;
cluster
Rotate
(
f
,
p
)
->
standard
;
coherence
Rotate
(
f
,
p
) is
standard
proof
end;
end;
theorem
Th35
:
:: REVROT_1:35
for
f
being
V8
()
standard
special_circular_sequence
for
p
being
Point
of
(
TOP-REAL
2
)
for
k
being
Nat
st
p
in
rng
f
& 1
<=
k
&
k
<
p
..
f
holds
left_cell
(
f
,
k
)
=
left_cell
(
(
Rotate
(
f
,
p
)
)
,
(
(
k
+
(
len
f
)
)
-'
(
p
..
f
)
)
)
proof
end;
theorem
Th36
:
:: REVROT_1:36
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
V8
()
standard
special_circular_sequence
holds
LeftComp
(
Rotate
(
f
,
p
)
)
=
LeftComp
f
proof
end;
theorem
:: REVROT_1:37
for
p
being
Point
of
(
TOP-REAL
2
)
for
f
being
V8
()
standard
special_circular_sequence
holds
RightComp
(
Rotate
(
f
,
p
)
)
=
RightComp
f
proof
end;
Lm1
:
for
f
being
V8
()
standard
special_circular_sequence
holds
( not
f
/.
1
=
N-min
(
L~
f
)
or
f
is
clockwise_oriented
or
Rev
f
is
clockwise_oriented
)
proof
end;
registration
let
p
be
Point
of
(
TOP-REAL
2
)
;
let
f
be
V8
()
standard
clockwise_oriented
special_circular_sequence
;
cluster
Rotate
(
f
,
p
)
->
clockwise_oriented
;
coherence
Rotate
(
f
,
p
) is
clockwise_oriented
proof
end;
end;
theorem
:: REVROT_1:38
for
f
being
V8
()
standard
special_circular_sequence
holds
(
f
is
clockwise_oriented
or
Rev
f
is
clockwise_oriented
)
proof
end;