YES
Time: 0.040590
TRS:
 {     active f x -> mark x,
       active f x -> f active x,
         f mark x -> mark f x,
           f ok x -> ok f x,
        f found x -> found f x,
       top mark x -> top check x,
   top active c() -> top mark c(),
      top found x -> top active x,
          check x -> start match(f X(), x),
        check f x -> f check x,
       start ok x -> found x,
  match(f x, f y) -> f match(x, y),
    match(X(), x) -> proper x,
       proper f x -> f proper x,
       proper c() -> ok c()}
 DP:
  DP:
   {     active# f x -> active# x,
         active# f x -> f# active x,
           f# mark x -> f# x,
             f# ok x -> f# x,
          f# found x -> f# x,
         top# mark x -> top# check x,
         top# mark x -> check# x,
     top# active c() -> top# mark c(),
        top# found x -> active# x,
        top# found x -> top# active x,
            check# x -> f# X(),
            check# x -> start# match(f X(), x),
            check# x -> match#(f X(), x),
          check# f x -> f# check x,
          check# f x -> check# x,
    match#(f x, f y) -> f# match(x, y),
    match#(f x, f y) -> match#(x, y),
      match#(X(), x) -> proper# x,
         proper# f x -> f# proper x,
         proper# f x -> proper# x}
  TRS:
  {     active f x -> mark x,
        active f x -> f active x,
          f mark x -> mark f x,
            f ok x -> ok f x,
         f found x -> found f x,
        top mark x -> top check x,
    top active c() -> top mark c(),
       top found x -> top active x,
           check x -> start match(f X(), x),
         check f x -> f check x,
        start ok x -> found x,
   match(f x, f y) -> f match(x, y),
     match(X(), x) -> proper x,
        proper f x -> f proper x,
        proper c() -> ok c()}
  EDG:
   {(top# mark x -> top# check x, top# found x -> top# active x)
    (top# mark x -> top# check x, top# found x -> active# x)
    (top# mark x -> top# check x, top# mark x -> check# x)
    (top# mark x -> top# check x, top# mark x -> top# check x)
    (check# f x -> f# check x, f# found x -> f# x)
    (check# f x -> f# check x, f# ok x -> f# x)
    (check# f x -> f# check x, f# mark x -> f# x)
    (check# x -> match#(f X(), x), match#(f x, f y) -> match#(x, y))
    (check# x -> match#(f X(), x), match#(f x, f y) -> f# match(x, y))
    (match#(f x, f y) -> f# match(x, y), f# found x -> f# x)
    (match#(f x, f y) -> f# match(x, y), f# ok x -> f# x)
    (match#(f x, f y) -> f# match(x, y), f# mark x -> f# x)
    (active# f x -> active# x, active# f x -> f# active x)
    (active# f x -> active# x, active# f x -> active# x)
    (f# ok x -> f# x, f# found x -> f# x)
    (f# ok x -> f# x, f# ok x -> f# x)
    (f# ok x -> f# x, f# mark x -> f# x)
    (top# mark x -> check# x, check# f x -> check# x)
    (top# mark x -> check# x, check# f x -> f# check x)
    (top# mark x -> check# x, check# x -> match#(f X(), x))
    (top# mark x -> check# x, check# x -> start# match(f X(), x))
    (top# mark x -> check# x, check# x -> f# X())
    (check# f x -> check# x, check# f x -> check# x)
    (check# f x -> check# x, check# f x -> f# check x)
    (check# f x -> check# x, check# x -> match#(f X(), x))
    (check# f x -> check# x, check# x -> start# match(f X(), x))
    (check# f x -> check# x, check# x -> f# X())
    (proper# f x -> proper# x, proper# f x -> proper# x)
    (proper# f x -> proper# x, proper# f x -> f# proper x)
    (match#(f x, f y) -> match#(x, y), match#(X(), x) -> proper# x)
    (match#(f x, f y) -> match#(x, y), match#(f x, f y) -> match#(x, y))
    (match#(f x, f y) -> match#(x, y), match#(f x, f y) -> f# match(x, y))
    (match#(X(), x) -> proper# x, proper# f x -> f# proper x)
    (match#(X(), x) -> proper# x, proper# f x -> proper# x)
    (top# found x -> active# x, active# f x -> active# x)
    (top# found x -> active# x, active# f x -> f# active x)
    (f# found x -> f# x, f# mark x -> f# x)
    (f# found x -> f# x, f# ok x -> f# x)
    (f# found x -> f# x, f# found x -> f# x)
    (f# mark x -> f# x, f# mark x -> f# x)
    (f# mark x -> f# x, f# ok x -> f# x)
    (f# mark x -> f# x, f# found x -> f# x)
    (top# active c() -> top# mark c(), top# mark x -> top# check x)
    (top# active c() -> top# mark c(), top# mark x -> check# x)
    (proper# f x -> f# proper x, f# mark x -> f# x)
    (proper# f x -> f# proper x, f# ok x -> f# x)
    (proper# f x -> f# proper x, f# found x -> f# x)
    (top# found x -> top# active x, top# mark x -> top# check x)
    (top# found x -> top# active x, top# mark x -> check# x)
    (top# found x -> top# active x, top# active c() -> top# mark c())
    (top# found x -> top# active x, top# found x -> active# x)
    (top# found x -> top# active x, top# found x -> top# active x)
    (active# f x -> f# active x, f# mark x -> f# x)
    (active# f x -> f# active x, f# ok x -> f# x)
    (active# f x -> f# active x, f# found x -> f# x)}
   SCCS (6):
    Scc:
     {proper# f x -> proper# x}
    Scc:
     {match#(f x, f y) -> match#(x, y)}
    Scc:
     {check# f x -> check# x}
    Scc:
     {    top# mark x -> top# check x,
      top# active c() -> top# mark c(),
         top# found x -> top# active x}
    Scc:
     { f# mark x -> f# x,
         f# ok x -> f# x,
      f# found x -> f# x}
    Scc:
     {active# f x -> active# x}
    SCC (1):
     Strict:
      {proper# f x -> proper# x}
     Weak:
     {     active f x -> mark x,
           active f x -> f active x,
             f mark x -> mark f x,
               f ok x -> ok f x,
            f found x -> found f x,
           top mark x -> top check x,
       top active c() -> top mark c(),
          top found x -> top active x,
              check x -> start match(f X(), x),
            check f x -> f check x,
           start ok x -> found x,
      match(f x, f y) -> f match(x, y),
        match(X(), x) -> proper x,
           proper f x -> f proper x,
           proper c() -> ok c()}
     SPSC:
      Simple Projection:
       pi(proper#) = 0
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {match#(f x, f y) -> match#(x, y)}
     Weak:
     {     active f x -> mark x,
           active f x -> f active x,
             f mark x -> mark f x,
               f ok x -> ok f x,
            f found x -> found f x,
           top mark x -> top check x,
       top active c() -> top mark c(),
          top found x -> top active x,
              check x -> start match(f X(), x),
            check f x -> f check x,
           start ok x -> found x,
      match(f x, f y) -> f match(x, y),
        match(X(), x) -> proper x,
           proper f x -> f proper x,
           proper c() -> ok c()}
     SPSC:
      Simple Projection:
       pi(match#) = 1
      Strict:
       {}
      Qed
    SCC (1):
     Strict:
      {check# f x -> check# x}
     Weak:
     {     active f x -> mark x,
           active f x -> f active x,
             f mark x -> mark f x,
               f ok x -> ok f x,
            f found x -> found f x,
           top mark x -> top check x,
       top active c() -> top mark c(),
          top found x -> top active x,
              check x -> start match(f X(), x),
            check f x -> f check x,
           start ok x -> found x,
      match(f x, f y) -> f match(x, y),
        match(X(), x) -> proper x,
           proper f x -> f proper x,
           proper c() -> ok c()}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {}
      Qed
    SCC (3):
     Strict:
      {    top# mark x -> top# check x,
       top# active c() -> top# mark c(),
          top# found x -> top# active x}
     Weak:
     {     active f x -> mark x,
           active f x -> f active x,
             f mark x -> mark f x,
               f ok x -> ok f x,
            f found x -> found f x,
           top mark x -> top check x,
       top active c() -> top mark c(),
          top found x -> top active x,
              check x -> start match(f X(), x),
            check f x -> f check x,
           start ok x -> found x,
      match(f x, f y) -> f match(x, y),
        match(X(), x) -> proper x,
           proper f x -> f proper x,
           proper c() -> ok c()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [match](x0, x1) = x0,
       
       [mark](x0) = 0,
       
       [active](x0) = x0,
       
       [f](x0) = 0,
       
       [top](x0) = x0 + 1,
       
       [check](x0) = 0,
       
       [start](x0) = x0,
       
       [proper](x0) = 1,
       
       [ok](x0) = x0,
       
       [found](x0) = x0,
       
       [c] = 1,
       
       [X] = 1,
       
       [top#](x0) = x0
      Strict:
       top# found x -> top# active x
       0 + 1x >= 0 + 1x
       top# active c() -> top# mark c()
       1 >= 0
       top# mark x -> top# check x
       0 + 0x >= 0 + 0x
      Weak:
       
     EDG:
      {(top# found x -> top# active x, top# found x -> top# active x)
       (top# found x -> top# active x, top# mark x -> top# check x)
       (top# mark x -> top# check x, top# mark x -> top# check x)
       (top# mark x -> top# check x, top# found x -> top# active x)}
      SCCS (1):
       Scc:
        { top# mark x -> top# check x,
         top# found x -> top# active x}
       SCC (2):
        Strict:
         { top# mark x -> top# check x,
          top# found x -> top# active x}
        Weak:
        {     active f x -> mark x,
              active f x -> f active x,
                f mark x -> mark f x,
                  f ok x -> ok f x,
               f found x -> found f x,
              top mark x -> top check x,
          top active c() -> top mark c(),
             top found x -> top active x,
                 check x -> start match(f X(), x),
               check f x -> f check x,
              start ok x -> found x,
         match(f x, f y) -> f match(x, y),
           match(X(), x) -> proper x,
              proper f x -> f proper x,
              proper c() -> ok c()}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [match](x0, x1) = x0,
          
          [mark](x0) = x0 + 1,
          
          [active](x0) = x0,
          
          [f](x0) = x0 + 1,
          
          [top](x0) = x0 + 1,
          
          [check](x0) = x0 + 1,
          
          [start](x0) = x0 + 1,
          
          [proper](x0) = x0,
          
          [ok](x0) = x0,
          
          [found](x0) = x0 + 1,
          
          [c] = 1,
          
          [X] = 0,
          
          [top#](x0) = x0
         Strict:
          top# found x -> top# active x
          1 + 1x >= 0 + 1x
          top# mark x -> top# check x
          1 + 1x >= 1 + 1x
         Weak:
          
        EDG:
         {(top# mark x -> top# check x, top# mark x -> top# check x)}
         SCCS (1):
          Scc:
           {top# mark x -> top# check x}
          SCC (1):
           Strict:
            {top# mark x -> top# check x}
           Weak:
           {     active f x -> mark x,
                 active f x -> f active x,
                   f mark x -> mark f x,
                     f ok x -> ok f x,
                  f found x -> found f x,
                 top mark x -> top check x,
             top active c() -> top mark c(),
                top found x -> top active x,
                    check x -> start match(f X(), x),
                  check f x -> f check x,
                 start ok x -> found x,
            match(f x, f y) -> f match(x, y),
              match(X(), x) -> proper x,
                 proper f x -> f proper x,
                 proper c() -> ok c()}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [match](x0, x1) = 0,
             
             [mark](x0) = 1,
             
             [active](x0) = 0,
             
             [f](x0) = x0,
             
             [top](x0) = x0 + 1,
             
             [check](x0) = 0,
             
             [start](x0) = 0,
             
             [proper](x0) = 0,
             
             [ok](x0) = 0,
             
             [found](x0) = 0,
             
             [c] = 0,
             
             [X] = 0,
             
             [top#](x0) = x0 + 1
            Strict:
             top# mark x -> top# check x
             2 + 0x >= 1 + 0x
            Weak:
             
           Qed
  SCC (3):
   Strict:
    { f# mark x -> f# x,
        f# ok x -> f# x,
     f# found x -> f# x}
   Weak:
   {     active f x -> mark x,
         active f x -> f active x,
           f mark x -> mark f x,
             f ok x -> ok f x,
          f found x -> found f x,
         top mark x -> top check x,
     top active c() -> top mark c(),
        top found x -> top active x,
            check x -> start match(f X(), x),
          check f x -> f check x,
         start ok x -> found x,
    match(f x, f y) -> f match(x, y),
      match(X(), x) -> proper x,
         proper f x -> f proper x,
         proper c() -> ok c()}
   SPSC:
    Simple Projection:
     pi(f#) = 0
    Strict:
     { f# mark x -> f# x,
      f# found x -> f# x}
    EDG:
     {(f# found x -> f# x, f# found x -> f# x)
      (f# found x -> f# x, f# mark x -> f# x)
      (f# mark x -> f# x, f# mark x -> f# x)
      (f# mark x -> f# x, f# found x -> f# x)}
     SCCS (1):
      Scc:
       { f# mark x -> f# x,
        f# found x -> f# x}
      SCC (2):
       Strict:
        { f# mark x -> f# x,
         f# found x -> f# x}
       Weak:
       {     active f x -> mark x,
             active f x -> f active x,
               f mark x -> mark f x,
                 f ok x -> ok f x,
              f found x -> found f x,
             top mark x -> top check x,
         top active c() -> top mark c(),
            top found x -> top active x,
                check x -> start match(f X(), x),
              check f x -> f check x,
             start ok x -> found x,
        match(f x, f y) -> f match(x, y),
          match(X(), x) -> proper x,
             proper f x -> f proper x,
             proper c() -> ok c()}
       SPSC:
        Simple Projection:
         pi(f#) = 0
        Strict:
         {f# found x -> f# x}
        EDG:
         {(f# found x -> f# x, f# found x -> f# x)}
         SCCS (1):
          Scc:
           {f# found x -> f# x}
          SCC (1):
           Strict:
            {f# found x -> f# x}
           Weak:
           {     active f x -> mark x,
                 active f x -> f active x,
                   f mark x -> mark f x,
                     f ok x -> ok f x,
                  f found x -> found f x,
                 top mark x -> top check x,
             top active c() -> top mark c(),
                top found x -> top active x,
                    check x -> start match(f X(), x),
                  check f x -> f check x,
                 start ok x -> found x,
            match(f x, f y) -> f match(x, y),
              match(X(), x) -> proper x,
                 proper f x -> f proper x,
                 proper c() -> ok c()}
           SPSC:
            Simple Projection:
             pi(f#) = 0
            Strict:
             {}
            Qed
  SCC (1):
   Strict:
    {active# f x -> active# x}
   Weak:
   {     active f x -> mark x,
         active f x -> f active x,
           f mark x -> mark f x,
             f ok x -> ok f x,
          f found x -> found f x,
         top mark x -> top check x,
     top active c() -> top mark c(),
        top found x -> top active x,
            check x -> start match(f X(), x),
          check f x -> f check x,
         start ok x -> found x,
    match(f x, f y) -> f match(x, y),
      match(X(), x) -> proper x,
         proper f x -> f proper x,
         proper c() -> ok c()}
   SPSC:
    Simple Projection:
     pi(active#) = 0
    Strict:
     {}
    Qed