Problem TCT 09 ma6

YES(?,ELEMENTARY)

We consider the following Problem:

  Strict Trs:
    {  ite(tt(), u, v) -> u
     , ite(ff(), u, v) -> v
     , find(u, v, nil()) -> ff()
     , find(u, v, cons(cons(u, v), E)) -> tt()
     , find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
     , complete(u, nil(), E) -> tt()
     , complete(u, cons(v, S), E) ->
       ite(find(u, v, E), complete(u, S, E), ff())
     , clique(nil(), E) -> tt()
     , clique(cons(u, K), E) ->
       ite(complete(u, K, E), clique(K, E), ff())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,ELEMENTARY)

Proof:
  The input was oriented with the instance of
  Lightweight Multiset Path Order () as induced by the safe mapping
  
   safe(ite) = {1, 2}, safe(tt) = {}, safe(ff) = {}, safe(find) = {2},
   safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {},
   safe(clique) = {}
  
  and precedence
  
   complete > ite, complete > find, clique > ite, clique > complete .
  
  Following symbols are considered recursive:
  
   {ite, find, complete, clique}
  
  The recursion depth is 3 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  ite(v; tt(), u) -> u
      , ite(v; ff(), u) -> v
      , find(u, nil(); v) -> ff()
      , find(u, cons(; cons(; u, v), E); v) -> tt()
      , find(u, cons(; cons(; u2, v2), E); v) -> find(u, E; v)
      , complete(u, nil(), E;) -> tt()
      , complete(u, cons(; v, S), E;) ->
        ite(ff(); find(u, E; v), complete(u, S, E;))
      , clique(nil(), E;) -> tt()
      , clique(cons(; u, K), E;) ->
        ite(ff(); complete(u, K, E;), clique(K, E;))}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We consider the following Problem:

  Strict Trs:
    {  ite(tt(), u, v) -> u
     , ite(ff(), u, v) -> v
     , find(u, v, nil()) -> ff()
     , find(u, v, cons(cons(u, v), E)) -> tt()
     , find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
     , complete(u, nil(), E) -> tt()
     , complete(u, cons(v, S), E) ->
       ite(find(u, v, E), complete(u, S, E), ff())
     , clique(nil(), E) -> tt()
     , clique(cons(u, K), E) ->
       ite(complete(u, K, E), clique(K, E), ff())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,PRIMREC)

Proof:
  The input was oriented with the instance of
  'multiset path orders' as induced by the precedence
  
   find > tt, nil > tt, nil > ff, cons > ff, complete > ite,
   clique > ite, clique > complete, find ~ complete .

Hurray, we answered YES(?,PRIMREC)

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  ite(tt(), u, v) -> u
     , ite(ff(), u, v) -> v
     , find(u, v, nil()) -> ff()
     , find(u, v, cons(cons(u, v), E)) -> tt()
     , find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
     , complete(u, nil(), E) -> tt()
     , complete(u, cons(v, S), E) ->
       ite(find(u, v, E), complete(u, S, E), ff())
     , clique(nil(), E) -> tt()
     , clique(cons(u, K), E) ->
       ite(complete(u, K, E), clique(K, E), ff())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order () as induced by the safe mapping
  
   safe(ite) = {2}, safe(tt) = {}, safe(ff) = {}, safe(find) = {1, 2},
   safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {},
   safe(clique) = {}
  
  and precedence
  
   complete > ite, complete > find, clique > ite, clique > complete .
  
  Following symbols are considered recursive:
  
   {ite, find, complete, clique}
  
  The recursion depth is 3 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  ite(tt(), v; u) -> u
      , ite(ff(), v; u) -> v
      , find(nil(); u, v) -> ff()
      , find(cons(; cons(; u, v), E); u, v) -> tt()
      , find(cons(; cons(; u2, v2), E); u, v) -> find(E; u, v)
      , complete(u, nil(), E;) -> tt()
      , complete(u, cons(; v, S), E;) ->
        ite(find(E; u, v), ff(); complete(u, S, E;))
      , clique(nil(), E;) -> tt()
      , clique(cons(; u, K), E;) ->
        ite(complete(u, K, E;), ff(); clique(K, E;))}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

YES(?,POLY)

We consider the following Problem:

  Strict Trs:
    {  ite(tt(), u, v) -> u
     , ite(ff(), u, v) -> v
     , find(u, v, nil()) -> ff()
     , find(u, v, cons(cons(u, v), E)) -> tt()
     , find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
     , complete(u, nil(), E) -> tt()
     , complete(u, cons(v, S), E) ->
       ite(find(u, v, E), complete(u, S, E), ff())
     , clique(nil(), E) -> tt()
     , clique(cons(u, K), E) ->
       ite(complete(u, K, E), clique(K, E), ff())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,POLY)

