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

theorem :: JORDAN8:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for f being FinSequence of D st len f >= 2 holds
f | 2 = <*(f /. 1),(f /. 2)*>
proof end;

theorem :: JORDAN8:2  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 + 1 <= len f holds
f | (k + 1) = (f | k) ^ <*(f /. (k + 1))*>
proof end;

theorem :: JORDAN8:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for G being Matrix of D holds <*> D is_sequence_on G
proof end;

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

theorem :: JORDAN8:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for D being non empty set
for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
proof end;

theorem Th6: :: JORDAN8:6  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
for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds
ex i1, j1, i2, j2 being Nat st
( [i1,j1] in Indices G & f /. k = G * i1,j1 & [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )
proof end;

theorem :: JORDAN8: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 f being non empty FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
( f is standard & f is special )
proof end;

theorem :: JORDAN8: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 f being non empty FinSequence of (TOP-REAL 2) st len f >= 2 & f is_sequence_on G holds
not f is constant
proof end;

theorem :: JORDAN8: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 p being Point of (TOP-REAL 2)
for f being non empty 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 & f /. (len f) = G * i1,j1 & p = G * i2,j2 holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1 ) holds
f ^ <*p*> is_sequence_on G
proof end;

theorem :: JORDAN8:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, k, j being Nat
for G being Go-board st i + k < len G & 1 <= j & j < width G & cell G,i,j meets cell G,(i + k),j holds
k <= 1
proof end;

theorem Th11: :: JORDAN8:11  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 Subset of (TOP-REAL 2) holds
( C is vertical iff E-bound C <= W-bound C )
proof end;

theorem Th12: :: JORDAN8:12  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 Subset of (TOP-REAL 2) holds
( C is horizontal iff N-bound C <= S-bound C )
proof end;

definition
let C be Subset of (TOP-REAL 2);
let n be Nat;
deffunc H1( Nat, Nat) -> Element of the carrier of (TOP-REAL 2) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ($1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ($2 - 2)))]|;
A1: (2 |^ n) + 3 > 0 by NAT_1:19;
func Gauge C,n -> Matrix of (TOP-REAL 2) means :Def1: :: JORDAN8:def 1
( len it = (2 |^ n) + 3 & len it = width it & ( for i, j being Nat st [i,j] in Indices it holds
it * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) );
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = (2 |^ n) + 3 & len b1 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) )
proof end;
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = (2 |^ n) + 3 & len b1 = width b1 & ( for i, j being Nat st [i,j] in Indices b1 holds
b1 * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) & len b2 = (2 |^ n) + 3 & len b2 = width b2 & ( for i, j being Nat st [i,j] in Indices b2 holds
b2 * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Gauge JORDAN8:def 1 :
for C being Subset of (TOP-REAL 2)
for n being Nat
for b3 being Matrix of (TOP-REAL 2) holds
( b3 = Gauge C,n iff ( len b3 = (2 |^ n) + 3 & len b3 = width b3 & ( for i, j being Nat st [i,j] in Indices b3 holds
b3 * i,j = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (j - 2)))]| ) ) );

registration
let C be non empty Subset of (TOP-REAL 2);
let n be Nat;
cluster Gauge C,n -> V4 X_equal-in-line Y_equal-in-column ;
coherence
( not Gauge C,n is empty-yielding & Gauge C,n is X_equal-in-line & Gauge C,n is Y_equal-in-column )
proof end;
end;

registration
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Gauge C,n -> V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;
coherence
( Gauge C,n is Y_increasing-in-line & Gauge C,n is X_increasing-in-column )
proof end;
end;

theorem Th13: :: JORDAN8: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 T being non empty Subset of (TOP-REAL 2) holds len (Gauge T,n) >= 4
proof end;

theorem :: JORDAN8:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, n being Nat
for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge T,n) holds
((Gauge T,n) * 2,j) `1 = W-bound T
proof end;

theorem :: JORDAN8:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, n being Nat
for T being non empty Subset of (TOP-REAL 2) st 1 <= j & j <= len (Gauge T,n) holds
((Gauge T,n) * ((len (Gauge T,n)) -' 1),j) `1 = E-bound T
proof end;

theorem :: JORDAN8:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge T,n) holds
((Gauge T,n) * i,2) `2 = S-bound T
proof end;

theorem :: JORDAN8:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for T being non empty Subset of (TOP-REAL 2) st 1 <= i & i <= len (Gauge T,n) holds
((Gauge T,n) * i,((len (Gauge T,n)) -' 1)) `2 = N-bound T
proof end;

theorem :: JORDAN8:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge C,n) holds
cell (Gauge C,n),i,(len (Gauge C,n)) misses C
proof end;

theorem :: JORDAN8:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, n being Nat
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st j <= len (Gauge C,n) holds
cell (Gauge C,n),(len (Gauge C,n)),j misses C
proof end;

theorem :: JORDAN8:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, n being Nat
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st i <= len (Gauge C,n) holds
cell (Gauge C,n),i,0 misses C
proof end;

theorem :: JORDAN8:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for j, n being Nat
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st j <= len (Gauge C,n) holds
cell (Gauge C,n),0,j misses C
proof end;