:: REVROT_1 semantic presentation

registration

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

end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
redefine attr constant as a₂ is constant means :Def1: :: REVROT_1:def 1
for b₁, b₂ being Nat st b₁ in dom a₂ & b₂ in dom a₂ holds
a₂ /. b₁ = a₂ /. b₂;
compatibility

proof end;

end;

:: deftheorem Def1 defines constant REVROT_1:def 1 :

theorem Th1: :: REVROT_1:1

for b₁ being non empty set
for b₂ being FinSequence of b₁ st b₂ just_once_values b₂ /. (len b₂) holds
(b₂ /. (len b₂)) .. b₂ = len b₂

proof end;

theorem Th2: :: REVROT_1:2

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds b₂ /^ (len b₂) = {}

proof end;

theorem Th3: :: REVROT_1:3

for b₁ being non empty set
for b₂ being non empty FinSequence of b₁ holds b₂ /. (len b₂) in rng b₂

proof end;

definition

let c₁ be non empty set ;
let c₂ be FinSequence of c₁;
let c₃ be set ;
redefine pred just_once_values as c₂ just_once_values c₃ means :: REVROT_1:def 2
ex b₁ being set st
( b₁ in dom a₂ & a₃ = a₂ /. b₁ & ( for b₂ being set st b₂ in dom a₂ & b₂ <> b₁ holds
a₂ /. b₂ <> a₃ ) );
compatibility

proof end;

end;

:: deftheorem Def2 defines just_once_values REVROT_1:def 2 :

theorem Th4: :: REVROT_1:4

for b₁ being non empty set
for b₂ being FinSequence of b₁ st b₂ just_once_values b₂ /. (len b₂) holds
b₂ -: (b₂ /. (len b₂)) = b₂

proof end;

theorem Th5: :: REVROT_1:5

for b₁ being non empty set
for b₂ being FinSequence of b₁ st b₂ just_once_values b₂ /. (len b₂) holds
b₂ :- (b₂ /. (len b₂)) = <*(b₂ /. (len b₂))*>

proof end;

theorem Th6: :: REVROT_1:6

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds 1 <= len (b₃ :- b₂)

proof end;

theorem Th7: :: REVROT_1:7

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
len (b₃ :- b₂) <= len b₃

proof end;

theorem Th8: :: REVROT_1:8

for b₁ being non empty set
for b₂ being non empty circular FinSequence of b₁ holds Rev b₂ is circular

proof end;

