:: JORDAN1F semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: JORDAN1F:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg (G * i,j),(G * i,k) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * i,n) `2 = inf (proj2 .: ((LSeg (G * i,j),(G * i,k)) /\ (L~ f))) )
proof end;

theorem :: JORDAN1F:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg (G * i,j),(G * i,k) meets L~ f & [i,j] in Indices G & [i,k] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * i,n) `2 = sup (proj2 .: ((LSeg (G * i,j),(G * i,k)) /\ (L~ f))) )
proof end;

theorem :: JORDAN1F:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg (G * j,i),(G * k,i) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * n,i) `1 = inf (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) )
proof end;

theorem :: JORDAN1F:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, i, k being Nat
for f being FinSequence of the carrier of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & LSeg (G * j,i),(G * k,i) meets L~ f & [j,i] in Indices G & [k,i] in Indices G & j <= k holds
ex n being Nat st
( j <= n & n <= k & (G * n,i) `1 = sup (proj1 .: ((LSeg (G * j,i),(G * k,i)) /\ (L~ f))) )
proof end;

theorem Th5: :: JORDAN1F:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Upper_Seq C,n) /. 1 = W-min (L~ (Cage C,n))
proof end;

theorem Th6: :: JORDAN1F:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Lower_Seq C,n) /. 1 = E-max (L~ (Cage C,n))
proof end;

theorem Th7: :: JORDAN1F:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Upper_Seq C,n) /. (len (Upper_Seq C,n)) = E-max (L~ (Cage C,n))
proof end;

theorem Th8: :: JORDAN1F:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (Lower_Seq C,n) /. (len (Lower_Seq C,n)) = W-min (L~ (Cage C,n))
proof end;

theorem Th9: :: JORDAN1F:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( ( L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n)) & L~ (Lower_Seq C,n) = Lower_Arc (L~ (Cage C,n)) ) or ( L~ (Upper_Seq C,n) = Lower_Arc (L~ (Cage C,n)) & L~ (Lower_Seq C,n) = Upper_Arc (L~ (Cage C,n)) ) )
proof end;

theorem Th10: :: JORDAN1F:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Upper_Seq C,n is_sequence_on Gauge C,n
proof end;

theorem Th11: :: JORDAN1F:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for p being Point of (TOP-REAL 2)
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & ex i, j being Nat st
( [i,j] in Indices G & p = G * i,j ) & ( for i1, j1, i2, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & p = G * i1,j1 & f /. 1 = G * i2,j2 holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
<*p*> ^ f is_sequence_on G
proof end;

theorem Th12: :: JORDAN1F:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq C,n is_sequence_on Gauge C,n
proof end;

theorem :: JORDAN1F:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = inf (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )
proof end;