On trace languages generated by (small) spiking neural P systems

In all proofs we try to keep the size of used systems (number of neurons, of rules in each neuron, of spikes consumed or removed by rules) as small as possible.