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