:: JORDAN11 semantic presentation

Lemma1: for b₁, b₂, b₃ being Nat
for b₄ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ > 0 & 1 <= b₂ & b₂ <= width (Gauge b₄,b₁) & b₃ <= b₂ & 1 <= b₃ & b₃ <= width (Gauge b₄,b₁) & (LSeg ((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₂),((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₃)) /\ (Upper_Arc (L~ (Cage b₄,b₁))) = {((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₂)} & (LSeg ((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₂),((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₃)) /\ (Lower_Arc (L~ (Cage b₄,b₁))) = {((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₃)} holds
LSeg ((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₂),((Gauge b₄,b₁) * (Center (Gauge b₄,b₁)),b₃) c= Cl (RightComp (Cage b₄,b₁))

proof end;

Lemma2: for b₁ being being_simple_closed_curve Subset of (TOP-REAL 2) ex b₂ being Nat st b₂ is_sufficiently_large_for b₁

proof end;

definition

let c₁ be being_simple_closed_curve Subset of (TOP-REAL 2);
func ApproxIndex c₁ -> Nat means :Def1: :: JORDAN11:def 1
( a₂ is_sufficiently_large_for a₁ & ( for b₁ being Nat st b₁ is_sufficiently_large_for a₁ holds
b₁ >= a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines ApproxIndex JORDAN11:def 1 :

theorem Th1: :: JORDAN11:1

for b₁ being being_simple_closed_curve Subset of (TOP-REAL 2) holds ApproxIndex b₁ >= 1

proof end;

definition

let c₁ be being_simple_closed_curve Subset of (TOP-REAL 2);
func Y-InitStart c₁ -> Nat means :Def2: :: JORDAN11:def 2
( a₂ < width (Gauge a₁,(ApproxIndex a₁)) & cell (Gauge a₁,(ApproxIndex a₁)),((X-SpanStart a₁,(ApproxIndex a₁)) -' 1),a₂ c= BDD a₁ & ( for b₁ being Nat st b₁ < width (Gauge a₁,(ApproxIndex a₁)) & cell (Gauge a₁,(ApproxIndex a₁)),((X-SpanStart a₁,(ApproxIndex a₁)) -' 1),b₁ c= BDD a₁ holds
b₁ >= a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Y-InitStart JORDAN11:def 2 :

theorem Th2: :: JORDAN11:2

for b₁ being being_simple_closed_curve Subset of (TOP-REAL 2) holds Y-InitStart b₁ > 1

proof end;

theorem Th3: :: JORDAN11:3

for b₁ being being_simple_closed_curve Subset of (TOP-REAL 2) holds (Y-InitStart b₁) + 1 < width (Gauge b₁,(ApproxIndex b₁))

proof end;

definition

let c₁ be being_simple_closed_curve Subset of (TOP-REAL 2);
let c₂ be Nat;
assume E8: c₂ is_sufficiently_large_for c₁ ;
E9: c₂ >= ApproxIndex c₁ by E8, Def1;
set c₃ = X-SpanStart c₁,c₂;
func Y-SpanStart c₁,c₂ -> Nat means :Def3: :: JORDAN11:def 3
( a₃ <= width (Gauge a₁,a₂) & ( for b₁ being Nat st a₃ <= b₁ & b₁ <= ((2 |^ (a₂ -' (ApproxIndex a₁))) * ((Y-InitStart a₁) -' 2)) + 2 holds
cell (Gauge a₁,a₂),((X-SpanStart a₁,a₂) -' 1),b₁ c= BDD a₁ ) & ( for b₁ being Nat st b₁ <= width (Gauge a₁,a₂) & ( for b₂ being Nat st b₁ <= b₂ & b₂ <= ((2 |^ (a₂ -' (ApproxIndex a₁))) * ((Y-InitStart a₁) -' 2)) + 2 holds
cell (Gauge a₁,a₂),((X-SpanStart a₁,a₂) -' 1),b₂ c= BDD a₁ ) holds
b₁ >= a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines Y-SpanStart JORDAN11:def 3 :

theorem Th4: :: JORDAN11:4

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
X-SpanStart b₂,b₁ = ((2 |^ (b₁ -' (ApproxIndex b₂))) * ((X-SpanStart b₂,(ApproxIndex b₂)) - 2)) + 2

proof end;

theorem Th5: :: JORDAN11:5

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
Y-SpanStart b₂,b₁ <= ((2 |^ (b₁ -' (ApproxIndex b₂))) * ((Y-InitStart b₂) -' 2)) + 2

proof end;

theorem Th6: :: JORDAN11:6

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
cell (Gauge b₂,b₁),((X-SpanStart b₂,b₁) -' 1),(Y-SpanStart b₂,b₁) c= BDD b₂

proof end;

theorem Th7: :: JORDAN11:7

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
( 1 < Y-SpanStart b₂,b₁ & Y-SpanStart b₂,b₁ <= width (Gauge b₂,b₁) )

proof end;

theorem Th8: :: JORDAN11:8

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
[(X-SpanStart b₂,b₁),(Y-SpanStart b₂,b₁)] in Indices (Gauge b₂,b₁)

proof end;

theorem Th9: :: JORDAN11:9

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
[((X-SpanStart b₂,b₁) -' 1),(Y-SpanStart b₂,b₁)] in Indices (Gauge b₂,b₁)

proof end;

theorem Th10: :: JORDAN11:10

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
cell (Gauge b₂,b₁),((X-SpanStart b₂,b₁) -' 1),((Y-SpanStart b₂,b₁) -' 1) meets b₂

proof end;

theorem Th11: :: JORDAN11:11

for b₁ being Nat
for b₂ being being_simple_closed_curve Subset of (TOP-REAL 2) st b₁ is_sufficiently_large_for b₂ holds
cell (Gauge b₂,b₁),((X-SpanStart b₂,b₁) -' 1),(Y-SpanStart b₂,b₁) misses b₂

proof end;