:: JORDAN8 semantic presentation

theorem Th1: :: JORDAN8:1
for b1 being set
for b2 being FinSequence of b1 st len b2 >= 2 holds
b2 | 2 = <*(b2 /. 1),(b2 /. 2)*>
proof end;

theorem Th2: :: JORDAN8:2
for b1 being Nat
for b2 being set
for b3 being FinSequence of b2 st b1 + 1 <= len b3 holds
b3 | (b1 + 1) = (b3 | b1) ^ <*(b3 /. (b1 + 1))*>
proof end;

theorem Th3: :: JORDAN8:3
for b1 being set
for b2 being Matrix of b1 holds <*> b1 is_sequence_on b2
proof end;

theorem Th4: :: JORDAN8:4
canceled;

theorem Th5: :: JORDAN8:5
for b1 being Nat
for b2 being non empty set
for b3 being FinSequence of b2
for b4 being Matrix of b2 st b3 is_sequence_on b4 holds
b3 /^ b1 is_sequence_on b4
proof end;

theorem Th6: :: JORDAN8:6
for b1 being Nat
for b2 being set
for b3 being FinSequence of b2
for b4 being Matrix of b2 st 1 <= b1 & b1 + 1 <= len b3 & b3 is_sequence_on b4 holds
ex b5, b6, b7, b8 being Nat st
( [b5,b6] in Indices b4 & b3 /. b1 = b4 * b5,b6 & [b7,b8] in Indices b4 & b3 /. (b1 + 1) = b4 * b7,b8 & ( ( b5 = b7 & b6 + 1 = b8 ) or ( b5 + 1 = b7 & b6 = b8 ) or ( b5 = b7 + 1 & b6 = b8 ) or ( b5 = b7 & b6 = b8 + 1 ) ) )
proof end;

theorem Th7: :: JORDAN8:7
for b1 being Go-board
for b2 being non empty FinSequence of (TOP-REAL 2) st b2 is_sequence_on b1 holds
( b2 is standard & b2 is special )
proof end;

theorem Th8: :: JORDAN8:8
for b1 being Go-board
for b2 being non empty FinSequence of (TOP-REAL 2) st len b2 >= 2 & b2 is_sequence_on b1 holds
not b2 is constant
proof end;

theorem Th9: :: JORDAN8:9
for b1 being Go-board
for b2 being Point of (TOP-REAL 2)
for b3 being non empty FinSequence of (TOP-REAL 2) st b3 is_sequence_on b1 & ex b4, b5 being Nat st
( [b4,b5] in Indices b1 & b2 = b1 * b4,b5 ) & ( for b4, b5, b6, b7 being Nat st [b4,b5] in Indices b1 & [b6,b7] in Indices b1 & b3 /. (len b3) = b1 * b4,b5 & b2 = b1 * b6,b7 holds
(abs (b6 - b4)) + (abs (b7 - b5)) = 1 ) holds
b3 ^ <*b2*> is_sequence_on b1
proof end;

theorem Th10: :: JORDAN8:10
for b1, b2, b3 being Nat
for b4 being Go-board st b1 + b2 < len b4 & 1 <= b3 & b3 < width b4 & cell b4,b1,b3 meets cell b4,(b1 + b2),b3 holds
b2 <= 1
proof end;

theorem Th11: :: JORDAN8:11
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( b1 is vertical iff E-bound b1 <= W-bound b1 )
proof end;

theorem Th12: :: JORDAN8:12
for b1 being non empty compact Subset of (TOP-REAL 2) holds
( b1 is horizontal iff N-bound b1 <= S-bound b1 )
proof end;

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

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

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

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

theorem Th13: :: JORDAN8:13
for b1 being Nat
for b2 being non empty Subset of (TOP-REAL 2) holds len (Gauge b2,b1) >= 4
proof end;

theorem Th14: :: JORDAN8:14
for b1, b2 being Nat
for b3 being non empty Subset of (TOP-REAL 2) st 1 <= b1 & b1 <= len (Gauge b3,b2) holds
((Gauge b3,b2) * 2,b1) `1 = W-bound b3
proof end;

theorem Th15: :: JORDAN8:15
for b1, b2 being Nat
for b3 being non empty Subset of (TOP-REAL 2) st 1 <= b1 & b1 <= len (Gauge b3,b2) holds
((Gauge b3,b2) * ((len (Gauge b3,b2)) -' 1),b1) `1 = E-bound b3
proof end;

theorem Th16: :: JORDAN8:16
for b1, b2 being Nat
for b3 being non empty Subset of (TOP-REAL 2) st 1 <= b1 & b1 <= len (Gauge b3,b2) holds
((Gauge b3,b2) * b1,2) `2 = S-bound b3
proof end;

theorem Th17: :: JORDAN8:17
for b1, b2 being Nat
for b3 being non empty Subset of (TOP-REAL 2) st 1 <= b1 & b1 <= len (Gauge b3,b2) holds
((Gauge b3,b2) * b1,((len (Gauge b3,b2)) -' 1)) `2 = N-bound b3
proof end;

theorem Th18: :: JORDAN8:18
for b1, b2 being Nat
for b3 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= len (Gauge b3,b2) holds
cell (Gauge b3,b2),b1,(len (Gauge b3,b2)) misses b3
proof end;

theorem Th19: :: JORDAN8:19
for b1, b2 being Nat
for b3 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= len (Gauge b3,b2) holds
cell (Gauge b3,b2),(len (Gauge b3,b2)),b1 misses b3
proof end;

theorem Th20: :: JORDAN8:20
for b1, b2 being Nat
for b3 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= len (Gauge b3,b2) holds
cell (Gauge b3,b2),b1,0 misses b3
proof end;

theorem Th21: :: JORDAN8:21
for b1, b2 being Nat
for b3 being non empty compact non horizontal non vertical Subset of (TOP-REAL 2) st b1 <= len (Gauge b3,b2) holds
cell (Gauge b3,b2),0,b1 misses b3
proof end;