Why is there a unique solution to the frog puzzle? I'm pretty sure this is a trivial question but eh...
The Frog Puzzle is a famous 8th-grade problem (playable here):

$3$ red frogs and $3$ blue frogs are sitting on lily pads, with a spare lily pad in between them. 
Frogs can slide onto adjacent lily pads or  jump over a frog; frogs can't jump over more than one frog. Frogs can't move backwards.
Can we swap the red frogs with the blue frogs?

It's fairly easy to solve, even for $n$ red frogs and $m$ blue frogs. But I find it very hard to "mathematize" it : should we see the "pond" as an element of $(\mathbb{Z}_3)^7$ ? Then how can we describe the possible moves ?
Unable to translate this into familiar mathematical terms, I'm thereby very puzzled by this... puzzle. In particular, I can't seem to find why is there always a solution, and only one (up to symetry of course), for any number of frogs. I've tried to make it work in Scylab but I'm very rusty in programmation...
All I've managed to prove is that a frog can't jump over a frog of the same color but I'm not sure this will lead somewhere.
Bonus question : is the number of solution equal to the number of empty lily pads?
 A: I have been unable to come up with anything resembling a formal proof, but I have noticed several things that may help someone do so.


*

*At each step, you must choose between moving a frog of color $A$ or color $B$. (Fairly obvious, I know, but two frogs of the same color are never both moveable.)


Therefore, let $a$ denote moving the only moveable frog of color $A$ (moving to the right), and let $b$ denote moving the only moveable frog of color $B$ (moving to the left).


*

*The number of total moves used in any solution is fixed, and equals $mn + m+n$

*There are exactly $2$ solutions to any frog problem, as the OP noted

*If, at any point, two frogs of the same color are in adjacent positions, there is a frog of the other color ahead of them, and the open lilypad is behind them, you have lost.


*

*Losing case #1: ... $A$ ... $BB$ ... $\_$ ...

*Losing case #2: ... $\_$ ... $AA$ ... $B$ ...


*Using this, it's impossible to ever move $aa$ (if there is a $B$ frog to the right), unless one of the $A$ frogs jumps a $B$ frog.


*

*For example, you cannot start the game with $aa$ or $bb$.

