Ops delete:2 cons:2 nil:0 A:0 B:0 ite:3 true:0 false:0 eq:2 Const A B nil cons true false Vars X Y Z TRS R eq(A,A) -> true eq(A,B) -> false eq(B,A) -> false eq(B,B) -> true delete(X,nil) -> nil delete(X,cons(Y,Z)) -> ite(eq(X,Y),delete(X,Z),cons(Y,delete(X,Z))) ite(true,X,Y) -> X ite(false,X,Y) -> Y SRegexp A0 delete(A,[cons((A|B),*|nil)]) Automaton TC States qe ql qb Final States qe ql qb Transitions A -> qe B -> qe nil -> ql cons(qe,ql) -> ql true -> qb false -> qb Patterns cons(A,_)