@Carl Love Thanks. I suspect this is because Maple is too "smart" to ignore argument checking when not all parameters are used, but I'm more inclined to believe this is simply a hidden bug. 

@Carl Love Many thanks.

There exists another problem: I think that 

f := overload([proc(a::seq(Non(2)), b::2, c::seq(Non(3)), d::3)
	option overload:
	[a, b, c, d, _rest]
end, ERROR]):

is equivalent to 

g := overload([proc(a::seq(Non(2)), b::2, c::seq(Non(3)), d::3)
	option overload:
	[args]
end, ERROR]):

yet g(4, 3, 2, 1); does not work as desired. It seems like I have to write out the parameters explicitly (even if they will never be used in the procedure), but I cannot find any mention of this in the help page. Is this limitation documented?
Currently, I have to write something like 

overload([proc(a::seq(Non(2)), b::2, c::seq(Non(3)), d::3)
    options overload;
    'a, b, c, d': true
end, unapply(false)]);

where the italicized part makes no sense ….

@acer & @Thomas Richard I believe that if certain statements could be invoked in function call form, there would be no dilemma about the ending delimiters.
For instance, instead of using

or

I can simply use 

or

(or even a (flat) piecewise function) and now I don't need to worry about whether to write fi or end if. However, I don't why Maple doesn't support compound expressions (while supporting expression sequences), which makes the use of the function form largely useless (for example, I cannot use something like `if`(a, b; c, d; e) …). 

@Thomas Richard Thanks. Long ending delimiters are often more readable in nested proc/module/try/use, but I think it's better to keep ending delimiters of proc/module/try/use consistent when setting interface('longdelim' = false). 
(Another inconsistency is that while some other statements can be embedded as an expression or within an expression (probably by enclosing it in parentheses). the use statement can still only be used as a stand-alone statement.) 

@Carl Love Thanks. This workaround is simple but really effective. If this potential bug (?) can be fixed in the future, it will be more convenient to compress large numbers of cumbersome conditional cases and awkward looping constructs into a few succinct and elegant lines of pattern specifications (although pattern matching does not seem to be a Maple idiom …).  

The default method seems to be good enough in general cases 

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'mpqs')),n=16..64,8);
      0.694, 0.785, 1.065, 3.407, 10.953, 47.328, 146.828

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'morrbril')),n=16..64,8);
       0.763, 0.867, 1.027, 3.829, 9.016, 25.598, 48.291

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'squfof')),n=16..64,8);
      0.685, 0.901, 1.200, 3.463, 11.968, 68.843, 363.656

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'pollard')),n=16..64,8);
       0.760, 0.809, 1.106, 3.679, 9.265, 30.781, 129.406

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'lenstra')),n=16..64,8);
      0.674, 0.944, 1.147, 5.713, 28.875, 111.687, 322.093

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'mpqsmixed')),n=16..64,8);
        0.671, 0.793, 1.028, 3.128, 5.263, 8.670, 33.047

forget(ifactor):seq(time[real](ifactor(2**(n-1)+~[$1e4],'mixed')),n=16..64,8);
       0.677, 0.806, 1.085, 3.575, 8.888, 23.312, 46.424

though it still seems a bit slow (compared to some other computer algebra systems) ….

@Thomas Richard Thanks. Anyway, the default font of the code editor window seems to be more recognizable. 

@Thomas Richard What is the default font used by the code editor? The default font used by the code edit region seems to be Courier New, while the default font used by the code editor window (including the Startup Code region and certain component properties editor) appears to be Consolas. May you confirm this? (BTW, why are the two not consistent?)

Code edit region: . 
Code editor window: . 

@nm Thanks. I noticed another weird problem: 

MmaTranslator:-FromMma("!a->b//@c");
 = 
                                 (1/2)
                         a = c(b)     

