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

registration
cluster with_non-empty_element set ;
existence
ex b1 being set st b1 is with_non-empty_element
proof end;
end;

registration
let D be non empty with_non-empty_element set ;
cluster non empty non-empty FinSequence of D * ;
existence
ex b1 being FinSequence of D * st
( not b1 is empty & b1 is non-empty )
proof end;
end;

registration
let D be non empty with_non-empty_elements set ;
cluster non empty non-empty FinSequence of D * ;
existence
ex b1 being FinSequence of D * st
( not b1 is empty & b1 is non-empty )
proof end;
end;

registration
let F be non-empty Function-yielding Function;
cluster rngs F -> non-empty ;
coherence
rngs F is non-empty
proof end;
end;

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

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

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

theorem Th4: :: JORDAN1H:4  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) holds (LSeg p,q) \ {p,q} is convex
proof end;

theorem :: JORDAN1H:5  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) holds (LSeg p,q) \ {p,q} is connected
proof end;

theorem Th6: :: JORDAN1H:6  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
p in Cl ((LSeg p,q) \ {p,q})
proof end;

theorem Th7: :: JORDAN1H:7  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
Cl ((LSeg p,q) \ {p,q}) = LSeg p,q
proof end;

theorem :: JORDAN1H:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being Subset of (TOP-REAL 2)
for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg p,q) \ {p,q} c= S holds
LSeg p,q c= Cl S
proof end;

definition
func RealOrd -> Relation of REAL equals :: JORDAN1H:def 1
{ [r,s] where r, s is Real : r <= s } ;
coherence
{ [r,s] where r, s is Real : r <= s } is Relation of REAL
proof end;
end;

:: deftheorem defines RealOrd JORDAN1H:def 1 :
RealOrd = { [r,s] where r, s is Real : r <= s } ;

theorem Th9: :: JORDAN1H:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, s being Real st [r,s] in RealOrd holds
r <= s
proof end;

Lm1: RealOrd is_reflexive_in REAL
proof end;

Lm2: RealOrd is_antisymmetric_in REAL
proof end;

Lm3: RealOrd is_transitive_in REAL
proof end;

Lm4: RealOrd is_connected_in REAL
proof end;

theorem Th10: :: JORDAN1H:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
field RealOrd = REAL
proof end;

registration
cluster RealOrd -> reflexive antisymmetric transitive total being_linear-order ;
coherence
( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )
proof end;
end;

theorem Th11: :: JORDAN1H:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
RealOrd linearly_orders REAL
proof end;

theorem Th12: :: JORDAN1H:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite Subset of REAL holds SgmX RealOrd ,A is increasing
proof end;

theorem Th13: :: JORDAN1H:13  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 REAL
for A being finite Subset of REAL st A = rng f holds
SgmX RealOrd ,A = Incr f
proof end;

registration
let A be finite Subset of REAL ;
cluster SgmX RealOrd ,A -> increasing ;
coherence
SgmX RealOrd ,A is increasing by Th12;
end;

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

theorem Th15: :: JORDAN1H:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being non empty set
for A being finite Subset of X
for R being being_linear-order Order of X holds len (SgmX R,A) = card A
proof end;

theorem Th16: :: JORDAN1H:16  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) holds X_axis f = proj1 * f
proof end;

theorem Th17: :: JORDAN1H: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) holds Y_axis f = proj2 * f
proof end;

definition
let D be non empty set ;
let M be FinSequence of D * ;
:: original: Values
redefine func Values M -> Subset of D;
coherence
Values M is Subset of D
proof end;
end;

registration
let D be non empty with_non-empty_elements set ;
let M be non empty non-empty FinSequence of D * ;
cluster Values M -> non empty ;
coherence
not Values M is empty
proof end;
end;

theorem Th18: :: JORDAN1H: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 empty set
for M being Matrix of D
for i being Nat st i in Seg (width M) holds
rng (Col M,i) c= Values M
proof end;

theorem Th19: :: JORDAN1H:19  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 i being Nat st i in dom M holds
rng (Line M,i) c= Values M
proof end;

theorem Th20: :: JORDAN1H:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being V4 X_increasing-in-column Matrix of (TOP-REAL 2) holds len G <= card (proj1 .: (Values G))
proof end;

theorem Th21: :: JORDAN1H:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being X_equal-in-line Matrix of (TOP-REAL 2) holds card (proj1 .: (Values G)) <= len G
proof end;

theorem Th22: :: JORDAN1H:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being V4 X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len G = card (proj1 .: (Values G))
proof end;

