MAYBE

Problem:
 rev(ls) -> r1(ls,empty())
 r1(empty(),a) -> a
 r1(cons(x,k),a) -> r1(k,cons(x,a))

Proof:
 DP Processor:
  DPs:
   rev#(ls) -> r1#(ls,empty())
   r1#(cons(x,k),a) -> r1#(k,cons(x,a))
  TRS:
   rev(ls) -> r1(ls,empty())
   r1(empty(),a) -> a
   r1(cons(x,k),a) -> r1(k,cons(x,a))
  Usable Rule Processor:
   DPs:
    rev#(ls) -> r1#(ls,empty())
    r1#(cons(x,k),a) -> r1#(k,cons(x,a))
   TRS:
    
   ADG Processor:
    DPs:
     rev#(ls) -> r1#(ls,empty())
     r1#(cons(x,k),a) -> r1#(k,cons(x,a))
    TRS:
     
    graph:
     r1#(cons(x,k),a) -> r1#(k,cons(x,a)) ->
     r1#(cons(x,k),a) -> r1#(k,cons(x,a))
     rev#(ls) -> r1#(ls,empty()) -> r1#(cons(x,k),a) -> r1#(k,cons(x,a))
    Restore Modifier:
     DPs:
      rev#(ls) -> r1#(ls,empty())
      r1#(cons(x,k),a) -> r1#(k,cons(x,a))
     TRS:
      rev(ls) -> r1(ls,empty())
      r1(empty(),a) -> a
      r1(cons(x,k),a) -> r1(k,cons(x,a))
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 2/4
      DPs:
       r1#(cons(x,k),a) -> r1#(k,cons(x,a))
      TRS:
       rev(ls) -> r1(ls,empty())
       r1(empty(),a) -> a
       r1(cons(x,k),a) -> r1(k,cons(x,a))
      Open