MAYBE

Problem:
 rev(a()) -> a()
 rev(b()) -> b()
 rev(++(x,y)) -> ++(rev(y),rev(x))
 rev(++(x,x)) -> rev(x)

Proof:
 DP Processor:
  DPs:
   rev#(++(x,y)) -> rev#(x)
   rev#(++(x,y)) -> rev#(y)
   rev#(++(x,x)) -> rev#(x)
  TRS:
   rev(a()) -> a()
   rev(b()) -> b()
   rev(++(x,y)) -> ++(rev(y),rev(x))
   rev(++(x,x)) -> rev(x)
  Usable Rule Processor:
   DPs:
    rev#(++(x,y)) -> rev#(x)
    rev#(++(x,y)) -> rev#(y)
    rev#(++(x,x)) -> rev#(x)
   TRS:
    
   Restore Modifier:
    DPs:
     rev#(++(x,y)) -> rev#(x)
     rev#(++(x,y)) -> rev#(y)
     rev#(++(x,x)) -> rev#(x)
    TRS:
     rev(a()) -> a()
     rev(b()) -> b()
     rev(++(x,y)) -> ++(rev(y),rev(x))
     rev(++(x,x)) -> rev(x)
    SCC Processor:
     #sccs: 1
     #rules: 3
     #arcs: 9/9
     DPs:
      rev#(++(x,y)) -> rev#(x)
      rev#(++(x,y)) -> rev#(y)
      rev#(++(x,x)) -> rev#(x)
     TRS:
      rev(a()) -> a()
      rev(b()) -> b()
      rev(++(x,y)) -> ++(rev(y),rev(x))
      rev(++(x,x)) -> rev(x)
     Open