Ops app:2 filter:0 o:0 s:1 nz:0 nil:0 cons:2 ite:0 true:0 false:0
    exists:0 even:0 odd:0

Const o s nil cons true false

Vars F X Y Z U Xs

TRS R1

    app(app(app(ite,true),X),Y) -> X
    app(app(app(ite,false),X),Y) -> Y
    
    app(even, o) -> true
    app(odd, o) -> false
    app(even, s(X)) -> app(odd, X)
    app(odd, s(X)) -> app(even, X)

    app(app(filter, X), nil) -> nil
    app(app(filter, X), cons(Y,Z)) -> 
           app(app(app(ite,app(X,Y)), cons(Y, app(app(filter, X), Z))), 
                     app(app(filter, X), Z))
                     
    app(app(exists, X), nil) -> false
    app(app(exists, X), cons(Y,Z)) ->
           app(app(app(ite,app(X,Y)), true), app(app(exists, X), Z))

Automaton A0
States q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 
Final States q0 
Transitions
        app(q5,q6) -> q1
        app(q1,q2) -> q0
        s(q9) -> q9
        o -> q9
        exists -> q5
        cons(q9,q4) -> q4
        nil -> q4
        app(q7,q8) -> q3
        filter -> q7
        odd -> q8
        app(q3,q4) -> q2
        even -> q6

SRegexp A0
        app(app(exists, even), app(app(filter,odd),[cons([s(*|o)],*|nil)]))

Automaton TC
States qb qn ql
Final States qb qn ql
Transitions
      true -> qb
      false -> qb
      o -> qn
      s(qn) -> qn
      nil -> ql
      cons(qn,ql) -> ql

Patterns
        true