:: JORDAN9 semantic presentation

Lemma1: for b₁ being Nat st 1 <= b₁ holds
(b₁ -' 1) + 2 = b₁ + 1

proof end;

theorem Th1: :: JORDAN9:1

canceled;

theorem Th2: :: JORDAN9:2

canceled;

theorem Th3: :: JORDAN9:3

for b₁ being non empty TopSpace
for b₂, b₃, b₄, b₅ being Subset of b₁ st b₂ is connected & b₃ is_a_component_of b₅ & b₄ is_a_component_of b₅ & b₂ meets b₃ & b₂ meets b₄ & b₂ c= b₅ holds
b₃ = b₄

proof end;

theorem Th4: :: JORDAN9:4

for b₁ being non empty set
for b₂, b₃ being FinSequence of b₁ st ( for b₄ being Nat holds b₂ | b₄ = b₃ | b₄ ) holds
b₂ = b₃

proof end;

theorem Th5: :: JORDAN9:5

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₁ in dom b₃ holds
ex b₄ being Nat st
( b₄ in dom (Rev b₃) & b₁ + b₄ = (len b₃) + 1 & b₃ /. b₁ = (Rev b₃) /. b₄ )

proof end;

theorem Th6: :: JORDAN9:6

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂ st b₁ in dom (Rev b₃) holds
ex b₄ being Nat st
( b₄ in dom b₃ & b₁ + b₄ = (len b₃) + 1 & (Rev b₃) /. b₁ = b₃ /. b₄ )

proof end;

theorem Th7: :: JORDAN9:7

for b₁ being non empty set
for b₂ being Matrix of b₁
for b₃ being FinSequence of b₁ holds
( b₃ is_sequence_on b₂ iff Rev b₃ is_sequence_on b₂ )

proof end;

theorem Th8: :: JORDAN9:8

for b₁ being Nat
for b₂ being Matrix of (TOP-REAL 2)
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ <= len b₃ holds
b₃ /. b₁ in Values b₂

proof end;

Lemma8: for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ <= len b₃ holds
ex b₄, b₅ being Nat st
( [b₄,b₅] in Indices b₂ & b₃ /. b₁ = b₂ * b₄,b₅ )

proof end;

theorem Th9: :: JORDAN9:9

for b₁ being Nat
for b₂ being FinSequence of (TOP-REAL 2)
for b₃ being set st b₁ <= len b₂ & b₃ in L~ (b₂ /^ b₁) holds
ex b₄ being Nat st
( b₁ + 1 <= b₄ & b₄ + 1 <= len b₂ & b₃ in LSeg b₂,b₄ )

proof end;

theorem Th10: :: JORDAN9:10

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ + 1 <= len b₃ holds
( b₃ /. b₁ in left_cell b₃,b₁,b₂ & b₃ /. b₁ in right_cell b₃,b₁,b₂ )

proof end;

theorem Th11: :: JORDAN9:11

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ + 1 <= len b₃ holds
( Int (left_cell b₃,b₁,b₂) <> {} & Int (right_cell b₃,b₁,b₂) <> {} )

proof end;

theorem Th12: :: JORDAN9:12

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ + 1 <= len b₃ holds
( Int (left_cell b₃,b₁,b₂) is connected & Int (right_cell b₃,b₁,b₂) is connected )

proof end;

theorem Th13: :: JORDAN9:13

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ + 1 <= len b₃ holds
( Cl (Int (left_cell b₃,b₁,b₂)) = left_cell b₃,b₁,b₂ & Cl (Int (right_cell b₃,b₁,b₂)) = right_cell b₃,b₁,b₂ )

proof end;

theorem Th14: :: JORDAN9:14

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & LSeg b₃,b₁ is horizontal holds
ex b₄ being Nat st
( 1 <= b₄ & b₄ <= width b₂ & ( for b₅ being Point of (TOP-REAL 2) st b₅ in LSeg b₃,b₁ holds
b₅ `2 = (b₂ * 1,b₄) `2 ) )

proof end;

theorem Th15: :: JORDAN9:15

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & LSeg b₃,b₁ is vertical holds
ex b₄ being Nat st
( 1 <= b₄ & b₄ <= len b₂ & ( for b₅ being Point of (TOP-REAL 2) st b₅ in LSeg b₃,b₁ holds
b₅ `1 = (b₂ * b₄,1) `1 ) )

proof end;

theorem Th16: :: JORDAN9:16

for b₁, b₂ being Nat
for b₃ being Go-board
for b₄ being FinSequence of (TOP-REAL 2) st b₄ is_sequence_on b₃ & b₄ is special & b₁ <= len b₃ & b₂ <= width b₃ holds
Int (cell b₃,b₁,b₂) misses L~ b₄

proof end;

theorem Th17: :: JORDAN9:17

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & b₃ is special & 1 <= b₁ & b₁ + 1 <= len b₃ holds
( Int (left_cell b₃,b₁,b₂) misses L~ b₃ & Int (right_cell b₃,b₁,b₂) misses L~ b₃ )

proof end;

theorem Th18: :: JORDAN9:18

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₃ & 1 <= b₂ & b₂ + 1 <= width b₃ holds
( (b₃ * b₁,b₂) `1 = (b₃ * b₁,(b₂ + 1)) `1 & (b₃ * b₁,b₂) `2 = (b₃ * (b₁ + 1),b₂) `2 & (b₃ * (b₁ + 1),(b₂ + 1)) `1 = (b₃ * (b₁ + 1),b₂) `1 & (b₃ * (b₁ + 1),(b₂ + 1)) `2 = (b₃ * b₁,(b₂ + 1)) `2 )

proof end;

theorem Th19: :: JORDAN9:19

for b₁ being Go-board
for b₂ being Point of (TOP-REAL 2)
for b₃, b₄ being Nat st 1 <= b₃ & b₃ + 1 <= len b₁ & 1 <= b₄ & b₄ + 1 <= width b₁ holds
( b₂ in cell b₁,b₃,b₄ iff ( (b₁ * b₃,b₄) `1 <= b₂ `1 & b₂ `1 <= (b₁ * (b₃ + 1),b₄) `1 & (b₁ * b₃,b₄) `2 <= b₂ `2 & b₂ `2 <= (b₁ * b₃,(b₄ + 1)) `2 ) )

proof end;

theorem Th20: :: JORDAN9:20

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₃ & 1 <= b₂ & b₂ + 1 <= width b₃ holds
cell b₃,b₁,b₂ = { |[b₄,b₅]| where B is Real, B is Real : ( (b₃ * b₁,b₂) `1 <= b₄ & b₄ <= (b₃ * (b₁ + 1),b₂) `1 & (b₃ * b₁,b₂) `2 <= b₅ & b₅ <= (b₃ * b₁,(b₂ + 1)) `2 ) }

proof end;

theorem Th21: :: JORDAN9:21

for b₁, b₂ being Nat
for b₃ being Go-board
for b₄ being Point of (TOP-REAL 2) st 1 <= b₁ & b₁ + 1 <= len b₃ & 1 <= b₂ & b₂ + 1 <= width b₃ & b₄ in Values b₃ & b₄ in cell b₃,b₁,b₂ & not b₄ = b₃ * b₁,b₂ & not b₄ = b₃ * b₁,(b₂ + 1) & not b₄ = b₃ * (b₁ + 1),(b₂ + 1) holds
b₄ = b₃ * (b₁ + 1),b₂

proof end;

theorem Th22: :: JORDAN9:22

for b₁, b₂ being Nat
for b₃ being Go-board st 1 <= b₁ & b₁ + 1 <= len b₃ & 1 <= b₂ & b₂ + 1 <= width b₃ holds
( b₃ * b₁,b₂ in cell b₃,b₁,b₂ & b₃ * b₁,(b₂ + 1) in cell b₃,b₁,b₂ & b₃ * (b₁ + 1),(b₂ + 1) in cell b₃,b₁,b₂ & b₃ * (b₁ + 1),b₂ in cell b₃,b₁,b₂ )

proof end;

theorem Th23: :: JORDAN9:23

for b₁, b₂ being Nat
for b₃ being Go-board
for b₄ being Point of (TOP-REAL 2) st 1 <= b₁ & b₁ + 1 <= len b₃ & 1 <= b₂ & b₂ + 1 <= width b₃ & b₄ in Values b₃ & b₄ in cell b₃,b₁,b₂ holds
b₄ is_extremal_in cell b₃,b₁,b₂

proof end;

theorem Th24: :: JORDAN9:24

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2) st 2 <= len b₂ & 2 <= width b₂ & b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ + 1 <= len b₃ holds
ex b₄, b₅ being Nat st
( 1 <= b₄ & b₄ + 1 <= len b₂ & 1 <= b₅ & b₅ + 1 <= width b₂ & LSeg b₃,b₁ c= cell b₂,b₄,b₅ )

