Skip to main content
deleted 34 characters in body
Source Link
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are truehold at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ Throughout this ball we now have, much more simply, $$ \phi(x) \iff \bigvee_{i\in I} (p_i(x)=0), $$ where $I$ is the set of indices for which $p_i(a)=0$. This is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$. This is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where hold at the point $a$.

Throughout this ball we now have, much more simply, $$ \phi(x) \iff \bigvee_{i\in I} (p_i(x)=0), $$ where $I$ is the set of indices for which $p_i(a)=0$. This is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

added 150 characters in body
Source Link
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$. This is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$. This is because, in the cases where $p_i(a)=0$ holds, $q_{ij}(x)>0$ throughout the ball, but in the cases where it fails, $p_i(x)\neq 0$ throughout.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

added 2 characters in body
Source Link
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j f_j(x)\iff \sum_j f_j(x)^2>0$$\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j f_j(x)\iff \sum_j f_j(x)^2>0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Answer using the classical theorem

My bounded predicates define open subspaces of $\mathbb R$. The one difficult case is the universal quantifier over a bounded closed interval, but this may be derived from the Heine–Borel theorem.

On the other hand, these subspaces are semi-algebraic. For this we need to replace bounded quantifiers with unbounded ones, but $$\forall x:[a,b].\phi x\iff\forall x:{\mathbb R}.x<a\lor\phi x\lor b<x$$ $$\exists x:[a,b].\phi x\iff\exists x:{\mathbb R}.a\leq x\land\phi x\land x\leq b.$$

The classical Tarski-Seidenberg eliminates quantifiers from semi-algebraic predicates, but this may be at the cost of introducing ${=},{\leq},{\geq},{\lnot},{\Rightarrow}$.

First we eliminate ${\lnot}$ and ${\Rightarrow}$ in the usual classical way, rewrite ${\neq},{\leq},{\geq}$ as disjunctions of ${=}$ and ${>}$ and put the expression in disjunctive normal form.

(From now on, $x$ and $a$ are vectors.)

There is one further easy transformation, $\bigwedge_j (f_j(x)=0)\iff (\sum_j f_j(x)^2)=0$, and in particular the empty conjunction ($\top$) is $0(x)=0$.

So the predicate is now $$ \phi(x) \quad\equiv\quad \bigvee_i (p_i(x)=0 \ \land\ \bigwedge_j q_{ij}> 0). $$ Suppose that $a$ satisfies this.

By hypothesis $\phi$ defines an open subset, so $\phi$ is true thoughout some ball around $a$.

The finitely many polynomial inequalities $p_i(x)\neq 0$ and $q_{ij}(x)>0$ also define open subspaces, so choose this ball small enough to make them true thoughout the ball in all the cases where they are true according as they are true at the point $a$.

$$ \forall x.|x-a|<\epsilon \quad \Longrightarrow\quad \phi(x) \iff \bigvee_{i\in I} p_i(x)=0, $$ where $I$ is the set of indices for which $p_i(a)=0$.

This means that we have an open ball that is covered by the solutions of finitely many polynomial equations.

This can only happen if one of those polynomials is identically zero.

I would be grateful if someone with better intuition about (semi-)algebraic geometry could check this.

Attempt at a direct constructive proof

If the polynomial is of degree $\leq6$ in the quantified variable then there are formulae (in the other variables) for the zeroes of its second derivative.

These (and the endpoints) provide the extreme values, so substituting them eliminates the quantifier in favour of finite disjunctions or conjunctions.

This is at the cost of using square and cube roots, but I believe that there are old ways of eliminating these too.

Is there a way of doing this without the formulae for the roots or for higher-degree polynomials?

Source Link
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58
Loading