begin
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
canceled;
theorem
theorem Th9:
theorem Th10:
theorem Th11:
Lm1:
for f, ff being non empty FinSequence of st ff = Rev f holds
GoB ff = GoB f
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
definition
let f be non
constant standard special_circular_sequence;
A1:
1
+ 1
< len f
by GOBOARD7:36, XXREAL_0:2;
then A2:
Int (left_cell f,1) <> {}
by Th18;
A3:
Int (right_cell f,1) <> {}
by A1, Th19;
func LeftComp f -> Subset of
means :
Def1:
(
it is_a_component_of (L~ f) ` &
Int (left_cell f,1) c= it );
existence
ex b1 being Subset of st
( b1 is_a_component_of (L~ f) ` & Int (left_cell f,1) c= b1 )
uniqueness
for b1, b2 being Subset of st b1 is_a_component_of (L~ f) ` & Int (left_cell f,1) c= b1 & b2 is_a_component_of (L~ f) ` & Int (left_cell f,1) c= b2 holds
b1 = b2
by A2, Th3, XBOOLE_1:67;
func RightComp f -> Subset of
means :
Def2:
(
it is_a_component_of (L~ f) ` &
Int (right_cell f,1) c= it );
existence
ex b1 being Subset of st
( b1 is_a_component_of (L~ f) ` & Int (right_cell f,1) c= b1 )
uniqueness
for b1, b2 being Subset of st b1 is_a_component_of (L~ f) ` & Int (right_cell f,1) c= b1 & b2 is_a_component_of (L~ f) ` & Int (right_cell f,1) c= b2 holds
b1 = b2
by A3, Th3, XBOOLE_1:67;
end;
:: deftheorem Def1 defines LeftComp GOBOARD9:def 1 :
:: deftheorem Def2 defines RightComp GOBOARD9:def 2 :
theorem Th24:
theorem
theorem Th26:
theorem
theorem