theorem Th9: :: REVROT_1:9

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & 1 <= b₁ & b₁ <= len (b₄ :- b₃) holds
(Rotate b₄,b₃) /. b₁ = b₄ /. ((b₁ -' 1) + (b₃ .. b₄))

proof end;

theorem Th10: :: REVROT_1:10

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & b₃ .. b₄ <= b₁ & b₁ <= len b₄ holds
b₄ /. b₁ = (Rotate b₄,b₃) /. ((b₁ + 1) -' (b₃ .. b₄))

proof end;

theorem Th11: :: REVROT_1:11

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ st b₂ in rng b₃ holds
(Rotate b₃,b₂) /. (len (b₃ :- b₂)) = b₃ /. (len b₃)

proof end;

theorem Th12: :: REVROT_1:12

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & len (b₄ :- b₃) < b₁ & b₁ <= len b₄ holds
(Rotate b₄,b₃) /. b₁ = b₄ /. ((b₁ + (b₃ .. b₄)) -' (len b₄))

proof end;

theorem Th13: :: REVROT_1:13

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being FinSequence of b₂ st b₃ in rng b₄ & 1 < b₁ & b₁ <= b₃ .. b₄ holds
b₄ /. b₁ = (Rotate b₄,b₃) /. ((b₁ + (len b₄)) -' (b₃ .. b₄))

proof end;

theorem Th14: :: REVROT_1:14

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds len (Rotate b₃,b₂) = len b₃

proof end;

theorem Th15: :: REVROT_1:15

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being FinSequence of b₁ holds dom (Rotate b₃,b₂) = dom b₃

proof end;

theorem Th16: :: REVROT_1:16

for b₁ being non empty set
for b₂ being circular FinSequence of b₁
for b₃ being Element of b₁ st ( for b₄ being Nat st 1 < b₄ & b₄ < len b₂ holds
b₂ /. b₄ <> b₂ /. 1 ) holds
Rotate (Rotate b₂,b₃),(b₂ /. 1) = b₂

proof end;

theorem Th17: :: REVROT_1:17

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being circular FinSequence of b₂ st b₃ in rng b₄ & len (b₄ :- b₃) <= b₁ & b₁ <= len b₄ holds
(Rotate b₄,b₃) /. b₁ = b₄ /. ((b₁ + (b₃ .. b₄)) -' (len b₄))

proof end;

theorem Th18: :: REVROT_1:18

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being circular FinSequence of b₂ st b₃ in rng b₄ & 1 <= b₁ & b₁ <= b₃ .. b₄ holds
b₄ /. b₁ = (Rotate b₄,b₃) /. ((b₁ + (len b₄)) -' (b₃ .. b₄))

proof end;

registration

let c₁ be non trivial set ;
cluster V38 circular FinSequence of a₁;
existence

proof end;

end;

registration

let c₁ be non trivial set ;
let c₂ be Element of c₁;
let c₃ be V38 circular FinSequence of c₁;
cluster Rotate a₃,a₂ -> V38 ;
coherence

proof end;

end;

theorem Th19: :: REVROT_1:19

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

proof end;

registration

let c₁ be non empty Nat;
cluster TOP-REAL a₁ -> non trivial ;
coherence

proof end;

end;

theorem Th20: :: REVROT_1:20

for b₁, b₂ being FinSequence of (TOP-REAL 2) st rng b₁ c= rng b₂ holds
rng (X_axis b₁) c= rng (X_axis b₂)

proof end;

theorem Th21: :: REVROT_1:21

for b₁, b₂ being FinSequence of (TOP-REAL 2) st rng b₁ = rng b₂ holds
rng (X_axis b₁) = rng (X_axis b₂)

proof end;

theorem Th22: :: REVROT_1:22

for b₁, b₂ being FinSequence of (TOP-REAL 2) st rng b₁ c= rng b₂ holds
rng (Y_axis b₁) c= rng (Y_axis b₂)

proof end;

theorem Th23: :: REVROT_1:23

for b₁, b₂ being FinSequence of (TOP-REAL 2) st rng b₁ = rng b₂ holds
rng (Y_axis b₁) = rng (Y_axis b₂)

proof end;

registration

let c₁ be Point of (TOP-REAL 2);
let c₂ be special circular FinSequence of (TOP-REAL 2);
cluster Rotate a₂,a₁ -> special ;
coherence

proof end;

end;

theorem Th24: :: REVROT_1:24

for b₁ being Nat
for b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₂ in rng b₃ & 1 <= b₁ & b₁ < len (b₃ :- b₂) holds
LSeg (Rotate b₃,b₂),b₁ = LSeg b₃,((b₁ -' 1) + (b₂ .. b₃))

proof end;

theorem Th25: :: REVROT_1:25

for b₁ being Nat
for b₂ being Point of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₂ in rng b₃ & b₂ .. b₃ <= b₁ & b₁ < len b₃ holds
LSeg b₃,b₁ = LSeg (Rotate b₃,b₂),((b₁ -' (b₂ .. b₃)) + 1)

proof end;

theorem Th26: :: REVROT_1:26

for b₁ being Point of (TOP-REAL 2)
for b₂ being circular FinSequence of (TOP-REAL 2) holds Incr (X_axis b₂) = Incr (X_axis (Rotate b₂,b₁))

proof end;

theorem Th27: :: REVROT_1:27

for b₁ being Point of (TOP-REAL 2)
for b₂ being circular FinSequence of (TOP-REAL 2) holds Incr (Y_axis b₂) = Incr (Y_axis (Rotate b₂,b₁))

proof end;

theorem Th28: :: REVROT_1:28

for b₁ being Point of (TOP-REAL 2)
for b₂ being non empty circular FinSequence of (TOP-REAL 2) holds GoB (Rotate b₂,b₁) = GoB b₂

proof end;

theorem Th29: :: REVROT_1:29

for b₁ being Point of (TOP-REAL 2)
for b₂ being V38 standard special_circular_sequence holds Rev (Rotate b₂,b₁) = Rotate (Rev b₂),b₁

proof end;

theorem Th30: :: REVROT_1:30

for b₁ being circular s.c.c. FinSequence of (TOP-REAL 2) st len b₁ > 4 holds
(LSeg b₁,((len b₁) -' 1)) /\ (LSeg b₁,1) = {(b₁ /. 1)}

proof end;

theorem Th31: :: REVROT_1:31

for b₁ being Nat
for b₂ being Point of (TOP-REAL 2)
for b₃ being circular FinSequence of (TOP-REAL 2) st b₂ in rng b₃ & len (b₃ :- b₂) <= b₁ & b₁ < len b₃ holds
LSeg (Rotate b₃,b₂),b₁ = LSeg b₃,((b₁ + (b₂ .. b₃)) -' (len b₃))

proof end;

registration

let c₁ be Point of (TOP-REAL 2);
let c₂ be circular s.c.c. FinSequence of (TOP-REAL 2);
cluster Rotate a₂,a₁ -> s.c.c. ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th32: :: REVROT_1:32

for b₁ being Nat
for b₂ being Point of (TOP-REAL 2)
for b₃ being circular FinSequence of (TOP-REAL 2) st b₂ in rng b₃ & 1 <= b₁ & b₁ < b₂ .. b₃ holds
LSeg b₃,b₁ = LSeg (Rotate b₃,b₂),((b₁ + (len b₃)) -' (b₂ .. b₃))

proof end;

theorem Th33: :: REVROT_1:33

for b₁ being Point of (TOP-REAL 2)
for b₂ being circular FinSequence of (TOP-REAL 2) holds L~ (Rotate b₂,b₁) = L~ b₂

proof end;

theorem Th34: :: REVROT_1:34

for b₁ being Point of (TOP-REAL 2)
for b₂ being circular FinSequence of (TOP-REAL 2)
for b₃ being Go-board holds
( b₂ is_sequence_on b₃ iff Rotate b₂,b₁ is_sequence_on b₃ )

proof end;

registration

let c₁ be Point of (TOP-REAL 2);
let c₂ be non empty circular standard FinSequence of (TOP-REAL 2);
cluster Rotate a₂,a₁ -> standard ;
coherence

proof end;

end;

theorem Th35: :: REVROT_1:35

for b₁ being V38 standard special_circular_sequence
for b₂ being Point of (TOP-REAL 2)
for b₃ being Nat st b₂ in rng b₁ & 1 <= b₃ & b₃ < b₂ .. b₁ holds
left_cell b₁,b₃ = left_cell (Rotate b₁,b₂),((b₃ + (len b₁)) -' (b₂ .. b₁))

proof end;

theorem Th36: :: REVROT_1:36

for b₁ being Point of (TOP-REAL 2)
for b₂ being V38 standard special_circular_sequence holds LeftComp (Rotate b₂,b₁) = LeftComp b₂

proof end;

theorem Th37: :: REVROT_1:37

for b₁ being Point of (TOP-REAL 2)
for b₂ being V38 standard special_circular_sequence holds RightComp (Rotate b₂,b₁) = RightComp b₂

proof end;

Lemma35: for b₁ being V38 standard special_circular_sequence holds
( not b₁ /. 1 = N-min (L~ b₁) or b₁ is clockwise_oriented or Rev b₁ is clockwise_oriented )

proof end;

registration

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

proof end;

end;

theorem Th38: :: REVROT_1:38

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

proof end;