proof end;

theorem Th25: :: JORDAN9:25

for b₁ being Nat
for b₂ being Go-board
for b₃ being FinSequence of (TOP-REAL 2)
for b₄ being Point of (TOP-REAL 2) st 2 <= len b₂ & 2 <= width b₂ & b₃ is_sequence_on b₂ & 1 <= b₁ & b₁ + 1 <= len b₃ & b₄ in Values b₂ & b₄ in LSeg b₃,b₁ & not b₄ = b₃ /. b₁ holds
b₄ = b₃ /. (b₁ + 1)

proof end;

theorem Th26: :: JORDAN9:26

for b₁, b₂, b₃ being Nat
for b₄ being Go-board st [b₁,b₂] in Indices b₄ & 1 <= b₃ & b₃ <= width b₄ holds
(b₄ * b₁,b₂) `1 <= (b₄ * (len b₄),b₃) `1

proof end;

theorem Th27: :: JORDAN9:27

for b₁, b₂, b₃ being Nat
for b₄ being Go-board st [b₁,b₂] in Indices b₄ & 1 <= b₃ & b₃ <= len b₄ holds
(b₄ * b₁,b₂) `2 <= (b₄ * b₃,(width b₄)) `2

proof end;

theorem Th28: :: JORDAN9:28

for b₁ being Nat
for b₂ being Go-board
for b₃, b₄ being FinSequence of (TOP-REAL 2) st b₃ is_sequence_on b₂ & b₃ is special & L~ b₄ c= L~ b₃ & 1 <= b₁ & b₁ + 1 <= len b₃ holds
for b₅ being Subset of (TOP-REAL 2) st ( b₅ = (right_cell b₃,b₁,b₂) \ (L~ b₄) or b₅ = (left_cell b₃,b₁,b₂) \ (L~ b₄) ) holds
b₅ is connected

