YES
Time: 0.001760
TRS:
 {                f 0() -> true(),
                  f 1() -> false(),
                  f s x -> f x,
   if(true(), s x, s y) -> s x,
  if(false(), s x, s y) -> s y,
              g(x, c y) -> c g(x, y),
              g(x, c y) -> g(x, if(f x, c g(s x, y), c y))}
 DP:
  DP:
   {    f# s x -> f# x,
    g#(x, c y) -> f# x,
    g#(x, c y) -> if#(f x, c g(s x, y), c y),
    g#(x, c y) -> g#(x, y),
    g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)),
    g#(x, c y) -> g#(s x, y)}
  TRS:
  {                f 0() -> true(),
                   f 1() -> false(),
                   f s x -> f x,
    if(true(), s x, s y) -> s x,
   if(false(), s x, s y) -> s y,
               g(x, c y) -> c g(x, y),
               g(x, c y) -> g(x, if(f x, c g(s x, y), c y))}
  EDG:
   {(g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(s x, y))
    (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)))
    (g#(x, c y) -> g#(x, y), g#(x, c y) -> g#(x, y))
    (g#(x, c y) -> g#(x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y))
    (g#(x, c y) -> g#(x, y), g#(x, c y) -> f# x)
    (f# s x -> f# x, f# s x -> f# x)
    (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(s x, y))
    (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, if(f x, c g(s x, y), c y)))
    (g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(x, y))
    (g#(x, c y) -> g#(s x, y), g#(x, c y) -> if#(f x, c g(s x, y), c y))
    (g#(x, c y) -> g#(s x, y), g#(x, c y) -> f# x)
    (g#(x, c y) -> f# x, f# s x -> f# x)}
   SCCS (2):
    Scc:
     {g#(x, c y) -> g#(x, y),
      g#(x, c y) -> g#(s x, y)}
    Scc:
     {f# s x -> f# x}
    SCC (2):
     Strict:
      {g#(x, c y) -> g#(x, y),
       g#(x, c y) -> g#(s x, y)}
     Weak:
     {                f 0() -> true(),
                      f 1() -> false(),
                      f s x -> f x,
       if(true(), s x, s y) -> s x,
      if(false(), s x, s y) -> s y,
                  g(x, c y) -> c g(x, y),
                  g(x, c y) -> g(x, if(f x, c g(s x, y), c y))}
     SPSC:
      Simple Projection:
       pi(g#) = 1
      Strict:
       {g#(x, c y) -> g#(s x, y)}
      EDG:
       {(g#(x, c y) -> g#(s x, y), g#(x, c y) -> g#(s x, y))}
       SCCS (1):
        Scc:
         {g#(x, c y) -> g#(s x, y)}
        SCC (1):
         Strict:
          {g#(x, c y) -> g#(s x, y)}
         Weak:
         {                f 0() -> true(),
                          f 1() -> false(),
                          f s x -> f x,
           if(true(), s x, s y) -> s x,
          if(false(), s x, s y) -> s y,
                      g(x, c y) -> c g(x, y),
                      g(x, c y) -> g(x, if(f x, c g(s x, y), c y))}
         SPSC:
          Simple Projection:
           pi(g#) = 1
          Strict:
           {}
          Qed
    SCC (1):
     Strict:
      {f# s x -> f# x}
     Weak:
     {                f 0() -> true(),
                      f 1() -> false(),
                      f s x -> f x,
       if(true(), s x, s y) -> s x,
      if(false(), s x, s y) -> s y,
                  g(x, c y) -> c g(x, y),
                  g(x, c y) -> g(x, if(f x, c g(s x, y), c y))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {}
      Qed