Proof:
  The input was oriented with the instance of
  Polynomial Path Order (PS) as induced by the safe mapping
  
   safe(ite) = {2, 3}, safe(tt) = {}, safe(ff) = {}, safe(find) = {},
   safe(nil) = {}, safe(cons) = {1, 2}, safe(complete) = {},
   safe(clique) = {}
  
  and precedence
  
   complete > ite, complete > find, clique > ite, clique > complete .
  
  Following symbols are considered recursive:
  
   {ite, find, complete, clique}
  
  The recursion depth is 3 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  ite(tt(); u, v) -> u
      , ite(ff(); u, v) -> v
      , find(u, v, nil();) -> ff()
      , find(u, v, cons(; cons(; u, v), E);) -> tt()
      , find(u, v, cons(; cons(; u2, v2), E);) -> find(u, v, E;)
      , complete(u, nil(), E;) -> tt()
      , complete(u, cons(; v, S), E;) ->
        ite(find(u, v, E;); complete(u, S, E;), ff())
      , clique(nil(), E;) -> tt()
      , clique(cons(; u, K), E;) ->
        ite(complete(u, K, E;); clique(K, E;), ff())}
   Weak Trs  : {}

Hurray, we answered YES(?,POLY)

YES(?,O(n^3))

We consider the following Problem:

  Strict Trs:
    {  ite(tt(), u, v) -> u
     , ite(ff(), u, v) -> v
     , find(u, v, nil()) -> ff()
     , find(u, v, cons(cons(u, v), E)) -> tt()
     , find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
     , complete(u, nil(), E) -> tt()
     , complete(u, cons(v, S), E) ->
       ite(find(u, v, E), complete(u, S, E), ff())
     , clique(nil(), E) -> tt()
     , clique(cons(u, K), E) ->
       ite(complete(u, K, E), clique(K, E), ff())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^3))

Proof:
  The input was oriented with the instance of
  Small Polynomial Path Order (WSC) as induced by the safe mapping
  
   safe(ite) = {1, 2, 3}, safe(tt) = {}, safe(ff) = {},
   safe(find) = {1}, safe(nil) = {}, safe(cons) = {1, 2},
   safe(complete) = {}, safe(clique) = {}
  
  and precedence
  
   complete > ite, complete > find, clique > ite, clique > complete .
  
  Following symbols are considered recursive:
  
   {ite, find, complete, clique}
  
  The recursion depth is 3 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  ite(; tt(), u, v) -> u
      , ite(; ff(), u, v) -> v
      , find(v, nil(); u) -> ff()
      , find(v, cons(; cons(; u, v), E); u) -> tt()
      , find(v, cons(; cons(; u2, v2), E); u) -> find(v, E; u)
      , complete(u, nil(), E;) -> tt()
      , complete(u, cons(; v, S), E;) ->
        ite(; find(v, E; u), complete(u, S, E;), ff())
      , clique(nil(), E;) -> tt()
      , clique(cons(; u, K), E;) ->
        ite(; complete(u, K, E;), clique(K, E;), ff())}
   Weak Trs  : {}

Hurray, we answered YES(?,O(n^3))

YES(?,O(n^3))

We consider the following Problem:

  Strict Trs:
    {  ite(tt(), u, v) -> u
     , ite(ff(), u, v) -> v
     , find(u, v, nil()) -> ff()
     , find(u, v, cons(cons(u, v), E)) -> tt()
     , find(u, v, cons(cons(u2, v2), E)) -> find(u, v, E)
     , complete(u, nil(), E) -> tt()
     , complete(u, cons(v, S), E) ->
       ite(find(u, v, E), complete(u, S, E), ff())
     , clique(nil(), E) -> tt()
     , clique(cons(u, K), E) ->
       ite(complete(u, K, E), clique(K, E), ff())}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^3))

Proof:
  The input was oriented with the instance of
  Small Polynomial Path Order (WSC,
                             PS) as induced by the safe mapping
  
   safe(ite) = {1, 2, 3}, safe(tt) = {}, safe(ff) = {},
   safe(find) = {1, 2}, safe(nil) = {}, safe(cons) = {1, 2},
   safe(complete) = {1}, safe(clique) = {}
  
  and precedence
  
   complete > ite, complete > find, clique > ite, clique > complete .
  
  Following symbols are considered recursive:
  
   {ite, find, complete, clique}
  
  The recursion depth is 3 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  ite(; tt(), u, v) -> u
      , ite(; ff(), u, v) -> v
      , find(nil(); u, v) -> ff()
      , find(cons(; cons(; u, v), E); u, v) -> tt()
      , find(cons(; cons(; u2, v2), E); u, v) -> find(E; u, v)
      , complete(nil(), E; u) -> tt()
      , complete(cons(; v, S), E; u) ->
        ite(; find(E; u, v), complete(S, E; u), ff())
      , clique(nil(), E;) -> tt()
      , clique(cons(; u, K), E;) ->
        ite(; complete(K, E; u), clique(K, E;), ff())}
   Weak Trs  : {}

Hurray, we answered YES(?,O(n^3))