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