MmaTranslator:-FromMma("!!a->b//d");
 = 
                        `read`(a->b//d)

However, the output should be  and  instead of  and . 
It seems that I have to always use the less readable FullForm as input to the translator. 

@Samir Khan Many thanks! I hope this is useful in some cases.

@vv It's in `convert/to_special_function`, yet I don't think it's very useful in practice. 

@acer Thank you for your reminder. I forgot that I had changed the default “output display” option before. 
I believe that Maple has an internal function to appropriately abbreviate repeated common subexpressions in large output, yet I cannot find it. (As you said, the codegen:-optimize often over-optimizes common subexpressions, which is not the default behavior of "subexpression labeling".) 

@acer Sometimes the documentation seems to tend to describe those subtle things too briefly. Anyway, thanks for your valuable comments! 

@acer Sorry for the late reply. I try to find a simpler example, yet ended up with nothing. 

Well, here is the nested integral: 

expr := (x + Pi/2) - (Pi/(2*sqrt(3))*sin(x) + Pi/2*cos(x) + 2*x*sin(x/2)):

simplify(combine(1/4*sin(x)*int(1/cos(x1/2)**2*int(cos(x2/2)**2/sin(x2/2)**3*int(sin(x3/2)/(1 + sin(x3/2))*int((1 + sin(x4/2))*(2*sin(x4/2) - 1) + x4/2*(cos(x4/2) + sin(x4)), x4 = 0 .. x3), x3 = 0 .. x2), x2 = x1 .. Pi), x1 = Pi/3 .. x)) - expr) assuming RealRange(Open(Pi/3), Open(Pi));
simplify(combine(1/4*sin(x)*int(1/cos(x/2)**2*int(cos(x/2)**2/sin(x/2)**3*int(sin(x/2)/(1 + sin(x/2))*int((1 + sin(x/2))*(2*sin(x/2) - 1) + x/2*(cos(x/2) + sin(x)), x = 0 .. x), x = 0 .. x), x = x .. Pi), x = Pi/3 .. x)) - expr, assume = RealRange(Open(Pi/3), Open(Pi)));

Ideally, both results should be , but in fact, there will be several WARNING messages. 
At last, I have to use 

assume(Pi/3 < x, x < Pi):
simplify(combine(1/4*sin(x)*int(1/cos(x/2)**2*int(cos(x/2)**2/sin(x/2)**3*int(sin(x/2)/(1 + sin(x/2))*int((1 + sin(x/2))*(2*sin(x/2) - 1) + x/2*(cos(x/2) + sin(x)), x = 0 .. x), x = 0 .. x), x = x .. Pi), x = Pi/3 .. x)) - expr);

or 

undefine('x'): # free from `assume` 
`assuming`([simplify(combine(1/4*sin(x)*int(unapply(1/cos(x/2)**2*int(unapply(cos(x/2)**2/sin(x/2)**3*int(unapply(sin(x/2)/(1 + sin(x/2))*int(unapply((1 + sin(x/2))*(2*sin(x/2) - 1) + x/2*(cos(x/2) + sin(x)), x), 0 .. x), x), 0 .. x), x), x .. Pi), x), Pi/3 .. x)) - expr)], [Pi/3 < x, x < Pi]);

Besides, the help page states that 

while I notice that assuming does not appear to strictly distinguish between the bound variables (i.e., the variables of integration) and free variables (e.g., the limits of integration) in definite integrals whenever there exists a possibility of confusion like duplication of names: 

int(…*int(…*int(…*…, x = 0 .. x), x = 0 .. x), x = 0 .. x) assuming x::…:

In my opinion, setting global assumptions (using assume) may be convenient but also dangerous; perhaps the limitation that no assumptions are placed on the variables when using assuming can be disabled in future releases. 

@acer Thanks for your detailed reply. But there exists an addition problem. If int is not invoked when executing coulditbe (or is), why is the returned value below still true? 

trace(int):
coulditbe(x = 1) assuming 0 < x, x < 1;
 = 
                             false

int(RETURN(coulditbe(x = 1)), x = 0 .. x) assuming 0 < x, x < 1;
 = 
                              true

Although this is just confusing … in my opinion, as the int procedure has not been called yet, no renaming of the formal parameter (i.e., the red x in the first argument) is done at this time; nevertheless, the result is still true. Did I miss something again? 

(Note. My original problems originate from the calculation of nested integrals, but I think that the simplified version above is enough to illustrate the problem.)