:: JORDAN12 semantic presentation

Lemma1: for b1 being Relation st b1 is trivial holds
dom b1 is trivial
proof end;

Lemma2: for b1 being FinSequence st dom b1 is trivial holds
len b1 is trivial
proof end;

Lemma3: for b1 being FinSequence st b1 is trivial holds
len b1 is trivial
proof end;

theorem Th1: :: JORDAN12:1
for b1 being Nat st 1 < b1 holds
0 < b1 -' 1
proof end;

theorem Th2: :: JORDAN12:2
canceled;

theorem Th3: :: JORDAN12:3
not 1 is even
proof end;

theorem Th4: :: JORDAN12:4
for b1 being Nat
for b2 being FinSequence of (TOP-REAL b1)
for b3 being Nat st 1 <= b3 & b3 + 1 <= len b2 holds
( b2 /. b3 in rng b2 & b2 /. (b3 + 1) in rng b2 )
proof end;

registration
cluster s.n.c. -> s.c.c. FinSequence of the carrier of (TOP-REAL 2);
coherence
for b1 being FinSequence of (TOP-REAL 2) st b1 is s.n.c. holds
b1 is s.c.c.
proof end;
end;

theorem Th5: :: JORDAN12:5
for b1, b2 being FinSequence of (TOP-REAL 2) st b1 ^' b2 is unfolded & b1 ^' b2 is s.c.c. & len b2 >= 2 holds
( b1 is unfolded & b1 is s.n.c. )
proof end;

theorem Th6: :: JORDAN12:6
for b1, b2 being FinSequence of (TOP-REAL 2) holds L~ b1 c= L~ (b1 ^' b2)
proof end;

definition
let c1 be Nat;
let c2, c3 be FinSequence of (TOP-REAL c1);
pred c2 is_in_general_position_wrt c3 means :Def1: :: JORDAN12:def 1
( L~ a2 misses rng a3 & ( for b1 being Nat st 1 <= b1 & b1 < len a3 holds
(L~ a2) /\ (LSeg a3,b1) is trivial ) );
end;

:: deftheorem Def1 defines is_in_general_position_wrt JORDAN12:def 1 :
for b1 being Nat
for b2, b3 being FinSequence of (TOP-REAL b1) holds
( b2 is_in_general_position_wrt b3 iff ( L~ b2 misses rng b3 & ( for b4 being Nat st 1 <= b4 & b4 < len b3 holds
(L~ b2) /\ (LSeg b3,b4) is trivial ) ) );

definition
let c1 be Nat;
let c2, c3 be FinSequence of (TOP-REAL c1);
pred c2,c3 are_in_general_position means :Def2: :: JORDAN12:def 2
( a2 is_in_general_position_wrt a3 & a3 is_in_general_position_wrt a2 );
symmetry
for b1, b2 being FinSequence of (TOP-REAL c1) st b1 is_in_general_position_wrt b2 & b2 is_in_general_position_wrt b1 holds
( b2 is_in_general_position_wrt b1 & b1 is_in_general_position_wrt b2 ) ;
end;

:: deftheorem Def2 defines are_in_general_position JORDAN12:def 2 :
for b1 being Nat
for b2, b3 being FinSequence of (TOP-REAL b1) holds
( b2,b3 are_in_general_position iff ( b2 is_in_general_position_wrt b3 & b3 is_in_general_position_wrt b2 ) );

theorem Th7: :: JORDAN12:7
for b1 being Nat
for b2, b3 being FinSequence of (TOP-REAL 2) st b2,b3 are_in_general_position holds
for b4 being FinSequence of (TOP-REAL 2) st b4 = b3 | (Seg b1) holds
b2,b4 are_in_general_position
proof end;

theorem Th8: :: JORDAN12:8
for b1, b2, b3, b4 being FinSequence of (TOP-REAL 2) st b1 ^' b2,b3 ^' b4 are_in_general_position holds
b1 ^' b2,b3 are_in_general_position
proof end;

theorem Th9: :: JORDAN12:9
for b1 being Nat
for b2, b3 being FinSequence of (TOP-REAL 2) st 1 <= b1 & b1 + 1 <= len b3 & b2,b3 are_in_general_position holds
( b3 . b1 in (L~ b2) ` & b3 . (b1 + 1) in (L~ b2) ` )
proof end;

theorem Th10: :: JORDAN12:10
for b1, b2 being FinSequence of (TOP-REAL 2) st b1,b2 are_in_general_position holds
for b3, b4 being Nat st 1 <= b3 & b3 + 1 <= len b1 & 1 <= b4 & b4 + 1 <= len b2 holds
(LSeg b1,b3) /\ (LSeg b2,b4) is trivial
proof end;

theorem Th11: :: JORDAN12:11
for b1, b2 being FinSequence of (TOP-REAL 2) holds INTERSECTION { (LSeg b1,b3) where B is Nat : ( 1 <= b3 & b3 + 1 <= len b1 ) } ,{ (LSeg b2,b3) where B is Nat : ( 1 <= b3 & b3 + 1 <= len b2 ) } is finite
proof end;

theorem Th12: :: JORDAN12:12
for b1, b2 being FinSequence of (TOP-REAL 2) st b1,b2 are_in_general_position holds
(L~ b1) /\ (L~ b2) is finite
proof end;

theorem Th13: :: JORDAN12:13
for b1, b2 being FinSequence of (TOP-REAL 2) st b1,b2 are_in_general_position holds
for b3 being Nat holds (L~ b1) /\ (LSeg b2,b3) is finite
proof end;

theorem Th14: :: JORDAN12:14
for b1 being non constant standard special_circular_sequence
for b2, b3 being Point of (TOP-REAL 2) st LSeg b2,b3 misses L~ b1 holds
ex b4 being Subset of (TOP-REAL 2) st
( b4 is_a_component_of (L~ b1) ` & b2 in b4 & b3 in b4 )
proof end;

theorem Th15: :: JORDAN12:15
for b1, b2 being set
for b3 being non constant standard special_circular_sequence holds
( ( ( b1 in RightComp b3 & b2 in RightComp b3 ) or ( b1 in LeftComp b3 & b2 in LeftComp b3 ) ) iff ex b4 being Subset of (TOP-REAL 2) st
( b4 is_a_component_of (L~ b3) ` & b1 in b4 & b2 in b4 ) )
proof end;

