let f, g be non trivial one-to-one unfolded s.n.c. FinSequence of (TOP-REAL 2); :: thesis: ( (L~ f) /\ (L~ g) = {(f /. 1),(g /. 1)} & f /. 1 = g /. (len g) & g /. 1 = f /. (len f) implies f ^' g is s.c.c. )
assume that
A1: (L~ f) /\ (L~ g) = {(f /. 1),(g /. 1)} and
A2: f /. 1 = g /. (len g) and
A3: g /. 1 = f /. (len f) ; :: thesis: f ^' g is s.c.c.
A4: for i being Nat st 1 <= i & i < len f holds
f /. i <> g /. 1
proof
A5: len f in dom f by FINSEQ_5:6;
then A6: f /. (len f) = f . (len f) by PARTFUN1:def 6;
let i be Nat; :: thesis: ( 1 <= i & i < len f implies f /. i <> g /. 1 )
assume that
A7: 1 <= i and
A8: i < len f ; :: thesis: f /. i <> g /. 1
A9: i in dom f by A7, A8, FINSEQ_3:25;
then f /. i = f . i by PARTFUN1:def 6;
hence f /. i <> g /. 1 by A3, A8, A9, A5, A6, FUNCT_1:def 4; :: thesis: verum
end;
A10: (len (f ^' g)) + 1 = (len f) + (len g) by FINSEQ_6:139;
A11: (len (g ^' f)) + 1 = (len f) + (len g) by FINSEQ_6:139;
let i be Nat; :: according to GOBOARD5:def 4 :: thesis: for b1 being set holds
( b1 <= i + 1 or ( ( i <= 1 or len (f ^' g) <= b1 ) & len (f ^' g) <= b1 + 1 ) or LSeg ((f ^' g),i) misses LSeg ((f ^' g),b1) )
let j be Nat; :: thesis: ( j <= i + 1 or ( ( i <= 1 or len (f ^' g) <= j ) & len (f ^' g) <= j + 1 ) or LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) )
assume that
A12: i + 1 < j and
A13: ( ( i > 1 & j < len (f ^' g) ) or j + 1 < len (f ^' g) ) ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)
A14: i < j by A12, NAT_1:13;
j <= j + 1 by NAT_1:11;
then A15: j < len (f ^' g) by A13, XXREAL_0:2;
per cases ( i = 0 or j < len f or i >= len f or ( j >= len f & i < len f & 1 <= i ) ) by NAT_1:14;
suppose i = 0 ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)
then LSeg ((f ^' g),i) = {} by TOPREAL1:def 3;
then (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) = {} ;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by XBOOLE_0:def 7; :: thesis: verum
end;
suppose A16: j < len f ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)
then i < len f by A14, XXREAL_0:2;
then A17: LSeg ((f ^' g),i) = LSeg (f,i) by Th28;
LSeg ((f ^' g),j) = LSeg (f,j) by A16, Th28;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A12, A17, TOPREAL1:def 7; :: thesis: verum
end;
suppose A18: i >= len f ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)
then consider m being Nat such that
A19: i = (len f) + m by NAT_1:10;
consider n being Nat such that
A20: j = (len f) + n by A14, A18, NAT_1:10, XXREAL_0:2;
reconsider m = m, n = n as Nat ;
A21: 1 <= m + 1 by NAT_1:11;
j + 1 < (len f) + (len g) by A15, A10, XREAL_1:6;
then (len f) + (n + 1) < (len f) + (len g) by A20;
then A22: n + 1 < len g by XREAL_1:6;
A23: m < n by A14, A19, A20, XREAL_1:6;
then m + 1 <= n by NAT_1:13;
then 1 <= n by A21, XXREAL_0:2;
then A24: LSeg ((f ^' g),j) = LSeg (g,(n + 1)) by A20, A22, Th29;
(i + 1) + 1 < j + 1 by A12, XREAL_1:6;
then (len f) + (m + (1 + 1)) < (len f) + (n + 1) by A19, A20;
then A25: (m + 1) + 1 < n + 1 by XREAL_1:6;
m + 1 < n + 1 by A23, XREAL_1:6;
then m + 1 < len g by A22, XXREAL_0:2;
then LSeg ((f ^' g),i) = LSeg (g,(m + 1)) by A3, A19, Th31;
hence LSeg ((f ^' g),i) misses LSeg ((f ^' g),j) by A24, A25, TOPREAL1:def 7; :: thesis: verum
end;
suppose that A26: j >= len f and
A27: i < len f and
A28: 1 <= i ; :: thesis: LSeg ((f ^' g),i) misses LSeg ((f ^' g),j)
consider k being Nat such that
A29: j = (len f) + k by A26, NAT_1:10;
reconsider k = k as Nat ;
j + 1 < (len f) + (len g) by A15, A10, XREAL_1:6;
then (len f) + (k + 1) < (len f) + (len g) by A29;
then k + 1 < len g by XREAL_1:6;
then LSeg ((f ^' g),j) = LSeg (g,(k + 1)) by A3, A29, Th31;
then A30: LSeg ((f ^' g),j) c= L~ g by TOPREAL3:19;
assume LSeg ((f ^' g),i) meets LSeg ((f ^' g),j) ; :: thesis: contradiction
then consider x being object such that
A31: x in (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) by XBOOLE_0:4;
LSeg ((f ^' g),i) = LSeg (f,i) by A27, Th28;
then LSeg ((f ^' g),i) c= L~ f by TOPREAL3:19;
then A32: (LSeg ((f ^' g),i)) /\ (LSeg ((f ^' g),j)) c= {(f /. 1),(g /. 1)} by A1, A30, XBOOLE_1:27;
now :: thesis: contradiction
per cases ( ( 1 < i & x = f /. 1 ) or ( j > (len f) + 0 & x = g /. 1 ) or ( j = len f & x = g /. 1 ) or ( j > len f & x = f /. 1 & j + 1 < len (f ^' g) ) or ( j = len f & x = f /. 1 & j + 1 < len (f ^' g) ) ) by A13, A26, A31, A32, TARSKI:def 2, XXREAL_0:1;
suppose ( 1 < i & x = f /. 1 ) ; :: thesis: contradiction
hence contradiction by A27, A31, Lm2; :: thesis: verum
end;
suppose that A33: j > (len f) + 0 and
A34: x = g /. 1 ; :: thesis: contradiction
j + 0 < j + 1 by XREAL_1:6;
then A35: len f < j + 1 by A33, XXREAL_0:2;
j + 1 < (len (g ^' f)) + 1 by A15, A10, A11, XREAL_1:6;
then (j + 1) -' (len f) < len g by A11, A35, NAT_D:54;
then A36: (j -' (len f)) + 1 < len g by A33, NAT_D:38;
A37: Rotate ((f ^' g),(g /. 1)) = g ^' f by A3, A4, Th18;
0 < j -' (len f) by A33, NAT_D:52;
then A38: 0 + 1 < (j -' (len f)) + 1 by XREAL_1:6;
A39: len f in dom f by FINSEQ_5:6;
then f . (len f) = f /. (len f) by PARTFUN1:def 6;
then A40: g /. 1 in rng f by A3, A39, FUNCT_1:3;
then A41: (g /. 1) .. (f ^' g) = (g /. 1) .. f by Th8
.= len f by A3, Th6 ;
A42: rng f c= rng (f ^' g) by Th10;
then A43: LSeg ((f ^' g),j) = LSeg ((Rotate ((f ^' g),(g /. 1))),((j -' ((g /. 1) .. (f ^' g))) + 1)) by A15, A33, A40, A41, REVROT_1:25;
f ^' g is circular by A2, Th11;
then LSeg ((f ^' g),i) = LSeg ((Rotate ((f ^' g),(g /. 1))),((i + (len (f ^' g))) -' ((g /. 1) .. (f ^' g)))) by A27, A28, A40, A41, A42, REVROT_1:32;
hence contradiction by A31, A34, A37, A41, A43, A36, A38, Lm2; :: thesis: verum
end;
suppose that A48: j > len f and
A49: x = f /. 1 and
A50: j + 1 < len (f ^' g) ; :: thesis: contradiction
thus contradiction by A2, A31, A48, A49, A50, Lm3; :: thesis: verum
end;
suppose that A51: j = len f and
A52: x = f /. 1 and
A53: j + 1 < len (f ^' g) ; :: thesis: contradiction
0 + 1 < len g by Th2;
then LSeg ((f ^' g),((len f) + 0)) = LSeg (g,(0 + 1)) by A3, Th31;
then A54: g /. (len g) in LSeg (g,1) by A2, A31, A51, A52, XBOOLE_0:def 4;
(j + 1) + 1 < (len f) + (len g) by A10, A53, XREAL_1:6;
then A55: j + (1 + 1) < (len f) + (len g) ;
then 1 + 1 < len g by A51, XREAL_1:6;
then A56: 1 + 1 in dom g by FINSEQ_3:25;
1 in dom g by FINSEQ_5:6;
hence contradiction by A51, A55, A54, A56, GOBOARD2:2; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
end;