MAYBE
TRS:
 {       f(ok(X)) -> ok(f(X)),
         g(ok(X)) -> ok(g(X)),
  active(f(g(X))) -> mark(g(X)),
      active(c()) -> mark(f(g(c()))),
     proper(f(X)) -> f(proper(X)),
     proper(g(X)) -> g(proper(X)),
      proper(c()) -> ok(c()),
     top(mark(X)) -> top(proper(X)),
       top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {    f#(ok(X)) -> f#(X),
        g#(ok(X)) -> g#(X),
     active#(c()) -> f#(g(c())),
     active#(c()) -> g#(c()),
    proper#(f(X)) -> f#(proper(X)),
    proper#(f(X)) -> proper#(X),
    proper#(g(X)) -> g#(proper(X)),
    proper#(g(X)) -> proper#(X),
    top#(mark(X)) -> proper#(X),
    top#(mark(X)) -> top#(proper(X)),
      top#(ok(X)) -> active#(X),
      top#(ok(X)) -> top#(active(X))}
  Weak:
  {       f(ok(X)) -> ok(f(X)),
          g(ok(X)) -> ok(g(X)),
   active(f(g(X))) -> mark(g(X)),
       active(c()) -> mark(f(g(c()))),
      proper(f(X)) -> f(proper(X)),
      proper(g(X)) -> g(proper(X)),
       proper(c()) -> ok(c()),
      top(mark(X)) -> top(proper(X)),
        top(ok(X)) -> top(active(X))}
  EDG:
   {(f#(ok(X)) -> f#(X), f#(ok(X)) -> f#(X))
    (proper#(f(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (proper#(f(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (proper#(f(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (proper#(f(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (proper#(g(X)) -> g#(proper(X)), g#(ok(X)) -> g#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(f(X)) -> f#(proper(X)), f#(ok(X)) -> f#(X))
    (top#(ok(X)) -> active#(X), active#(c()) -> f#(g(c())))
    (top#(ok(X)) -> active#(X), active#(c()) -> g#(c()))
    (proper#(g(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (proper#(g(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (proper#(g(X)) -> proper#(X), proper#(g(X)) -> g#(proper(X)))
    (proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))
    (g#(ok(X)) -> g#(X), g#(ok(X)) -> g#(X))}
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(f(X)) -> proper#(X),
      proper#(g(X)) -> proper#(X)}
    Scc:
     {g#(ok(X)) -> g#(X)}
    Scc:
     {f#(ok(X)) -> f#(X)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {       f(ok(X)) -> ok(f(X)),
             g(ok(X)) -> ok(g(X)),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c()))),
         proper(f(X)) -> f(proper(X)),
         proper(g(X)) -> g(proper(X)),
          proper(c()) -> ok(c()),
         top(mark(X)) -> top(proper(X)),
           top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      {proper#(f(X)) -> proper#(X),
       proper#(g(X)) -> proper#(X)}
     Weak:
     {       f(ok(X)) -> ok(f(X)),
             g(ok(X)) -> ok(g(X)),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c()))),
         proper(f(X)) -> f(proper(X)),
         proper(g(X)) -> g(proper(X)),
          proper(c()) -> ok(c()),
         top(mark(X)) -> top(proper(X)),
           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(g(X)) -> proper#(X)}
      EDG:
       {(proper#(g(X)) -> proper#(X), proper#(g(X)) -> proper#(X))}
       SCCS:
        Scc:
         {proper#(g(X)) -> proper#(X)}
        SCC:
         Strict:
          {proper#(g(X)) -> proper#(X)}
         Weak:
         {       f(ok(X)) -> ok(f(X)),
                 g(ok(X)) -> ok(g(X)),
          active(f(g(X))) -> mark(g(X)),
              active(c()) -> mark(f(g(c()))),
             proper(f(X)) -> f(proper(X)),
             proper(g(X)) -> g(proper(X)),
              proper(c()) -> ok(c()),
             top(mark(X)) -> top(proper(X)),
               top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {g#(ok(X)) -> g#(X)}
     Weak:
     {       f(ok(X)) -> ok(f(X)),
             g(ok(X)) -> ok(g(X)),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c()))),
         proper(f(X)) -> f(proper(X)),
         proper(g(X)) -> g(proper(X)),
          proper(c()) -> ok(c()),
         top(mark(X)) -> top(proper(X)),
           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {f#(ok(X)) -> f#(X)}
     Weak:
     {       f(ok(X)) -> ok(f(X)),
             g(ok(X)) -> ok(g(X)),
      active(f(g(X))) -> mark(g(X)),
          active(c()) -> mark(f(g(c()))),
         proper(f(X)) -> f(proper(X)),
         proper(g(X)) -> g(proper(X)),
          proper(c()) -> ok(c()),
         top(mark(X)) -> top(proper(X)),
           top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {}
      Qed