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

theorem :: JORDAN15:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of (TOP-REAL 2) st A meets B holds
proj1 .: A meets proj1 .: B
proof end;

theorem :: JORDAN15:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being Subset of (TOP-REAL 2)
for s being real number st A misses B & A c= Horizontal_Line s & B c= Horizontal_Line s holds
proj1 .: A misses proj1 .: B
proof end;

theorem Th3: :: JORDAN15:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being closed Subset of (TOP-REAL 2) st S is Bounded holds
proj1 .: S is closed
proof end;

theorem Th4: :: JORDAN15:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being compact Subset of (TOP-REAL 2) holds proj1 .: S is compact
proof end;

theorem Th5: :: JORDAN15:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, p1, q1 being Point of (TOP-REAL 2) st LSeg p,q is vertical & LSeg p1,q1 is vertical & p `1 = p1 `1 & p `2 <= p1 `2 & p1 `2 <= q1 `2 & q1 `2 <= q `2 holds
LSeg p1,q1 c= LSeg p,q
proof end;

theorem Th6: :: JORDAN15:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, p1, q1 being Point of (TOP-REAL 2) st LSeg p,q is horizontal & LSeg p1,q1 is horizontal & p `2 = p1 `2 & p `1 <= p1 `1 & p1 `1 <= q1 `1 & q1 `1 <= q `1 holds
LSeg p1,q1 c= LSeg p,q
proof end;

theorem Th7: :: JORDAN15:7  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 i, j, k, j1, k1 being Nat st 1 <= i & i <= len G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg (G * i,j1),(G * i,k1) c= LSeg (G * i,j),(G * i,k)
proof end;

theorem Th8: :: JORDAN15:8  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 i, j, k, j1, k1 being Nat st 1 <= i & i <= width G & 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg (G * j1,i),(G * k1,i) c= LSeg (G * j,i),(G * k,i)
proof end;

theorem :: JORDAN15:9  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 j, k, j1, k1 being Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= width G holds
LSeg (G * (Center G),j1),(G * (Center G),k1) c= LSeg (G * (Center G),j),(G * (Center G),k)
proof end;

theorem :: JORDAN15:10  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 st len G = width G holds
for j, k, j1, k1 being Nat st 1 <= j & j <= j1 & j1 <= k1 & k1 <= k & k <= len G holds
LSeg (G * j1,(Center G)),(G * k1,(Center G)) c= LSeg (G * j,(Center G)),(G * k,(Center G))
proof end;

theorem Th11: :: JORDAN15:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Lower_Seq C,n) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} )
proof end;

theorem :: JORDAN15:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k1)} )
proof end;

theorem Th13: :: JORDAN15:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Lower_Seq C,n) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j1)} & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k1)} )
proof end;

theorem :: JORDAN15:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq C,n) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j1,i)} )
proof end;

theorem Th15: :: JORDAN15:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k1,i)} )
proof end;

theorem Th16: :: JORDAN15:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq C,n) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j1,i)} & (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k1,i)} )
proof end;

theorem :: JORDAN15:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Upper_Seq C,n) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,j1)} )
proof end;

theorem :: JORDAN15:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Lower_Seq C,n) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,k1)} )
proof end;

theorem :: JORDAN15:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Upper_Seq C,n) & (Gauge C,n) * i,k in L~ (Lower_Seq C,n) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,j1)} & (LSeg ((Gauge C,n) * i,j1),((Gauge C,n) * i,k1)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,k1)} )
proof end;

theorem Th20: :: JORDAN15:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * j,i in L~ (Upper_Seq C,n) holds
ex j1 being Nat st
( j <= j1 & j1 <= k & (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j1,i)} )
proof end;

theorem :: JORDAN15:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * k,i in L~ (Lower_Seq C,n) holds
ex k1 being Nat st
( j <= k1 & k1 <= k & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k1,i)} )
proof end;

theorem Th22: :: JORDAN15:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 <= j & j <= k & k <= len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * j,i in L~ (Upper_Seq C,n) & (Gauge C,n) * k,i in L~ (Lower_Seq C,n) holds
ex j1, k1 being Nat st
( j <= j1 & j1 <= k1 & k1 <= k & (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j1,i)} & (LSeg ((Gauge C,n) * j1,i),((Gauge C,n) * k1,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k1,i)} )
proof end;

theorem Th23: :: JORDAN15:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) & (Gauge C,n) * i,j in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th24: :: JORDAN15:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) & (Gauge C,n) * i,j in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem Th25: :: JORDAN15:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (Gauge C,n) * i,k in Upper_Arc (L~ (Cage C,n)) & (Gauge C,n) * i,j in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th26: :: JORDAN15:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (Gauge C,n) * i,k in Upper_Arc (L~ (Cage C,n)) & (Gauge C,n) * i,j in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem :: JORDAN15:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C
proof end;