theorem Th16: :: JORDAN12:16
for b1, b2 being set
for b3 being non constant standard special_circular_sequence holds
( ( b1 in (L~ b3) ` & b2 in (L~ b3) ` & ( for b4 being Subset of (TOP-REAL 2) holds
( not b4 is_a_component_of (L~ b3) ` or not b1 in b4 or not b2 in b4 ) ) ) iff ( ( b1 in LeftComp b3 & b2 in RightComp b3 ) or ( b1 in RightComp b3 & b2 in LeftComp b3 ) ) )
proof end;

theorem Th17: :: JORDAN12:17
for b1 being non constant standard special_circular_sequence
for b2, b3, b4 being set st ex b5 being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b1) ` & b2 in b5 & b3 in b5 ) & ex b5 being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b1) ` & b3 in b5 & b4 in b5 ) holds
ex b5 being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b1) ` & b2 in b5 & b4 in b5 )
proof end;

theorem Th18: :: JORDAN12:18
for b1 being non constant standard special_circular_sequence
for b2, b3, b4 being set st b2 in (L~ b1) ` & b3 in (L~ b1) ` & b4 in (L~ b1) ` & ( for b5 being Subset of (TOP-REAL 2) holds
( not b5 is_a_component_of (L~ b1) ` or not b2 in b5 or not b3 in b5 ) ) & ( for b5 being Subset of (TOP-REAL 2) holds
( not b5 is_a_component_of (L~ b1) ` or not b3 in b5 or not b4 in b5 ) ) holds
ex b5 being Subset of (TOP-REAL 2) st
( b5 is_a_component_of (L~ b1) ` & b2 in b5 & b4 in b5 )
proof end;

E22: now
let c1 be Go-board;
let c2 be Nat;
assume E23: c2 <= len c1 ;
let c3, c4 be Point of (TOP-REAL 2);
assume that
E24: ( c3 in v_strip c1,c2 & c4 in v_strip c1,c2 ) and
E25: c3 `1 <= c4 `1 ;
thus LSeg c3,c4 c= v_strip c1,c2
proof
let c5 be set ; :: according to TARSKI:def 3
assume E26: c5 in LSeg c3,c4 ;
reconsider c6 = c5 as Point of (TOP-REAL 2) by E26;
E27: c6 = |[(c6 `1 ),(c6 `2 )]| by EUCLID:57;
E28: ( c3 `1 <= c6 `1 & c6 `1 <= c4 `1 ) by E25, E26, TOPREAL1:9;
per cases ( c2 = 0 or c2 = len c1 or ( 1 <= c2 & c2 < len c1 ) ) by E23, XREAL_1:1, NAT_1:39;
suppose c2 = 0 ;
then E29: v_strip c1,c2 = { |[b1,b2]| where B is Real, B is Real : b1 <= (c1 * 1,1) `1 } by GOBRD11:18;
then consider c7, c8 being Real such that
E30: ( c4 = |[c7,c8]| & c7 <= (c1 * 1,1) `1 ) by E24;
c4 `1 <= (c1 * 1,1) `1 by E30, EUCLID:56;
then c6 `1 <= (c1 * 1,1) `1 by E28, XREAL_1:2;
hence c5 in v_strip c1,c2 by E27, E29;
end;
suppose c2 = len c1 ;
then E29: v_strip c1,c2 = { |[b1,b2]| where B is Real, B is Real : (c1 * (len c1),1) `1 <= b1 } by GOBRD11:19;
then consider c7, c8 being Real such that
E30: ( c3 = |[c7,c8]| & (c1 * (len c1),1) `1 <= c7 ) by E24;
(c1 * (len c1),1) `1 <= c3 `1 by E30, EUCLID:56;
then (c1 * (len c1),1) `1 <= c6 `1 by E28, XREAL_1:2;
hence c5 in v_strip c1,c2 by E27, E29;
end;
suppose ( 1 <= c2 & c2 < len c1 ) ;
then E29: v_strip c1,c2 = { |[b1,b2]| where B is Real, B is Real : ( (c1 * c2,1) `1 <= b1 & b1 <= (c1 * (c2 + 1),1) `1 ) } by GOBRD11:20;
then consider c7, c8 being Real such that
E30: ( c3 = |[c7,c8]| & (c1 * c2,1) `1 <= c7 & c7 <= (c1 * (c2 + 1),1) `1 ) by E24;
( (c1 * c2,1) `1 <= c3 `1 & c3 `1 <= (c1 * (c2 + 1),1) `1 ) by E30, EUCLID:56;
then E31: (c1 * c2,1) `1 <= c6 `1 by E28, XREAL_1:2;
consider c9, c10 being Real such that
E32: ( c4 = |[c9,c10]| & (c1 * c2,1) `1 <= c9 & c9 <= (c1 * (c2 + 1),1) `1 ) by E24, E29;
( (c1 * c2,1) `1 <= c4 `1 & c4 `1 <= (c1 * (c2 + 1),1) `1 ) by E32, EUCLID:56;
then c6 `1 <= (c1 * (c2 + 1),1) `1 by E28, XREAL_1:2;
hence c5 in v_strip c1,c2 by E27, E29, E31;
end;
end;
end;
end;

theorem Th19: :: JORDAN12:19
for b1 being Nat
for b2 being Go-board st b1 <= len b2 holds
v_strip b2,b1 is convex
proof end;

E24: now
let c1 be Go-board;
let c2 be Nat;
assume E25: c2 <= width c1 ;
let c3, c4 be Point of (TOP-REAL 2);
assume that
E26: ( c3 in h_strip c1,c2 & c4 in h_strip c1,c2 ) and
E27: c3 `2 <= c4 `2 ;
thus LSeg c3,c4 c= h_strip c1,c2
proof
let c5 be set ; :: according to TARSKI:def 3
assume E28: c5 in LSeg c3,c4 ;
then reconsider c6 = c5 as Point of (TOP-REAL 2) ;
E29: c6 = |[(c6 `1 ),(c6 `2 )]| by EUCLID:57;
E30: ( c3 `2 <= c6 `2 & c6 `2 <= c4 `2 ) by E27, E28, TOPREAL1:10;
per cases ( c2 = 0 or c2 = width c1 or ( 1 <= c2 & c2 < width c1 ) ) by E25, XREAL_1:1, NAT_1:39;
suppose c2 = 0 ;
then E31: h_strip c1,c2 = { |[b1,b2]| where B is Real, B is Real : b2 <= (c1 * 1,1) `2 } by GOBRD11:21;
then consider c7, c8 being Real such that
E32: ( c4 = |[c7,c8]| & c8 <= (c1 * 1,1) `2 ) by E26;
c4 `2 <= (c1 * 1,1) `2 by E32, EUCLID:56;
then c6 `2 <= (c1 * 1,1) `2 by E30, XREAL_1:2;
hence c5 in h_strip c1,c2 by E29, E31;
end;
suppose c2 = width c1 ;
then E31: h_strip c1,c2 = { |[b1,b2]| where B is Real, B is Real : (c1 * 1,(width c1)) `2 <= b2 } by GOBRD11:22;
then consider c7, c8 being Real such that
E32: ( c3 = |[c7,c8]| & (c1 * 1,(width c1)) `2 <= c8 ) by E26;
(c1 * 1,(width c1)) `2 <= c3 `2 by E32, EUCLID:56;
then (c1 * 1,(width c1)) `2 <= c6 `2 by E30, XREAL_1:2;
hence c5 in h_strip c1,c2 by E29, E31;
end;
suppose ( 1 <= c2 & c2 < width c1 ) ;
then E31: h_strip c1,c2 = { |[b1,b2]| where B is Real, B is Real : ( (c1 * 1,c2) `2 <= b2 & b2 <= (c1 * 1,(c2 + 1)) `2 ) } by GOBRD11:23;
then consider c7, c8 being Real such that
E32: ( c3 = |[c7,c8]| & (c1 * 1,c2) `2 <= c8 & c8 <= (c1 * 1,(c2 + 1)) `2 ) by E26;
( (c1 * 1,c2) `2 <= c3 `2 & c3 `2 <= (c1 * 1,(c2 + 1)) `2 ) by E32, EUCLID:56;
then E33: (c1 * 1,c2) `2 <= c6 `2 by E30, XREAL_1:2;
consider c9, c10 being Real such that
E34: ( c4 = |[c9,c10]| & (c1 * 1,c2) `2 <= c10 & c10 <= (c1 * 1,(c2 + 1)) `2 ) by E26, E31;
( (c1 * 1,c2) `2 <= c4 `2 & c4 `2 <= (c1 * 1,(c2 + 1)) `2 ) by E34, EUCLID:56;
then c6 `2 <= (c1 * 1,(c2 + 1)) `2 by E30, XREAL_1:2;
hence c5 in h_strip c1,c2 by E29, E31, E33;
end;
end;
end;
end;

theorem Th20: :: JORDAN12:20
for b1 being Nat
for b2 being Go-board st b1 <= width b2 holds
h_strip b2,b1 is convex
proof end;

theorem Th21: :: JORDAN12:21
for b1, b2 being Nat
for b3 being Go-board st b1 <= len b3 & b2 <= width b3 holds
cell b3,b1,b2 is convex
proof end;

theorem Th22: :: JORDAN12:22
for b1 being non constant standard special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 1 <= len b1 holds
left_cell b1,b2 is convex
proof end;

theorem Th23: :: JORDAN12:23
for b1 being non constant standard special_circular_sequence
for b2 being Nat st 1 <= b2 & b2 + 1 <= len b1 holds
( left_cell b1,b2,(GoB b1) is convex & right_cell b1,b2,(GoB b1) is convex )
proof end;

theorem Th24: :: JORDAN12:24
for b1, b2 being Point of (TOP-REAL 2)
for b3 being non constant standard special_circular_sequence
for b4 being Point of (TOP-REAL 2) st b4 in LSeg b1,b2 & ex b5 being set st (L~ b3) /\ (LSeg b1,b2) = {b5} & not b4 in L~ b3 & not L~ b3 misses LSeg b1,b4 holds
L~ b3 misses LSeg b4,b2
proof end;

E30: now
let c1, c2 be Point of (TOP-REAL 2);
let c3 be non constant standard special_circular_sequence;
let c4 be Point of (TOP-REAL 2);
assume E31: c4 in LSeg c1,c2 ;
assume that
E32: ex b1 being set st (L~ c3) /\ (LSeg c1,c2) = {b1} and
E33: not c4 in L~ c3 ;
per cases ( L~ c3 misses LSeg c1,c4 or L~ c3 misses LSeg c4,c2 ) by E31, E32, E33, Th24;
suppose L~ c3 misses LSeg c1,c4 ;
hence ( ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ c3) ` & c4 in b1 & c1 in b1 ) or ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ c3) ` & c4 in b1 & c2 in b1 ) ) by Th14;
end;
suppose L~ c3 misses LSeg c4,c2 ;
hence ( ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ c3) ` & c4 in b1 & c1 in b1 ) or ex b1 being Subset of (TOP-REAL 2) st
( b1 is_a_component_of (L~ c3) ` & c4 in b1 & c2 in b1 ) ) by Th14;
end;
end;
end;

