%-*- mode: TeX -*- 

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

Const Node Leaf true false zero s

Vars U V X Y Z X1 X2 X3 

TRS R1

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

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

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

app(app(plus,zero),X) -> X
app(app(plus,s(X)),Y) -> s(app(app(plus,X),Y))


SRegexp A1
        app(app(member,zero),app(app(map,app(plus,s(zero))),[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