Ops append:2 rev:1 nil:0 cons:2 A:0 B:0 leq:2 invsorted:1 true:0 false:0
    ite:3 
Const nil cons A B true false
Vars X Y Z U Xs

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

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

invsorted(nil) -> true
invsorted(cons(X,nil)) -> true
invsorted(cons(X,cons(Y,Z))) -> ite(leq(Y,X),invsorted(cons(Y,Z)),false)

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


SRegexp A1
       invsorted(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