MAYBE

Problem:
 isEmpty(empty()) -> true()
 isEmpty(node(l,x,r)) -> false()
 left(empty()) -> empty()
 left(node(l,x,r)) -> l
 right(empty()) -> empty()
 right(node(l,x,r)) -> r
 elem(node(l,x,r)) -> x
 append(nil(),x) -> cons(x,nil())
 append(cons(y(),ys),x) -> cons(y(),append(ys,x))
 listify(n,xs) ->
 if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                              node(right(left(n)),elem(n),right(n))),
    xs,append(xs,n))
 if(true(),b,n,m,xs,ys) -> xs
 if(false(),false(),n,m,xs,ys) -> listify(m,xs)
 if(false(),true(),n,m,xs,ys) -> listify(n,ys)
 toList(n) -> listify(n,nil())

Proof:
 DP Processor:
  DPs:
   append#(cons(y(),ys),x) -> append#(ys,x)
   listify#(n,xs) -> append#(xs,n)
   listify#(n,xs) -> elem#(n)
   listify#(n,xs) -> right#(left(n))
   listify#(n,xs) -> elem#(left(n))
   listify#(n,xs) -> left#(left(n))
   listify#(n,xs) -> right#(n)
   listify#(n,xs) -> left#(n)
   listify#(n,xs) -> isEmpty#(left(n))
   listify#(n,xs) -> isEmpty#(n)
   listify#(n,xs) ->
   if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                 node(right(left(n)),elem(n),right(n))),
       xs,append(xs,n))
   if#(false(),false(),n,m,xs,ys) -> listify#(m,xs)
   if#(false(),true(),n,m,xs,ys) -> listify#(n,ys)
   toList#(n) -> listify#(n,nil())
  TRS:
   isEmpty(empty()) -> true()
   isEmpty(node(l,x,r)) -> false()
   left(empty()) -> empty()
   left(node(l,x,r)) -> l
   right(empty()) -> empty()
   right(node(l,x,r)) -> r
   elem(node(l,x,r)) -> x
   append(nil(),x) -> cons(x,nil())
   append(cons(y(),ys),x) -> cons(y(),append(ys,x))
   listify(n,xs) ->
   if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                node(right(left(n)),elem(n),right(n))),
      xs,append(xs,n))
   if(true(),b,n,m,xs,ys) -> xs
   if(false(),false(),n,m,xs,ys) -> listify(m,xs)
   if(false(),true(),n,m,xs,ys) -> listify(n,ys)
   toList(n) -> listify(n,nil())
  TDG Processor:
   DPs:
    append#(cons(y(),ys),x) -> append#(ys,x)
    listify#(n,xs) -> append#(xs,n)
    listify#(n,xs) -> elem#(n)
    listify#(n,xs) -> right#(left(n))
    listify#(n,xs) -> elem#(left(n))
    listify#(n,xs) -> left#(left(n))
    listify#(n,xs) -> right#(n)
    listify#(n,xs) -> left#(n)
    listify#(n,xs) -> isEmpty#(left(n))
    listify#(n,xs) -> isEmpty#(n)
    listify#(n,xs) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs)
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys)
    toList#(n) -> listify#(n,nil())
   TRS:
    isEmpty(empty()) -> true()
    isEmpty(node(l,x,r)) -> false()
    left(empty()) -> empty()
    left(node(l,x,r)) -> l
    right(empty()) -> empty()
    right(node(l,x,r)) -> r
    elem(node(l,x,r)) -> x
    append(nil(),x) -> cons(x,nil())
    append(cons(y(),ys),x) -> cons(y(),append(ys,x))
    listify(n,xs) ->
    if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                 node(right(left(n)),elem(n),right(n))),
       xs,append(xs,n))
    if(true(),b,n,m,xs,ys) -> xs
    if(false(),false(),n,m,xs,ys) -> listify(m,xs)
    if(false(),true(),n,m,xs,ys) -> listify(n,ys)
    toList(n) -> listify(n,nil())
   graph:
    toList#(n) -> listify#(n,nil()) ->
    listify#(n,xs) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
    toList#(n) -> listify#(n,nil()) -> listify#(n,xs) -> isEmpty#(n)
    toList#(n) -> listify#(n,nil()) ->
    listify#(n,xs) -> isEmpty#(left(n))
    toList#(n) -> listify#(n,nil()) -> listify#(n,xs) -> left#(n)
    toList#(n) -> listify#(n,nil()) -> listify#(n,xs) -> right#(n)
    toList#(n) -> listify#(n,nil()) ->
    listify#(n,xs) -> left#(left(n))
    toList#(n) -> listify#(n,nil()) ->
    listify#(n,xs) -> elem#(left(n))
    toList#(n) -> listify#(n,nil()) ->
    listify#(n,xs) -> right#(left(n))
    toList#(n) -> listify#(n,nil()) -> listify#(n,xs) -> elem#(n)
    toList#(n) -> listify#(n,nil()) ->
    listify#(n,xs) -> append#(xs,n)
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> isEmpty#(n)
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> isEmpty#(left(n))
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> left#(n)
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> right#(n)
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> left#(left(n))
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> elem#(left(n))
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> right#(left(n))
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> elem#(n)
    if#(false(),false(),n,m,xs,ys) -> listify#(m,xs) ->
    listify#(n,xs) -> append#(xs,n)
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> isEmpty#(n)
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> isEmpty#(left(n))
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> left#(n)
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> right#(n)
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> left#(left(n))
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> elem#(left(n))
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> right#(left(n))
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> elem#(n)
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys) ->
    listify#(n,xs) -> append#(xs,n)
    listify#(n,xs) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
    ->
    if#(false(),true(),n,m,xs,ys) -> listify#(n,ys)
    listify#(n,xs) ->
    if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
    -> if#(false(),false(),n,m,xs,ys) -> listify#(m,xs)
    listify#(n,xs) -> append#(xs,n) ->
    append#(cons(y(),ys),x) -> append#(ys,x)
    append#(cons(y(),ys),x) -> append#(ys,x) -> append#(cons(y(),ys),x) -> append#(ys,x)
   SCC Processor:
    #sccs: 2
    #rules: 4
    #arcs: 34/196
    DPs:
     listify#(n,xs) ->
     if#(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                   node(right(left(n)),elem(n),right(n))),
         xs,append(xs,n))
     if#(false(),false(),n,m,xs,ys) -> listify#(m,xs)
     if#(false(),true(),n,m,xs,ys) -> listify#(n,ys)
    TRS:
     isEmpty(empty()) -> true()
     isEmpty(node(l,x,r)) -> false()
     left(empty()) -> empty()
     left(node(l,x,r)) -> l
     right(empty()) -> empty()
     right(node(l,x,r)) -> r
     elem(node(l,x,r)) -> x
     append(nil(),x) -> cons(x,nil())
     append(cons(y(),ys),x) -> cons(y(),append(ys,x))
     listify(n,xs) ->
     if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
     if(true(),b,n,m,xs,ys) -> xs
     if(false(),false(),n,m,xs,ys) -> listify(m,xs)
     if(false(),true(),n,m,xs,ys) -> listify(n,ys)
     toList(n) -> listify(n,nil())
    Open
    
    DPs:
     append#(cons(y(),ys),x) -> append#(ys,x)
    TRS:
     isEmpty(empty()) -> true()
     isEmpty(node(l,x,r)) -> false()
     left(empty()) -> empty()
     left(node(l,x,r)) -> l
     right(empty()) -> empty()
     right(node(l,x,r)) -> r
     elem(node(l,x,r)) -> x
     append(nil(),x) -> cons(x,nil())
     append(cons(y(),ys),x) -> cons(y(),append(ys,x))
     listify(n,xs) ->
     if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                  node(right(left(n)),elem(n),right(n))),
        xs,append(xs,n))
     if(true(),b,n,m,xs,ys) -> xs
     if(false(),false(),n,m,xs,ys) -> listify(m,xs)
     if(false(),true(),n,m,xs,ys) -> listify(n,ys)
     toList(n) -> listify(n,nil())
    Subterm Criterion Processor:
     simple projection:
      pi(append#) = 0
     problem:
      DPs:
       
      TRS:
       isEmpty(empty()) -> true()
       isEmpty(node(l,x,r)) -> false()
       left(empty()) -> empty()
       left(node(l,x,r)) -> l
       right(empty()) -> empty()
       right(node(l,x,r)) -> r
       elem(node(l,x,r)) -> x
       append(nil(),x) -> cons(x,nil())
       append(cons(y(),ys),x) -> cons(y(),append(ys,x))
       listify(n,xs) ->
       if(isEmpty(n),isEmpty(left(n)),right(n),node(left(left(n)),elem(left(n)),
                                                    node(right(left(n)),elem(n),right(n))),
          xs,append(xs,n))
       if(true(),b,n,m,xs,ys) -> xs
       if(false(),false(),n,m,xs,ys) -> listify(m,xs)
       if(false(),true(),n,m,xs,ys) -> listify(n,ys)
       toList(n) -> listify(n,nil())
     Qed