Ops Node:3 Leaf:0 true:0 false:0 leq:2 A:0 B:0 ite:3 cons:2 nil:0
    traversalPre:1 append:2 sorted:1

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

TRS R1

% If we use a Prefix-traversal the order might not be preserved

traversalPre(Leaf) -> nil
traversalPre(Node(Y,Z,U)) -> cons(Y,append(traversalPre(Z),traversalPre(U)))

append(nil,X) -> X
append(cons(X,Y), Z) -> cons(X, append(Y,Z))

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

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 tree of A and B
Automaton A0
States qta qtb qtab ql qa qb qtr qf
Final States qf
Transitions
        sorted(qtr) -> qf
        traversalPre(qta) -> qtr
        traversalPre(qtb) -> qtr
        traversalPre(qtab) -> qtr
        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 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