MAYBE
TRS:
 {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
        if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                  f(mark(X)) -> mark(f(X)),
                    f(ok(X)) -> ok(f(X)),
      active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
    active(if(true(), X, Y)) -> mark(X),
   active(if(false(), X, Y)) -> mark(Y),
                active(f(X)) -> mark(if(X, c(), f(true()))),
                active(f(X)) -> f(active(X)),
      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                 proper(c()) -> ok(c()),
                proper(f(X)) -> f(proper(X)),
              proper(true()) -> ok(true()),
             proper(false()) -> ok(false()),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))}
 DP:
  Strict:
   {      if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
          if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
    if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3),
                    f#(mark(X)) -> f#(X),
                      f#(ok(X)) -> f#(X),
        active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3),
        active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3),
        active#(if(X1, X2, X3)) -> active#(X1),
        active#(if(X1, X2, X3)) -> active#(X2),
                  active#(f(X)) -> if#(X, c(), f(true())),
                  active#(f(X)) -> f#(true()),
                  active#(f(X)) -> f#(active(X)),
                  active#(f(X)) -> active#(X),
        proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)),
        proper#(if(X1, X2, X3)) -> proper#(X1),
        proper#(if(X1, X2, X3)) -> proper#(X2),
        proper#(if(X1, X2, X3)) -> proper#(X3),
                  proper#(f(X)) -> f#(proper(X)),
                  proper#(f(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:
  {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
         if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
   if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                   f(mark(X)) -> mark(f(X)),
                     f(ok(X)) -> ok(f(X)),
       active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
       active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
     active(if(true(), X, Y)) -> mark(X),
    active(if(false(), X, Y)) -> mark(Y),
                 active(f(X)) -> mark(if(X, c(), f(true()))),
                 active(f(X)) -> f(active(X)),
       proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                  proper(c()) -> ok(c()),
                 proper(f(X)) -> f(proper(X)),
               proper(true()) -> ok(true()),
              proper(false()) -> ok(false()),
                 top(mark(X)) -> top(proper(X)),
                   top(ok(X)) -> top(active(X))}
  EDG:
   {(proper#(if(X1, X2, X3)) -> proper#(X1), proper#(f(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(f(X)) -> f#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (f#(ok(X)) -> f#(X), f#(ok(X)) -> f#(X))
    (f#(ok(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (active#(f(X)) -> active#(X), active#(f(X)) -> active#(X))
    (active#(f(X)) -> active#(X), active#(f(X)) -> f#(active(X)))
    (active#(f(X)) -> active#(X), active#(f(X)) -> f#(true()))
    (active#(f(X)) -> active#(X), active#(f(X)) -> if#(X, c(), f(true())))
    (active#(f(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X2))
    (active#(f(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(f(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(f(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3))
    (top#(mark(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (top#(mark(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (top#(mark(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (active#(f(X)) -> f#(active(X)), f#(ok(X)) -> f#(X))
    (active#(f(X)) -> f#(active(X)), f#(mark(X)) -> f#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> top#(active(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(ok(X)) -> active#(X))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(mark(X)) -> top#(proper(X)), top#(mark(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(f(X)) -> proper#(X))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(f(X)) -> f#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
    (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(f(X)) -> f#(proper(X)))
    (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(f(X)) -> proper#(X))
    (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
    (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
    (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(if(X1, X2, X3)) -> active#(X2))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(f(X)) -> if#(X, c(), f(true())))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(f(X)) -> f#(true()))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(f(X)) -> f#(active(X)))
    (active#(if(X1, X2, X3)) -> active#(X2), active#(f(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> proper#(X))
    (top#(ok(X)) -> top#(active(X)), top#(mark(X)) -> top#(proper(X)))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> active#(X))
    (top#(ok(X)) -> top#(active(X)), top#(ok(X)) -> top#(active(X)))
    (proper#(f(X)) -> f#(proper(X)), f#(mark(X)) -> f#(X))
    (proper#(f(X)) -> f#(proper(X)), f#(ok(X)) -> f#(X))
    (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3))
    (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
    (top#(ok(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X2))
    (top#(ok(X)) -> active#(X), active#(f(X)) -> if#(X, c(), f(true())))
    (top#(ok(X)) -> active#(X), active#(f(X)) -> f#(true()))
    (top#(ok(X)) -> active#(X), active#(f(X)) -> f#(active(X)))
    (top#(ok(X)) -> active#(X), active#(f(X)) -> active#(X))
    (proper#(f(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> if#(proper(X1), proper(X2), proper(X3)))
    (proper#(f(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X1))
    (proper#(f(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X2))
    (proper#(f(X)) -> proper#(X), proper#(if(X1, X2, X3)) -> proper#(X3))
    (proper#(f(X)) -> proper#(X), proper#(f(X)) -> f#(proper(X)))
    (proper#(f(X)) -> proper#(X), proper#(f(X)) -> proper#(X))
    (active#(f(X)) -> if#(X, c(), f(true())), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
    (f#(mark(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (f#(mark(X)) -> f#(X), f#(ok(X)) -> f#(X))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(X1, active(X2), X3))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> if#(active(X1), X2, X3))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X2))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(f(X)) -> if#(X, c(), f(true())))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(f(X)) -> f#(true()))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(f(X)) -> f#(active(X)))
    (active#(if(X1, X2, X3)) -> active#(X1), active#(f(X)) -> active#(X))}
   SCCS:
    Scc:
     {top#(mark(X)) -> top#(proper(X)),
        top#(ok(X)) -> top#(active(X))}
    Scc:
     {proper#(if(X1, X2, X3)) -> proper#(X1),
      proper#(if(X1, X2, X3)) -> proper#(X2),
      proper#(if(X1, X2, X3)) -> proper#(X3),
                proper#(f(X)) -> proper#(X)}
    Scc:
     {active#(if(X1, X2, X3)) -> active#(X1),
      active#(if(X1, X2, X3)) -> active#(X2),
                active#(f(X)) -> active#(X)}
    Scc:
     {f#(mark(X)) -> f#(X),
        f#(ok(X)) -> f#(X)}
    Scc:
     {      if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
            if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
      if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)}
    SCC:
     Strict:
      {top#(mark(X)) -> top#(proper(X)),
         top#(ok(X)) -> top#(active(X))}
     Weak:
     {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
            if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                      f(mark(X)) -> mark(f(X)),
                        f(ok(X)) -> ok(f(X)),
          active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                    active(f(X)) -> mark(if(X, c(), f(true()))),
                    active(f(X)) -> f(active(X)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(c()) -> ok(c()),
                    proper(f(X)) -> f(proper(X)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     Fail
    SCC:
     Strict:
      {proper#(if(X1, X2, X3)) -> proper#(X1),
       proper#(if(X1, X2, X3)) -> proper#(X2),
       proper#(if(X1, X2, X3)) -> proper#(X3),
                 proper#(f(X)) -> proper#(X)}
     Weak:
     {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
            if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                      f(mark(X)) -> mark(f(X)),
                        f(ok(X)) -> ok(f(X)),
          active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                    active(f(X)) -> mark(if(X, c(), f(true()))),
                    active(f(X)) -> f(active(X)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(c()) -> ok(c()),
                    proper(f(X)) -> f(proper(X)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {proper#(if(X1, X2, X3)) -> proper#(X1),
        proper#(if(X1, X2, X3)) -> proper#(X2),
        proper#(if(X1, X2, X3)) -> proper#(X3)}
      EDG:
       {(proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X2), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X1))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X2))
        (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))}
       SCCS:
        Scc:
         {proper#(if(X1, X2, X3)) -> proper#(X1),
          proper#(if(X1, X2, X3)) -> proper#(X2),
          proper#(if(X1, X2, X3)) -> proper#(X3)}
        SCC:
         Strict:
          {proper#(if(X1, X2, X3)) -> proper#(X1),
           proper#(if(X1, X2, X3)) -> proper#(X2),
           proper#(if(X1, X2, X3)) -> proper#(X3)}
         Weak:
         {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                          f(mark(X)) -> mark(f(X)),
                            f(ok(X)) -> ok(f(X)),
              active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                        active(f(X)) -> mark(if(X, c(), f(true()))),
                        active(f(X)) -> f(active(X)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(c()) -> ok(c()),
                        proper(f(X)) -> f(proper(X)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(proper#) = 0
          Strict:
           {proper#(if(X1, X2, X3)) -> proper#(X1),
            proper#(if(X1, X2, X3)) -> proper#(X3)}
          EDG:
           {(proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X3))
            (proper#(if(X1, X2, X3)) -> proper#(X1), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X1))
            (proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))}
           SCCS:
            Scc:
             {proper#(if(X1, X2, X3)) -> proper#(X1),
              proper#(if(X1, X2, X3)) -> proper#(X3)}
            SCC:
             Strict:
              {proper#(if(X1, X2, X3)) -> proper#(X1),
               proper#(if(X1, X2, X3)) -> proper#(X3)}
             Weak:
             {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                    if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                              f(mark(X)) -> mark(f(X)),
                                f(ok(X)) -> ok(f(X)),
                  active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                            active(f(X)) -> mark(if(X, c(), f(true()))),
                            active(f(X)) -> f(active(X)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                             proper(c()) -> ok(c()),
                            proper(f(X)) -> f(proper(X)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(proper#) = 0
              Strict:
               {proper#(if(X1, X2, X3)) -> proper#(X3)}
              EDG:
               {(proper#(if(X1, X2, X3)) -> proper#(X3), proper#(if(X1, X2, X3)) -> proper#(X3))}
               SCCS:
                Scc:
                 {proper#(if(X1, X2, X3)) -> proper#(X3)}
                SCC:
                 Strict:
                  {proper#(if(X1, X2, X3)) -> proper#(X3)}
                 Weak:
                 {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                        if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
                  if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                                  f(mark(X)) -> mark(f(X)),
                                    f(ok(X)) -> ok(f(X)),
                      active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
                      active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                    active(if(true(), X, Y)) -> mark(X),
                   active(if(false(), X, Y)) -> mark(Y),
                                active(f(X)) -> mark(if(X, c(), f(true()))),
                                active(f(X)) -> f(active(X)),
                      proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                                 proper(c()) -> ok(c()),
                                proper(f(X)) -> f(proper(X)),
                              proper(true()) -> ok(true()),
                             proper(false()) -> ok(false()),
                                top(mark(X)) -> top(proper(X)),
                                  top(ok(X)) -> top(active(X))}
                 SPSC:
                  Simple Projection:
                   pi(proper#) = 0
                  Strict:
                   {}
                  Qed
    SCC:
     Strict:
      {active#(if(X1, X2, X3)) -> active#(X1),
       active#(if(X1, X2, X3)) -> active#(X2),
                 active#(f(X)) -> active#(X)}
     Weak:
     {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
            if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                      f(mark(X)) -> mark(f(X)),
                        f(ok(X)) -> ok(f(X)),
          active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                    active(f(X)) -> mark(if(X, c(), f(true()))),
                    active(f(X)) -> f(active(X)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(c()) -> ok(c()),
                    proper(f(X)) -> f(proper(X)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(active#) = 0
      Strict:
       {active#(if(X1, X2, X3)) -> active#(X1),
                  active#(f(X)) -> active#(X)}
      EDG:
       {(active#(if(X1, X2, X3)) -> active#(X1), active#(f(X)) -> active#(X))
        (active#(if(X1, X2, X3)) -> active#(X1), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(f(X)) -> active#(X), active#(if(X1, X2, X3)) -> active#(X1))
        (active#(f(X)) -> active#(X), active#(f(X)) -> active#(X))}
       SCCS:
        Scc:
         {active#(if(X1, X2, X3)) -> active#(X1),
                    active#(f(X)) -> active#(X)}
        SCC:
         Strict:
          {active#(if(X1, X2, X3)) -> active#(X1),
                     active#(f(X)) -> active#(X)}
         Weak:
         {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                          f(mark(X)) -> mark(f(X)),
                            f(ok(X)) -> ok(f(X)),
              active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                        active(f(X)) -> mark(if(X, c(), f(true()))),
                        active(f(X)) -> f(active(X)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(c()) -> ok(c()),
                        proper(f(X)) -> f(proper(X)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(active#) = 0
          Strict:
           {active#(f(X)) -> active#(X)}
          EDG:
           {(active#(f(X)) -> active#(X), active#(f(X)) -> active#(X))}
           SCCS:
            Scc:
             {active#(f(X)) -> active#(X)}
            SCC:
             Strict:
              {active#(f(X)) -> active#(X)}
             Weak:
             {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                    if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                              f(mark(X)) -> mark(f(X)),
                                f(ok(X)) -> ok(f(X)),
                  active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                            active(f(X)) -> mark(if(X, c(), f(true()))),
                            active(f(X)) -> f(active(X)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                             proper(c()) -> ok(c()),
                            proper(f(X)) -> f(proper(X)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(active#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {f#(mark(X)) -> f#(X),
         f#(ok(X)) -> f#(X)}
     Weak:
     {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
            if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                      f(mark(X)) -> mark(f(X)),
                        f(ok(X)) -> ok(f(X)),
          active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                    active(f(X)) -> mark(if(X, c(), f(true()))),
                    active(f(X)) -> f(active(X)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(c()) -> ok(c()),
                    proper(f(X)) -> f(proper(X)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(ok(X)) -> f#(X)}
      EDG:
       {(f#(ok(X)) -> f#(X), f#(ok(X)) -> f#(X))}
       SCCS:
        Scc:
         {f#(ok(X)) -> f#(X)}
        SCC:
         Strict:
          {f#(ok(X)) -> f#(X)}
         Weak:
         {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                          f(mark(X)) -> mark(f(X)),
                            f(ok(X)) -> ok(f(X)),
              active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                        active(f(X)) -> mark(if(X, c(), f(true()))),
                        active(f(X)) -> f(active(X)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(c()) -> ok(c()),
                        proper(f(X)) -> f(proper(X)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {      if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
             if#(mark(X1), X2, X3) -> if#(X1, X2, X3),
       if#(ok(X1), ok(X2), ok(X3)) -> if#(X1, X2, X3)}
     Weak:
     {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
            if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
      if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                      f(mark(X)) -> mark(f(X)),
                        f(ok(X)) -> ok(f(X)),
          active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
          active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
        active(if(true(), X, Y)) -> mark(X),
       active(if(false(), X, Y)) -> mark(Y),
                    active(f(X)) -> mark(if(X, c(), f(true()))),
                    active(f(X)) -> f(active(X)),
          proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                     proper(c()) -> ok(c()),
                    proper(f(X)) -> f(proper(X)),
                  proper(true()) -> ok(true()),
                 proper(false()) -> ok(false()),
                    top(mark(X)) -> top(proper(X)),
                      top(ok(X)) -> top(active(X))}
     SPSC:
      Simple Projection:
       pi(if#) = 0
      Strict:
       {if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
        if#(mark(X1), X2, X3) -> if#(X1, X2, X3)}
      EDG:
       {(if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))
        (if#(mark(X1), X2, X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
        (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))
        (if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(mark(X1), X2, X3) -> if#(X1, X2, X3))}
       SCCS:
        Scc:
         {if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
          if#(mark(X1), X2, X3) -> if#(X1, X2, X3)}
        SCC:
         Strict:
          {if#(X1, mark(X2), X3) -> if#(X1, X2, X3),
           if#(mark(X1), X2, X3) -> if#(X1, X2, X3)}
         Weak:
         {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
          if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                          f(mark(X)) -> mark(f(X)),
                            f(ok(X)) -> ok(f(X)),
              active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
              active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
            active(if(true(), X, Y)) -> mark(X),
           active(if(false(), X, Y)) -> mark(Y),
                        active(f(X)) -> mark(if(X, c(), f(true()))),
                        active(f(X)) -> f(active(X)),
              proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                         proper(c()) -> ok(c()),
                        proper(f(X)) -> f(proper(X)),
                      proper(true()) -> ok(true()),
                     proper(false()) -> ok(false()),
                        top(mark(X)) -> top(proper(X)),
                          top(ok(X)) -> top(active(X))}
         SPSC:
          Simple Projection:
           pi(if#) = 0
          Strict:
           {if#(X1, mark(X2), X3) -> if#(X1, X2, X3)}
          EDG:
           {(if#(X1, mark(X2), X3) -> if#(X1, X2, X3), if#(X1, mark(X2), X3) -> if#(X1, X2, X3))}
           SCCS:
            Scc:
             {if#(X1, mark(X2), X3) -> if#(X1, X2, X3)}
            SCC:
             Strict:
              {if#(X1, mark(X2), X3) -> if#(X1, X2, X3)}
             Weak:
             {      if(X1, mark(X2), X3) -> mark(if(X1, X2, X3)),
                    if(mark(X1), X2, X3) -> mark(if(X1, X2, X3)),
              if(ok(X1), ok(X2), ok(X3)) -> ok(if(X1, X2, X3)),
                              f(mark(X)) -> mark(f(X)),
                                f(ok(X)) -> ok(f(X)),
                  active(if(X1, X2, X3)) -> if(X1, active(X2), X3),
                  active(if(X1, X2, X3)) -> if(active(X1), X2, X3),
                active(if(true(), X, Y)) -> mark(X),
               active(if(false(), X, Y)) -> mark(Y),
                            active(f(X)) -> mark(if(X, c(), f(true()))),
                            active(f(X)) -> f(active(X)),
                  proper(if(X1, X2, X3)) -> if(proper(X1), proper(X2), proper(X3)),
                             proper(c()) -> ok(c()),
                            proper(f(X)) -> f(proper(X)),
                          proper(true()) -> ok(true()),
                         proper(false()) -> ok(false()),
                            top(mark(X)) -> top(proper(X)),
                              top(ok(X)) -> top(active(X))}
             SPSC:
              Simple Projection:
               pi(if#) = 1
              Strict:
               {}
              Qed