Ops Node:3 Leaf:0 insert:2 true:0 false:0 leq:2 A:0 B:0 ite:3 
    ordered:1 and:2 cons:2 nil:0

Const Node Leaf true false A B cons nil
Vars U V X Y Z X1 X2 X3 

TRS R1
insert(nil,Leaf) -> Leaf
insert(nil,Node(Y,Z,U)) -> Node(Y,Z,U)
insert(cons(X,Y),Leaf) -> insert(Y,Node(X,Leaf,Leaf))
insert(cons(X,X1),Node(Y,Z,U)) -> insert(X1,ite(leq(X,Y),Node(Y,insert(X,Z),U),Node(Y,Z,insert(X,U))))

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

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

ordered(Leaf) -> true
ordered(Node(X,Leaf,Leaf)) -> true
ordered(Node(X,Node(Y,Z,U),Leaf)) -> and(leq(Y,X),ordered(Node(Y,Z,U)))
ordered(Node(X,Leaf,Node(Y,Z,U))) -> and(leq(X,Y),ordered(Node(Y,Z,U)))
ordered(Node(X,Node(X1,X2,X3),Node(Y,Z,U))) -> and(leq(X1,X),and(leq(X,Y),and(ordered(Node(X1,X2,X3)),ordered(Node(Y,Z,U)))))

and(true,X) -> X
and(false,X) -> false


SRegexp A1
    ordered(insert([cons((A|B),*|nil)],Leaf))

Automaton TC
States qb qv qt ql
Final States qb qv qt ql
Transitions
  true -> qb
  false -> qb
  A -> qv
  B -> qv
  Node(qv,qt,qt) -> qt
  Leaf -> qt
  nil -> ql
  cons(qv,ql) -> ql

Patterns
    false