:: JORDAN23 semantic presentation

theorem Th1: :: JORDAN23:1
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
len (L_Cut b1,b2) >= 1
proof end;

theorem Th2: :: JORDAN23:2
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) holds len (R_Cut b1,b2) >= 1
proof end;

theorem Th3: :: JORDAN23:3
for b1 being FinSequence of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) holds B_Cut b1,b2,b3 <> {}
proof end;

registration
let c1 be set ;
cluster <*a1*> -> one-to-one ;
coherence
<*c1*> is one-to-one by FINSEQ_3:102;
end;

definition
let c1 be FinSequence;
attr a1 is almost-one-to-one means :Def1: :: JORDAN23:def 1
for b1, b2 being Nat st b1 in dom a1 & b2 in dom a1 & ( b1 <> 1 or b2 <> len a1 ) & ( b1 <> len a1 or b2 <> 1 ) & a1 . b1 = a1 . b2 holds
b1 = b2;
end;

:: deftheorem Def1 defines almost-one-to-one JORDAN23:def 1 :
for b1 being FinSequence holds
( b1 is almost-one-to-one iff for b2, b3 being Nat st b2 in dom b1 & b3 in dom b1 & ( b2 <> 1 or b3 <> len b1 ) & ( b2 <> len b1 or b3 <> 1 ) & b1 . b2 = b1 . b3 holds
b2 = b3 );

definition
let c1 be FinSequence;
attr a1 is weakly-one-to-one means :Def2: :: JORDAN23:def 2
for b1 being Nat st 1 <= b1 & b1 < len a1 holds
a1 . b1 <> a1 . (b1 + 1);
end;

:: deftheorem Def2 defines weakly-one-to-one JORDAN23:def 2 :
for b1 being FinSequence holds
( b1 is weakly-one-to-one iff for b2 being Nat st 1 <= b2 & b2 < len b1 holds
b1 . b2 <> b1 . (b2 + 1) );

definition
let c1 be FinSequence;
attr a1 is poorly-one-to-one means :Def3: :: JORDAN23:def 3
for b1 being Nat st 1 <= b1 & b1 < len a1 holds
a1 . b1 <> a1 . (b1 + 1) if len a1 <> 2
otherwise verum;
consistency
verum ;
end;

:: deftheorem Def3 defines poorly-one-to-one JORDAN23:def 3 :
for b1 being FinSequence holds
( ( len b1 <> 2 implies ( b1 is poorly-one-to-one iff for b2 being Nat st 1 <= b2 & b2 < len b1 holds
b1 . b2 <> b1 . (b2 + 1) ) ) & ( not len b1 <> 2 implies ( b1 is poorly-one-to-one iff verum ) ) );

theorem Th4: :: JORDAN23:4
for b1 being set
for b2 being FinSequence of b1 holds
( b2 is almost-one-to-one iff for b3, b4 being Nat st b3 in dom b2 & b4 in dom b2 & ( b3 <> 1 or b4 <> len b2 ) & ( b3 <> len b2 or b4 <> 1 ) & b2 /. b3 = b2 /. b4 holds
b3 = b4 )
proof end;

theorem Th5: :: JORDAN23:5
for b1 being set
for b2 being FinSequence of b1 holds
( b2 is weakly-one-to-one iff for b3 being Nat st 1 <= b3 & b3 < len b2 holds
b2 /. b3 <> b2 /. (b3 + 1) )
proof end;

theorem Th6: :: JORDAN23:6
for b1 being set
for b2 being FinSequence of b1 holds
( b2 is poorly-one-to-one iff ( len b2 <> 2 implies for b3 being Nat st 1 <= b3 & b3 < len b2 holds
b2 /. b3 <> b2 /. (b3 + 1) ) )
proof end;

registration
cluster one-to-one -> almost-one-to-one set ;
coherence
for b1 being FinSequence st b1 is one-to-one holds
b1 is almost-one-to-one
proof end;
end;

registration
cluster almost-one-to-one -> poorly-one-to-one set ;
coherence
for b1 being FinSequence st b1 is almost-one-to-one holds
b1 is poorly-one-to-one
proof end;
end;

theorem Th7: :: JORDAN23:7
for b1 being FinSequence st len b1 <> 2 holds
( b1 is weakly-one-to-one iff b1 is poorly-one-to-one )
proof end;

registration
cluster {} -> almost-one-to-one weakly-one-to-one poorly-one-to-one ;
coherence
{} is weakly-one-to-one
proof end;
end;

registration
let c1 be set ;
cluster <*a1*> -> one-to-one almost-one-to-one weakly-one-to-one poorly-one-to-one ;
coherence
<*c1*> is weakly-one-to-one
proof end;
end;

