@Kitonum Yes, I know that the actual sequence is increasing. I am saying that your sequence of floating-point approximations produced at Digits = 10 is not monotonic, so that you can't say that the "accuracy falls". Actually, the accuracy varies erratically. 

@lham Sorry, I counted wrong. The equation has five variables (or one variable and four parameters), not four. So your question isn't as ridiculous as I first thought. The command to solve such equations is

solve(..., parametric);

But I wouldn't call it a "parametric equation"; I'd call it an "equation with parameters". Unfortunately, the above command only works for polynomial equations. See ?solve,parametric.

If you want help with MapleSim, it sure would be helpful if you selected MapleSim from the pull-down list in the editor. For the vast majority of us here who know Maple but know nothing of MapleSim, and who automatically try to interpret Questions in a Maple context, your question probably appears as utter jibberish. For example, the first thing that I think of seeing "CAD" is "Cylindrical Algebraic Decomposition". I only know to suspect MapleSim because I recognize your name as someone who often asks Questions about MapleSim.

@Kitonum 

Your sequence is not monotonic. It is just random floating-point effects because you have Digits set to 10, which isn't sufficient to accurately deal with your 11-digit integers.

@Kitonum 

That's fairly impressive considering that Maple's numeric summation capability is very weak. But that's no algorithm. I hope that that's not the way that Mathematica does it. The technique could be used to make a good guess at the answer, and a correct guess could be a substantial part of an analytic solution.

@lham 

So, you have one equation with four variables and no other conditions and you want to know what four-tuples satisfy the equation. Nothing can be said other than that they satisfy the equation; there's no other information. Perhaps the equation can be simplified a bit, and obviously it can be solved for phi[0], but that's all.

@Kanellopoulos 

No, to me it is not at all "obvious what will happen". It doesn't help that you don't show your Maple code for the above plots.

You say that you checked that the splines are solutions to the PDE system. How is it possible to do that without any variation in the t dimension? In other words, how did you approximate the derivatives with respect to t?

You say the orange curve is Maple and the blue curve is Mathematica. I admit to not knowing much about waves and PDEs, but the blue curve looks highly suspicious to me, and the orange curve looks reasonable. Why does the blue curve look more accurate to you?

The ::real is redundant---it is implied by the inequalities. So, the same bug is revealed by the simpler contrast of

is(a=b) assuming a^2=b^2, a>0, b>0;
is(a=b) assuming a^2=b^2, a>=0, b>=0;

I just point this out because it should make the bug easier to find/fix.

Now, given that Maple can correctly prove the second assertion above, shouldn't it be able to prove the following, which is much simpler (since it has half the number of variables) and is implied by the one above? Yet, it gets it wrong:

is(a=1) assuming a^2=1, a>=0;

     false

Weirder still, consider the negation of that assertion. One might guess that if Maple incorrectly answers false for an assertion, that it will answer true for the negation of that assertion. Yet

coulditbe(a <> 1) assuming a^2=1, a>=0;

     FAIL

The take-away from this is that it might be a good idea to also check the negation of an assertion. If one returns FAIL and the other doesn't, then the other can't be trusted.

@Kitonum Okay, you've changed my mind. I was thinking that the problem was in general too hard to be solved by an algorithm, but if Mathematica can do it, then Maple should be able to also.

@Mac Dude 

The with command is not needed to use a command in a module; any command in a module is accessible using :-. 

@Kitonum 

assume(n::posint);
limit(simplify(sin(convert(asympt(sqrt(n^2+n)*Pi, n, 1), polynom))^2), n= infinity);

     1

@tomleslie 

The Answer is satisfactory for me. In those cases where the sequence limit exists but the continuous doesn't, you need to use the positive integer property to do some sort of simplification. 

@Mac Dude The only significant difference between my original Answer and my update is an update to the second argument of subsindets, the one that selects the subexpressions by their type. In the Answer, this is specfunc({sum,Sum}), which selects any function whose name is sum or Sum. This is updated to 

And(specfunc({sum,Sum}), patfunc(`+`, anything))

which selects any functions whose name is sum or Sum And whose first argument is type `+` and whose remaining argument(s) can be anything.

@Mac Dude 

A problem with your DistSum is that it requires the overall expression to be of the specified type rather than looking for subexpressions of the specified type. Thus it won't work on your original example, which, indeed, isn't a sum or Sum. So, the thing to do is to fine tune the second argument to subsindets, which determines which subexpressions to work on. Here it is:

DistSum:= (xpr)->
     subsindets[flat](
          xpr,
          And(specfunc({sum,Sum}), patfunc(`+`, anything)),
          S-> map(op(0,S), op(S))
     )
:

Things like specfunc and patfunc are documented on the page ?type,structured---an extremely dense help page that I've been studying for years. I find it strange that with all the options on that page, there's not one that combines this use of specfunc and patfunc. Well, at least there's not one that I could spot. I can't figure them all out just from the documentation.

@MDD 

Okay, I'm glad that you already understand some of it. That means I can move faster through this. Let's consider the next line:

S:= solve({coeffs(expand(`+`((C*~L)[])), V)}, C),

especially the part at its heart, `+`((C*~L)[]).

Your question gave me the impression that you thought that the C* and the ~ were separate operations. No: The ~ preceded by almost any other binary operator makes the operator an elementwise operator (see ?elementwise). So C*~L multiplies the coefficients by the polynomials and produces a new list or set (it doesn't matter which in this case) containing the products.

Appending [] to a set or list extracts its underlying sequence of elements. Passing these to `+` adds them. So `+`((C*~L)[]) computes the dot product of C and L. The rest of the line expands this polynomial, extracts its coefficients with respect to V, sets them to 0, and solves this linear system for the variables C. The final result of this is a set S of the form

{c[1]=..., c[2]=..., ..., c[n]=...}.

Note that it's a homogenous and square linear system, so it always has a solution, which solve always finds.

Now let's consider the next line

F:= indets(rhs~(S), name) intersect C=~ 1;

First consider the rhs~(S). This applies rhs to every element of S, producing a new set containing just the right-hand sides of the equations in S. All the names in this set are extracted. This represents the free variables in the solution set S, which is why I call it F. From these free variables, I only want the linear coefficients, not the parameters; so, I intersect with C. 

Then I want to equate all these free variables to 1. My choice of 1 is arbitrary; I could use any nonzero value, because I want to return, if possible, a definite but nontrivial solution to the homogenous linear system. The elementwise operation A =~ 1 forms with every member of A an equation whose right side is 1. So the final result of this line is a set F of the form

{c[a]=1, c[b]=1, ...},

where the c[a], c[b], etc., represent only the free variables in S that are also in C.

Now let's consider the last line of CoeffsOfLinComb, which forms the return value:

eval([C[]], eval(S,F) union F) .

This takes the set C, forms the corresponding list [C[]], and evaluates each of these using 1 for all the free linear coefficients. The final result is a list of length nops(L) that contains only numbers and parameters.

Now let's consider the next procedure, PolyLinearCombo, and its first executable line

C:= CoeffsOfLinComb([f, F[]], V);

This takes the target polynomial f, makes it the first element of a list [f, F[]] and finds the linear coefficients, if any, that are needed to produce 0.

The final line is 

if C[1]=0 then (false, []) else (true, -C[2..] /~ C[1]) end if.

If the coefficient of f is 0, then f is linearly independent of F. Otherwise, the dependency coefficients are the coefficients of F divided by the negative of the coefficient of f. The elementwise operator /~ performs the division on all the other coefficients. The C[2..] means the sublist of C starting with the second element and going to the end.