MAYBE

Problem:
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 inc(0()) -> 0()
 inc(s(x)) -> s(inc(x))
 zero(0()) -> true()
 zero(s(x)) -> false()
 p(0()) -> 0()
 p(s(x)) -> x
 bits(x) -> bitIter(x,0())
 bitIter(x,y) -> if(zero(x),x,inc(y))
 if(true(),x,y) -> p(y)
 if(false(),x,y) -> bitIter(half(x),y)

Proof:
 DP Processor:
  DPs:
   half#(s(s(x))) -> half#(x)
   inc#(s(x)) -> inc#(x)
   bits#(x) -> bitIter#(x,0())
   bitIter#(x,y) -> inc#(y)
   bitIter#(x,y) -> zero#(x)
   bitIter#(x,y) -> if#(zero(x),x,inc(y))
   if#(true(),x,y) -> p#(y)
   if#(false(),x,y) -> half#(x)
   if#(false(),x,y) -> bitIter#(half(x),y)
  TRS:
   half(0()) -> 0()
   half(s(0())) -> 0()
   half(s(s(x))) -> s(half(x))
   inc(0()) -> 0()
   inc(s(x)) -> s(inc(x))
   zero(0()) -> true()
   zero(s(x)) -> false()
   p(0()) -> 0()
   p(s(x)) -> x
   bits(x) -> bitIter(x,0())
   bitIter(x,y) -> if(zero(x),x,inc(y))
   if(true(),x,y) -> p(y)
   if(false(),x,y) -> bitIter(half(x),y)
  Usable Rule Processor:
   DPs:
    half#(s(s(x))) -> half#(x)
    inc#(s(x)) -> inc#(x)
    bits#(x) -> bitIter#(x,0())
    bitIter#(x,y) -> inc#(y)
    bitIter#(x,y) -> zero#(x)
    bitIter#(x,y) -> if#(zero(x),x,inc(y))
    if#(true(),x,y) -> p#(y)
    if#(false(),x,y) -> half#(x)
    if#(false(),x,y) -> bitIter#(half(x),y)
   TRS:
    f18(x,y) -> x
    f18(x,y) -> y
    inc(0()) -> 0()
    inc(s(x)) -> s(inc(x))
    zero(0()) -> true()
    zero(s(x)) -> false()
    half(0()) -> 0()
    half(s(0())) -> 0()
    half(s(s(x))) -> s(half(x))
   EDG Processor:
    DPs:
     half#(s(s(x))) -> half#(x)
     inc#(s(x)) -> inc#(x)
     bits#(x) -> bitIter#(x,0())
     bitIter#(x,y) -> inc#(y)
     bitIter#(x,y) -> zero#(x)
     bitIter#(x,y) -> if#(zero(x),x,inc(y))
     if#(true(),x,y) -> p#(y)
     if#(false(),x,y) -> half#(x)
     if#(false(),x,y) -> bitIter#(half(x),y)
    TRS:
     f18(x,y) -> x
     f18(x,y) -> y
     inc(0()) -> 0()
     inc(s(x)) -> s(inc(x))
     zero(0()) -> true()
     zero(s(x)) -> false()
     half(0()) -> 0()
     half(s(0())) -> 0()
     half(s(s(x))) -> s(half(x))
    graph:
     if#(false(),x,y) -> bitIter#(half(x),y) ->
     bitIter#(x,y) -> inc#(y)
     if#(false(),x,y) -> bitIter#(half(x),y) ->
     bitIter#(x,y) -> zero#(x)
     if#(false(),x,y) -> bitIter#(half(x),y) ->
     bitIter#(x,y) -> if#(zero(x),x,inc(y))
     if#(false(),x,y) -> half#(x) ->
     half#(s(s(x))) -> half#(x)
     bitIter#(x,y) -> if#(zero(x),x,inc(y)) ->
     if#(true(),x,y) -> p#(y)
     bitIter#(x,y) -> if#(zero(x),x,inc(y)) ->
     if#(false(),x,y) -> half#(x)
     bitIter#(x,y) -> if#(zero(x),x,inc(y)) ->
     if#(false(),x,y) -> bitIter#(half(x),y)
     bitIter#(x,y) -> inc#(y) -> inc#(s(x)) -> inc#(x)
     bits#(x) -> bitIter#(x,0()) -> bitIter#(x,y) -> inc#(y)
     bits#(x) -> bitIter#(x,0()) -> bitIter#(x,y) -> zero#(x)
     bits#(x) -> bitIter#(x,0()) -> bitIter#(x,y) -> if#(zero(x),x,inc(y))
     inc#(s(x)) -> inc#(x) -> inc#(s(x)) -> inc#(x)
     half#(s(s(x))) -> half#(x) -> half#(s(s(x))) -> half#(x)
    Restore Modifier:
     DPs:
      half#(s(s(x))) -> half#(x)
      inc#(s(x)) -> inc#(x)
      bits#(x) -> bitIter#(x,0())
      bitIter#(x,y) -> inc#(y)
      bitIter#(x,y) -> zero#(x)
      bitIter#(x,y) -> if#(zero(x),x,inc(y))
      if#(true(),x,y) -> p#(y)
      if#(false(),x,y) -> half#(x)
      if#(false(),x,y) -> bitIter#(half(x),y)
     TRS:
      half(0()) -> 0()
      half(s(0())) -> 0()
      half(s(s(x))) -> s(half(x))
      inc(0()) -> 0()
      inc(s(x)) -> s(inc(x))
      zero(0()) -> true()
      zero(s(x)) -> false()
      p(0()) -> 0()
      p(s(x)) -> x
      bits(x) -> bitIter(x,0())
      bitIter(x,y) -> if(zero(x),x,inc(y))
      if(true(),x,y) -> p(y)
      if(false(),x,y) -> bitIter(half(x),y)
     SCC Processor:
      #sccs: 3
      #rules: 4
      #arcs: 13/81
      DPs:
       if#(false(),x,y) -> bitIter#(half(x),y)
       bitIter#(x,y) -> if#(zero(x),x,inc(y))
      TRS:
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       inc(0()) -> 0()
       inc(s(x)) -> s(inc(x))
       zero(0()) -> true()
       zero(s(x)) -> false()
       p(0()) -> 0()
       p(s(x)) -> x
       bits(x) -> bitIter(x,0())
       bitIter(x,y) -> if(zero(x),x,inc(y))
       if(true(),x,y) -> p(y)
       if(false(),x,y) -> bitIter(half(x),y)
      Open
      
      DPs:
       inc#(s(x)) -> inc#(x)
      TRS:
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       inc(0()) -> 0()
       inc(s(x)) -> s(inc(x))
       zero(0()) -> true()
       zero(s(x)) -> false()
       p(0()) -> 0()
       p(s(x)) -> x
       bits(x) -> bitIter(x,0())
       bitIter(x,y) -> if(zero(x),x,inc(y))
       if(true(),x,y) -> p(y)
       if(false(),x,y) -> bitIter(half(x),y)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [inc#](x0) = x0 + 1,
        
        [if](x0, x1, x2) = x2,
        
        [bitIter](x0, x1) = x1,
        
        [bits](x0) = 1,
        
        [p](x0) = x0,
        
        [false] = 0,
        
        [true] = 0,
        
        [zero](x0) = 0,
        
        [inc](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [half](x0) = x0,
        
        [0] = 0
       orientation:
        inc#(s(x)) = x + 2 >= x + 1 = inc#(x)
        
        half(0()) = 0 >= 0 = 0()
        
        half(s(0())) = 1 >= 0 = 0()
        
        half(s(s(x))) = x + 2 >= x + 1 = s(half(x))
        
        inc(0()) = 0 >= 0 = 0()
        
        inc(s(x)) = x + 1 >= x + 1 = s(inc(x))
        
        zero(0()) = 0 >= 0 = true()
        
        zero(s(x)) = 0 >= 0 = false()
        
        p(0()) = 0 >= 0 = 0()
        
        p(s(x)) = x + 1 >= x = x
        
        bits(x) = 1 >= 0 = bitIter(x,0())
        
        bitIter(x,y) = y >= y = if(zero(x),x,inc(y))
        
        if(true(),x,y) = y >= y = p(y)
        
        if(false(),x,y) = y >= y = bitIter(half(x),y)
       problem:
        DPs:
         
        TRS:
         half(0()) -> 0()
         half(s(0())) -> 0()
         half(s(s(x))) -> s(half(x))
         inc(0()) -> 0()
         inc(s(x)) -> s(inc(x))
         zero(0()) -> true()
         zero(s(x)) -> false()
         p(0()) -> 0()
         p(s(x)) -> x
         bits(x) -> bitIter(x,0())
         bitIter(x,y) -> if(zero(x),x,inc(y))
         if(true(),x,y) -> p(y)
         if(false(),x,y) -> bitIter(half(x),y)
       Qed
      
      DPs:
       half#(s(s(x))) -> half#(x)
      TRS:
       half(0()) -> 0()
       half(s(0())) -> 0()
       half(s(s(x))) -> s(half(x))
       inc(0()) -> 0()
       inc(s(x)) -> s(inc(x))
       zero(0()) -> true()
       zero(s(x)) -> false()
       p(0()) -> 0()
       p(s(x)) -> x
       bits(x) -> bitIter(x,0())
       bitIter(x,y) -> if(zero(x),x,inc(y))
       if(true(),x,y) -> p(y)
       if(false(),x,y) -> bitIter(half(x),y)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [half#](x0) = x0,
        
        [if](x0, x1, x2) = x2,
        
        [bitIter](x0, x1) = x1,
        
        [bits](x0) = 1,
        
        [p](x0) = x0,
        
        [false] = 0,
        
        [true] = 0,
        
        [zero](x0) = 0,
        
        [inc](x0) = x0,
        
        [s](x0) = x0 + 1,
        
        [half](x0) = x0,
        
        [0] = 1
       orientation:
        half#(s(s(x))) = x + 2 >= x = half#(x)
        
        half(0()) = 1 >= 1 = 0()
        
        half(s(0())) = 2 >= 1 = 0()
        
        half(s(s(x))) = x + 2 >= x + 1 = s(half(x))
        
        inc(0()) = 1 >= 1 = 0()
        
        inc(s(x)) = x + 1 >= x + 1 = s(inc(x))
        
        zero(0()) = 0 >= 0 = true()
        
        zero(s(x)) = 0 >= 0 = false()
        
        p(0()) = 1 >= 1 = 0()
        
        p(s(x)) = x + 1 >= x = x
        
        bits(x) = 1 >= 1 = bitIter(x,0())
        
        bitIter(x,y) = y >= y = if(zero(x),x,inc(y))
        
        if(true(),x,y) = y >= y = p(y)
        
        if(false(),x,y) = y >= y = bitIter(half(x),y)
       problem:
        DPs:
         
        TRS:
         half(0()) -> 0()
         half(s(0())) -> 0()
         half(s(s(x))) -> s(half(x))
         inc(0()) -> 0()
         inc(s(x)) -> s(inc(x))
         zero(0()) -> true()
         zero(s(x)) -> false()
         p(0()) -> 0()
         p(s(x)) -> x
         bits(x) -> bitIter(x,0())
         bitIter(x,y) -> if(zero(x),x,inc(y))
         if(true(),x,y) -> p(y)
         if(false(),x,y) -> bitIter(half(x),y)
       Qed