MAYBE

Problem:
 nonZero(0()) -> false()
 nonZero(s(x)) -> true()
 p(s(0())) -> 0()
 p(s(s(x))) -> s(p(s(x)))
 id_inc(x) -> x
 id_inc(x) -> s(x)
 random(x) -> rand(x,0())
 rand(x,y) -> if(nonZero(x),x,y)
 if(false(),x,y) -> y
 if(true(),x,y) -> rand(p(x),id_inc(y))

Proof:
 DP Processor:
  DPs:
   p#(s(s(x))) -> p#(s(x))
   random#(x) -> rand#(x,0())
   rand#(x,y) -> nonZero#(x)
   rand#(x,y) -> if#(nonZero(x),x,y)
   if#(true(),x,y) -> id_inc#(y)
   if#(true(),x,y) -> p#(x)
   if#(true(),x,y) -> rand#(p(x),id_inc(y))
  TRS:
   nonZero(0()) -> false()
   nonZero(s(x)) -> true()
   p(s(0())) -> 0()
   p(s(s(x))) -> s(p(s(x)))
   id_inc(x) -> x
   id_inc(x) -> s(x)
   random(x) -> rand(x,0())
   rand(x,y) -> if(nonZero(x),x,y)
   if(false(),x,y) -> y
   if(true(),x,y) -> rand(p(x),id_inc(y))
  TDG Processor:
   DPs:
    p#(s(s(x))) -> p#(s(x))
    random#(x) -> rand#(x,0())
    rand#(x,y) -> nonZero#(x)
    rand#(x,y) -> if#(nonZero(x),x,y)
    if#(true(),x,y) -> id_inc#(y)
    if#(true(),x,y) -> p#(x)
    if#(true(),x,y) -> rand#(p(x),id_inc(y))
   TRS:
    nonZero(0()) -> false()
    nonZero(s(x)) -> true()
    p(s(0())) -> 0()
    p(s(s(x))) -> s(p(s(x)))
    id_inc(x) -> x
    id_inc(x) -> s(x)
    random(x) -> rand(x,0())
    rand(x,y) -> if(nonZero(x),x,y)
    if(false(),x,y) -> y
    if(true(),x,y) -> rand(p(x),id_inc(y))
   graph:
    if#(true(),x,y) -> rand#(p(x),id_inc(y)) ->
    rand#(x,y) -> if#(nonZero(x),x,y)
    if#(true(),x,y) -> rand#(p(x),id_inc(y)) -> rand#(x,y) -> nonZero#(x)
    if#(true(),x,y) -> p#(x) -> p#(s(s(x))) -> p#(s(x))
    rand#(x,y) -> if#(nonZero(x),x,y) ->
    if#(true(),x,y) -> rand#(p(x),id_inc(y))
    rand#(x,y) -> if#(nonZero(x),x,y) -> if#(true(),x,y) -> p#(x)
    rand#(x,y) -> if#(nonZero(x),x,y) -> if#(true(),x,y) -> id_inc#(y)
    random#(x) -> rand#(x,0()) -> rand#(x,y) -> if#(nonZero(x),x,y)
    random#(x) -> rand#(x,0()) -> rand#(x,y) -> nonZero#(x)
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 9/49
    DPs:
     if#(true(),x,y) -> rand#(p(x),id_inc(y))
     rand#(x,y) -> if#(nonZero(x),x,y)
    TRS:
     nonZero(0()) -> false()
     nonZero(s(x)) -> true()
     p(s(0())) -> 0()
     p(s(s(x))) -> s(p(s(x)))
     id_inc(x) -> x
     id_inc(x) -> s(x)
     random(x) -> rand(x,0())
     rand(x,y) -> if(nonZero(x),x,y)
     if(false(),x,y) -> y
     if(true(),x,y) -> rand(p(x),id_inc(y))
    Open
    
    DPs:
     p#(s(s(x))) -> p#(s(x))
    TRS:
     nonZero(0()) -> false()
     nonZero(s(x)) -> true()
     p(s(0())) -> 0()
     p(s(s(x))) -> s(p(s(x)))
     id_inc(x) -> x
     id_inc(x) -> s(x)
     random(x) -> rand(x,0())
     rand(x,y) -> if(nonZero(x),x,y)
     if(false(),x,y) -> y
     if(true(),x,y) -> rand(p(x),id_inc(y))
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      TRS:
       nonZero(0()) -> false()
       nonZero(s(x)) -> true()
       p(s(0())) -> 0()
       p(s(s(x))) -> s(p(s(x)))
       id_inc(x) -> x
       id_inc(x) -> s(x)
       random(x) -> rand(x,0())
       rand(x,y) -> if(nonZero(x),x,y)
       if(false(),x,y) -> y
       if(true(),x,y) -> rand(p(x),id_inc(y))
     Qed