Ops A:0 B:0 and:2 true:0 false:0 member:2 eq:2
    cons:2 nil:0 ite:3 pair:2 let1:3 let2:3 split:1 not:1 let3:2

Vars X Y Z U

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

    member(X,nil)->false
    member(X,cons(Y,Z))->ite(eq(X,Y),true,member(X,Z))

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

    split(nil) -> pair(nil,nil)
    split(cons(X,nil)) -> pair(cons(X,nil),nil)
    split(cons(X,cons(Y,Z))) -> let1(X,Y,split(Z))

    let1(X,Y,pair(Z,U)) -> pair(cons(X,Z),cons(Y,U))

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

    not(true) -> false
    not(false) -> true

    let2(X,Y,pair(Z,U)) -> and(not(member(X,Z)),not(member(Y,U)))

    let3(X,pair(Z,U)) -> member(X,Z)
    
SRegexp A1
        let2(B,A,split([cons(A,cons(B,*|nil))]))
        
Automaton TC
States qi ql qb
Final States qi ql qb
Transitions
        A -> qi
        B -> qi
        cons(qi,ql) -> ql
        nil -> ql   
        true -> qb
        false -> qb

Patterns
        false