:: REVROT_1 semantic presentation

registration

let S be non trivial 1-sorted ;
cluster the carrier of S -> non trivial ;
coherence by REALSET2:def 5;

end;

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

proof end;

end;

:: deftheorem Def1 defines constant REVROT_1:def 1 :

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 Th2: :: REVROT_1:2

for D being non empty set
for f being FinSequence of D holds f /^ (len f) = {}

proof end;

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

proof end;

end;

:: deftheorem defines just_once_values REVROT_1:def 2 :

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 V38 circular FinSequence of D;
existence

proof end;

end;

registration

let D be non trivial set ;
let p be Element of D;
let f be V38 circular FinSequence of D;
cluster Rotate f,p -> V38 ;
coherence

proof end;

end;

theorem Th19: :: REVROT_1:19

for n being non empty Nat holds 0.REAL n <> 1.REAL n

proof end;

registration

let n be non empty Nat;
cluster TOP-REAL n -> non trivial ;
coherence

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)

proof end;

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)

proof end;

registration

let p be Point of (TOP-REAL 2);
let f be special circular FinSequence of (TOP-REAL 2);
cluster Rotate f,p -> special ;
coherence

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

proof end;

end;

registration

let p be Point of (TOP-REAL 2);
let f be V38 standard special_circular_sequence;
cluster Rotate f,p -> V38 special unfolded s.c.c. ;
coherence

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

proof end;

end;

theorem Th35: :: REVROT_1:35

for f being V38 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 V38 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 V38 standard special_circular_sequence holds RightComp (Rotate f,p) = RightComp f

proof end;

Lm1: for f being V38 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 V38 standard clockwise_oriented special_circular_sequence;
cluster Rotate f,p -> V38 special unfolded s.c.c. standard clockwise_oriented ;
coherence

proof end;

end;

theorem :: REVROT_1:38

for f being V38 standard special_circular_sequence holds
( f is clockwise_oriented or Rev f is clockwise_oriented )

proof end;