Ops Node:3 Leaf:0 inc:1 zero:0 s:1 member:2 true:0 false:0
ite:3 or:2 eq:2

Const Node Leaf true false zero s

Vars U V X Y Z X1 X2 X3 

TRS R1

inc(Leaf) -> Leaf
inc(Node(X,Y,Z)) -> Node(s(X),inc(Y),inc(Z))
                                        
member(X,Leaf) -> false
member(X,Node(Y,Z,U)) -> ite(eq(X,Y),true,or(member(X,Z),member(X,U)))
eq(zero,zero) -> true
eq(zero,s(X)) -> false
eq(s(X),zero) -> false
eq(s(X),s(Y)) -> eq(X,Y)

or(true,Y) -> true
or(false,Y) -> Y

ite(true,X,Y) -> X
ite(false,X,Y) -> Y

SRegexp A1
                member(zero,inc([Node([s(*|zero)],*|Leaf,*|Leaf)]))

Automaton TC
States qb qi qt 
Final States qb qi qt        
Transitions
  true -> qb
  false -> qb
  zero -> qi
  s(qi) -> qi
  Node(qi,qt,qt) -> qt
  Leaf -> qt

Patterns
    true