proof end;

theorem Th29: :: JORDAN9:29

for b₁ being Go-board
for b₂ being non constant standard special_circular_sequence st b₂ is_sequence_on b₁ holds
for b₃ being Nat st 1 <= b₃ & b₃ + 1 <= len b₂ holds
( (right_cell b₂,b₃,b₁) \ (L~ b₂) c= RightComp b₂ & (left_cell b₂,b₃,b₁) \ (L~ b₂) c= LeftComp b₂ )

proof end;

theorem Th30: :: JORDAN9:30

for b₁ being Nat
for b₂ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex b₃ being Nat st
( 1 <= b₃ & b₃ + 1 <= len (Gauge b₂,b₁) & N-min b₂ in cell (Gauge b₂,b₁),b₃,((width (Gauge b₂,b₁)) -' 1) & N-min b₂ <> (Gauge b₂,b₁) * b₃,((width (Gauge b₂,b₁)) -' 1) )

proof end;

theorem Th31: :: JORDAN9:31

for b₁ being Nat
for b₂ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃, b₄ being Nat st 1 <= b₃ & b₃ + 1 <= len (Gauge b₂,b₁) & N-min b₂ in cell (Gauge b₂,b₁),b₃,((width (Gauge b₂,b₁)) -' 1) & N-min b₂ <> (Gauge b₂,b₁) * b₃,((width (Gauge b₂,b₁)) -' 1) & 1 <= b₄ & b₄ + 1 <= len (Gauge b₂,b₁) & N-min b₂ in cell (Gauge b₂,b₁),b₄,((width (Gauge b₂,b₁)) -' 1) & N-min b₂ <> (Gauge b₂,b₁) * b₄,((width (Gauge b₂,b₁)) -' 1) holds
b₃ = b₄

