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

theorem Th1: :: JORDAN5B:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1 being Nat st 1 <= i1 holds
i1 -' 1 < i1
proof end;

theorem :: JORDAN5B:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat st i + 1 <= k holds
1 <= k -' i
proof end;

theorem :: JORDAN5B:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k being Nat st 1 <= i & 1 <= k holds
(k -' i) + 1 <= k
proof end;

Lm1: for r being real number st 0 <= r & r <= 1 holds
( 0 <= 1 - r & 1 - r <= 1 )
proof end;

theorem :: JORDAN5B:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real number st r in the carrier of I[01] holds
1 - r in the carrier of I[01]
proof end;

theorem :: JORDAN5B: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 being Point of (TOP-REAL 2) st p `2 <> q `2 & p1 in LSeg p,q & p1 `2 = p `2 holds
p1 = p
proof end;

theorem :: JORDAN5B: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 being Point of (TOP-REAL 2) st p `1 <> q `1 & p1 in LSeg p,q & p1 `1 = p `1 holds
p1 = p
proof end;

Lm2: for P being Point of I[01] holds P is Real
proof end;

theorem Th7: :: JORDAN5B:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for P being non empty Subset of (TOP-REAL 2)
for F being Function of I[01] ,((TOP-REAL 2) | P)
for i being Nat st 1 <= i & i + 1 <= len f & f is_S-Seq & P = L~ f & F is_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) holds
ex p1, p2 being Real st
( p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg f,i = F .: [.p1,p2.] & F . p1 = f /. i & F . p2 = f /. (i + 1) )
proof end;

theorem :: JORDAN5B:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for Q, R being non empty Subset of (TOP-REAL 2)
for F being Function of I[01] ,((TOP-REAL 2) | Q)
for i being Nat
for P being non empty Subset of I[01] st f is_S-Seq & F is_homeomorphism & F . 0 = f /. 1 & F . 1 = f /. (len f) & 1 <= i & i + 1 <= len f & F .: P = LSeg f,i & Q = L~ f & R = LSeg f,i holds
ex G being Function of (I[01] | P),((TOP-REAL 2) | R) st
( G = F | P & G is_homeomorphism )
proof end;

theorem Th9: :: JORDAN5B:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg p1,p2 holds
LE p,p,p1,p2
proof end;

theorem Th10: :: JORDAN5B:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p in LSeg p1,p2 holds
LE p1,p,p1,p2
proof end;

theorem Th11: :: JORDAN5B:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, p1, p2 being Point of (TOP-REAL 2) st p in LSeg p1,p2 & p1 <> p2 holds
LE p,p2,p1,p2
proof end;

theorem :: JORDAN5B:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, q1, q2, q3 being Point of (TOP-REAL 2) st p1 <> p2 & LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds
LE q1,q3,p1,p2
proof end;

theorem :: JORDAN5B:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Point of (TOP-REAL 2) st p <> q holds
LSeg p,q = { p1 where p1 is Point of (TOP-REAL 2) : ( LE p,p1,p,q & LE p1,q,p,q ) }
proof end;

theorem :: JORDAN5B: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 P being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st P is_an_arc_of p1,p2 holds
P is_an_arc_of p2,p1
proof end;

theorem :: JORDAN5B:15  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 f being FinSequence of (TOP-REAL 2)
for P being Subset of (TOP-REAL 2) st f is_S-Seq & 1 <= i & i + 1 <= len f & P = LSeg f,i holds
P is_an_arc_of f /. i,f /. (i + 1)
proof end;

theorem :: JORDAN5B:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for g1 being FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i <= len g1 & g1 is_S-Seq & g1 /. 1 in L~ (mid g1,i,(len g1)) holds
i = 1
proof end;

theorem :: JORDAN5B:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is_S-Seq & p = f . (len f) holds
L_Cut f,p = <*p*>
proof end;

theorem :: JORDAN5B:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN5B:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN5B:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN5B:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & p <> f . (len f) & f is_S-Seq holds
Index p,(L_Cut f,p) = 1
proof end;

theorem Th22: :: JORDAN5B:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & f is_S-Seq & p <> f . (len f) holds
p in L~ (L_Cut f,p)
proof end;

theorem :: JORDAN5B:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & f is_S-Seq & p <> f . 1 holds
p in L~ (R_Cut f,p)
proof end;

theorem Th24: :: JORDAN5B:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & f is one-to-one holds
B_Cut f,p,p = <*p*>
proof end;

Lm3: for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & p <> f . (len f) & q <> f . (len f) & f is_S-Seq & not p in L~ (L_Cut f,q) holds
q in L~ (L_Cut f,p)
proof end;

theorem Th25: :: JORDAN5B:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & q <> f . (len f) & p = f . (len f) & f is_S-Seq holds
p in L~ (L_Cut f,q)
proof end;

theorem :: JORDAN5B:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st ( p <> f . (len f) or q <> f . (len f) ) & p in L~ f & q in L~ f & f is_S-Seq & not p in L~ (L_Cut f,q) holds
q in L~ (L_Cut f,p)
proof end;

Lm4: for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) & p <> q holds
L~ (B_Cut f,p,q) c= L~ f
proof end;

theorem :: JORDAN5B:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & f is_S-Seq holds
L~ (B_Cut f,p,q) c= L~ f
proof end;

theorem :: JORDAN5B:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & j <= len (GoB f) & i < j holds
(LSeg ((GoB f) * 1,(width (GoB f))),((GoB f) * i,(width (GoB f)))) /\ (LSeg ((GoB f) * j,(width (GoB f))),((GoB f) * (len (GoB f)),(width (GoB f)))) = {}
proof end;

theorem :: JORDAN5B:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for i, j being Nat st 1 <= i & j <= width (GoB f) & i < j holds
(LSeg ((GoB f) * (len (GoB f)),1),((GoB f) * (len (GoB f)),i)) /\ (LSeg ((GoB f) * (len (GoB f)),j),((GoB f) * (len (GoB f)),(width (GoB f)))) = {}
proof end;

theorem Th30: :: JORDAN5B:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st f is_S-Seq holds
L_Cut f,(f /. 1) = f
proof end;

theorem :: JORDAN5B:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2) st f is_S-Seq holds
R_Cut f,(f /. (len f)) = f
proof end;

theorem :: JORDAN5B:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
p in LSeg (f /. (Index p,f)),(f /. ((Index p,f) + 1))
proof end;

theorem :: JORDAN5B:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & len f >= 2 & f /. 1 in LSeg f,i holds
i = 1
proof end;

theorem :: JORDAN5B:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for j being Nat
for P being Subset of (TOP-REAL 2) st 1 <= j & j <= width (GoB f) & P = LSeg ((GoB f) * 1,j),((GoB f) * (len (GoB f)),j) holds
P is_S-P_arc_joining (GoB f) * 1,j,(GoB f) * (len (GoB f)),j
proof end;

theorem :: JORDAN5B:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for j being Nat
for P being Subset of (TOP-REAL 2) st 1 <= j & j <= len (GoB f) & P = LSeg ((GoB f) * j,1),((GoB f) * j,(width (GoB f))) holds
P is_S-P_arc_joining (GoB f) * j,1,(GoB f) * j,(width (GoB f))
proof end;

theorem :: JORDAN5B:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p in L~ f & q in L~ f & ( Index p,f < Index q,f or ( Index p,f = Index q,f & LE p,q,f /. (Index p,f),f /. ((Index p,f) + 1) ) ) & p <> q holds
L~ (B_Cut f,p,q) c= L~ f by Lm4;