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

scheme :: GOBOARD2:sch 1
PiLambdaD{ F1() -> non empty set , F2() -> Nat, F3( set ) -> Element of F1() } :
ex g being FinSequence of F1() st
( len g = F2() & ( for n being Nat st n in dom g holds
g /. n = F3(n) ) )
proof end;

defpred S1[ Nat] means for R being finite Subset of REAL st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );

Lm1: S1[0]
by CARD_2:59;

Lm2: for n being Nat st S1[n] holds
S1[n + 1]
proof end;

Lm3: for n being Nat holds S1[n]
from NAT_1:sch 1(, Lm1, Lm2);

theorem Th1: :: GOBOARD2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being finite Subset of REAL st R <> {} holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R )
proof end;

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

theorem Th3: :: GOBOARD2:3  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 f being FinSequence holds
( 1 <= n & n + 1 <= len f iff ( n in dom f & n + 1 in dom f ) )
proof end;

theorem Th4: :: GOBOARD2:4  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 f being FinSequence holds
( 1 <= n & n + 2 <= len f iff ( n in dom f & n + 1 in dom f & n + 2 in dom f ) )
proof end;

theorem Th5: :: GOBOARD2:5  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 f1, f2 being FinSequence of D
for n being Nat st 1 <= n & n <= len f2 holds
(f1 ^ f2) /. (n + (len f1)) = f2 /. n
proof end;

theorem :: GOBOARD2:6  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 ( for n, m being Nat st m > n + 1 & n in dom f & n + 1 in dom f & m in dom f & m + 1 in dom f holds
LSeg f,n misses LSeg f,m ) holds
f is s.n.c.
proof end;

theorem :: GOBOARD2: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 i being Nat st f is unfolded & f is s.n.c. & f is one-to-one & f /. (len f) in LSeg f,i & i in dom f & i + 1 in dom f holds
i + 1 = len f
proof end;

theorem Th8: :: GOBOARD2: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 k being Nat st k <> 0 & len f = k + 1 holds
L~ f = (L~ (f | k)) \/ (LSeg f,k)
proof end;

theorem :: GOBOARD2:9  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 k being Nat st 1 < k & len f = k + 1 & f is unfolded & f is s.n.c. holds
(L~ (f | k)) /\ (LSeg f,k) = {(f /. k)}
proof end;

theorem :: GOBOARD2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of (TOP-REAL 2)
for n, m being Nat st len f1 < n & n + 1 <= len (f1 ^ f2) & m + (len f1) = n holds
LSeg (f1 ^ f2),n = LSeg f2,m
proof end;

theorem Th11: :: GOBOARD2:11  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) holds L~ f c= L~ (f ^ g)
proof end;

theorem :: GOBOARD2:12  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 s.n.c. holds
f | i is s.n.c.
proof end;

theorem :: GOBOARD2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f1, f2 being FinSequence of (TOP-REAL 2) st f1 is special & f2 is special & ( (f1 /. (len f1)) `1 = (f2 /. 1) `1 or (f1 /. (len f1)) `2 = (f2 /. 1) `2 ) holds
f1 ^ f2 is special
proof end;

theorem Th14: :: GOBOARD2:14  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 <> {} holds
X_axis f <> {}
proof end;

theorem Th15: :: GOBOARD2:15  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 <> {} holds
Y_axis f <> {}
proof end;

registration
let f be non empty FinSequence of (TOP-REAL 2);
cluster X_axis f -> non empty ;
coherence
not X_axis f is empty
by Th14;
cluster Y_axis f -> non empty ;
coherence
not Y_axis f is empty
by Th15;
end;

theorem Th16: :: GOBOARD2: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)
for G being Go-board st f is special holds
for n being Nat st n in dom f & n + 1 in dom f holds
for i, j, m, k being Nat st [i,j] in Indices G & [m,k] in Indices G & f /. n = G * i,j & f /. (n + 1) = G * m,k & not i = m holds
k = j
proof end;

theorem :: GOBOARD2: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 G being Go-board 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 ) ) & f is special & ( for n being Nat st n in dom f & n + 1 in dom f holds
f /. n <> f /. (n + 1) ) holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & L~ f = L~ g & g /. 1 = f /. 1 & g /. (len g) = f /. (len f) & len f <= len g )
proof end;

theorem :: GOBOARD2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being FinSequence of REAL st v is increasing holds
for n, m being Nat st n in dom v & m in dom v & n <= m holds
v . n <= v . m
proof end;

theorem Th19: :: GOBOARD2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being FinSequence of REAL st v is increasing holds
for n, m being Nat st n in dom v & m in dom v & n <> m holds
v . n <> v . m
proof end;

theorem Th20: :: GOBOARD2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v, v1 being FinSequence of REAL
for n being Nat st v is increasing & v1 = v | (Seg n) holds
v1 is increasing
proof end;

defpred S2[ Nat] means for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );

Lm4: S2[0]
proof end;

Lm5: for n being Nat st S2[n] holds
S2[n + 1]
proof end;

Lm6: for n being Nat holds S2[n]
from NAT_1:sch 1(, Lm4, Lm5);

theorem :: GOBOARD2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being FinSequence of REAL ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing ) by Lm6;

defpred S3[ Nat] means for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;

Lm7: S3[0]
proof end;

