Ops Node:3 Leaf:0 insert:2 true:0 false:0 eq:2 A:0 B:0 C:0 ite:3 
    replace:3 or:2 member:2

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

TRS R1
eq(A,A) -> true
eq(B,B) -> true
eq(C,C) -> true
eq(A,B) -> false
eq(A,C) -> false
eq(B,A) -> false
eq(B,C) -> false
eq(C,A) -> false
eq(C,B) -> false

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

replace(X,Y,Leaf) -> Leaf
replace(X1,X2,Node(Y,Z,U)) -> ite(eq(X1,Y),Node(X2,replace(X1,X2,Z),replace(X1,X2,U)),
                                           Node(Y,replace(X1,X2,Z),replace(X1,X2,U)))

member(X,Leaf) -> false
member(X,Node(Y,Z,U)) -> or(eq(X,Y),or(member(X,Z),member(X,U)))

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

SRegexp A1
    member(A,replace(A,C,[Node((A|B),*|Leaf,*|Leaf)]))

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

Patterns
    true