let f be FinSequence; :: thesis: for k1, k2 being Nat holds len (mid (f,k1,k2)) <= len f
let k1, k2 be Nat; :: thesis: len (mid (f,k1,k2)) <= len f
per cases ( k1 <= k2 or k1 > k2 ) ;
suppose k1 <= k2 ; :: thesis: len (mid (f,k1,k2)) <= len f
then A1: mid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 -' k1) + 1) by Def3;
per cases ( len (f /^ (k1 -' 1)) <= (k2 -' k1) + 1 or len (f /^ (k1 -' 1)) > (k2 -' k1) + 1 ) ;
suppose len (f /^ (k1 -' 1)) <= (k2 -' k1) + 1 ; :: thesis: len (mid (f,k1,k2)) <= len f
then A2: mid (f,k1,k2) = f /^ (k1 -' 1) by A1, FINSEQ_1:58;
per cases ( k1 -' 1 <= len f or not k1 -' 1 <= len f ) ;
suppose A3: k1 -' 1 <= len f ; :: thesis: len (mid (f,k1,k2)) <= len f
(len f) - (k1 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len (mid (f,k1,k2)) <= len f by A2, A3, RFINSEQ:def 1; :: thesis: verum
end;
suppose not k1 -' 1 <= len f ; :: thesis: len (mid (f,k1,k2)) <= len f
then f /^ (k1 -' 1) = {} by RFINSEQ:def 1;
hence len (mid (f,k1,k2)) <= len f by A2; :: thesis: verum
end;
end;
end;
suppose len (f /^ (k1 -' 1)) > (k2 -' k1) + 1 ; :: thesis: len (mid (f,k1,k2)) <= len f
then A5: len (mid (f,k1,k2)) <= len (f /^ (k1 -' 1)) by A1, FINSEQ_1:59;
per cases ( k1 -' 1 <= len f or not k1 -' 1 <= len f ) ;
suppose k1 -' 1 <= len f ; :: thesis: len (mid (f,k1,k2)) <= len f
then A6: len (mid (f,k1,k2)) <= (len f) - (k1 -' 1) by A5, RFINSEQ:def 1;
(len f) - (k1 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len (mid (f,k1,k2)) <= len f by A6, XXREAL_0:2; :: thesis: verum
end;
suppose not k1 -' 1 <= len f ; :: thesis: len (mid (f,k1,k2)) <= len f
then f /^ (k1 -' 1) = {} by RFINSEQ:def 1;
hence len (mid (f,k1,k2)) <= len f by A5; :: thesis: verum
end;
end;
end;
end;
end;
suppose k1 > k2 ; :: thesis: len (mid (f,k1,k2)) <= len f
then A7: mid (f,k1,k2) = Rev ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) by Def3;
set m = (f /^ (k2 -' 1)) | ((k1 -' k2) + 1);
len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
proof
per cases ( len (f /^ (k2 -' 1)) <= (k1 -' k2) + 1 or len (f /^ (k2 -' 1)) > (k1 -' k2) + 1 ) ;
suppose len (f /^ (k2 -' 1)) <= (k1 -' k2) + 1 ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
then A8: (f /^ (k2 -' 1)) | ((k1 -' k2) + 1) = f /^ (k2 -' 1) by FINSEQ_1:58;
per cases ( k2 -' 1 <= len f or not k2 -' 1 <= len f ) ;
suppose A9: k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
(len f) - (k2 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f by A8, A9, RFINSEQ:def 1; :: thesis: verum
end;
suppose not k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
then f /^ (k2 -' 1) = {} by RFINSEQ:def 1;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f ; :: thesis: verum
end;
end;
end;
suppose len (f /^ (k2 -' 1)) > (k1 -' k2) + 1 ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
then A11: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len (f /^ (k2 -' 1)) by FINSEQ_1:59;
per cases ( k2 -' 1 <= len f or not k2 -' 1 <= len f ) ;
suppose k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
then A12: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= (len f) - (k2 -' 1) by A11, RFINSEQ:def 1;
(len f) - (k2 -' 1) <= (len f) - 0 by XREAL_1:10;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f by A12, XXREAL_0:2; :: thesis: verum
end;
suppose not k2 -' 1 <= len f ; :: thesis: len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f
then f /^ (k2 -' 1) = {} by RFINSEQ:def 1;
hence len ((f /^ (k2 -' 1)) | ((k1 -' k2) + 1)) <= len f ; :: thesis: verum
end;
end;
end;
end;
end;
hence len (mid (f,k1,k2)) <= len f by A7, FINSEQ_5:def 3; :: thesis: verum
end;
end;