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