counter k;
abstract node n[k];
pointer x->n;
abstract node n2[k];
succ n=n2;
succ n2=NULL;