theorem Th23: :: JORDAN1H:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being V4 Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G <= card (proj2 .: (Values G))
proof end;

theorem Th24: :: JORDAN1H:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being V4 Y_equal-in-column Matrix of (TOP-REAL 2) holds card (proj2 .: (Values G)) <= width G
proof end;

theorem Th25: :: JORDAN1H:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being V4 Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G = card (proj2 .: (Values G))
proof end;

theorem :: JORDAN1H:26  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 f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg f,k c= left_cell f,k,G
proof end;

theorem :: JORDAN1H:27  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 f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
left_cell f,k,(GoB f) = left_cell f,k
proof end;

theorem Th28: :: JORDAN1H:28  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 f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
LSeg f,k c= right_cell f,k,G
proof end;

theorem Th29: :: JORDAN1H:29  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 f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
right_cell f,k,(GoB f) = right_cell f,k
proof end;

theorem :: JORDAN1H:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2)
for f being non constant standard special_circular_sequence holds
( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )
proof end;

theorem :: JORDAN1H:31  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 non constant standard special_circular_sequence st f is_sequence_on G holds
for k being Nat st 1 <= k & k + 1 <= len f holds
( Int (right_cell f,k,G) c= RightComp f & Int (left_cell f,k,G) c= LeftComp f )
proof end;

theorem Th32: :: JORDAN1H:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, j1, i2, j2 being Nat
for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * i1,j1 = G * i2,j2 holds
( i1 = i2 & j1 = j2 )
proof end;

theorem Th33: :: JORDAN1H:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i1, i2 being Nat
for f being FinSequence of (TOP-REAL 2)
for M being Go-board st f is_sequence_on M holds
mid f,i1,i2 is_sequence_on M
proof end;

registration
cluster -> non empty non-empty FinSequence of the carrier of (TOP-REAL 2) * ;
coherence
for b1 being Go-board holds
( not b1 is empty & b1 is non-empty )
proof end;
end;

theorem Th34: :: JORDAN1H:34  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 G being Go-board st 1 <= i & i <= len G holds
(SgmX RealOrd ,(proj1 .: (Values G))) . i = (G * i,1) `1
proof end;

theorem Th35: :: JORDAN1H:35  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 G being Go-board st 1 <= j & j <= width G holds
(SgmX RealOrd ,(proj2 .: (Values G))) . j = (G * 1,j) `2
proof end;

theorem Th36: :: JORDAN1H:36  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 Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * 1,i in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * (len G),i in rng f ) holds
proj1 .: (rng f) = proj1 .: (Values G)
proof end;

theorem Th37: :: JORDAN1H:37  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 Go-board st f is_sequence_on G & ex i being Nat st
( [i,1] in Indices G & G * i,1 in rng f ) & ex i being Nat st
( [i,(width G)] in Indices G & G * i,(width G) in rng f ) holds
proj2 .: (rng f) = proj2 .: (Values G)
proof end;

registration
let G be Go-board;
cluster Values G -> non empty ;
coherence
not Values G is empty
proof end;
end;

theorem Th38: :: JORDAN1H:38  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 holds G = GoB (SgmX RealOrd ,(proj1 .: (Values G))),(SgmX RealOrd ,(proj2 .: (Values G)))
proof end;

theorem Th39: :: JORDAN1H:39  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 Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds
G = GoB f
proof end;

theorem Th40: :: JORDAN1H:40  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 Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * 1,i in rng f ) & ex i being Nat st
( [i,1] in Indices G & G * i,1 in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * (len G),i in rng f ) & ex i being Nat st
( [i,(width G)] in Indices G & G * i,(width G) in rng f ) holds
G = GoB f
proof end;

theorem Th41: :: JORDAN1H:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, i being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge C,n) holds
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Nat
proof end;

theorem Th42: :: JORDAN1H:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, i being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge C,n) holds
( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge C,m) )
proof end;

theorem Th43: :: JORDAN1H:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) holds
ex i1, j1 being Nat st
( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell (Gauge C,n),i,j c= cell (Gauge C,m),i1,j1 )
proof end;

theorem Th44: :: JORDAN1H:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n, i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge C,n) & 1 <= j & j + 1 <= width (Gauge C,n) holds
ex i1, j1 being Nat st
( 1 <= i1 & i1 + 1 <= len (Gauge C,m) & 1 <= j1 & j1 + 1 <= width (Gauge C,m) & cell (Gauge C,n),i,j c= cell (Gauge C,m),i1,j1 )
proof end;

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

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

