MAYBE

Problem:
 check(0()) -> zero()
 check(s(0())) -> odd()
 check(s(s(0()))) -> even()
 check(s(s(s(x)))) -> check(s(x))
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 times(x,y) -> timesIter(x,y,0())
 timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
 p(s(x)) -> x
 p(0()) -> 0()
 if(zero(),x,y,z,u) -> z
 if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
 if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))

Proof:
 DP Processor:
  DPs:
   check#(s(s(s(x)))) -> check#(s(x))
   half#(s(s(x))) -> half#(x)
   plus#(s(x),y) -> plus#(x,y)
   times#(x,y) -> timesIter#(x,y,0())
   timesIter#(x,y,z) -> plus#(z,y)
   timesIter#(x,y,z) -> check#(x)
   timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
   if#(odd(),x,y,z,u) -> p#(x)
   if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u)
   if#(even(),x,y,z,u) -> half#(s(z))
   if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z)))
   if#(even(),x,y,z,u) -> half#(z)
   if#(even(),x,y,z,u) -> half#(x)
   if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z))
   if#(even(),x,y,z,u) -> plus#(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
  TRS:
   check(0()) -> zero()
   check(s(0())) -> odd()
   check(s(s(0()))) -> even()
   check(s(s(s(x)))) -> check(s(x))
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   times(x,y) -> timesIter(x,y,0())
   timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
   p(s(x)) -> x
   p(0()) -> 0()
   if(zero(),x,y,z,u) -> z
   if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
   if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
  TDG Processor:
   DPs:
    check#(s(s(s(x)))) -> check#(s(x))
    half#(s(s(x))) -> half#(x)
    plus#(s(x),y) -> plus#(x,y)
    times#(x,y) -> timesIter#(x,y,0())
    timesIter#(x,y,z) -> plus#(z,y)
    timesIter#(x,y,z) -> check#(x)
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
    if#(odd(),x,y,z,u) -> p#(x)
    if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u)
    if#(even(),x,y,z,u) -> half#(s(z))
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z)))
    if#(even(),x,y,z,u) -> half#(z)
    if#(even(),x,y,z,u) -> half#(x)
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z))
    if#(even(),x,y,z,u) -> plus#(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
   TRS:
    check(0()) -> zero()
    check(s(0())) -> odd()
    check(s(s(0()))) -> even()
    check(s(s(s(x)))) -> check(s(x))
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    times(x,y) -> timesIter(x,y,0())
    timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
    p(s(x)) -> x
    p(0()) -> 0()
    if(zero(),x,y,z,u) -> z
    if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
    if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
   graph:
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z))) ->
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z))) ->
    timesIter#(x,y,z) -> check#(x)
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z))) ->
    timesIter#(x,y,z) -> plus#(z,y)
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z)) ->
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z)) ->
    timesIter#(x,y,z) -> check#(x)
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z)) ->
    timesIter#(x,y,z) -> plus#(z,y)
    if#(even(),x,y,z,u) -> plus#(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z)))) ->
    plus#(s(x),y) -> plus#(x,y)
    if#(even(),x,y,z,u) -> half#(s(z)) -> half#(s(s(x))) -> half#(x)
    if#(even(),x,y,z,u) -> half#(z) -> half#(s(s(x))) -> half#(x)
    if#(even(),x,y,z,u) -> half#(x) ->
    half#(s(s(x))) -> half#(x)
    if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u) ->
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
    if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u) ->
    timesIter#(x,y,z) -> check#(x)
    if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u) ->
    timesIter#(x,y,z) -> plus#(z,y)
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(even(),x,y,z,u) -> plus#(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z))
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(even(),x,y,z,u) -> half#(x)
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(even(),x,y,z,u) -> half#(z)
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z)))
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(even(),x,y,z,u) -> half#(s(z))
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u)
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y)) ->
    if#(odd(),x,y,z,u) -> p#(x)
    timesIter#(x,y,z) -> plus#(z,y) -> plus#(s(x),y) -> plus#(x,y)
    timesIter#(x,y,z) -> check#(x) ->
    check#(s(s(s(x)))) -> check#(s(x))
    times#(x,y) -> timesIter#(x,y,0()) ->
    timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
    times#(x,y) -> timesIter#(x,y,0()) ->
    timesIter#(x,y,z) -> check#(x)
    times#(x,y) -> timesIter#(x,y,0()) ->
    timesIter#(x,y,z) -> plus#(z,y)
    plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
    half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    check#(s(s(s(x)))) -> check#(s(x)) -> check#(s(s(s(x)))) -> check#(s(x))
   SCC Processor:
    #sccs: 4
    #rules: 7
    #arcs: 29/225
    DPs:
     if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(s(z)))
     timesIter#(x,y,z) -> if#(check(x),x,y,z,plus(z,y))
     if#(odd(),x,y,z,u) -> timesIter#(p(x),y,u)
     if#(even(),x,y,z,u) -> timesIter#(half(x),y,half(z))
    TRS:
     check(0()) -> zero()
     check(s(0())) -> odd()
     check(s(s(0()))) -> even()
     check(s(s(s(x)))) -> check(s(x))
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0())
     timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
     p(s(x)) -> x
     p(0()) -> 0()
     if(zero(),x,y,z,u) -> z
     if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
     if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
    Open
    
    DPs:
     half#(s(s(x))) -> half#(x)
    TRS:
     check(0()) -> zero()
     check(s(0())) -> odd()
     check(s(s(0()))) -> even()
     check(s(s(s(x)))) -> check(s(x))
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0())
     timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
     p(s(x)) -> x
     p(0()) -> 0()
     if(zero(),x,y,z,u) -> z
     if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
     if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
    Subterm Criterion Processor:
     simple projection:
      pi(half#) = 0
     problem:
      DPs:
       
      TRS:
       check(0()) -> zero()
       check(s(0())) -> odd()
       check(s(s(0()))) -> even()
       check(s(s(s(x)))) -> check(s(x))
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(x,y) -> timesIter(x,y,0())
       timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
       p(s(x)) -> x
       p(0()) -> 0()
       if(zero(),x,y,z,u) -> z
       if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
       if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
     Qed
    
    DPs:
     check#(s(s(s(x)))) -> check#(s(x))
    TRS:
     check(0()) -> zero()
     check(s(0())) -> odd()
     check(s(s(0()))) -> even()
     check(s(s(s(x)))) -> check(s(x))
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0())
     timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
     p(s(x)) -> x
     p(0()) -> 0()
     if(zero(),x,y,z,u) -> z
     if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
     if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
    Subterm Criterion Processor:
     simple projection:
      pi(check#) = 0
     problem:
      DPs:
       
      TRS:
       check(0()) -> zero()
       check(s(0())) -> odd()
       check(s(s(0()))) -> even()
       check(s(s(s(x)))) -> check(s(x))
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(x,y) -> timesIter(x,y,0())
       timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
       p(s(x)) -> x
       p(0()) -> 0()
       if(zero(),x,y,z,u) -> z
       if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
       if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
     Qed
    
    DPs:
     plus#(s(x),y) -> plus#(x,y)
    TRS:
     check(0()) -> zero()
     check(s(0())) -> odd()
     check(s(s(0()))) -> even()
     check(s(s(s(x)))) -> check(s(x))
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     times(x,y) -> timesIter(x,y,0())
     timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
     p(s(x)) -> x
     p(0()) -> 0()
     if(zero(),x,y,z,u) -> z
     if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
     if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       check(0()) -> zero()
       check(s(0())) -> odd()
       check(s(s(0()))) -> even()
       check(s(s(s(x)))) -> check(s(x))
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       times(x,y) -> timesIter(x,y,0())
       timesIter(x,y,z) -> if(check(x),x,y,z,plus(z,y))
       p(s(x)) -> x
       p(0()) -> 0()
       if(zero(),x,y,z,u) -> z
       if(odd(),x,y,z,u) -> timesIter(p(x),y,u)
       if(even(),x,y,z,u) -> plus(timesIter(half(x),y,half(z)),timesIter(half(x),y,half(s(z))))
     Qed