proof end;

theorem Th32: :: JORDAN9:32

for b₁ being Nat
for b₂ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for b₃ being non constant standard special_circular_sequence st b₃ is_sequence_on Gauge b₂,b₁ & ( for b₄ being Nat st 1 <= b₄ & b₄ + 1 <= len b₃ holds
( left_cell b₃,b₄,(Gauge b₂,b₁) misses b₂ & right_cell b₃,b₄,(Gauge b₂,b₁) meets b₂ ) ) & ex b₄ being Nat st
( 1 <= b₄ & b₄ + 1 <= len (Gauge b₂,b₁) & b₃ /. 1 = (Gauge b₂,b₁) * b₄,(width (Gauge b₂,b₁)) & b₃ /. 2 = (Gauge b₂,b₁) * (b₄ + 1),(width (Gauge b₂,b₁)) & N-min b₂ in cell (Gauge b₂,b₁),b₄,((width (Gauge b₂,b₁)) -' 1) & N-min b₂ <> (Gauge b₂,b₁) * b₄,((width (Gauge b₂,b₁)) -' 1) ) holds
N-min (L~ b₃) = b₃ /. 1

proof end;

definition

let c₁ be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
let c₂ be Nat;
assume E30: c₁ is connected ;
func Cage c₁,c₂ -> clockwise_oriented non constant standard special_circular_sequence means :Def1: :: JORDAN9:def 1
( a₃ is_sequence_on Gauge a₁,a₂ & ex b₁ being Nat st
( 1 <= b₁ & b₁ + 1 <= len (Gauge a₁,a₂) & a₃ /. 1 = (Gauge a₁,a₂) * b₁,(width (Gauge a₁,a₂)) & a₃ /. 2 = (Gauge a₁,a₂) * (b₁ + 1),(width (Gauge a₁,a₂)) & N-min a₁ in cell (Gauge a₁,a₂),b₁,((width (Gauge a₁,a₂)) -' 1) & N-min a₁ <> (Gauge a₁,a₂) * b₁,((width (Gauge a₁,a₂)) -' 1) ) & ( for b₁ being Nat st 1 <= b₁ & b₁ + 2 <= len a₃ holds
( ( front_left_cell a₃,b₁,(Gauge a₁,a₂) misses a₁ & front_right_cell a₃,b₁,(Gauge a₁,a₂) misses a₁ implies a₃ turns_right b₁, Gauge a₁,a₂ ) & ( front_left_cell a₃,b₁,(Gauge a₁,a₂) misses a₁ & front_right_cell a₃,b₁,(Gauge a₁,a₂) meets a₁ implies a₃ goes_straight b₁, Gauge a₁,a₂ ) & ( front_left_cell a₃,b₁,(Gauge a₁,a₂) meets a₁ implies a₃ turns_left b₁, Gauge a₁,a₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines Cage JORDAN9:def 1 :

theorem Th33: :: JORDAN9:33

for b₁, b₂ being Nat
for b₃ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st b₃ is connected & 1 <= b₁ & b₁ + 1 <= len (Cage b₃,b₂) holds
( left_cell (Cage b₃,b₂),b₁,(Gauge b₃,b₂) misses b₃ & right_cell (Cage b₃,b₂),b₁,(Gauge b₃,b₂) meets b₃ )

proof end;

theorem Th34: :: JORDAN9:34

for b₁ being Nat
for b₂ being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st b₂ is connected holds
N-min (L~ (Cage b₂,b₁)) = (Cage b₂,b₁) /. 1

proof end;