Finite equational basis for trigonometric identities

Question

Consider the structure $(\mathbb{R}, +,-,*,\sin,\cos,0,1)$, where $+$ is addition, $-$ is additive inverse, $*$ is multiplication, $\sin$ is the sine function, and $\cos$ is the cosine function.
Is there a finite basis for the equational identities of that structure? In fact, I conjecture that, in addition to the axioms of a commutative ring, all you need are that $\sin(0)=0$, $\cos(0)=1$, $\sin(-x)=-\sin(x)$,$\cos(-x)=\cos(x)$, the sine of sum formula, the cosine of sum formula, and $\sin^2(x)+\cos^2(x)=1$.

Answer 1

I don't know the answer to this question, but it reminds me of a lemma I read in

Equations on real intervals
Walter Taylor
Algebra universalis 55 (2006) 409-456.

Lemma 5.2. (Expanded, so that it makes sense here.)
Suppose that $\mathbb R$ is the real line considered as a topological space. Suppose also that
$$ \mathbb A = \langle \mathbb R; \oplus, \odot, \ominus, \stackrel{\cdot}{0}, \stackrel{\cdot}{1}, c(x), s(x), \lambda(x)\rangle $$ is a topological algebra (meaning all operations are continuous) which satisfies the following identities:

identities saying that $ \langle \mathbb R; \oplus, \odot, \ominus, \stackrel{\cdot}{0}, \stackrel{\cdot}{1}\rangle $ is a commutative ring,

$c(x + y) = (c(x) · c(y)) − (s(x) · s(y))$,

$s(x + y) = (c(x) · s(y)) + (s(x) · c(y))$,

$c(\stackrel{\cdot}{0}) = \stackrel{\cdot}{1}$, $c(\stackrel{\cdot}{1}) = \stackrel{\cdot}{0}$, $s(\stackrel{\cdot}{1}) = \stackrel{\cdot}{1}$,

$c(s(x)) = (\lambda(x))^2$.

Let $\mathbb A^-$ be the topological algebra $\mathbb A$ with $\lambda(x)$ deleted from the signature.

There is a unique self-homeomorphism $\phi:\mathbb R\to \mathbb R$ that is an algebra isomorphism of $\mathbb A^-$ onto the algebra

$$ \mathbb B = \left\langle \mathbb R; +, \cdot, -, 0, 1, \cos\left(\frac{\pi}{2}x\right), \sin\left(\frac{\pi}{2}x\right)\right\rangle. $$