let f be non constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 & i1 > i2 holds
( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
let g be FinSequence of (TOP-REAL 2); :: thesis: for i1, i2 being Element of NAT st g is_a_part>_of f,i1,i2 & i1 > i2 holds
( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
let i1, i2 be Element of NAT ; :: thesis: ( g is_a_part>_of f,i1,i2 & i1 > i2 implies ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) ) )
assume that
A1: g is_a_part>_of f,i1,i2 and
A2: i1 > i2 ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) )
A3: 1 <= len g by A1, Def2;
g . (len g) = f . i2 by A1, Def2;
then A4: f . i2 = f . (S_Drop (((i1 + (len g)) -' 1),f)) by A1, A3, Def2;
A5: i2 <= i2 + 1 by NAT_1:11;
A6: i1 <= i1 + 1 by NAT_1:12;
A7: 1 <= i1 by A1, Def2;
A8: i1 + 1 <= len f by A1, Def2;
then A9: (i1 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A10: 1 <= (len f) - 1 by A7, XXREAL_0:2;
then A11: (len f) - 1 = (len f) -' 1 by NAT_D:39;
A12: now
per cases ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ) ;
case A13: ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: S_Drop (((i1 + (len g)) -' 1),f) < len f
A14: i1 <= (len f) -' 1 by A8, NAT_D:49;
then A15: ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 by A7, NAT_D:1;
1 <= (len f) -' 1 by A7, A14, XXREAL_0:2;
then A16: (len f) -' 1 < len f by NAT_D:51;
S_Drop (((i1 + (len g)) -' 1),f) = ((i1 + (len g)) -' 1) mod ((len f) -' 1) by A13, Def1;
hence S_Drop (((i1 + (len g)) -' 1),f) < len f by A15, A16, XXREAL_0:2; :: thesis: verum
end;
case A17: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: S_Drop (((i1 + (len g)) -' 1),f) < len f
i1 <= (len f) -' 1 by A8, NAT_D:49;
then A18: 1 <= (len f) -' 1 by A7, XXREAL_0:2;
S_Drop (((i1 + (len g)) -' 1),f) = (len f) -' 1 by A17, Def1;
hence S_Drop (((i1 + (len g)) -' 1),f) < len f by A18, NAT_D:51; :: thesis: verum
end;
end;
end;
i1 <= (len f) -' 1 by A8, NAT_D:49;
then 1 <= (len f) -' 1 by A7, XXREAL_0:2;
then A19: (len f) -' 1 < len f by NAT_D:51;
A20: now
per cases ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ) ;
case ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: 1 <= S_Drop (((i1 + (len g)) -' 1),f)
then 0 + 1 <= ((i1 + (len g)) -' 1) mod ((len f) -' 1) by NAT_1:13;
hence 1 <= S_Drop (((i1 + (len g)) -' 1),f) by Def1; :: thesis: verum
end;
case A21: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: 1 <= S_Drop (((i1 + (len g)) -' 1),f)
A22: i1 <= (len f) -' 1 by A8, NAT_D:49;
S_Drop (((i1 + (len g)) -' 1),f) = (len f) -' 1 by A21, Def1;
hence 1 <= S_Drop (((i1 + (len g)) -' 1),f) by A7, A22, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A23: 1 <= i2 by A1, Def2;
A24: i2 + 1 <= len f by A1, Def2;
then A25: i2 <= (len f) -' 1 by NAT_D:49;
then A26: 1 <= (len f) -' 1 by A23, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A27: i2 < len f by A25, XXREAL_0:2;
A28: len g < len f by A1, Def2;
A29: 0 <> (len f) -' 1 by A10, NAT_D:39;
now
per cases ( i2 < S_Drop (((i1 + (len g)) -' 1),f) or i2 > S_Drop (((i1 + (len g)) -' 1),f) or i2 = S_Drop (((i1 + (len g)) -' 1),f) ) by XXREAL_0:1;
case A30: i2 < S_Drop (((i1 + (len g)) -' 1),f) ; :: thesis: contradiction
i2 <= len f by A24, NAT_D:46;
then A31: f /. i2 = f . i2 by A23, FINSEQ_4:15;
A32: 1 <= S_Drop (((i1 + (len g)) -' 1),f) by A23, A30, XXREAL_0:2;
f /. i2 <> f /. (S_Drop (((i1 + (len g)) -' 1),f)) by A23, A12, A30, GOBOARD7:36;
hence contradiction by A4, A12, A31, A32, FINSEQ_4:15; :: thesis: verum
end;
case A33: i2 > S_Drop (((i1 + (len g)) -' 1),f) ; :: thesis: contradiction
i2 <= len f by A24, NAT_D:46;
then A34: f /. i2 = f . i2 by A23, FINSEQ_4:15;
f /. i2 <> f /. (S_Drop (((i1 + (len g)) -' 1),f)) by A20, A27, A33, GOBOARD7:36;
hence contradiction by A4, A20, A12, A34, FINSEQ_4:15; :: thesis: verum
end;
case A35: i2 = S_Drop (((i1 + (len g)) -' 1),f) ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )
now
per cases ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 or ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ) ;
case A36: ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )
( ex n being Nat st
( (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) & ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & (len f) -' 1 = 0 ) ) by NAT_D:def 2;
then consider n being Nat such that
A37: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) by A10, NAT_D:39;
A38: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + i2 by A35, A36, A37, Def1;
now
per cases ( n = 0 or n <> 0 ) ;
case n = 0 ; :: thesis: contradiction
then i2 = (i1 + (len g)) -' 1 by A35, A36, A37, Def1;
then i2 + 1 = ((i1 + (len g)) - 1) + 1 by A23, NAT_D:39
.= i1 + (len g) ;
hence contradiction by A2, A3, XREAL_1:8; :: thesis: verum
end;
case n <> 0 ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )
then A39: 0 + 1 <= n by NAT_1:13;
now
per cases ( 1 = n or 1 < n ) by A39, XXREAL_0:1;
case A40: 1 = n ; :: thesis: ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) )
(len f) -' 1 = (len f) - 1 by A26, NAT_D:39;
then A41: (i1 + (len g)) - 1 = ((len f) - 1) + i2 by A7, A38, A40, NAT_D:37;
then A42: len g = ((len f) + i2) - i1 ;
A43: (len f) -' 1 <= len f by NAT_D:50;
A44: dom g = Seg (len g) by FINSEQ_1:def 3;
A45: i1 <= len f by A8, A6, XXREAL_0:2;
A46: 1 <= (len f) -' 1 by A10, NAT_D:39;
A47: i1 <= (len f) -' 1 by A9, A10, NAT_D:39;
then A48: len (mid (f,i1,((len f) -' 1))) = (((len f) -' 1) -' i1) + 1 by A7, A45, A46, A43, FINSEQ_6:118;
A49: (((len f) -' 1) -' i1) + 1 = (((len f) - 1) - i1) + 1 by A9, A11, XREAL_1:233
.= (len f) - i1 ;
len ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) = (len (mid (f,i1,((len f) -' 1)))) + (len (f | i2)) by FINSEQ_1:22;
then len ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) = ((len f) - i1) + i2 by A24, A5, A48, A49, FINSEQ_1:59, XXREAL_0:2
.= ((len f) + i2) - i1
.= ((len f) + i2) -' i1 by A8, A6, NAT_D:37, XXREAL_0:2 ;
then A50: len ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) = len g by A8, A6, A42, NAT_D:37, XXREAL_0:2;
A51: ((len f) -' 1) -' i1 = ((len f) -' 1) - i1 by A9, A11, XREAL_1:233;
for j being Nat st j in dom g holds
g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j
proof
let j be Nat; :: thesis: ( j in dom g implies g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j )
assume A52: j in dom g ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j
then A53: 1 <= j by A44, FINSEQ_1:1;
then A54: (i1 + j) -' 1 = (i1 + j) - 1 by NAT_D:37;
i1 + j >= 1 + 1 by A7, A53, XREAL_1:7;
then A55: (i1 + j) -' 1 <> 0 by A54;
A56: j <= len g by A44, A52, FINSEQ_1:1;
then A57: g . j = f . (S_Drop (((i1 + j) -' 1),f)) by A1, A53, Def2;
A58: j in NAT by ORDINAL1:def 12;
now
per cases ( j <= len (mid (f,i1,((len f) -' 1))) or j > len (mid (f,i1,((len f) -' 1))) ) ;
case A59: j <= len (mid (f,i1,((len f) -' 1))) ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j
then A60: j + i1 <= ((((len f) -' 1) - i1) + 1) + i1 by A48, A51, XREAL_1:6;
A61: now
per cases ( i1 + j = len f or i1 + j <> len f ) ;
case A62: i1 + j = len f ; :: thesis: S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1
then ((i1 + j) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
hence S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 by A62, Def1; :: thesis: verum
end;
case i1 + j <> len f ; :: thesis: S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1
then i1 + j < len f by A11, A60, XXREAL_0:1;
then (i1 + j) - 1 < (len f) - 1 by XREAL_1:9;
then A63: (i1 + j) -' 1 < (len f) -' 1 by A7, A11, NAT_D:37;
then ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 by A55, NAT_D:24;
then S_Drop (((i1 + j) -' 1),f) = ((i1 + j) -' 1) mod ((len f) -' 1) by Def1;
hence S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 by A63, NAT_D:24; :: thesis: verum
end;
end;
end;
A64: (len f) -' 1 <= len f by NAT_D:50;
j in dom (mid (f,i1,((len f) -' 1))) by A53, A59, FINSEQ_3:25;
then A65: ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j = (mid (f,i1,((len f) -' 1))) . j by FINSEQ_1:def 7;
A66: 1 <= j by A44, A52, FINSEQ_1:1;
i1 <= (len f) -' 1 by A9, A10, NAT_D:39;
hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j by A7, A45, A46, A57, A58, A59, A65, A64, A66, A61, FINSEQ_6:118; :: thesis: verum
end;
case A67: j > len (mid (f,i1,((len f) -' 1))) ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j
j <= ((len f) + i2) - i1 by A41, A44, A52, FINSEQ_1:1;
then j + i1 <= (((len f) + i2) - i1) + i1 by XREAL_1:6;
then A68: (j + i1) - (len f) <= ((len f) + i2) - (len f) by XREAL_1:9;
j < len f by A28, A56, XXREAL_0:2;
then A69: j <= (len f) - 1 by SPPOL_1:1;
(i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:9;
then A70: i1 + j <= ((len f) -' 1) + ((len f) -' 1) by A11, A69, XREAL_1:7;
A71: ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j = (f | i2) . (j - (len (mid (f,i1,((len f) -' 1))))) by A50, A56, A67, FINSEQ_6:108;
A72: (i1 + j) - 1 = (i1 + j) -' 1 by A7, NAT_D:37;
(len (mid (f,i1,((len f) -' 1)))) + 1 <= j by A67, NAT_1:13;
then ((len (mid (f,i1,((len f) -' 1)))) + 1) - (len (mid (f,i1,((len f) -' 1)))) <= j - (len (mid (f,i1,((len f) -' 1)))) by XREAL_1:9;
then 1 + (len f) <= ((i1 + j) - (len f)) + (len f) by A48, A49, XREAL_1:6;
then (1 + (len f)) - 1 <= (i1 + j) - 1 by XREAL_1:9;
then A73: (len f) -' 1 < (i1 + j) -' 1 by A19, A72, XXREAL_0:2;
j + i1 > ((len f) - i1) + i1 by A48, A49, A67, XREAL_1:6;
then A74: (i1 + j) - (len f) > (len f) - (len f) by XREAL_1:9;
then A75: (i1 + j) -' (len f) = (i1 + j) - (len f) by XREAL_0:def 2;
j - (len (mid (f,i1,((len f) -' 1)))) = j - ((len f) - i1) by A7, A45, A46, A43, A47, A49, FINSEQ_6:118
.= (j + i1) - (len f) ;
then A76: (f | i2) . (j - (len (mid (f,i1,((len f) -' 1))))) = f . ((i1 + j) -' (len f)) by A75, A68, FINSEQ_3:112;
i1 + j < (i1 + j) + 1 by NAT_1:13;
then (i1 + j) - 1 < ((i1 + j) + 1) - 1 by XREAL_1:9;
then A77: (i1 + j) -' 1 < ((len f) -' 1) + ((len f) -' 1) by A72, A70, XXREAL_0:2;
now
per cases ( ((i1 + j) -' 1) mod ((len f) -' 1) = 0 or ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 ) ;
case ((i1 + j) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: contradiction
hence contradiction by A73, A77, Th6; :: thesis: verum
end;
case A78: ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 ; :: thesis: g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j
((i1 + j) -' (len f)) + ((len f) -' 1) = ((i1 + j) -' (len f)) + ((len f) - 1) by A10, NAT_D:39
.= ((i1 + j) - (len f)) + ((len f) - 1) by A74, XREAL_0:def 2
.= (i1 + j) - 1
.= (i1 + j) -' 1 by A53, NAT_D:37 ;
then A79: ((i1 + j) -' 1) mod ((len f) -' 1) = (((i1 + j) -' (len f)) + (((len f) -' 1) mod ((len f) -' 1))) mod ((len f) -' 1) by NAT_D:23
.= (((i1 + j) -' (len f)) + 0) mod ((len f) -' 1) by NAT_D:25
.= ((i1 + j) -' (len f)) mod ((len f) -' 1) ;
(i1 + j) - ((len f) -' 1) <= (((len f) -' 1) + ((len f) -' 1)) - ((len f) -' 1) by A70, XREAL_1:9;
then (i1 + j) - ((len f) - 1) <= (len f) -' 1 by A10, NAT_D:39;
then ((i1 + j) -' (len f)) + 1 <= (len f) -' 1 by A75;
then A80: (i1 + j) -' (len f) < (len f) -' 1 by NAT_1:13;
S_Drop (((i1 + j) -' 1),f) = ((i1 + j) -' 1) mod ((len f) -' 1) by A78, Def1;
hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j by A57, A71, A76, A79, A80, NAT_D:24; :: thesis: verum
end;
end;
end;
hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ; :: thesis: verum
end;
end;
end;
hence g . j = ((mid (f,i1,((len f) -' 1))) ^ (f | i2)) . j ; :: thesis: verum
end;
hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) by A8, A6, A42, A50, FINSEQ_2:9, NAT_D:37, XXREAL_0:2; :: thesis: verum
end;
case 1 < n ; :: thesis: contradiction
then 1 + 1 <= n by NAT_1:13;
then ((len f) -' 1) * n >= ((len f) -' 1) * (1 + 1) by XREAL_1:64;
then A81: (i1 + (len g)) -' 1 >= (((len f) -' 1) * (1 + 1)) + i2 by A38, XREAL_1:6;
A82: ((len f) -' 1) * (1 + 1) <= (((len f) -' 1) * (1 + 1)) + i2 by NAT_1:11;
A83: (i1 + 1) - 1 <= (len f) - 1 by A8, XREAL_1:9;
(len g) - 1 < (len f) -' 1 by A28, A11, XREAL_1:9;
then A84: i1 + ((len g) - 1) < ((len f) -' 1) + ((len f) -' 1) by A11, A83, XREAL_1:8;
(i1 + (len g)) - 1 = (i1 + (len g)) -' 1 by A7, NAT_D:37;
hence contradiction by A81, A84, A82, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) ; :: thesis: verum
end;
end;
end;
hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) ; :: thesis: verum
end;
case A85: ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 ; :: thesis: contradiction
ex n being Nat st
( (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) & ((i1 + (len g)) -' 1) mod ((len f) -' 1) < (len f) -' 1 ) by A29, NAT_D:def 2;
then consider n being Nat such that
A86: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) ;
A87: now
assume n > 1 ; :: thesis: contradiction
then n >= 1 + 1 by NAT_1:13;
then A88: (i1 + (len g)) -' 1 >= ((len f) -' 1) * (1 + 1) by A85, A86, NAT_1:4;
(len g) - 1 < (len f) - 1 by A28, XREAL_1:9;
then i1 + ((len g) - 1) < ((len f) -' 1) + ((len f) -' 1) by A9, A11, XREAL_1:8;
then (i1 + (len g)) - 1 < ((len f) -' 1) + ((len f) -' 1) ;
hence contradiction by A7, A88, NAT_1:12, XREAL_1:233; :: thesis: verum
end;
then n >= 0 + 1 by NAT_1:13;
then n = 1 by A87, XXREAL_0:1;
then (i1 + (len g)) -' 1 = i2 by A35, A85, A86, Def1;
then A90: (i1 + (len g)) - 1 = i2 by A23, NAT_D:39;
i2 - i2 < i1 - i2 by A2, XREAL_1:9;
then A91: - 0 > - (i1 - i2) by XREAL_1:24;
1 - 1 <= (len g) - 1 by A3, XREAL_1:9;
hence contradiction by A90, A91; :: thesis: verum
end;
end;
end;
hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) ) ; :: thesis: verum
end;
end;
end;
hence ( len g = ((len f) + i2) -' i1 & g = (mid (f,i1,((len f) -' 1))) ^ (f | i2) & g = (mid (f,i1,((len f) -' 1))) ^ (mid (f,1,i2)) ) by A23, FINSEQ_6:116; :: thesis: verum