:: GOBOARD3 semantic presentation

E1: now
let c1 be FinSequence of (TOP-REAL 2);
let c2 be Nat;
assume E2: len c1 = c2 + 1 ;
assume c2 <> 0 ;
then E3: ( 0 < c2 & c2 <= c2 + 1 ) by NAT_1:29;
then ( 0 + 1 <= c2 & c2 <= len c1 & c2 + 1 <= len c1 ) by E2, NAT_1:38;
then E4: c2 in dom c1 by FINSEQ_3:27;
E5: len (c1 | c2) = c2 by E2, E3, FINSEQ_1:80;
E6: dom (c1 | c2) = Seg (len (c1 | c2)) by FINSEQ_1:def 3;
assume E7: c1 is unfolded ;
thus c1 | c2 is unfolded
proof
set c3 = c1 | c2;
let c4 be Nat; :: according to TOPREAL1:def 8
assume E8: ( 1 <= c4 & c4 + 2 <= len (c1 | c2) ) ;
then ( c4 in dom (c1 | c2) & c4 + 1 in dom (c1 | c2) & c4 + 2 in dom (c1 | c2) & (c4 + 1) + 1 = c4 + (1 + 1) ) by GOBOARD2:4;
then E9: ( LSeg (c1 | c2),c4 = LSeg c1,c4 & LSeg (c1 | c2),(c4 + 1) = LSeg c1,(c4 + 1) & (c1 | c2) /. (c4 + 1) = c1 /. (c4 + 1) ) by E4, E5, E6, FINSEQ_4:86, TOPREAL3:24;
len (c1 | c2) <= len c1 by E2, E3, FINSEQ_1:80;
then c4 + 2 <= len c1 by E8, XREAL_1:2;
hence (LSeg (c1 | c2),c4) /\ (LSeg (c1 | c2),(c4 + 1)) = {((c1 | c2) /. (c4 + 1))} by E7, E8, E9, TOPREAL1:def 8;
end;
end;

theorem Th1: :: GOBOARD3:1
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Go-board st ( for b3 being Nat st b3 in dom b1 holds
ex b4, b5 being Nat st
( [b4,b5] in Indices b2 & b1 /. b3 = b2 * b4,b5 ) ) & b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special holds
ex b3 being FinSequence of (TOP-REAL 2) st
( b3 is_sequence_on b2 & b3 is one-to-one & b3 is unfolded & b3 is s.n.c. & b3 is special & L~ b1 = L~ b3 & b1 /. 1 = b3 /. 1 & b1 /. (len b1) = b3 /. (len b3) & len b1 <= len b3 )
proof end;

theorem Th2: :: GOBOARD3:2
for b1 being FinSequence of (TOP-REAL 2)
for b2 being Go-board st ( for b3 being Nat st b3 in dom b1 holds
ex b4, b5 being Nat st
( [b4,b5] in Indices b2 & b1 /. b3 = b2 * b4,b5 ) ) & b1 is_S-Seq holds
ex b3 being FinSequence of (TOP-REAL 2) st
( b3 is_sequence_on b2 & b3 is_S-Seq & L~ b1 = L~ b3 & b1 /. 1 = b3 /. 1 & b1 /. (len b1) = b3 /. (len b3) & len b1 <= len b3 )
proof end;