theorem Th25: :: JORDAN12:25
for b1, b2, b3, b4 being Point of (TOP-REAL 2) st LSeg b1,b2 is vertical & LSeg b3,b4 is vertical & LSeg b1,b2 meets LSeg b3,b4 holds
b1 `1 = b3 `1
proof end;

theorem Th26: :: JORDAN12:26
for b1, b2, b3 being Point of (TOP-REAL 2) st not b1 in LSeg b2,b3 & b2 `2 = b3 `2 & b3 `2 = b1 `2 & not b2 in LSeg b1,b3 holds
b3 in LSeg b1,b2
proof end;

theorem Th27: :: JORDAN12:27
for b1, b2, b3 being Point of (TOP-REAL 2) st not b1 in LSeg b2,b3 & b2 `1 = b3 `1 & b3 `1 = b1 `1 & not b2 in LSeg b1,b3 holds
b3 in LSeg b1,b2
proof end;

theorem Th28: :: JORDAN12:28
for b1, b2, b3 being Point of (TOP-REAL 2) st b1 <> b2 & b1 <> b3 & b1 in LSeg b2,b3 holds
not b2 in LSeg b1,b3
proof end;

theorem Th29: :: JORDAN12:29
for b1, b2, b3, b4 being Point of (TOP-REAL 2) st not b4 in LSeg b2,b3 & b1 in LSeg b2,b3 & b1 <> b2 & b1 <> b3 & ( ( b2 `1 = b3 `1 & b3 `1 = b4 `1 ) or ( b2 `2 = b3 `2 & b3 `2 = b4 `2 ) ) & not b2 in LSeg b4,b1 holds
b3 in LSeg b4,b1
proof end;

