YES
Time: 0.002176
TRS:
 {    f a() -> b(),
      f c() -> d(),
  f g(x, y) -> g(f x, f y),
  f h(x, y) -> g(h(y, f x), h(x, f y)),
    g(x, x) -> h(e(), x)}
 DP:
  DP:
   {f# g(x, y) -> f# x,
    f# g(x, y) -> f# y,
    f# g(x, y) -> g#(f x, f y),
    f# h(x, y) -> f# x,
    f# h(x, y) -> f# y,
    f# h(x, y) -> g#(h(y, f x), h(x, f y))}
  TRS:
  {    f a() -> b(),
       f c() -> d(),
   f g(x, y) -> g(f x, f y),
   f h(x, y) -> g(h(y, f x), h(x, f y)),
     g(x, x) -> h(e(), x)}
  EDG:
   {(f# h(x, y) -> f# y, f# h(x, y) -> g#(h(y, f x), h(x, f y)))
    (f# h(x, y) -> f# y, f# h(x, y) -> f# y)
    (f# h(x, y) -> f# y, f# h(x, y) -> f# x)
    (f# h(x, y) -> f# y, f# g(x, y) -> g#(f x, f y))
    (f# h(x, y) -> f# y, f# g(x, y) -> f# y)
    (f# h(x, y) -> f# y, f# g(x, y) -> f# x)
    (f# h(x, y) -> f# x, f# h(x, y) -> g#(h(y, f x), h(x, f y)))
    (f# h(x, y) -> f# x, f# h(x, y) -> f# y)
    (f# h(x, y) -> f# x, f# h(x, y) -> f# x)
    (f# h(x, y) -> f# x, f# g(x, y) -> g#(f x, f y))
    (f# h(x, y) -> f# x, f# g(x, y) -> f# y)
    (f# h(x, y) -> f# x, f# g(x, y) -> f# x)
    (f# g(x, y) -> f# x, f# g(x, y) -> f# x)
    (f# g(x, y) -> f# x, f# g(x, y) -> f# y)
    (f# g(x, y) -> f# x, f# g(x, y) -> g#(f x, f y))
    (f# g(x, y) -> f# x, f# h(x, y) -> f# x)
    (f# g(x, y) -> f# x, f# h(x, y) -> f# y)
    (f# g(x, y) -> f# x, f# h(x, y) -> g#(h(y, f x), h(x, f y)))
    (f# g(x, y) -> f# y, f# g(x, y) -> f# x)
    (f# g(x, y) -> f# y, f# g(x, y) -> f# y)
    (f# g(x, y) -> f# y, f# g(x, y) -> g#(f x, f y))
    (f# g(x, y) -> f# y, f# h(x, y) -> f# x)
    (f# g(x, y) -> f# y, f# h(x, y) -> f# y)
    (f# g(x, y) -> f# y, f# h(x, y) -> g#(h(y, f x), h(x, f y)))}
   SCCS (1):
    Scc:
     {f# g(x, y) -> f# x,
      f# g(x, y) -> f# y,
      f# h(x, y) -> f# x,
      f# h(x, y) -> f# y}
    SCC (4):
     Strict:
      {f# g(x, y) -> f# x,
       f# g(x, y) -> f# y,
       f# h(x, y) -> f# x,
       f# h(x, y) -> f# y}
     Weak:
     {    f a() -> b(),
          f c() -> d(),
      f g(x, y) -> g(f x, f y),
      f h(x, y) -> g(h(y, f x), h(x, f y)),
        g(x, x) -> h(e(), x)}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f# g(x, y) -> f# x,
        f# g(x, y) -> f# y,
        f# h(x, y) -> f# y}
      EDG:
       {(f# h(x, y) -> f# y, f# h(x, y) -> f# y)
        (f# h(x, y) -> f# y, f# g(x, y) -> f# y)
        (f# h(x, y) -> f# y, f# g(x, y) -> f# x)
        (f# g(x, y) -> f# x, f# g(x, y) -> f# x)
        (f# g(x, y) -> f# x, f# g(x, y) -> f# y)
        (f# g(x, y) -> f# x, f# h(x, y) -> f# y)
        (f# g(x, y) -> f# y, f# g(x, y) -> f# x)
        (f# g(x, y) -> f# y, f# g(x, y) -> f# y)
        (f# g(x, y) -> f# y, f# h(x, y) -> f# y)}
       SCCS (1):
        Scc:
         {f# g(x, y) -> f# x,
          f# g(x, y) -> f# y,
          f# h(x, y) -> f# y}
        SCC (3):
         Strict:
          {f# g(x, y) -> f# x,
           f# g(x, y) -> f# y,
           f# h(x, y) -> f# y}
         Weak:
         {    f a() -> b(),
              f c() -> d(),
          f g(x, y) -> g(f x, f y),
          f h(x, y) -> g(h(y, f x), h(x, f y)),
            g(x, x) -> h(e(), x)}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {f# g(x, y) -> f# x,
            f# h(x, y) -> f# y}
          EDG:
           {(f# g(x, y) -> f# x, f# h(x, y) -> f# y)
            (f# g(x, y) -> f# x, f# g(x, y) -> f# x)
            (f# h(x, y) -> f# y, f# g(x, y) -> f# x)
            (f# h(x, y) -> f# y, f# h(x, y) -> f# y)}
           SCCS (1):
            Scc:
             {f# g(x, y) -> f# x,
              f# h(x, y) -> f# y}
            SCC (2):
             Strict:
              {f# g(x, y) -> f# x,
               f# h(x, y) -> f# y}
             Weak:
             {    f a() -> b(),
                  f c() -> d(),
              f g(x, y) -> g(f x, f y),
              f h(x, y) -> g(h(y, f x), h(x, f y)),
                g(x, x) -> h(e(), x)}
             SPSC:
              Simple Projection:
               pi(f#) = 0
              Strict:
               {f# h(x, y) -> f# y}
              EDG:
               {(f# h(x, y) -> f# y, f# h(x, y) -> f# y)}
               SCCS (1):
                Scc:
                 {f# h(x, y) -> f# y}
                SCC (1):
                 Strict:
                  {f# h(x, y) -> f# y}
                 Weak:
                 {    f a() -> b(),
                      f c() -> d(),
                  f g(x, y) -> g(f x, f y),
                  f h(x, y) -> g(h(y, f x), h(x, f y)),
                    g(x, x) -> h(e(), x)}
                 SPSC:
                  Simple Projection:
                   pi(f#) = 0
                  Strict:
                   {}
                  Qed