theorem :: JORDAN15:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Upper_Arc C
proof end;

theorem Th29: :: JORDAN15:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j, k being Nat st 1 < j & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq C,n) holds
j <> k
proof end;

theorem Th30: :: JORDAN15:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k,i)} & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j,i)} holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Lower_Arc C
proof end;

theorem Th31: :: JORDAN15:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * k,i)} & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * j,i)} holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
proof end;

theorem Th32: :: JORDAN15:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Lower_Arc C
proof end;

theorem Th33: :: JORDAN15:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * k,i in L~ (Upper_Seq C,n) & (Gauge C,n) * j,i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
proof end;

theorem Th34: :: JORDAN15:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & n > 0 & (Gauge C,n) * k,i in Upper_Arc (L~ (Cage C,n)) & (Gauge C,n) * j,i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Lower_Arc C
proof end;

theorem Th35: :: JORDAN15:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & n > 0 & (Gauge C,n) * k,i in Upper_Arc (L~ (Cage C,n)) & (Gauge C,n) * j,i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
proof end;

theorem :: JORDAN15:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
proof end;

theorem :: JORDAN15:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Upper_Arc C
proof end;

theorem Th38: :: JORDAN15:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j,i)} & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k,i)} holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Lower_Arc C
proof end;

theorem Th39: :: JORDAN15:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * j,i)} & (LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * k,i)} holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
proof end;

theorem Th40: :: JORDAN15:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * j,i in L~ (Upper_Seq C,n) & (Gauge C,n) * k,i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Lower_Arc C
proof end;

theorem Th41: :: JORDAN15:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & (Gauge C,n) * j,i in L~ (Upper_Seq C,n) & (Gauge C,n) * k,i in L~ (Lower_Seq C,n) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
proof end;

theorem Th42: :: JORDAN15:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & n > 0 & (Gauge C,n) * j,i in Upper_Arc (L~ (Cage C,n)) & (Gauge C,n) * k,i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Lower_Arc C
proof end;

theorem Th43: :: JORDAN15:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < j & j <= k & k < len (Gauge C,n) & 1 <= i & i <= width (Gauge C,n) & n > 0 & (Gauge C,n) * j,i in Upper_Arc (L~ (Cage C,n)) & (Gauge C,n) * k,i in Lower_Arc (L~ (Cage C,n)) holds
LSeg ((Gauge C,n) * j,i),((Gauge C,n) * k,i) meets Upper_Arc C
proof end;

theorem :: JORDAN15:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Lower_Arc C
proof end;

theorem :: JORDAN15:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for j, k being Nat st 1 < j & j <= k & k < len (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1))) in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1))) in Lower_Arc (L~ (Cage C,(n + 1))) holds
LSeg ((Gauge C,(n + 1)) * j,(Center (Gauge C,(n + 1)))),((Gauge C,(n + 1)) * k,(Center (Gauge C,(n + 1)))) meets Upper_Arc C
proof end;

theorem Th46: :: JORDAN15:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Upper_Arc C
proof end;

theorem Th47: :: JORDAN15:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 <= i2 & i2 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Lower_Arc C
proof end;

theorem Th48: :: JORDAN15:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Upper_Arc C
proof end;

theorem Th49: :: JORDAN15:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i2 & i2 <= i1 & i1 < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i2,k)} & ((LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k))) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i1,j)} holds
(LSeg ((Gauge C,n) * i1,j),((Gauge C,n) * i1,k)) \/ (LSeg ((Gauge C,n) * i1,k),((Gauge C,n) * i2,k)) meets Lower_Arc C
proof end;

theorem Th50: :: JORDAN15:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge C,(n + 1)) & 1 < i2 & i2 < len (Gauge C,(n + 1)) & 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * i1,k in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * i2,j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) \/ (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) meets Upper_Arc C
proof end;

theorem Th51: :: JORDAN15:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i1, i2, j, k being Nat st 1 < i1 & i1 < len (Gauge C,(n + 1)) & 1 < i2 & i2 < len (Gauge C,(n + 1)) & 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * i1,k in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * i2,j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * i2,j),((Gauge C,(n + 1)) * i2,k)) \/ (LSeg ((Gauge C,(n + 1)) * i2,k),((Gauge C,(n + 1)) * i1,k)) meets Lower_Arc C
proof end;

theorem :: JORDAN15:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,(n + 1)) & 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * i,k in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) \/ (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k),((Gauge C,(n + 1)) * i,k)) meets Upper_Arc C
proof end;

theorem :: JORDAN15:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for C being Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,(n + 1)) & 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (Gauge C,(n + 1)) * i,k in Upper_Arc (L~ (Cage C,(n + 1))) & (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Lower_Arc (L~ (Cage C,(n + 1))) holds
(LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) \/ (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k),((Gauge C,(n + 1)) * i,k)) meets Lower_Arc C
proof end;