theorem :: JORDAN1H:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being Subset of (TOP-REAL 2) st P is Bounded holds
not UBD P is Bounded
proof end;

theorem Th48: :: JORDAN1H:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Point of (TOP-REAL 2)
for f being non constant standard special_circular_sequence st Rotate f,p is clockwise_oriented holds
f is clockwise_oriented
proof end;

theorem :: JORDAN1H:49  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 st LeftComp f = UBD (L~ f) holds
f is clockwise_oriented
proof end;

theorem Th50: :: JORDAN1H:50  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 holds (Cl (LeftComp f)) ` = RightComp f
proof end;

theorem :: JORDAN1H:51  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 holds (Cl (RightComp f)) ` = LeftComp f
proof end;

theorem Th52: :: JORDAN1H: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 compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
GoB (Cage C,n) = Gauge C,n
proof end;

theorem :: JORDAN1H: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 compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds
N-min C in right_cell (Cage C,n),1
proof end;

theorem Th54: :: JORDAN1H:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
L~ (Cage C,j) c= Cl (RightComp (Cage C,i))
proof end;

theorem Th55: :: JORDAN1H:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
LeftComp (Cage C,i) c= LeftComp (Cage C,j)
proof end;

theorem :: JORDAN1H:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
RightComp (Cage C,j) c= RightComp (Cage C,i)
proof end;

definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
func X-SpanStart C,n -> Nat equals :: JORDAN1H:def 2
(2 |^ (n -' 1)) + 2;
correctness
coherence
(2 |^ (n -' 1)) + 2 is Nat;
;
end;

:: deftheorem defines X-SpanStart JORDAN1H:def 2 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds X-SpanStart C,n = (2 |^ (n -' 1)) + 2;

theorem :: JORDAN1H:57  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 compact non horizontal non vertical Subset of (TOP-REAL 2) holds X-SpanStart C,n = Center (Gauge C,n) by JORDAN1B:17;

theorem Th58: :: JORDAN1H:58  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 compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 2 < X-SpanStart C,n & X-SpanStart C,n < len (Gauge C,n) )
proof end;

theorem Th59: :: JORDAN1H:59  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 compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( 1 <= (X-SpanStart C,n) -' 1 & (X-SpanStart C,n) -' 1 < len (Gauge C,n) )
proof end;

definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
pred n is_sufficiently_large_for C means :Def3: :: JORDAN1H:def 3
 ex j being Nat st
( j < width (Gauge C,n) & cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C );
end;

:: deftheorem Def3 defines is_sufficiently_large_for JORDAN1H:def 3 :
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( n is_sufficiently_large_for C iff ex j being Nat st
( j < width (Gauge C,n) & cell (Gauge C,n),((X-SpanStart C,n) -' 1),j c= BDD C ) );

theorem :: JORDAN1H:60  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 compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
n >= 1
proof end;

theorem :: JORDAN1H:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Nat st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[(i1 -' 1),(j1 + 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Nat st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for j1, i2 being Nat st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [(i2 + 1),j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * (i2 + 1),j1 & [i2,j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i2,j1 holds
[i2,(j1 -' 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j2 being Nat st left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[(i1 + 1),j2] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Nat st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[i1,(j1 + 2)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Nat st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 2),j1] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for j1, i2 being Nat st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [(i2 + 1),j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * (i2 + 1),j1 & [i2,j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i2,j1 holds
[(i2 -' 1),j1] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j2 being Nat st front_left_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[i1,(j2 -' 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Nat st front_right_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [i1,(j1 + 1)] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,(j1 + 1) holds
[(i1 + 1),(j1 + 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j1 being Nat st front_right_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,j1 & [(i1 + 1),j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * (i1 + 1),j1 holds
[(i1 + 1),(j1 -' 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for j1, i2 being Nat st front_right_cell f,((len f) -' 1),(Gauge C,n) meets C & [(i2 + 1),j1] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * (i2 + 1),j1 & [i2,j1] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i2,j1 holds
[i2,(j1 + 1)] in Indices (Gauge C,n)
proof end;

theorem :: JORDAN1H:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge C,n & len f > 1 holds
for i1, j2 being Nat st front_right_cell f,((len f) -' 1),(Gauge C,n) meets C & [i1,(j2 + 1)] in Indices (Gauge C,n) & f /. ((len f) -' 1) = (Gauge C,n) * i1,(j2 + 1) & [i1,j2] in Indices (Gauge C,n) & f /. (len f) = (Gauge C,n) * i1,j2 holds
[(i1 -' 1),j2] in Indices (Gauge C,n)
proof end;