registration
let c1, c2 be set ;
cluster <*a1,a2*> -> poorly-one-to-one ;
coherence
<*c1,c2*> is poorly-one-to-one
proof end;
end;

registration
cluster non empty weakly-one-to-one set ;
existence
ex b1 being FinSequence st
( b1 is weakly-one-to-one & not b1 is empty )
proof end;
end;

registration
let c1 be non empty set ;
cluster non empty circular weakly-one-to-one FinSequence of a1;
existence
ex b1 being FinSequence of c1 st
( b1 is weakly-one-to-one & b1 is circular & not b1 is empty )
proof end;
end;

theorem Th8: :: JORDAN23:8
for b1 being FinSequence st b1 is almost-one-to-one holds
Rev b1 is almost-one-to-one
proof end;

theorem Th9: :: JORDAN23:9
for b1 being FinSequence st b1 is weakly-one-to-one holds
Rev b1 is weakly-one-to-one
proof end;

theorem Th10: :: JORDAN23:10
for b1 being FinSequence st b1 is poorly-one-to-one holds
Rev b1 is poorly-one-to-one
proof end;

registration
cluster non empty one-to-one almost-one-to-one poorly-one-to-one set ;
existence
ex b1 being FinSequence st
( b1 is one-to-one & not b1 is empty )
proof end;
end;

registration
let c1 be almost-one-to-one FinSequence;
cluster Rev a1 -> almost-one-to-one poorly-one-to-one ;
coherence
Rev c1 is almost-one-to-one by Th8;
end;

registration
let c1 be weakly-one-to-one FinSequence;
cluster Rev a1 -> weakly-one-to-one ;
coherence
Rev c1 is weakly-one-to-one by Th9;
end;

registration
let c1 be poorly-one-to-one FinSequence;
cluster Rev a1 -> poorly-one-to-one ;
coherence
Rev c1 is poorly-one-to-one by Th10;
end;

theorem Th11: :: JORDAN23:11
for b1 being non empty set
for b2 being FinSequence of b1 st b2 is almost-one-to-one holds
for b3 being Element of b1 holds Rotate b2,b3 is almost-one-to-one
proof end;

theorem Th12: :: JORDAN23:12
for b1 being non empty set
for b2 being FinSequence of b1 st b2 is weakly-one-to-one & b2 is circular holds
for b3 being Element of b1 holds Rotate b2,b3 is weakly-one-to-one
proof end;

theorem Th13: :: JORDAN23:13
for b1 being non empty set
for b2 being FinSequence of b1 st b2 is poorly-one-to-one & b2 is circular holds
for b3 being Element of b1 holds Rotate b2,b3 is poorly-one-to-one
proof end;

registration
let c1 be non empty set ;
cluster non empty one-to-one circular almost-one-to-one poorly-one-to-one FinSequence of a1;
existence
ex b1 being FinSequence of c1 st
( b1 is one-to-one & b1 is circular & not b1 is empty )
proof end;
end;

registration
let c1 be non empty set ;
let c2 be almost-one-to-one FinSequence of c1;
let c3 be Element of c1;
cluster Rotate a2,a3 -> almost-one-to-one poorly-one-to-one ;
coherence
Rotate c2,c3 is almost-one-to-one by Th11;
end;

registration
let c1 be non empty set ;
let c2 be circular weakly-one-to-one FinSequence of c1;
let c3 be Element of c1;
cluster Rotate a2,a3 -> weakly-one-to-one ;
coherence
Rotate c2,c3 is weakly-one-to-one by Th12;
end;

registration
let c1 be non empty set ;
let c2 be circular poorly-one-to-one FinSequence of c1;
let c3 be Element of c1;
cluster Rotate a2,a3 -> poorly-one-to-one ;
coherence
Rotate c2,c3 is poorly-one-to-one by Th13;
end;

