Damped Pendulum, Bounded solutions Consider the following system of differential equations
$$\begin{cases} x' = y \\
y' = -w^2 \sin(x)-ay
\end{cases}$$
with $w > 0 $ and $ a \ge 0$. I know that $V(x,y) = \frac{y^2}{2} + w^2(1-\cos x) $ is a strict Ljapunov function.

I am looking for a proof that every solution $(x,y)$ to the initial value $(x_0,y_0) \in \mathbb{R}^2$ is bounded for $ t \ge 0$.

One can show that $y$ is bounded using a proof by contradiction and the properties of the Ljapunov function. Further I know one way to prove that $x$ is bounded but this one is very long and counterintuitive. (cf.  Gewöhnliche Differentialgleichungen und dynamischen Systeme written by Prüss/Wilke)
Therefore I ask you to provide another short/beautiful proof of the above claim. 
To clarify: I am looking for an rigorous proof and not an physical idea which somehow shows the boundedness of solutions. While these are the differential equations for the damped pendulum. It is nowhere stated that one of this variables is only an angle. So $(x,y)$ are both in $\mathbb{R}^2$ and I want them to be bounded as such. 
 A: Let $x=x(t)$, $y=y(t)$ be a solution satisfying the given initial conditions $x(0)=x_0$, $y(0)=y_0$. Let
$$ V(t)=\frac{y(t)^2}{2}+w^2(1-\cos x(t)).$$
Now for all $t$ it holds that $V(t)\ge 0$ and $V'(t)=-ay(t)^2\le 0$. So, it follows that the $V(t)$ has a limit at infinity. Let $W=\lim_{t\to\infty}V(t)$.
Assume toward a contradiction that $x(t)$ is unbounded. It follows that $\cos(x(t))=-1$ for arbitrarily large $t$, and therefore $W\ge 2w^2$. Thus
$$ y(t)^2=2(V(t)-w^2(1-\cos x(t)))\ge 2w^2(1+\cos x(t)).$$
Consider now $t_1$ such that $\cos x(t_1)=1$ and $V(t_1)<W+2aw$.
Let $t_2$ be the smallest $t$ such that $t>t_1$ and $\cos x(t)=0$. Then $|y(t)|\ge\sqrt{2}w$ for $t\in[t_1,t_2]$, and so
$$V(t_1)-V(t_2)=a\int_{t_1}^{t_2}y(t)^2\,dt\ge\sqrt{2}aw\int_{t_1}^{t_2}|y(t)|\,dt\ge\frac{\sqrt{2}\pi aw}{2}>2aw,$$
and consequently $V(t_2)<V(t_1)-2aw<W$, contradicting the choice of $W$.
Thus, $x(t)$ is bounded.
A: I will prove a more general proposition with a relaxed premise and a sharper conclusion.

Proposition: $H_1(x)\in C^1(R)$. $h_2(y)\in C(R)$ is a strictly increasing function, and $h_2(0)=0$. $\lim\sup_{x\to\infty}H_1(x)>\lim\inf_{x\to\infty} H_1(x)\ge 0=H_1(0)$. $\lim\sup_{x\to-\infty}H_1(x)>\lim\inf_{x\to-\infty} H_1(x)\ge 0=H_1(0)$. $h_1(x):=H_1'(x)$ is bounded. $g$ is a continuous strictly increasing function defined on all $R$ with $g(0)=0$. Consider
$$\begin{cases} 
x' = h_2(y) \\ 
y' = -h_1(x)-g(y) 
\end{cases}$$
  For any initial condition, as $t\to\infty$, $y(t)\to0$; $x(t)$ is bounded and its set of accumulation points is nonempty, contained in the set of stationary points of $H_1(x)$ ($h_1(x)=0$) and is in fact a closed interval. If we further assume $h_1(x)=0$ only at isolated points,  $x(t)$ to some stationary point of $H_1(x)$ where $X$ is the set of stationary points of $H_1$.

We need the following lemma.

Lemma: $f\in C(R)$, $f(0)=0$. $f(y)$ is positive away from $y=0$. $y:R^+\to R$ is differentiable and $|y'(t)|<M$. 
  $$\int_0^\infty f(y(t))<\infty.$$
  Then $y(t)\to 0$ as $t\to\infty$.

Proof of the Lemma:  Suppose the contrary. Without loss of generality, assume $y(t)$ has a positive accumulation point. That is $\exists y_0>0$ and $\{t_n\}_{n=1}^\infty$ where $t_{n+1}-t_n\ge1  \ni |y(t_n)-4y_0|< y_0$. Since $y'(t)$ is bounded by $M$, $\forall n\in\mathbf N$ and $|t-t_n|<\frac{y_0}M$, we have $|y(t)-y(t_n)|< y_0$ implying $|y(t)-4y_0|< 2y_0$. Let $T:= \bigcup_n \big\{t\,\big|\,|t-t_n|< \frac{y_0}M\big\}$. $y(T)$ is contained in a compact set $Y:=\big\{y\,\big|\,|y-4y_0|\le2y_0\big\}$. The property of $f(y)$ implies that $f(y(T))>f_0:=\min_Yf(Y)>0$. 
Let $l=\min\big(\frac12,\frac{y_0}M\big)$ Consider the integration of $f(y(t))$ over intervals $(t_n-l,t_n+l)$ over all $n$ which are all disjoint. We have
$$\int_0^\infty f(y(t))dt>\sum_{n=1}^\infty f_0 2l=\infty.$$
We have a contradiction. 
Therefore, $y(t)\to0$ as $t\to\infty$, as desired.
QED

