MAYBE

Problem:
 f(n__a(),X,X) -> f(activate(X),b(),n__b())
 b() -> a()
 a() -> n__a()
 b() -> n__b()
 activate(n__a()) -> a()
 activate(n__b()) -> b()
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   f#(n__a(),X,X) -> b#()
   f#(n__a(),X,X) -> activate#(X)
   f#(n__a(),X,X) -> f#(activate(X),b(),n__b())
   b#() -> a#()
   activate#(n__a()) -> a#()
   activate#(n__b()) -> b#()
  TRS:
   f(n__a(),X,X) -> f(activate(X),b(),n__b())
   b() -> a()
   a() -> n__a()
   b() -> n__b()
   activate(n__a()) -> a()
   activate(n__b()) -> b()
   activate(X) -> X
  Usable Rule Processor:
   DPs:
    f#(n__a(),X,X) -> b#()
    f#(n__a(),X,X) -> activate#(X)
    f#(n__a(),X,X) -> f#(activate(X),b(),n__b())
    b#() -> a#()
    activate#(n__a()) -> a#()
    activate#(n__b()) -> b#()
   TRS:
    b() -> a()
    b() -> n__b()
    a() -> n__a()
    activate(n__a()) -> a()
    activate(n__b()) -> b()
    activate(X) -> X
   EDG Processor:
    DPs:
     f#(n__a(),X,X) -> b#()
     f#(n__a(),X,X) -> activate#(X)
     f#(n__a(),X,X) -> f#(activate(X),b(),n__b())
     b#() -> a#()
     activate#(n__a()) -> a#()
     activate#(n__b()) -> b#()
    TRS:
     b() -> a()
     b() -> n__b()
     a() -> n__a()
     activate(n__a()) -> a()
     activate(n__b()) -> b()
     activate(X) -> X
    graph:
     activate#(n__b()) -> b#() -> b#() -> a#()
     f#(n__a(),X,X) -> activate#(X) -> activate#(n__a()) -> a#()
     f#(n__a(),X,X) -> activate#(X) -> activate#(n__b()) -> b#()
     f#(n__a(),X,X) -> b#() -> b#() -> a#()
     f#(n__a(),X,X) -> f#(activate(X),b(),n__b()) ->
     f#(n__a(),X,X) -> b#()
     f#(n__a(),X,X) -> f#(activate(X),b(),n__b()) ->
     f#(n__a(),X,X) -> activate#(X)
     f#(n__a(),X,X) -> f#(activate(X),b(),n__b()) -> f#(n__a(),X,X) -> f#(activate(X),b(),n__b())
    Restore Modifier:
     DPs:
      f#(n__a(),X,X) -> b#()
      f#(n__a(),X,X) -> activate#(X)
      f#(n__a(),X,X) -> f#(activate(X),b(),n__b())
      b#() -> a#()
      activate#(n__a()) -> a#()
      activate#(n__b()) -> b#()
     TRS:
      f(n__a(),X,X) -> f(activate(X),b(),n__b())
      b() -> a()
      a() -> n__a()
      b() -> n__b()
      activate(n__a()) -> a()
      activate(n__b()) -> b()
      activate(X) -> X
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 7/36
      DPs:
       f#(n__a(),X,X) -> f#(activate(X),b(),n__b())
      TRS:
       f(n__a(),X,X) -> f(activate(X),b(),n__b())
       b() -> a()
       a() -> n__a()
       b() -> n__b()
       activate(n__a()) -> a()
       activate(n__b()) -> b()
       activate(X) -> X
      Open