MAYBE

Problem:
 rev(nil()) -> nil()
 rev(rev(x)) -> x
 rev(++(x,y)) -> ++(rev(y),rev(x))
 ++(nil(),y) -> y
 ++(x,nil()) -> x
 ++(.(x,y),z) -> .(x,++(y,z))
 ++(x,++(y,z)) -> ++(++(x,y),z)
 make(x) -> .(x,nil())

Proof:
 DP Processor:
  DPs:
   rev#(++(x,y)) -> rev#(x)
   rev#(++(x,y)) -> rev#(y)
   rev#(++(x,y)) -> ++#(rev(y),rev(x))
   ++#(.(x,y),z) -> ++#(y,z)
   ++#(x,++(y,z)) -> ++#(x,y)
   ++#(x,++(y,z)) -> ++#(++(x,y),z)
  TRS:
   rev(nil()) -> nil()
   rev(rev(x)) -> x
   rev(++(x,y)) -> ++(rev(y),rev(x))
   ++(nil(),y) -> y
   ++(x,nil()) -> x
   ++(.(x,y),z) -> .(x,++(y,z))
   ++(x,++(y,z)) -> ++(++(x,y),z)
   make(x) -> .(x,nil())
  CDG Processor:
   DPs:
    rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(y)
    rev#(++(x,y)) -> ++#(rev(y),rev(x))
    ++#(.(x,y),z) -> ++#(y,z)
    ++#(x,++(y,z)) -> ++#(x,y)
    ++#(x,++(y,z)) -> ++#(++(x,y),z)
   TRS:
    rev(nil()) -> nil()
    rev(rev(x)) -> x
    rev(++(x,y)) -> ++(rev(y),rev(x))
    ++(nil(),y) -> y
    ++(x,nil()) -> x
    ++(.(x,y),z) -> .(x,++(y,z))
    ++(x,++(y,z)) -> ++(++(x,y),z)
    make(x) -> .(x,nil())
   graph:
    ++#(.(x,y),z) -> ++#(y,z) -> ++#(.(x,y),z) -> ++#(y,z)
    ++#(x,++(y,z)) -> ++#(++(x,y),z) -> ++#(.(x,y),z) -> ++#(y,z)
    ++#(x,++(y,z)) -> ++#(x,y) -> ++#(.(x,y),z) -> ++#(y,z)
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
    ++#(.(x,y),z) -> ++#(y,z)
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) ->
    ++#(x,++(y,z)) -> ++#(x,y)
    rev#(++(x,y)) -> ++#(rev(y),rev(x)) -> ++#(x,++(y,z)) -> ++#(++(x,y),z)
   SCC Processor:
    #sccs: 1
    #rules: 1
    #arcs: 6/36
    DPs:
     ++#(.(x,y),z) -> ++#(y,z)
    TRS:
     rev(nil()) -> nil()
     rev(rev(x)) -> x
     rev(++(x,y)) -> ++(rev(y),rev(x))
     ++(nil(),y) -> y
     ++(x,nil()) -> x
     ++(.(x,y),z) -> .(x,++(y,z))
     ++(x,++(y,z)) -> ++(++(x,y),z)
     make(x) -> .(x,nil())
    Open