:: by Andrzej Trybulec

::

:: Received January 21, 1999

:: Copyright (c) 1999-2018 Association of Mizar Users

definition

let D be non empty set ;

let f be FinSequence of D;

( f is constant iff for n, m being Nat st n in dom f & m in dom f holds

f /. n = f /. m )

end;
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 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;

( 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;

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

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

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

definition

let D be non empty set ;

let f be FinSequence of D;

let y be set ;

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

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

( 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;

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

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

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

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)

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

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

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

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)

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

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

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

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

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

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

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

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 ;

ex b_{1} being FinSequence of D st

( b_{1} is V8() & b_{1} is circular )

end;
cluster V1() V4( NAT ) V5(D) Function-like V8() V33() FinSequence-like FinSubsequence-like circular for of ;

existence ex b

( b

proof end;

registration

let D be non trivial set ;

let p be Element of D;

let f be V8() circular FinSequence of D;

coherence

not Rotate (f,p) is constant

end;
let p be Element of D;

let f be V8() circular FinSequence of D;

coherence

not Rotate (f,p) is constant

proof end;

registration

let p be Point of (TOP-REAL 2);

let f be circular special FinSequence of (TOP-REAL 2);

coherence

Rotate (f,p) is special

end;
let f be circular special FinSequence of (TOP-REAL 2);

coherence

Rotate (f,p) is special

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

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

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

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

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

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)

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

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

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

coherence

Rotate (f,p) is s.c.c.

end;
let f be circular s.c.c. FinSequence of (TOP-REAL 2);

coherence

Rotate (f,p) is s.c.c.

proof end;

registration

let p be Point of (TOP-REAL 2);

let f be V8() standard special_circular_sequence;

coherence

Rotate (f,p) is unfolded

end;
let f be V8() standard special_circular_sequence;

coherence

Rotate (f,p) is unfolded

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

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

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 )

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

coherence

Rotate (f,p) is standard

end;
let f be non empty circular standard FinSequence of (TOP-REAL 2);

coherence

Rotate (f,p) is standard

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

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

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

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;

coherence

Rotate (f,p) is clockwise_oriented

end;
let f be V8() standard clockwise_oriented special_circular_sequence;

coherence

Rotate (f,p) is clockwise_oriented

proof end;

theorem :: REVROT_1:38

for f being V8() standard special_circular_sequence holds

( f is clockwise_oriented or Rev f is clockwise_oriented )

( f is clockwise_oriented or Rev f is clockwise_oriented )

proof end;