Ops app:2 insert:0 sort:0 leq:0 geq:0 nil:0 cons:2 ite:0 true:0
    false:0 sorted:0 A:0 B:0

Const cons nil true false A B

Vars F X Y Z U Xs P

TRS R1

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

    app(app(sort,P),nil) -> nil
    app(app(sort,P),cons(X,Y)) -> app(app(app(insert,P),X),app(app(sort,P),Y))

    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)


SRegexp A0
        app(app(sorted,leq),app(app(sort,leq),[cons((A|B),*|nil)]))


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

Patterns
        false