theorem Th14: :: JORDAN23:14
for b1 being non empty set
for b2 being FinSequence of b1 holds
( b2 is almost-one-to-one iff ( b2 /^ 1 is one-to-one & b2 | ((len b2) -' 1) is one-to-one ) )
proof end;

registration
let c1 be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c2 be Nat;
cluster Cage a1,a2 -> almost-one-to-one poorly-one-to-one ;
coherence
Cage c1,c2 is almost-one-to-one
proof end;
end;

registration
let c1 be compact non horizontal non vertical Subset of (TOP-REAL 2);
let c2 be Nat;
cluster Cage a1,a2 -> almost-one-to-one weakly-one-to-one poorly-one-to-one ;
coherence
Cage c1,c2 is weakly-one-to-one
proof end;
end;

theorem Th15: :: JORDAN23:15
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 & b1 is weakly-one-to-one holds
B_Cut b1,b2,b2 = <*b2*>
proof end;

theorem Th16: :: JORDAN23:16
for b1 being FinSequence st b1 is one-to-one holds
b1 is weakly-one-to-one
proof end;

registration
cluster one-to-one -> weakly-one-to-one set ;
coherence
for b1 being FinSequence st b1 is one-to-one holds
b1 is weakly-one-to-one by Th16;
end;

theorem Th17: :: JORDAN23:17
for b1 being FinSequence of (TOP-REAL 2) st b1 is weakly-one-to-one holds
for b2, b3 being Point of (TOP-REAL 2) st b2 in L~ b1 & b3 in L~ b1 holds
B_Cut b1,b2,b3 = Rev (B_Cut b1,b3,b2)
proof end;

theorem Th18: :: JORDAN23:18
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2)
for b3 being Nat st b1 is poorly-one-to-one & b1 is unfolded & b1 is s.n.c. & 1 < b3 & b3 <= len b1 & b2 = b1 . b3 holds
(Index b2,b1) + 1 = b3
proof end;

theorem Th19: :: JORDAN23:19
for b1 being FinSequence of (TOP-REAL 2) st b1 is weakly-one-to-one holds
for b2, b3 being Point of (TOP-REAL 2) st b2 in L~ b1 & b3 in L~ b1 holds
(B_Cut b1,b2,b3) /. 1 = b2
proof end;

theorem Th20: :: JORDAN23:20
for b1 being FinSequence of (TOP-REAL 2) st b1 is weakly-one-to-one holds
for b2, b3 being Point of (TOP-REAL 2) st b2 in L~ b1 & b3 in L~ b1 holds
(B_Cut b1,b2,b3) /. (len (B_Cut b1,b2,b3)) = b3
proof end;

theorem Th21: :: JORDAN23:21
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
L~ (L_Cut b1,b2) c= L~ b1
proof end;

theorem Th22: :: JORDAN23:22
for b1 being FinSequence of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b2 in L~ b1 & b3 in L~ b1 & b1 is weakly-one-to-one holds
L~ (B_Cut b1,b2,b3) c= L~ b1
proof end;

theorem Th23: :: JORDAN23:23
for b1, b2 being FinSequence holds dom b1 c= dom (b1 ^' b2)
proof end;

theorem Th24: :: JORDAN23:24
for b1 being non empty FinSequence
for b2 being FinSequence holds dom b2 c= dom (b1 ^' b2)
proof end;

theorem Th25: :: JORDAN23:25
for b1, b2 being FinSequence st b1 ^' b2 is constant holds
b1 is constant
proof end;

theorem Th26: :: JORDAN23:26
for b1, b2 being FinSequence st b1 ^' b2 is constant & b1 . (len b1) = b2 . 1 & b1 <> {} holds
b2 is constant
proof end;

theorem Th27: :: JORDAN23:27
for b1 being special FinSequence of (TOP-REAL 2)
for b2, b3 being Nat holds mid b1,b2,b3 is special
proof end;

theorem Th28: :: JORDAN23:28
for b1 being unfolded FinSequence of (TOP-REAL 2)
for b2, b3 being Nat holds mid b1,b2,b3 is unfolded
proof end;

theorem Th29: :: JORDAN23:29
for b1 being FinSequence of (TOP-REAL 2) st b1 is special holds
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
L_Cut b1,b2 is special
proof end;

theorem Th30: :: JORDAN23:30
for b1 being FinSequence of (TOP-REAL 2) st b1 is special holds
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
R_Cut b1,b2 is special
proof end;

theorem Th31: :: JORDAN23:31
for b1 being FinSequence of (TOP-REAL 2) st b1 is special & b1 is weakly-one-to-one holds
for b2, b3 being Point of (TOP-REAL 2) st b2 in L~ b1 & b3 in L~ b1 holds
B_Cut b1,b2,b3 is special
proof end;

theorem Th32: :: JORDAN23:32
for b1 being FinSequence of (TOP-REAL 2) st b1 is unfolded holds
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
L_Cut b1,b2 is unfolded
proof end;

theorem Th33: :: JORDAN23:33
for b1 being FinSequence of (TOP-REAL 2) st b1 is unfolded holds
for b2 being Point of (TOP-REAL 2) st b2 in L~ b1 holds
R_Cut b1,b2 is unfolded
proof end;

theorem Th34: :: JORDAN23:34
for b1 being FinSequence of (TOP-REAL 2) st b1 is unfolded & b1 is weakly-one-to-one holds
for b2, b3 being Point of (TOP-REAL 2) st b2 in L~ b1 & b3 in L~ b1 holds
B_Cut b1,b2,b3 is unfolded
proof end;

theorem Th35: :: JORDAN23:35
for b1, b2 being FinSequence of (TOP-REAL 2)
for b3 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & b3 in L~ b1 & b3 <> b1 . 1 & b2 = (mid b1,1,(Index b3,b1)) ^ <*b3*> holds
b2 is_S-Seq_joining b1 /. 1,b3
proof end;

theorem Th36: :: JORDAN23:36
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is poorly-one-to-one & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b2 = b1 . ((Index b2,b1) + 1) & b2 <> b1 . (len b1) holds
((Index b2,(Rev b1)) + (Index b2,b1)) + 1 = len b1
proof end;

theorem Th37: :: JORDAN23:37
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is weakly-one-to-one & len b1 >= 2 holds
L_Cut b1,(b1 /. 1) = b1
proof end;

theorem Th38: :: JORDAN23:38
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is poorly-one-to-one & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b2 <> b1 . (len b1) holds
L_Cut (Rev b1),b2 = Rev (R_Cut b1,b2)
proof end;

theorem Th39: :: JORDAN23:39
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b2 <> b1 . 1 holds
R_Cut b1,b2 is_S-Seq_joining b1 /. 1,b2
proof end;

theorem Th40: :: JORDAN23:40
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b2 <> b1 . (len b1) & b2 <> b1 . 1 holds
L_Cut b1,b2 is_S-Seq_joining b2,b1 /. (len b1)
proof end;

theorem Th41: :: JORDAN23:41
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b2 <> b1 . 1 holds
R_Cut b1,b2 is_S-Seq
proof end;

theorem Th42: :: JORDAN23:42
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b2 <> b1 . (len b1) & b2 <> b1 . 1 holds
L_Cut b1,b2 is_S-Seq
proof end;

Lemma35: for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & b2 in L~ b1 & b3 in L~ b1 & b2 <> b3 & b2 <> b1 . 1 & ( Index b2,b1 < Index b3,b1 or ( Index b2,b1 = Index b3,b1 & LE b2,b3,b1 /. (Index b2,b1),b1 /. ((Index b2,b1) + 1) ) ) holds
B_Cut b1,b2,b3 is_S-Seq_joining b2,b3
proof end;

theorem Th43: :: JORDAN23:43
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & len b1 <> 2 & b2 in L~ b1 & b3 in L~ b1 & b2 <> b3 & b2 <> b1 . 1 & b3 <> b1 . 1 holds
B_Cut b1,b2,b3 is_S-Seq_joining b2,b3
proof end;

theorem Th44: :: JORDAN23:44
for b1 being non empty FinSequence of (TOP-REAL 2)
for b2, b3 being Point of (TOP-REAL 2) st b1 is almost-one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & len b1 <> 2 & b2 in L~ b1 & b3 in L~ b1 & b2 <> b3 & b2 <> b1 . 1 & b3 <> b1 . 1 holds
B_Cut b1,b2,b3 is_S-Seq
proof end;

theorem Th45: :: JORDAN23:45
for b1 being Nat
for b2 being compact non horizontal non vertical Subset of (TOP-REAL 2)
for b3, b4 being Point of (TOP-REAL 2) st b3 in BDD (L~ (Cage b2,b1)) holds
ex b5 being S-Sequence_in_R2 st
( b5 = B_Cut ((Rotate (Cage b2,b1),((Cage b2,b1) /. (Index (South-Bound b3,(L~ (Cage b2,b1))),(Cage b2,b1)))) | ((len (Rotate (Cage b2,b1),((Cage b2,b1) /. (Index (South-Bound b3,(L~ (Cage b2,b1))),(Cage b2,b1))))) -' 1)),(South-Bound b3,(L~ (Cage b2,b1))),(North-Bound b3,(L~ (Cage b2,b1))) & ex b6 being S-Sequence_in_R2 st
( b6 is_sequence_on GoB (b5 ^' <*(North-Bound b3,(L~ (Cage b2,b1))),(South-Bound b3,(L~ (Cage b2,b1)))*>) & L~ <*(North-Bound b3,(L~ (Cage b2,b1))),(South-Bound b3,(L~ (Cage b2,b1)))*> = L~ b6 & b6 /. 1 = North-Bound b3,(L~ (Cage b2,b1)) & b6 /. (len b6) = South-Bound b3,(L~ (Cage b2,b1)) & len b6 >= 2 & ex b7 being S-Sequence_in_R2 st
( b7 is_sequence_on GoB (b5 ^' <*(North-Bound b3,(L~ (Cage b2,b1))),(South-Bound b3,(L~ (Cage b2,b1)))*>) & L~ b5 = L~ b7 & b5 /. 1 = b7 /. 1 & b5 /. (len b5) = b7 /. (len b7) & len b5 <= len b7 & ex b8 being non constant standard special_circular_sequence st b8 = b7 ^' b6 ) ) )
proof end;