*If you start with $a$, your next move must be $b$. You can do $b$ or $bb$, but $bbb$ would result in the (losing case #1) arrangement $AAA$ ... $BABB\_$ ... $BBB$.


*Extending this, if you have moved $k$ of your $A$-colored frogs, there are at most $k$ jumps possible for the $B$ frogs, and you cannot make more than $(k+1)$ $b$-type moves consecutively.

*Stepping through the game case by case, it's pretty easy to manually show that there's one possible choice for the next sequence of moves. (I have no proof for this, but I have not yet found a counterexample).


*

*Start: (due to symmetry, two possible moves)
\begin{gather}
A...AA\_BB...B\\
aa = \mathrm{lose}\\
bb = \mathrm{lose}\\
ab = \mathrm{okay}\\
ba = \mathrm{okay}
\end{gather}

*Suppose we chose to move $ab$
\begin{gather}
A...ABA\_B...B\\
aa = \mathrm{lose}\\
bb = \mathrm{lose}\\
ab = \mathrm{lose}\\
ba = \mathrm{okay}
\end{gather}

*We have now moved $abba$
\begin{gather}
A...AAB\_BA...B\\
b = \mathrm{lose}\\
aaa = \mathrm{lose}\\
aab = \mathrm{okay}\\
aba = \mathrm{lose}\\
abb = \mathrm{lose}
\end{gather}

*We have now moved $abbaaab$
\begin{gather}
A...BA\_ABA...B\\
a = \mathrm{lose}\\
ba = \mathrm{lose}\\
bb = \mathrm{okay}
\end{gather}



You get the idea by now, but it shouldn't be too difficult to write an automated prover for small $m$ and $n$.


*

*Various Example Solutions:


*

*$3$ vs $3$: $abbaaabbbaaabba$

*$4$ vs $3$: $abbaaabbbaaaabbbaab$

*$5$ vs $3$: $abbaaabbbaaaaabbbaaabba$

*$6$ vs $3$: $abbaaabbbaaaaabbbaaaabbbaab$

*$7$ vs $3$: $abbaaabbbaaaaabbbaaaaabbbaaabba$


A: When there is only one empty pad, Tim510's answer can be improved into an automatic algorithm predicting the (unique) next step from only looking two positions from the spare pad, left and right. I'll change his notation a little bit, denoting $R$ed frogs by $R$, $B$lue frogs by $B$ and the $S$pare lily pad by $S$.
For convenience, we can add two blue frogs on the left and two red frogs on the right, 
(as though they were "already successfully placed" from a challenge with more frogs)
this way there will always be at least two characters left and right to S.
As noticed by Tim510, the patterns $RBB(...)S$, $S(...)RRB$ cannot appear  at any time in any solution. In particular, $RBBS$ and $SRRB$ are forbidden subwords. It follows that $RBSRB$ is also a forbidden subword, since it leads in one move to either of the two forbidden subwords above. Here goes our algorithm :
$$
\begin{array}{rclcl}
RR & S & RR &:& \text{unreachable state} \\
RR & S & RB &\to& RRBRS \\
RR & S & BR &\to& RSRBR \text{ ( nontrivial case, see explanation below )} \\
RR & S & BB &:& \text{initial state, choose } RSRBB \text{ or } RRBSB \\
 &  &  & &  \\
RB & S & RR &\to& SBRRR \\
RB & S & RB &:& \text{forbidden state} \\
RB & S & BR &\to& SBRBR \\
RB & S & BB &\to& SBRBB \\
 &  &  & &  \\
BR & S & RR &\to& BSRRR  \\
BR & S & RB &\to &BRBRS  \\
BR & S & BR &:& \text{unreachable state}  \\
BR & S & BB &\to& BRBSB \text{ ( nontrivial case, see explanation below )} \\
&  &  & &  \\
BB & S & RR &:& \text{final state} \\
BB & S & RB &\to& BBBRS \\
BB & S & BR &\to& BBBSR \\
BB & S & BB &:& \text{unreachable state} \\
\end{array}
$$
Explanation on the nontrivial cases. The reader might wonder why  we wrote
$RRSBR \to RSRBR$, since (a priori) nothing in our rules prohibits us from 
doing $RRSBR \to RRBSR$. If we look at the entries in our algorithm, we see that
an $RRSBR$ state can only come from one of
$$
\begin{array}{rclcl}
RRRB & S & RR &\to& RRSBRRR \\
RRRB & S & BR &\to& RRSBRBR \\
RRRB & S & BB &\to& RRSBRBB \\
\end{array}
$$
In the last two cases, the forbidden subword $RBSRB$ leaves us no choice as to the next move. And the first case is in fact unreachable, since it is easy to show by induction that any subword of the form $R^{x}BSR^{y}$ or $R^{x}SBR^{y}$ with $x,y\geq 2$ is unreachable. 
The other nontrivial case is explained similarly.  
A: Let red and blue flog, $1$ and $2$, and empty pad is $0$, at first we move every $1$s left.
$$\\11・・・100・・・022・・・2$$
$→00・・・011・・・1022・・・2\tag 1$
Now, we prove [$11・・・1022・・・2$] can be [$01212・・・12$]. 
One previous step is $10212・・・12$. We move every $1$s left, $$11212・・・121202$$ Next, move every $2$s right, $$11「01212・・・1212」22$$ Since $「」$ is same with first sequence, repeating this operation, then we get first term $(1)$ [$11・・・1022・・・2$]. Therefore we could say the question has definitely one solution.
Also If one frog can jump same color, it generates a sequence $1220$ or $0112$. 
These cases can never go advance anymore.   About bonus question, I think it become recurrence sequence, though.
If the numbers of red and blue frogs and empty pad are $n,m,l$, numbers of jump move is $nm$, side move is $l(n+m)$. Because left frogs meet right flog $nm$ times. I got this by a bit borrowing from a Japanese site. 
A: Well I guess there is no other way than induction. Let A go to the right, B go to the left. We say that the frogs are jumping only in one direction unless a configuration of the form $$\{..XX\}\_\{BABABA\}..AB\{YY..\}$$ or its mirror reverse are reached and the direction of jumping is reversed.
The base: There are actually two possibilities for the first move. So lets consider a case when the first move is already done. Obviously we have a configuration of the form described above, only the part in the brackets has zero length (that's why it is in brackets, that implicates that part need not to be there at all).
Suppose it is true at some point during the game
Then we inevitable arrive to this kind of state again. Since in this configuration, only  one of the frogs can move, and it is the X in case X=A ( otherwise we end up in a configuration AB_AB, and either B jumps to it or A jumps to it, in both cases you will be unable to finish the game). Or in case X=A A jumps over A, but that will again be a failure. Or for X=B or the $\{..XX\}$ not being there, just and only B moves to it, since there is simply no other choice. In both cases we end up in a configuration:
$$\{...XXX\}\_ABABA...AB\{YYY...\}$$
Here it is obvious that the frogs always have to jump up until the $B\{YYY...\}$ is reached, otherwise a A ends up "barriered" unable to get where it needs, because the free pod is on the left from it and can't end up on the right unless the frog moves, which is impossible in the state _BBA. So they are stuck. And it is going to arrive to the state $$\{...XXX\}AB...BABA\_\{YY...\}$$ which is the aforementioned mirror state, that will lead back to the preivous kind of state based on the same argumentation.
Since no other configuration is possible, we are always going to have only one choice that will bring us closer to the end. We either always are jumping in one direction or we must move with the frog on the end(start) of the line of frogs, that has not moved yet or is not going to move anymore. So we always have only and just one option how to get closer to the successful end.
Not mathematics, rather exhaustive argumentation, but sometimes there are no other ways to prove things.
EDIT: There is not a single solution if one set of frogs is at most the same cardinality as the number of free pods (in case the free pods are in the middle). So for instance one free pod and one frog against  $m$ frogs actually has $2^m$ solutions.
A: I have only worked with the 3x3 puzzle.  One interesting thing that I noticed is that the last position is the mirror image of the last (obviously), and the second position is the mirror image of the second to last, and so on.  In the middle, there is a transition from a position to its mirror image.  If you have been keeping track of your moves, once you reach this middle position, you can now solve the rest of the problem
