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