Lm8: for n being Nat st S3[n] holds
S3[n + 1]
proof end;

Lm9: for n being Nat holds S3[n]
from NAT_1:sch 1(, Lm7, Lm8);

theorem :: GOBOARD2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v1, v2 being FinSequence of REAL st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2 by Lm9;

definition
let v1, v2 be increasing FinSequence of REAL ;
assume A1: ( v1 <> {} & v2 <> {} ) ;
func GoB v1,v2 -> Matrix of (TOP-REAL 2) means :Def1: :: GOBOARD2:def 1
( len it = len v1 & width it = len v2 & ( for n, m being Nat st [n,m] in Indices it holds
it * n,m = |[(v1 . n),(v2 . m)]| ) );
existence
ex b1 being Matrix of (TOP-REAL 2) st
( len b1 = len v1 & width b1 = len v2 & ( for n, m being Nat st [n,m] in Indices b1 holds
b1 * n,m = |[(v1 . n),(v2 . m)]| ) )
proof end;
uniqueness
for b1, b2 being Matrix of (TOP-REAL 2) st len b1 = len v1 & width b1 = len v2 & ( for n, m being Nat st [n,m] in Indices b1 holds
b1 * n,m = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Nat st [n,m] in Indices b2 holds
b2 * n,m = |[(v1 . n),(v2 . m)]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines GoB GOBOARD2:def 1 :
for v1, v2 being increasing FinSequence of REAL st v1 <> {} & v2 <> {} holds
for b3 being Matrix of (TOP-REAL 2) holds
( b3 = GoB v1,v2 iff ( len b3 = len v1 & width b3 = len v2 & ( for n, m being Nat st [n,m] in Indices b3 holds
b3 * n,m = |[(v1 . n),(v2 . m)]| ) ) );

registration
let v1, v2 be non empty increasing FinSequence of REAL ;
cluster GoB v1,v2 -> V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;
coherence
( not GoB v1,v2 is empty-yielding & GoB v1,v2 is X_equal-in-line & GoB v1,v2 is Y_equal-in-column & GoB v1,v2 is Y_increasing-in-line & GoB v1,v2 is X_increasing-in-column )
proof end;
end;

definition
let v be FinSequence of REAL ;
func Incr v -> increasing FinSequence of REAL means :Def2: :: GOBOARD2:def 2
( rng it = rng v & len it = card (rng v) );
existence
ex b1 being increasing FinSequence of REAL st
( rng b1 = rng v & len b1 = card (rng v) )
proof end;
uniqueness
for b1, b2 being increasing FinSequence of REAL st rng b1 = rng v & len b1 = card (rng v) & rng b2 = rng v & len b2 = card (rng v) holds
b1 = b2
by Lm9;
end;

:: deftheorem Def2 defines Incr GOBOARD2:def 2 :
for v being FinSequence of REAL
for b2 being increasing FinSequence of REAL holds
( b2 = Incr v iff ( rng b2 = rng v & len b2 = card (rng v) ) );

definition
let f be non empty FinSequence of (TOP-REAL 2);
func GoB f -> Matrix of (TOP-REAL 2) equals :: GOBOARD2:def 3
GoB (Incr (X_axis f)),(Incr (Y_axis f));
correctness
coherence
GoB (Incr (X_axis f)),(Incr (Y_axis f)) is Matrix of (TOP-REAL 2)
;
;
end;

:: deftheorem defines GoB GOBOARD2:def 3 :
for f being non empty FinSequence of (TOP-REAL 2) holds GoB f = GoB (Incr (X_axis f)),(Incr (Y_axis f));

theorem Th23: :: GOBOARD2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v being FinSequence of REAL st v <> {} holds
Incr v <> {}
proof end;

registration
let v be non empty FinSequence of REAL ;
cluster Incr v -> non empty increasing ;
coherence
not Incr v is empty
by Th23;
end;

registration
let f be non empty FinSequence of (TOP-REAL 2);
cluster GoB f -> V4 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column ;
coherence
( not GoB f is empty-yielding & GoB f is X_equal-in-line & GoB f is Y_equal-in-column & GoB f is Y_increasing-in-line & GoB f is X_increasing-in-column )
;
end;

theorem Th24: :: GOBOARD2:24  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) holds
( len (GoB f) = card (rng (X_axis f)) & width (GoB f) = card (rng (Y_axis f)) )
proof end;

theorem :: GOBOARD2:25  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 n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices (GoB f) & f /. n = (GoB f) * i,j )
proof end;

theorem :: GOBOARD2:26  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 f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds
(X_axis f) . n <= (X_axis f) . m ) holds
f /. n in rng (Line (GoB f),1)
proof end;

theorem :: GOBOARD2:27  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 f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds
(X_axis f) . m <= (X_axis f) . n ) holds
f /. n in rng (Line (GoB f),(len (GoB f)))
proof end;

theorem :: GOBOARD2:28  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 f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds
(Y_axis f) . n <= (Y_axis f) . m ) holds
f /. n in rng (Col (GoB f),1)
proof end;

theorem :: GOBOARD2:29  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 f being non empty FinSequence of (TOP-REAL 2) st n in dom f & ( for m being Nat st m in dom f holds
(Y_axis f) . m <= (Y_axis f) . n ) holds
f /. n in rng (Col (GoB f),(width (GoB f)))
proof end;