Ops append:0 rev:0 nil:0 cons:2 A:0 B:0 leq:0 geq:0 sorted:0 true:0
false:0 ite:0 app:2

Const nil cons A B true false
Vars X Y Z P

TRS R1
app(app(append,nil),X) -> X
app(app(append,cons(X,Y)), Z) -> cons(X, app(app(append,Y),Z))
app(rev,nil) -> nil
app(rev,cons(X,Y)) -> app(app(append,app(rev,Y)), cons(X,nil))

app(app(leq,A),A) -> true
app(app(leq,A),B) -> true
app(app(leq,B),A) -> false
app(app(leq,B),B) -> true

app(app(geq,A),A) -> true
app(app(geq,A),B) -> false
app(app(geq,B),A) -> true
app(app(geq,B),B) -> true

app(app(sorted,P),nil) -> true
app(app(sorted,P),cons(X,nil)) -> true
app(app(sorted,P),cons(X,cons(Y,Z))) -> 
app(app(app(ite,app(app(P,X),Y)),app(app(sorted,P),cons(Y,Z))),false)


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

SRegexp A1
        app(app(sorted,geq),app(rev,[cons(A,*|[cons(B,*|nil)])]))

Automaton TC
States qe ql qb
Final States ql qe qb
Transitions
        A -> qe
        B -> qe
        cons(qe,ql) -> ql
        nil -> ql
        true -> qb
        false -> qb


Patterns
        false