Unrestricted grammar for the language of strings whose length is not $2^n$ The following exercise is inspired by an old exam question (note that this is not the question):

Let us define a single-letter alphabet $\Sigma = \{a\}$ and the language $L = \{ w \in \Sigma^*: |w| = 2^n, n \in \mathbb Z_+\}$. (In other words, $L = \{a^2, a^4, a^8, \ldots \}$.) What is an unrestricted grammar for $L$?

I thought of a solution using binary number representation. Consider the grammar:

$S \rightarrow 10TaX$ 
$T \rightarrow 0T | \epsilon$ 
$0a \rightarrow aa0$ 
$0X \rightarrow X$ 
$1a \rightarrow a1$ 
$1X \rightarrow \epsilon$ 

$\epsilon$ signifies the empty string. Using the first two production rules, we can produce a string of the type $10^naX$, for example $100aX$. One route here to get rid of the non-terminal symbols is $100aX \Rightarrow 10aa0X \Rightarrow 1aa0a0X \Rightarrow 1aaaa00X \Rightarrow 1aaaa0X$ $\Rightarrow 1aaaaX \Rightarrow \ldots \Rightarrow aaaa1X \Rightarrow aaaa = a^4$. 

Assuming that this solution is correct, one interesting thing about it is that by modifying the third production rule to $0a \rightarrow a^k0$ one can get a restriction-free grammar for strings of length $k^n$ instead. But maybe there is a cleaner solution, so I am interested in seeing other examples of unrestricted grammars for the language. 

However, here comes the actual question: the existence of an unrestricted grammar for $L$ only proves that it is recursively enumerable. Therefore I would like to ask for an unrestricted grammar of $\overline{L}$ (then we have one proof that $L$ is a Turing-decidable language).

Edit: In case the question here is unclear, please read the discussion in the comments.
Your method is correct to generate $L$. But if you change the rule to $0a \to a^k0$ then the language you generate is $L^{'}=\{a^k,a^{k^2},a^{k^3}....\}$ ( $k &gt;2$) .
You can show that language $L$ is indeed decidable. One way is to give an algorithm that halts on every input in $\sum^{*}$ and gives the correct result. Following is the approach

(1) If the input is empty reject. 
(2) If not empty , check if there are even number of 'a' or odd. If only one 'a' is there accept. If odd 'a' ( > 1 ) are there reject. 
(3) If even 'a' are there, go back to starting of input and cross off alternate 'a' from beginning to end of input. Go back to step (2).
The algorithm accepts the string $a$ in addition. You can always modify the above algorithm, keeping a special check that if the input is 'a' reject.