The Equational Theory of < N, 0, 1, +, ×, uparrow > Is Decidable, but Not Finitely Axiomatisable. - Roberto Di Cosmo; Thomas Dufour (LPAR, 2004)