let f be constant standard special_circular_sequence; :: thesis: for g being FinSequence of (TOP-REAL 2)
for i1, i2 being 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 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 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;
A4: 1 <= i1 by A1;
A5: i1 + 1 <= len f by A1;
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 :: thesis: ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & S_Drop (((i1 + (len g)) -' 1),f) < len f ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & S_Drop (((i1 + (len g)) -' 1),f) < len f ) )
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;
A16: f . i2 = f . (S_Drop (((i1 + (len g)) -' 1),f)) by A1;
A17: i2 + 1 <= len f by A1;
A18: now :: thesis: ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & 1 <= S_Drop (((i1 + (len g)) -' 1),f) ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & 1 <= S_Drop (((i1 + (len g)) -' 1),f) ) )
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;
A24: 1 <= i2 by A1;
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 :: thesis: ( ( i2 < S_Drop (((i1 + (len g)) -' 1),f) & contradiction ) or ( i2 > S_Drop (((i1 + (len g)) -' 1),f) & contradiction ) or ( i2 = S_Drop (((i1 + (len g)) -' 1),f) & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) )
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 :: thesis: ( ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) <> 0 & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) or ( ((i1 + (len g)) -' 1) mod ((len f) -' 1) = 0 & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) )
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 :: thesis: ( ( n = 0 & len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) or ( n <> 0 & contradiction ) )
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 )
assume A43: j in dom g ; :: thesis: g . j = (mid (f,i1,i2)) . j
then A44: 1 <= j by A38, FINSEQ_1:1;
then A45: (i1 + j) -' 1 = (i1 + j) - 1 by NAT_D:37;
i1 + j >= 1 + 1 by A4, A44, XREAL_1:7;
then A46: (i1 + j) -' 1 <> 0 by A45;
A47: j <= len g by A38, A43, FINSEQ_1:1;
then j + i1 <= ((i2 - i1) + 1) + i1 by A40, A39, XREAL_1:6;
then A48: i1 + j <= len f by A17, XXREAL_0:2;
A49: now :: thesis: ( ( i1 + j = len f & S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 ) or ( i1 + j <> len f & S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 ) )
per cases ( i1 + j = len f or i1 + j <> len f ) ;
case A50: 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 A50, 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 A48, 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 A46, Def1; :: thesis: verum
end;
end;
end;
g . j = f . (S_Drop (((i1 + j) -' 1),f)) by A1, A44, A47;
hence g . j = (mid (f,i1,i2)) . j by A2, A4, A25, A41, A44, A47, A49, FINSEQ_6:122; :: thesis: verum
end;
A51: (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, A51, A42, FINSEQ_2:9, XREAL_1:233; :: thesis: verum
end;
case n <> 0 ; :: thesis: contradiction
then 0 + 1 <= n by NAT_1:13;
then A52: ((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 A53: (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 A53, XREAL_1:14;
hence contradiction by A36, A52; :: thesis: verum
end;
end;
end;
hence ( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum
end;
case A54: ((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
A55: (i1 + (len g)) -' 1 = (((len f) -' 1) * n) + (((i1 + (len g)) -' 1) mod ((len f) -' 1)) ;
A56: now :: thesis: not n > 1
assume n > 1 ; :: thesis: contradiction
then n >= 1 + 1 by NAT_1:13;
then A57: (i1 + (len g)) -' 1 >= ((len f) -' 1) * (1 + 1) by A54, A55, 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, A57, NAT_1:12, XREAL_1:233; :: thesis: verum
end;
then n >= 0 + 1 by NAT_1:13;
then A59: n = 1 by A56, XXREAL_0:1;
(i1 + (len g)) -' 1 = i2 * n by A33, A54, A55, Def1;
then A60: (i1 + (len g)) - 1 = i2 by A24, A59, NAT_D:39;
A61: i2 - i1 = i2 -' i1 by A2, XREAL_1:233;
then A62: len g = (i2 -' i1) + 1 by A60;
A63: dom g = Seg (len g) by FINSEQ_1:def 3;
A64: 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 )
assume A65: j in dom g ; :: thesis: g . j = (mid (f,i1,i2)) . j
then A66: 1 <= j by A63, FINSEQ_1:1;
then A67: (i1 + j) -' 1 = (i1 + j) - 1 by NAT_D:37;
A68: j <= len g by A63, A65, FINSEQ_1:1;
then j + i1 <= ((i2 - i1) + 1) + i1 by A60, XREAL_1:6;
then A69: i1 + j <= len f by A17, XXREAL_0:2;
i1 + j >= 1 + 1 by A4, A66, XREAL_1:7;
then A70: (i1 + j) -' 1 <> 0 by A67;
A71: now :: thesis: ( ( i1 + j = len f & S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 ) or ( i1 + j <> len f & S_Drop (((i1 + j) -' 1),f) = (i1 + j) -' 1 ) )
per cases ( i1 + j = len f or i1 + j <> len f ) ;
case A72: 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 A72, 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 A69, XXREAL_0:1;
then (i1 + j) - 1 < (len f) - 1 by XREAL_1:9;
then A73: (i1 + j) -' 1 < (len f) -' 1 by A4, A8, NAT_D:37;
then ((i1 + j) -' 1) mod ((len f) -' 1) <> 0 by A70, 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 A73, NAT_D:24; :: thesis: verum
end;
end;
end;
g . j = f . (S_Drop (((i1 + j) -' 1),f)) by A1, A66, A68;
hence g . j = (mid (f,i1,i2)) . j by A2, A4, A25, A62, A66, A68, A71, FINSEQ_6:122; :: thesis: verum
end;
len (mid (f,i1,i2)) = len g by A2, A4, A24, A21, A25, A62, FINSEQ_6:118;
hence ( len g = (i2 -' i1) + 1 & g = mid (f,i1,i2) ) by A60, A61, A64, 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