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

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

TRS R1
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


% ordered applied to Ordered tree of A and B
Automaton A0
States qta qtb qtab ql qa qb qtr qf
Final States qf
Transitions
        ordered(qta) -> qf
        ordered(qtb) -> qf
        ordered(qtab) -> qf
        Leaf -> qta
        Leaf -> qtb
        Leaf -> qtab
        Node(qa,qta,qta) -> qta
        Node(qa,qta,qtb) -> qtab
        Node(qa,qta,qtab) -> qtab
        Node(qb,qta,qtb) -> qtab
        Node(qb,qtb,qtb) -> qtb
        A -> qa
        B -> qb

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


Patterns
    false