pvs specifications of order crossover

hello..

I am trying to write order crossover specifications in pvs . i have done with cut, head and tail functions specifications now i need a delete function which delete a sequence to another sequence

here is a fuction that del

del_element(a:T, p):RECURSIVE finseq[T]=

(# length:= p`length,

seq := LAMBDA (i:below[p`length]):(if p`seq(i) =a THEN empty_seq[T]

ELSE del_element(a,p) ENDIF)#)

MEASURE p`length

delete all occurrences of element a. can any body guide me what changes it acquires to delete n element recursively with correct syntax.