let f be V26() 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 = (i1 -' i2) + 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 = (i1 -' i2) + 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 = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) )
assume that
A1: g is_a_part<_of f,i1,i2 and
A2: i1 >= i2 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
A3: 1 <= len g by A1;
A4: f . i2 = f . (S_Drop ((((len f) + i1) -' (len g)),f)) by A1;
A5: i1 + 1 <= len f by A1;
i1 <= i1 + 1 by NAT_1:11;
then A6: i1 <= len f by A5, XXREAL_0:2;
A7: 1 <= i2 by A1;
A8: i2 + 1 <= len f by A1;
then (i2 + 1) - 1 <= (len f) - 1 by XREAL_1:9;
then A9: 1 <= (len f) - 1 by A7, XXREAL_0:2;
then A10: (len f) - 1 = (len f) -' 1 by NAT_D:39;
A11: now :: thesis: ( ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 & S_Drop ((((len f) + i1) -' (len g)),f) < len f ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & S_Drop ((((len f) + i1) -' (len g)),f) < len f ) )
per cases ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 or (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ) ;
case A12: (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: S_Drop ((((len f) + i1) -' (len g)),f) < len f
A13: i2 <= (len f) -' 1 by A8, NAT_D:49;
then A14: (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 by A7, NAT_D:1;
1 <= (len f) -' 1 by A7, A13, XXREAL_0:2;
then A15: (len f) -' 1 < len f by NAT_D:51;
S_Drop ((((len f) + i1) -' (len g)),f) = (((len f) + i1) -' (len g)) mod ((len f) -' 1) by A12, Def1;
hence S_Drop ((((len f) + i1) -' (len g)),f) < len f by A14, A15, XXREAL_0:2; :: thesis: verum
end;
case A16: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: S_Drop ((((len f) + i1) -' (len g)),f) < len f
i2 <= (len f) -' 1 by A8, NAT_D:49;
then A17: 1 <= (len f) -' 1 by A7, XXREAL_0:2;
S_Drop ((((len f) + i1) -' (len g)),f) = (len f) -' 1 by A16, Def1;
hence S_Drop ((((len f) + i1) -' (len g)),f) < len f by A17, NAT_D:51; :: thesis: verum
end;
end;
end;
A18: i2 <= (len f) -' 1 by A8, NAT_D:49;
then 1 <= (len f) -' 1 by A7, XXREAL_0:2;
then (len f) -' 1 < len f by NAT_D:51;
then A19: i2 < len f by A18, XXREAL_0:2;
A20: 0 <> (len f) -' 1 by A9, NAT_D:39;
A21: now :: thesis: ( ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 & 1 <= S_Drop ((((len f) + i1) -' (len g)),f) ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & 1 <= S_Drop ((((len f) + i1) -' (len g)),f) ) )
per cases ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 or (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ) ;
case (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: 1 <= S_Drop ((((len f) + i1) -' (len g)),f)
then 0 + 1 <= (((len f) + i1) -' (len g)) mod ((len f) -' 1) by NAT_1:13;
hence 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by Def1; :: thesis: verum
end;
case A22: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: 1 <= S_Drop ((((len f) + i1) -' (len g)),f)
A23: i2 <= (len f) -' 1 by A8, NAT_D:49;
S_Drop ((((len f) + i1) -' (len g)),f) = (len f) -' 1 by A22, Def1;
hence 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by A7, A23, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A24: len g < len f by A1;
A25: 0 < (len f) -' 1 by A9, NAT_D:39;
now :: thesis: ( ( i2 < S_Drop ((((len f) + i1) -' (len g)),f) & contradiction ) or ( i2 > S_Drop ((((len f) + i1) -' (len g)),f) & contradiction ) or ( i2 = S_Drop ((((len f) + i1) -' (len g)),f) & len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) )
per cases ( i2 < S_Drop ((((len f) + i1) -' (len g)),f) or i2 > S_Drop ((((len f) + i1) -' (len g)),f) or i2 = S_Drop ((((len f) + i1) -' (len g)),f) ) by XXREAL_0:1;
case A26: i2 < S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: contradiction
i2 <= len f by A8, NAT_1:13;
then A27: f /. i2 = f . i2 by A7, FINSEQ_4:15;
A28: 1 <= S_Drop ((((len f) + i1) -' (len g)),f) by A7, A26, XXREAL_0:2;
f /. i2 <> f /. (S_Drop ((((len f) + i1) -' (len g)),f)) by A7, A11, A26, GOBOARD7:36;
hence contradiction by A4, A11, A27, A28, FINSEQ_4:15; :: thesis: verum
end;
case A29: i2 > S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: contradiction
i2 <= len f by A8, NAT_1:13;
then A30: f /. i2 = f . i2 by A7, FINSEQ_4:15;
f /. i2 <> f /. (S_Drop ((((len f) + i1) -' (len g)),f)) by A21, A19, A29, GOBOARD7:36;
hence contradiction by A4, A21, A11, A30, FINSEQ_4:15; :: thesis: verum
end;
case A31: i2 = S_Drop ((((len f) + i1) -' (len g)),f) ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
now :: thesis: ( ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 & len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) )
per cases ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 or (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ) ;
case A32: (((len f) + i1) -' (len g)) mod ((len f) -' 1) <> 0 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
ex n being Nat st
( ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) & (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 ) by A20, NAT_D:def 2;
then consider n being Nat such that
A33: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) ;
A34: ( n = 0 or n >= 0 + 1 ) by NAT_1:13;
A35: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + i2 by A31, A32, A33, Def1;
now :: thesis: ( ( n = 0 & contradiction ) or ( n = 1 & len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) or ( n > 1 & contradiction ) )
per cases ( n = 0 or n = 1 or n > 1 ) by A34, XXREAL_0:1;
case n = 0 ; :: thesis: contradiction
then i2 = ((len f) + i1) -' (len g) by A31, A32, A33, Def1;
then i2 = ((len f) + i1) - (len g) by A24, NAT_D:37;
then i2 + (len g) = i1 + (len f) ;
hence contradiction by A2, A24, XREAL_1:8; :: thesis: verum
end;
case A36: n = 1 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
A37: ((len f) + i1) -' (len g) = ((len f) + i1) - (len g) by A24, NAT_D:37;
A38: ((len f) - 1) + i2 = ((len f) + i1) -' (len g) by A10, A31, A32, A33, A36, Def1;
then A39: len g = (i1 - i2) + 1 by A37;
then A40: len g = (i1 -' i2) + 1 by A2, XREAL_1:233;
A41: dom g = Seg (len g) by FINSEQ_1:def 3;
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 A41, FINSEQ_1:1;
A45: j <= len g by A41, A43, FINSEQ_1:1;
1 - 1 <= i2 - 1 by A7, XREAL_1:9;
then A46: i1 - 0 >= i1 - (i2 - 1) by XREAL_1:10;
then A47: (i1 -' j) + 1 = (i1 - j) + 1 by A38, A37, A45, XREAL_1:233, XXREAL_0:2;
A48: j <= i1 by A38, A37, A45, A46, XXREAL_0:2;
A49: now :: thesis: ( ( ((len f) + i1) -' j = (len f) -' 1 & contradiction ) or ( ((len f) + i1) -' j <> (len f) -' 1 & S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ) )
per cases ( ((len f) + i1) -' j = (len f) -' 1 or ((len f) + i1) -' j <> (len f) -' 1 ) ;
case ((len f) + i1) -' j = (len f) -' 1 ; :: thesis: contradiction
then ((len f) + i1) - j = (len f) -' 1 by A24, A45, NAT_D:37, XXREAL_0:2
.= (len f) - 1 by A9, NAT_D:39 ;
then i1 - j = - 1 ;
hence contradiction by A48, XREAL_1:48; :: thesis: verum
end;
case ((len f) + i1) -' j <> (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
(i1 + 1) + 0 < (len f) + j by A5, A44, XREAL_1:8;
then (i1 + 1) - j < ((len f) + j) - j by XREAL_1:9;
then ((i1 + 1) - j) - 1 < (len f) - 1 by XREAL_1:9;
then i1 - j < (len f) - 1 ;
then i1 -' j < (len f) -' 1 by A10, A38, A37, A45, A46, XREAL_1:233, XXREAL_0:2;
then A50: (i1 -' j) + 1 <= (len f) -' 1 by NAT_1:13;
A51: ((len f) + i1) -' j = ((len f) + i1) - j by A24, A45, NAT_D:37, XXREAL_0:2;
now :: thesis: ( ( (i1 -' j) + 1 = (len f) -' 1 & S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ) or ( (i1 -' j) + 1 < (len f) -' 1 & S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ) )
per cases ( (i1 -' j) + 1 = (len f) -' 1 or (i1 -' j) + 1 < (len f) -' 1 ) by A50, XXREAL_0:1;
case A52: (i1 -' j) + 1 = (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
((len f) + i1) -' j = ((((len f) - 1) + 1) + i1) - j by A24, A45, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + ((i1 - j) + 1) by A10
.= ((len f) -' 1) + ((len f) -' 1) by A38, A37, A45, A46, A52, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th3;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A52, Def1; :: thesis: verum
end;
case A53: (i1 -' j) + 1 < (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
A54: len f = ((len f) - 1) + 1
.= ((len f) -' 1) + 1 by A9, NAT_D:39 ;
((((len f) -' 1) + 1) + i1) -' j = ((((len f) -' 1) + 1) + i1) - j by A38, A37, A45, A46, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + (1 + (i1 - j))
.= ((len f) -' 1) + (1 + (i1 -' j)) by A38, A37, A45, A46, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = ((((len f) -' 1) mod ((len f) -' 1)) + (1 + (i1 -' j))) mod ((len f) -' 1) by A54, NAT_D:22
.= (0 + (1 + (i1 -' j))) mod ((len f) -' 1) by NAT_D:25
.= (i1 -' j) + 1 by A53, NAT_D:24 ;
then A55: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1;
((((len f) - 1) + 1) + i1) - j = ((len f) - 1) + ((i1 - j) + 1) ;
then A56: ((len f) + i1) -' j = ((i1 -' j) + 1) + ((len f) -' 1) by A9, A47, A51, NAT_D:39;
((len f) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
then S_Drop ((((len f) + i1) -' j),f) = (((i1 -' j) + 1) + 0) mod ((len f) -' 1) by A55, A56, NAT_D:22
.= ((i1 -' j) + 1) mod ((len f) -' 1) ;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A53, NAT_D:24; :: thesis: verum
end;
end;
end;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ; :: thesis: verum
end;
end;
end;
g . j = f . (S_Drop ((((len f) + i1) -' j),f)) by A1, A44, A45;
hence g . j = (mid (f,i1,i2)) . j by A2, A7, A6, A40, A44, A45, A49, Th12; :: thesis: verum
end;
len (mid (f,i1,i2)) = len g by A2, A7, A6, A40, Th9;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) by A2, A39, A42, FINSEQ_2:9, XREAL_1:233; :: thesis: verum
end;
case n > 1 ; :: thesis: contradiction
then 1 + 1 <= n by NAT_1:13;
then A57: (((len f) + i1) -' (len g)) - i2 >= ((len f) -' 1) * (1 + 1) by A35, XREAL_1:64;
A58: (len f) - i2 <= (len f) - 1 by A7, XREAL_1:10;
(i1 + 1) + 0 < (i1 + 1) + (len g) by A3, XREAL_1:8;
then (i1 + 1) - (len g) < ((i1 + 1) + (len g)) - (len g) by XREAL_1:14;
then ((i1 - (len g)) + 1) - i2 < (i1 + 1) - i2 by XREAL_1:14;
then A59: ((len f) - 1) + (((i1 - (len g)) - i2) + 1) < ((len f) - 1) + ((i1 + 1) - i2) by XREAL_1:8;
(i1 + 1) - i2 <= (len f) - i2 by A5, XREAL_1:9;
then (i1 + 1) - i2 <= (len f) - 1 by A58, XXREAL_0:2;
then ((len f) - 1) + ((i1 + 1) - i2) <= ((len f) - 1) + ((len f) - 1) by XREAL_1:7;
then (((len f) + i1) - (len g)) - i2 < ((len f) - 1) + ((len f) - 1) by A59, XXREAL_0:2;
hence contradiction by A24, A10, A57, NAT_D:37; :: thesis: verum
end;
end;
end;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum
end;
case A60: (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 ; :: thesis: ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) )
( ex n being Nat st
( ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) & (((len f) + i1) -' (len g)) mod ((len f) -' 1) < (len f) -' 1 ) or ( (((len f) + i1) -' (len g)) mod ((len f) -' 1) = 0 & (len f) -' 1 = 0 ) ) by NAT_D:def 2;
then consider n being Nat such that
A61: ((len f) + i1) -' (len g) = (((len f) -' 1) * n) + ((((len f) + i1) -' (len g)) mod ((len f) -' 1)) by A9, NAT_D:39;
A62: ((len f) + i1) -' (len g) = i2 * n by A31, A60, A61, Def1;
now :: thesis: not n = 0
assume n = 0 ; :: thesis: contradiction
then A63: len g >= (len f) + i1 by A60, A61, NAT_D:36;
len f <= (len f) + i1 by NAT_1:11;
hence contradiction by A24, A63, XXREAL_0:2; :: thesis: verum
end;
then A64: n >= 0 + 1 by NAT_1:13;
A65: now :: thesis: ( ( n > 1 & len g = (i1 -' i2) + 1 ) or ( n = 1 & contradiction ) )
per cases ( n > 1 or n = 1 ) by A64, XXREAL_0:1;
case A66: n > 1 ; :: thesis: len g = (i1 -' i2) + 1
A67: ((len f) -' 1) + ((len f) -' 1) = ((len f) -' 1) * (1 + 1) ;
(i1 + 1) + 1 <= (len f) + (len g) by A5, A3, XREAL_1:7;
then (1 + (i1 + 1)) - (len g) <= ((len f) + (len g)) - (len g) by XREAL_1:9;
then (1 + ((i1 + 1) - (len g))) - 1 <= (len f) - 1 by XREAL_1:9;
then ((len f) - 1) + ((i1 + 1) - (len g)) <= ((len f) - 1) + ((len f) - 1) by XREAL_1:6;
then ((len f) + i1) - (len g) <= ((len f) - 1) + ((len f) - 1) ;
then A68: ((len f) + i1) -' (len g) <= ((len f) -' 1) + ((len f) -' 1) by A24, A10, NAT_D:37;
A69: n >= 1 + 1 by A66, NAT_1:13;
now :: thesis: ( ( n > 1 + 1 & contradiction ) or ( n = 1 + 1 & len g = (i1 -' i2) + 1 ) )
per cases ( n > 1 + 1 or n = 1 + 1 ) by A69, XXREAL_0:1;
case A70: n = 1 + 1 ; :: thesis: len g = (i1 -' i2) + 1
then A71: (((len f) - 1) + (1 + i1)) - (len g) = ((len f) -' 1) + ((len f) -' 1) by A24, A60, A61, NAT_D:37;
then 1 + ((len f) -' 1) <= ((1 + i1) - ((len f) -' 1)) + ((len f) -' 1) by A3, A10, XREAL_1:6;
then 1 + ((len f) - 1) <= 1 + i1 by A9, NAT_D:39;
then A72: len f = i1 + 1 by A5, XXREAL_0:1;
then i2 = i1 by A60, A61, A62, A70, NAT_D:34;
then i1 -' i2 = 0 by XREAL_1:232;
hence len g = (i1 -' i2) + 1 by A10, A71, A72; :: thesis: verum
end;
end;
end;
hence len g = (i1 -' i2) + 1 ; :: thesis: verum
end;
case A73: n = 1 ; :: thesis: contradiction
((len f) + i1) -' (len g) = ((len f) + i1) - (len g) by A24, NAT_D:37;
then (len f) + i1 = i2 + (len g) by A62, A73;
hence contradiction by A2, A24, XREAL_1:8; :: thesis: verum
end;
end;
end;
A74: dom g = Seg (len g) by FINSEQ_1:def 3;
A75: 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 A76: j in dom g ; :: thesis: g . j = (mid (f,i1,i2)) . j
then A77: 1 <= j by A74, FINSEQ_1:1;
A78: j <= len g by A74, A76, FINSEQ_1:1;
1 - 1 <= i2 - 1 by A7, XREAL_1:9;
then A79: i1 - 0 >= i1 - (i2 - 1) by XREAL_1:10;
A80: (i1 -' i2) + 1 = (i1 - i2) + 1 by A2, XREAL_1:233
.= i1 - (i2 - 1) ;
then A81: (i1 -' j) + 1 = (i1 - j) + 1 by A65, A78, A79, XREAL_1:233, XXREAL_0:2;
A82: j <= i1 by A65, A78, A80, A79, XXREAL_0:2;
A83: now :: thesis: ( ( ((len f) + i1) -' j = (len f) -' 1 & contradiction ) or ( ((len f) + i1) -' j <> (len f) -' 1 & S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ) )
per cases ( ((len f) + i1) -' j = (len f) -' 1 or ((len f) + i1) -' j <> (len f) -' 1 ) ;
case ((len f) + i1) -' j = (len f) -' 1 ; :: thesis: contradiction
then ((len f) + i1) - j = (len f) -' 1 by A65, A78, A80, A79, NAT_D:37, XXREAL_0:2
.= (len f) - 1 by A9, NAT_D:39 ;
then i1 - j = - 1 ;
hence contradiction by A82, XREAL_1:48; :: thesis: verum
end;
case ((len f) + i1) -' j <> (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
(i1 + 1) + 0 < (len f) + j by A5, A77, XREAL_1:8;
then (i1 + 1) - j < ((len f) + j) - j by XREAL_1:9;
then ((i1 + 1) - j) - 1 < (len f) - 1 by XREAL_1:9;
then i1 - j < (len f) - 1 ;
then i1 -' j < (len f) -' 1 by A10, A65, A78, A80, A79, XREAL_1:233, XXREAL_0:2;
then A84: (i1 -' j) + 1 <= (len f) -' 1 by NAT_1:13;
A85: ((len f) + i1) -' j = ((len f) + i1) - j by A65, A78, A80, A79, NAT_D:37, XXREAL_0:2;
now :: thesis: ( ( (i1 -' j) + 1 = (len f) -' 1 & S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ) or ( (i1 -' j) + 1 < (len f) -' 1 & S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ) )
per cases ( (i1 -' j) + 1 = (len f) -' 1 or (i1 -' j) + 1 < (len f) -' 1 ) by A84, XXREAL_0:1;
case A86: (i1 -' j) + 1 = (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
((len f) + i1) -' j = ((((len f) - 1) + 1) + i1) - j by A65, A78, A80, A79, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + ((i1 - j) + 1) by A10
.= ((len f) -' 1) + ((len f) -' 1) by A65, A78, A80, A79, A86, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = 0 by Th3;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A86, Def1; :: thesis: verum
end;
case A87: (i1 -' j) + 1 < (len f) -' 1 ; :: thesis: S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1
A88: len f = ((len f) - 1) + 1
.= ((len f) -' 1) + 1 by A9, NAT_D:39 ;
((((len f) -' 1) + 1) + i1) -' j = ((((len f) -' 1) + 1) + i1) - j by A65, A78, A80, A79, NAT_D:37, XXREAL_0:2
.= ((len f) -' 1) + (1 + (i1 - j))
.= ((len f) -' 1) + (1 + (i1 -' j)) by A65, A78, A80, A79, XREAL_1:233, XXREAL_0:2 ;
then (((len f) + i1) -' j) mod ((len f) -' 1) = ((((len f) -' 1) mod ((len f) -' 1)) + (1 + (i1 -' j))) mod ((len f) -' 1) by A88, NAT_D:22
.= (0 + (1 + (i1 -' j))) mod ((len f) -' 1) by NAT_D:25
.= (i1 -' j) + 1 by A87, NAT_D:24 ;
then A89: S_Drop ((((len f) + i1) -' j),f) = (((len f) + i1) -' j) mod ((len f) -' 1) by Def1;
((((len f) - 1) + 1) + i1) - j = ((len f) - 1) + ((i1 - j) + 1) ;
then A90: ((len f) + i1) -' j = ((i1 -' j) + 1) + ((len f) -' 1) by A9, A81, A85, NAT_D:39;
((len f) -' 1) mod ((len f) -' 1) = 0 by NAT_D:25;
then S_Drop ((((len f) + i1) -' j),f) = (((i1 -' j) + 1) + 0) mod ((len f) -' 1) by A89, A90, NAT_D:22
.= ((i1 -' j) + 1) mod ((len f) -' 1) ;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 by A87, NAT_D:24; :: thesis: verum
end;
end;
end;
hence S_Drop ((((len f) + i1) -' j),f) = (i1 -' j) + 1 ; :: thesis: verum
end;
end;
end;
g . j = f . (S_Drop ((((len f) + i1) -' j),f)) by A1, A77, A78;
hence g . j = (mid (f,i1,i2)) . j by A2, A7, A6, A65, A77, A78, A83, Th12; :: thesis: verum
end;
len (mid (f,i1,i2)) = len g by A2, A7, A6, A65, Th9;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) by A65, A75, FINSEQ_2:9; :: thesis: verum
end;
end;
end;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum
end;
end;
end;
hence ( len g = (i1 -' i2) + 1 & g = mid (f,i1,i2) ) ; :: thesis: verum