Proof of the Proposition: Define $H_2(y):=\int_0^y h_2(u)\,du$, $H(x,y) := H_1(x) + H_2(y)$ and $H(t):=H(x(t),y(t))$. We have
$$\dot H(t):=\frac{d}{dt}H(t)=-h_2(y(t))g(y(t)).$$
$H(x,y)\ge0$ for all $(x,y)$ and $\dot H<0, \forall y\ne0$ and $\dot H(t=0)=0$. So $H$ is a Lyapunov function. $H(t)$ decreases. Thus, together with $H_1$ being nonnegative,
$H_2(y(t))=H(t)-H_1(x(t))\le H(0),\,\forall t\ge0$. Because $H_2(-\infty)=H_2(\infty)=\infty$, $H_2(y)$ is bounded implies $|y|$ is bounded. Since $|g(y)|$ is continuous it is also bounded on the compact set defined by the bounded $|y|$. $|y'(t)|\le |H_1'(x(t))|+|g(y(t))|$ is also bounded since both terms on the right hand side are bounded. 
Now, since $H(t)$ is non-increasing is bounded from below by $0$,
$$H(0)-H(\infty)=\int_0^\infty h_2(y(s))g(y(s))\,ds$$
is convergent. $h_2(y)g(y)$ strictly increases on $[0,\infty)$ and strictly decreases on $(-\infty,0]$, $h_2(y=0)g(y=0)=0$, since both $h_2(y)$ and $g(y)$ satisfy these conditions. Recall $|y'(t)|$ is bounded. As $t\to\infty$, by Lemma, $y(t)\to0$, consequently $H_2(y(t))\to0^+$ and $h_2(y(t))\to0$. 
$H_1(x(t))$ converges as $t\to\infty$, since
$H(t=\infty)=H_1(x(t=\infty))+H_2(y(t=\infty))=H_1(x(t=\infty))$. $x(t)$ is bounded. Otherwise, since $H_1$ has distinct $\lim\sup$ and $\lim\inf$, $H_1(x(t))$ assumes all values of a nonempty interval and thus diverges as $t\to\infty$. We show $x(t)$ converges as $t\to\infty$ by contradiction. Suppose $x(t)$ has two distinct accumulation points $x_1 < x_2$. As $x(t)$ is continuous, it assumes all values in $(x_1,x_2)$ as $t\to\infty$. We have two cases. We show both are impossible.
1) $H_1(x_1)\ne H_1(x_2)$. $H_1(x(t))$ diverges. 
2) $H_1(x_1)=H_2(x_2)$. That would mean $H_1(x)=H_1(x_1), \forall x\in [x_1,x_2]$. Otherwise, $\exists x_3\in (x_1,x_2)\ni H_1(x_3)\ne H_1(x_1)$ and as $x(t)$ is continuous, it assumes $x_3$ infinite times and $H_1(x(t))$ assumes $H_1(x_3)$ infinite times, as $t\to\infty$. That gives at least two distinct accumulation points to $H_1(x(t))$ making $H_1(x(t))$ diverge. However, that would entail $h_1(x)=0,\,\forall x\in[x_1,x_2]$ violating the premise that $h_1$ assumes $0$ only at isolated points. 
Both cases lead to contradiction. So $x(t)$ converges as claimed.
Finally, we show the limit $x_\infty$ of $x(t)$ is a stationary point of $H_1$ or $h_1(x_\infty)=0$. Suppose the contrary that $h_1(x_\infty)\ne0$. Assume without loss of generality that $h_1(x_infty)>0$. For an arbitrarily small $\epsilon>0$ and sufficiently large $T$, we have $y(T)>-\epsilon$, and $\forall t>T$, the equation of motion gives
$$y'(t)=h_1(x(t))-g(y(t))>(h_1(x_\infty)-\epsilon)-\epsilon>0,$$
implying
$$y(t)>-\epsilon+(h_1(x_\infty)-2\epsilon)(t-T)$$
making $y(t)\to\infty$ as $t\to\infty$, a contradiction.
So far, we have proved all the results we set out to prove.
QED
A: The derivative of Lyapunov function cannot decrease for ever unless its limit is zero .
$$\dot V(x,y)=y\dot y+w^2 \dot x \sin x$$
$$=y(-w^2\sin x-a y)+w^2 y\sin x =-a y^2$$
Therefore, $y(t=\infty)=0$. 
In addition, as Lyapunov function is monotonic, at $t=\infty$,
$$V(x,y)=\frac12y^2+w^2(1-\cos x)=0$$
or
$$(1-\cos x)=0$$
This means 
$$\exists k \in \mathbb{Z},\quad  x(t=\infty)=2k\pi$$
As $\dot x$ is bounded, $x$ cannot jump. Hence, $x$ is bounded.
A: The local LaSalle's invariant principle, stated for example here and here, guarantees $\lim_{t\to\infty}(x,y)=(k\pi,0)$ for some integer $k$ for an initial condition in some neighbourhood of $0$. The condition for the global version of the LaSalle's invariant principle is not satisfied. The global boundedness of the solution is proved by Taneli Huuskonen and me, Hans (in another answer that is more general and sharper).
In fact the wikipedia article gives precisely this very problem as an example of the application of the principle in the local sense. $0=\dot V(x,y)=-ay^2 \bigwedge a>0\Longleftrightarrow 0=y=\dot x$. The complete trajectory within should satisfy $0=\dot y=-w^2\sin(x)$ the solution set $x(t)$ of which is $\{k\pi|\,k\in\mathbf Z\}$. 
In addition we have the positive definiteness of the Lyapunov function that $V(x,y)>0,\, \forall (x,y)\neq 0$. In fact so long as $\dot V\le0$ in a compact neighbourhood $A$ of the fixed point (cf. the second reference above), in this case, $(k\pi,0)$, $\lim_{t\to\infty}x(t)=k\pi$ for some integer $k$, for all initial values$(x,y)\in A$.
