Ops app:2 filter:0 o:0 s:1 nz:0 nil:0 cons:2 ite:0 true:0 false:0
    forAll:0 

Const o s nil cons true false

Vars X Y Z 

TRS R1

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

    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(forAll, X), nil) -> true
    app(app(forAll, X), cons(Y,Z)) ->
           app(app(app(ite,app(X,Y)), app(app(forAll, X), Z)),false)

SRegexp A0
        app(app(forAll, nz), app(app(filter,nz),[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
        false