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

theorem Th1: :: TOPREAL8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, x, y being set st A c= {x,y} & x in A & not y in A holds
A = {x}
proof end;

registration
cluster trivial set ;
existence
ex b1 being Function st b1 is trivial
proof end;
end;

registration
cluster non constant set ;
existence
not for b1 being FinSequence holds b1 is constant
proof end;
end;

theorem Th2: :: TOPREAL8:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial FinSequence holds 1 < len f
proof end;

theorem Th3: :: TOPREAL8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non trivial set
for f being non constant circular FinSequence of D holds len f > 2
proof end;

theorem Th4: :: TOPREAL8:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence
for x being set holds
( x in rng f or x .. f = 0 )
proof end;

theorem Th5: :: TOPREAL8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being set
for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) |-- p = g
proof end;

theorem Th6: :: TOPREAL8:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being non empty one-to-one FinSequence of D holds (f /. (len f)) .. f = len f
proof end;

theorem Th7: :: TOPREAL8:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence holds len f <= len (f ^' g)
proof end;

theorem Th8: :: TOPREAL8:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence
for x being set st x in rng f holds
x .. f = x .. (f ^' g)
proof end;

theorem :: TOPREAL8:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non empty FinSequence
for g being FinSequence holds len g <= len (f ^' g)
proof end;

theorem Th10: :: TOPREAL8:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence holds rng f c= rng (f ^' g)
proof end;

theorem Th11: :: TOPREAL8:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g /. (len g) = f /. 1 holds
f ^' g is circular
proof end;

theorem Th12: :: TOPREAL8:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for M being Matrix of D
for f being FinSequence of D
for g being non empty FinSequence of D st f /. (len f) = g /. 1 & f is_sequence_on M & g is_sequence_on M holds
f ^' g is_sequence_on M
proof end;

theorem Th13: :: TOPREAL8:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being set
for f being FinSequence of D st 1 <= k holds
(k + 1),(len f) -cut f = f /^ k
proof end;

theorem Th14: :: TOPREAL8:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for D being set
for f being FinSequence of D st k <= len f holds
1,k -cut f = f | k
proof end;

theorem Th15: :: TOPREAL8:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being set
for D being non empty set
for f being non empty FinSequence of D
for g being FinSequence of D st p .. f = len f holds
(f ^ g) -| p = 1,((len f) -' 1) -cut f
proof end;

theorem Th16: :: TOPREAL8:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds
(f ^' g) :- (g /. 1) = g
proof end;

theorem Th17: :: TOPREAL8:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f, g being non empty FinSequence of D st (g /. 1) .. f = len f holds
(f ^' g) -: (g /. 1) = f
proof end;

theorem Th18: :: TOPREAL8:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non trivial set
for f being non empty FinSequence of D
for g being non trivial FinSequence of D st g /. 1 = f /. (len f) & ( for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1 ) holds
Rotate (f ^' g),(g /. 1) = g ^' f
proof end;

theorem Th19: :: TOPREAL8:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial FinSequence of (TOP-REAL 2) holds LSeg f,1 = L~ (f | 2)
proof end;

theorem Th20: :: TOPREAL8:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st n < len f holds
f | n is s.n.c.
proof end;

theorem Th21: :: TOPREAL8:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st 1 <= n holds
f /^ n is s.n.c.
proof end;

theorem Th22: :: TOPREAL8:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being circular s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st n < len f & len f > 4 holds
f | n is one-to-one
proof end;

theorem Th23: :: TOPREAL8:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
for i, j being Nat st 1 < i & i < j & j <= len f holds
f /. i <> f /. j
proof end;

theorem Th24: :: TOPREAL8:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being circular s.c.c. FinSequence of (TOP-REAL 2)
for n being Nat st 1 <= n & len f > 4 holds
f /^ n is one-to-one
proof end;

theorem Th25: :: TOPREAL8:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat
for f being non empty special FinSequence of (TOP-REAL 2) holds m,n -cut f is special
proof end;

theorem Th26: :: TOPREAL8:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non empty special FinSequence of (TOP-REAL 2)
for g being non trivial special FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds
f ^' g is special
proof end;

theorem Th27: :: TOPREAL8:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being unfolded circular s.c.c. FinSequence of (TOP-REAL 2) st len f > 4 holds
(LSeg f,1) /\ (L~ (f /^ 1)) = {(f /. 1),(f /. 2)}
proof end;

registration
cluster non empty one-to-one special unfolded s.n.c. FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being FinSequence of (TOP-REAL 2) st
( b1 is one-to-one & b1 is special & b1 is unfolded & b1 is s.n.c. & not b1 is empty )
proof end;
end;

theorem Th28: :: TOPREAL8:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for f, g being FinSequence of (TOP-REAL 2) st j < len f holds
LSeg (f ^' g),j = LSeg f,j
proof end;

theorem Th29: :: TOPREAL8:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for f, g being non empty FinSequence of (TOP-REAL 2) st 1 <= j & j + 1 < len g holds
LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)
proof end;

theorem Th30: :: TOPREAL8:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non empty FinSequence of (TOP-REAL 2)
for g being non trivial FinSequence of (TOP-REAL 2) st f /. (len f) = g /. 1 holds
LSeg (f ^' g),(len f) = LSeg g,1
proof end;

theorem Th31: :: TOPREAL8:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j being Nat
for f being non empty FinSequence of (TOP-REAL 2)
for g being non trivial FinSequence of (TOP-REAL 2) st j + 1 < len g & f /. (len f) = g /. 1 holds
LSeg (f ^' g),((len f) + j) = LSeg g,(j + 1)
proof end;

theorem Th32: :: TOPREAL8:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non empty unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i being Nat st 1 <= i & i < len f holds
(LSeg f,i) /\ (rng f) = {(f /. i),(f /. (i + 1))}
proof end;

Lm1: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Nat st i < len f & 1 < i holds
for x being Point of (TOP-REAL 2) st x in (LSeg (f ^' g),i) /\ (LSeg (f ^' g),j) holds
x <> f /. 1
proof end;

Lm2: for f being non empty one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2)
for g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2)
for i, j being Nat st j > len f & j + 1 < len (f ^' g) holds
for x being Point of (TOP-REAL 2) st x in (LSeg (f ^' g),i) /\ (LSeg (f ^' g),j) holds
x <> g /. (len g)
proof end;

theorem Th33: :: TOPREAL8:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being one-to-one non trivial unfolded s.n.c. FinSequence of (TOP-REAL 2) st (L~ f) /\ (L~ g) = {(f /. 1),(g /. 1)} & f /. 1 = g /. (len g) & g /. 1 = f /. (len f) holds
f ^' g is s.c.c.
proof end;

theorem Th34: :: TOPREAL8:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & g is unfolded & f /. (len f) = g /. 1 & (LSeg f,((len f) -' 1)) /\ (LSeg g,1) = {(f /. (len f))} holds
f ^' g is unfolded
proof end;

theorem Th35: :: TOPREAL8:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is trivial & f /. (len f) = g /. 1 holds
L~ (f ^' g) = (L~ f) \/ (L~ g)
proof end;

theorem :: TOPREAL8:36  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 f being FinSequence of (TOP-REAL 2) st ( for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * i,j ) ) & not f is constant & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
proof end;