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

Lm1: now
let f be FinSequence of (TOP-REAL 2); :: thesis: for k being Nat st len f = k + 1 & k <> 0 & f is unfolded holds
f | k is unfolded
let k be Nat; :: thesis: ( len f = k + 1 & k <> 0 & f is unfolded implies f | k is unfolded )
assume A1: len f = k + 1 ; :: thesis: ( k <> 0 & f is unfolded implies f | k is unfolded )
assume k <> 0 ; :: thesis: ( f is unfolded implies f | k is unfolded )
then A2: ( 0 < k & k <= k + 1 ) by NAT_1:29;
then ( 0 + 1 <= k & k <= len f & k + 1 <= len f ) by A1, NAT_1:38;
then A3: k in dom f by FINSEQ_3:27;
A4: len (f | k) = k by A1, A2, FINSEQ_1:80;
A5: dom (f | k) = Seg (len (f | k)) by FINSEQ_1:def 3;
assume A6: f is unfolded ; :: thesis: f | k is unfolded
thus f | k is unfolded :: thesis: verum
proof
set f1 = f | k;
let n be Nat; :: according to TOPREAL1:def 8 :: thesis: ( not 1 <= n or not n + 2 <= len (f | k) or (LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))} )
assume A7: ( 1 <= n & n + 2 <= len (f | k) ) ; :: thesis: (LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))}
then ( n in dom (f | k) & n + 1 in dom (f | k) & n + 2 in dom (f | k) & (n + 1) + 1 = n + (1 + 1) ) by GOBOARD2:4;
then A8: ( LSeg (f | k),n = LSeg f,n & LSeg (f | k),(n + 1) = LSeg f,(n + 1) & (f | k) /. (n + 1) = f /. (n + 1) ) by A3, A4, A5, FINSEQ_4:86, TOPREAL3:24;
len (f | k) <= len f by A1, A2, FINSEQ_1:80;
then n + 2 <= len f by A7, XREAL_1:2;
hence (LSeg (f | k),n) /\ (LSeg (f | k),(n + 1)) = {((f | k) /. (n + 1))} by A6, A7, A8, TOPREAL1:def 8; :: thesis: verum
end;
end;

theorem Th1: :: GOBOARD3:1  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 one-to-one & f is unfolded & f is s.n.c. & f is special holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is one-to-one & g is unfolded & g is s.n.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
proof end;

theorem :: GOBOARD3:2  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_S-Seq holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
proof end;