let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) 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 V25() & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
let f be FinSequence of (TOP-REAL 2); :: thesis: ( ( 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 V25() & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 implies ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g ) )
assume that
A1: 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) ) and
A2: ( f is V25() & f is circular & f is unfolded ) and
A3: f is s.c.c. and
A4: f is special and
A5: len f > 4 ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
reconsider f9 = f as V25() circular special unfolded s.c.c. FinSequence of (TOP-REAL 2) by A2, A3, A4;
reconsider f9 = f9 as non empty V25() circular special unfolded s.c.c. FinSequence of (TOP-REAL 2) ;
set h1 = f9 | 2;
set h2 = f9 /^ 1;
A6: len f > 1 + 1 by A2, Th3;
then A7: len (f9 | 2) = 1 + 1 by FINSEQ_1:59;
then reconsider h1 = f9 | 2 as non trivial FinSequence of (TOP-REAL 2) by NAT_D:60;
A8: h1 is s.n.c. by A6, Th20;
len h1 in dom h1 by A7, FINSEQ_3:25;
then A9: h1 /. (len h1) = f /. (1 + 1) by A7, FINSEQ_4:70;
1 <= len f by A2, Th3, XXREAL_0:2;
then A10: len (f9 /^ 1) = (len f) - 1 by RFINSEQ:def 1;
then A11: (len (f9 /^ 1)) + 1 = len f ;
A12: dom h1 c= dom f by FINSEQ_5:18;
A13: for n being Nat st n in dom h1 holds
ex i, j being Nat st
( [i,j] in Indices G & h1 /. n = G * (i,j) )
proof
let n be Nat; :: thesis: ( n in dom h1 implies ex i, j being Nat st
( [i,j] in Indices G & h1 /. n = G * (i,j) ) )
assume A14: n in dom h1 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & h1 /. n = G * (i,j) )
then consider i, j being Nat such that
A15: [i,j] in Indices G and
A16: f /. n = G * (i,j) by A1, A12;
reconsider i = i, j = j as Nat ;
take i ; :: thesis: ex j being Nat st
( [i,j] in Indices G & h1 /. n = G * (i,j) )
take j ; :: thesis: ( [i,j] in Indices G & h1 /. n = G * (i,j) )
thus [i,j] in Indices G by A15; :: thesis: h1 /. n = G * (i,j)
thus h1 /. n = G * (i,j) by A14, A16, FINSEQ_4:70; :: thesis: verum
end;
h1 is one-to-one by A5, Th3, Th22;
then consider g1 being FinSequence of (TOP-REAL 2) such that
A17: g1 is_sequence_on G and
A18: ( g1 is one-to-one & g1 is unfolded & g1 is s.n.c. & g1 is special ) and
A19: L~ h1 = L~ g1 and
A20: h1 /. 1 = g1 /. 1 and
A21: h1 /. (len h1) = g1 /. (len g1) and
A22: len h1 <= len g1 by A13, A8, GOBOARD3:1;
reconsider g1 = g1 as non trivial FinSequence of (TOP-REAL 2) by A7, A22, NAT_D:60;
A23: 1 <= (len g1) -' 1 by A7, A22, NAT_D:55;
((len g1) -' 1) + 1 = len g1 by A7, A22, XREAL_1:235, XXREAL_0:2;
then A24: g1 /. (len g1) in LSeg (g1,((len g1) -' 1)) by A23, TOPREAL1:21;
A25: LSeg (g1,((len g1) -' 1)) c= L~ g1 by TOPREAL3:19;
A26: len (f9 /^ 1) > (1 + 1) - 1 by A6, A10, XREAL_1:9;
then A27: len (f9 /^ 1) >= 2 by NAT_1:13;
then reconsider h2 = f9 /^ 1 as non trivial FinSequence of (TOP-REAL 2) by NAT_D:60;
A28: h2 is s.n.c. by Th21;
A29: len h2 in dom h2 by FINSEQ_5:6;
A30: 1 in dom h1 by FINSEQ_5:6;
then A31: h1 /. 1 = f /. 1 by FINSEQ_4:70;
then A32: h1 /. 1 = f /. (len f) by FINSEQ_6:def 1
.= h2 /. (len h2) by A11, A29, FINSEQ_5:27 ;
A33: for n being Nat st n in dom h2 holds
ex i, j being Nat st
( [i,j] in Indices G & h2 /. n = G * (i,j) )
proof
let n be Nat; :: thesis: ( n in dom h2 implies ex i, j being Nat st
( [i,j] in Indices G & h2 /. n = G * (i,j) ) )
assume A34: n in dom h2 ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & h2 /. n = G * (i,j) )
then consider i, j being Nat such that
A35: [i,j] in Indices G and
A36: f /. (n + 1) = G * (i,j) by A1, FINSEQ_5:26;
reconsider i = i, j = j as Nat ;
take i ; :: thesis: ex j being Nat st
( [i,j] in Indices G & h2 /. n = G * (i,j) )
take j ; :: thesis: ( [i,j] in Indices G & h2 /. n = G * (i,j) )
thus [i,j] in Indices G by A35; :: thesis: h2 /. n = G * (i,j)
thus h2 /. n = G * (i,j) by A34, A36, FINSEQ_5:27; :: thesis: verum
end;
h2 is one-to-one by A5, Th24;
then consider g2 being FinSequence of (TOP-REAL 2) such that
A37: g2 is_sequence_on G and
A38: ( g2 is one-to-one & g2 is unfolded & g2 is s.n.c. & g2 is special ) and
A39: L~ h2 = L~ g2 and
A40: h2 /. 1 = g2 /. 1 and
A41: h2 /. (len h2) = g2 /. (len g2) and
A42: len h2 <= len g2 by A33, A28, GOBOARD3:1;
A43: len g2 >= 1 + 1 by A27, A42, XXREAL_0:2;
then reconsider g2 = g2 as non trivial FinSequence of (TOP-REAL 2) by NAT_D:60;
A44: ((len g2) -' 1) + 1 = len g2 by A43, XREAL_1:235, XXREAL_0:2;
A45: LSeg (g2,1) c= L~ g2 by TOPREAL3:19;
take g = g1 ^' g2; :: thesis: ( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
1 in dom h2 by A26, FINSEQ_3:25;
then A46: h1 /. (len h1) = h2 /. 1 by A9, FINSEQ_5:27;
hence g is_sequence_on G by A17, A21, A37, A40, Th12; :: thesis: ( g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
(LSeg (f,1)) /\ (L~ h2) = {(h1 /. 1),(h2 /. 1)} by A5, A9, A46, A31, Th27;
then A47: (L~ g1) /\ (L~ g2) = {(g1 /. 1),(g2 /. 1)} by A19, A20, A39, A40, Th19;
len h2 > (3 + 1) - 1 by A5, A10, XREAL_1:9;
then 2 + 1 < len g2 by A42, XXREAL_0:2;
then A48: 1 + 1 < (len g2) -' 1 by NAT_D:52;
then 1 <= (len g2) -' 1 by NAT_1:13;
then A49: g2 /. (len g2) in LSeg (g2,((len g2) -' 1)) by A44, TOPREAL1:21;
LSeg (g2,1) misses LSeg (g2,((len g2) -' 1)) by A38, A48;
then not g2 /. (len g2) in LSeg (g2,1) by A49, XBOOLE_0:3;
then A50: not g2 /. (len g2) in (LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) by XBOOLE_0:def 4;
g2 /. 1 in LSeg (g2,1) by A43, TOPREAL1:21;
then g2 /. 1 in (LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) by A21, A40, A46, A24, XBOOLE_0:def 4;
then (LSeg (g1,((len g1) -' 1))) /\ (LSeg (g2,1)) = {(g2 /. 1)} by A20, A41, A32, A47, A50, A25, A45, Th1, XBOOLE_1:27;
hence g is unfolded by A18, A21, A38, A40, A46, Th34; :: thesis: ( g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
thus g is s.c.c. by A18, A20, A21, A38, A40, A41, A46, A32, A47, Th33; :: thesis: ( g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
thus g is special by A18, A21, A38, A40, A46, Th26; :: thesis: ( L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
A51: ((1 + 1),(len h2)) -cut h2 = h2 /^ 1 by Th13;
A52: f = h1 ^ (f /^ (1 + 1)) by RFINSEQ:8
.= h1 ^ ((2,(len h2)) -cut h2) by A51, FINSEQ_6:81
.= h1 ^' h2 by FINSEQ_6:def 5 ;
then A53: (len f) + 1 = (len h1) + (len h2) by FINSEQ_6:139;
thus L~ f = (L~ h1) \/ (L~ h2) by A52, A46, Th35
.= L~ g by A19, A21, A39, A40, A46, Th35 ; :: thesis: ( f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )
thus f /. 1 = h1 /. 1 by A30, FINSEQ_4:70
.= g /. 1 by A20, FINSEQ_6:155 ; :: thesis: ( f /. (len f) = g /. (len g) & len f <= len g )
thus f /. (len f) = h2 /. (len h2) by A11, A29, FINSEQ_5:27
.= g /. (len g) by A41, FINSEQ_6:156 ; :: thesis: len f <= len g
(len g) + 1 = (len g1) + (len g2) by FINSEQ_6:139;
then (len f) + 1 <= (len g) + 1 by A22, A42, A53, XREAL_1:7;
hence len f <= len g by XREAL_1:6; :: thesis: verum