theorem Th30: :: JORDAN12:30
for b1, b2, b3, b4, b5 being Point of (TOP-REAL 2) st ( ( b1 `1 = b2 `1 & b3 `1 = b4 `1 ) or ( b1 `2 = b2 `2 & b3 `2 = b4 `2 ) ) & (LSeg b1,b2) /\ (LSeg b3,b4) = {b5} & not b5 = b1 & not b5 = b2 holds
b5 = b3
proof end;

theorem Th31: :: JORDAN12:31
for b1, b2, b3 being Point of (TOP-REAL 2)
for b4 being non constant standard special_circular_sequence st (L~ b4) /\ (LSeg b2,b3) = {b1} holds
for b5 being Point of (TOP-REAL 2) st not b5 in LSeg b2,b3 & not b2 in L~ b4 & not b3 in L~ b4 & ( ( b2 `1 = b3 `1 & b2 `1 = b5 `1 ) or ( b2 `2 = b3 `2 & b2 `2 = b5 `2 ) ) & ex b6 being Nat st
( 1 <= b6 & b6 + 1 <= len b4 & ( b5 in right_cell b4,b6,(GoB b4) or b5 in left_cell b4,b6,(GoB b4) ) & b1 in LSeg b4,b6 ) & not b5 in L~ b4 & ( for b6 being Subset of (TOP-REAL 2) holds
( not b6 is_a_component_of (L~ b4) ` or not b5 in b6 or not b2 in b6 ) ) holds
ex b6 being Subset of (TOP-REAL 2) st
( b6 is_a_component_of (L~ b4) ` & b5 in b6 & b3 in b6 )
proof end;

theorem Th32: :: JORDAN12:32
for b1 being non constant standard special_circular_sequence
for b2, b3, b4 being Point of (TOP-REAL 2) st (L~ b1) /\ (LSeg b2,b3) = {b4} holds
for b5, b6 being Point of (TOP-REAL 2) st not b2 in L~ b1 & not b3 in L~ b1 & ( ( b2 `1 = b3 `1 & b2 `1 = b5 `1 & b5 `1 = b6 `1 ) or ( b2 `2 = b3 `2 & b2 `2 = b5 `2 & b5 `2 = b6 `2 ) ) & ex b7 being Nat st
( 1 <= b7 & b7 + 1 <= len b1 & b5 in left_cell b1,b7,(GoB b1) & b6 in right_cell b1,b7,(GoB b1) & b4 in LSeg b1,b7 ) & not b5 in L~ b1 & not b6 in L~ b1 holds
for b7 being Subset of (TOP-REAL 2) holds
( not b7 is_a_component_of (L~ b1) ` or not b2 in b7 or not b3 in b7 )
proof end;

theorem Th33: :: JORDAN12:33
for b1 being Point of (TOP-REAL 2)
for b2 being non constant standard special_circular_sequence
for b3, b4 being Point of (TOP-REAL 2) st (L~ b2) /\ (LSeg b3,b4) = {b1} & ( b3 `1 = b4 `1 or b3 `2 = b4 `2 ) & not b3 in L~ b2 & not b4 in L~ b2 & rng b2 misses LSeg b3,b4 holds
for b5 being Subset of (TOP-REAL 2) holds
( not b5 is_a_component_of (L~ b2) ` or not b3 in b5 or not b4 in b5 )
proof end;

theorem Th34: :: JORDAN12:34
for b1 being non constant standard special_circular_sequence
for b2 being special FinSequence of (TOP-REAL 2) st b1,b2 are_in_general_position holds
for b3 being Nat st 1 <= b3 & b3 + 1 <= len b2 holds
( Card ((L~ b1) /\ (LSeg b2,b3)) is even Nat iff ex b4 being Subset of (TOP-REAL 2) st
( b4 is_a_component_of (L~ b1) ` & b2 . b3 in b4 & b2 . (b3 + 1) in b4 ) )
proof end;

theorem Th35: :: JORDAN12:35
for b1, b2, b3 being special FinSequence of (TOP-REAL 2) st b1 ^' b2 is non constant standard special_circular_sequence & b1 ^' b2,b3 are_in_general_position & len b3 >= 2 & b3 is unfolded & b3 is s.n.c. holds
( Card ((L~ (b1 ^' b2)) /\ (L~ b3)) is even Nat iff ex b4 being Subset of (TOP-REAL 2) st
( b4 is_a_component_of (L~ (b1 ^' b2)) ` & b3 . 1 in b4 & b3 . (len b3) in b4 ) )
proof end;

theorem Th36: :: JORDAN12:36
for b1, b2, b3, b4 being special FinSequence of (TOP-REAL 2) st b1 ^' b2 is non constant standard special_circular_sequence & b3 ^' b4 is non constant standard special_circular_sequence & L~ b1 misses L~ b4 & L~ b2 misses L~ b3 & b1 ^' b2,b3 ^' b4 are_in_general_position holds
for b5, b6, b7, b8 being Point of (TOP-REAL 2) st b1 . 1 = b5 & b1 . (len b1) = b6 & b3 . 1 = b7 & b3 . (len b3) = b8 & b1 /. (len b1) = b2 /. 1 & b3 /. (len b3) = b4 /. 1 & b5 in (L~ b1) /\ (L~ b2) & b7 in (L~ b3) /\ (L~ b4) & ex b9 being Subset of (TOP-REAL 2) st
( b9 is_a_component_of (L~ (b1 ^' b2)) ` & b7 in b9 & b8 in b9 ) holds
ex b9 being Subset of (TOP-REAL 2) st
( b9 is_a_component_of (L~ (b3 ^' b4)) ` & b5 in b9 & b6 in b9 )
proof end;