MAYBE

Problem:
 le(0(),y) -> true()
 le(s(x),0()) -> false()
 le(s(x),s(y)) -> le(x,y)
 mod(x,0()) -> modZeroErro()
 mod(x,s(y)) -> modIter(x,s(y),0(),0())
 modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
 if(true(),x,y,z,u) -> u
 if(false(),x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
 if2(false(),x,y,z,u) -> modIter(x,y,z,u)
 if2(true(),x,y,z,u) -> modIter(x,y,z,0())

Proof:
 DP Processor:
  DPs:
   le#(s(x),s(y)) -> le#(x,y)
   mod#(x,s(y)) -> modIter#(x,s(y),0(),0())
   modIter#(x,s(y),z,u) -> le#(x,z)
   modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u)
   if#(false(),x,y,z,u) -> le#(y,s(u))
   if#(false(),x,y,z,u) -> if2#(le(y,s(u)),x,y,s(z),s(u))
   if2#(false(),x,y,z,u) -> modIter#(x,y,z,u)
   if2#(true(),x,y,z,u) -> modIter#(x,y,z,0())
  TRS:
   le(0(),y) -> true()
   le(s(x),0()) -> false()
   le(s(x),s(y)) -> le(x,y)
   mod(x,0()) -> modZeroErro()
   mod(x,s(y)) -> modIter(x,s(y),0(),0())
   modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
   if(true(),x,y,z,u) -> u
   if(false(),x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
   if2(false(),x,y,z,u) -> modIter(x,y,z,u)
   if2(true(),x,y,z,u) -> modIter(x,y,z,0())
  TDG Processor:
   DPs:
    le#(s(x),s(y)) -> le#(x,y)
    mod#(x,s(y)) -> modIter#(x,s(y),0(),0())
    modIter#(x,s(y),z,u) -> le#(x,z)
    modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u)
    if#(false(),x,y,z,u) -> le#(y,s(u))
    if#(false(),x,y,z,u) -> if2#(le(y,s(u)),x,y,s(z),s(u))
    if2#(false(),x,y,z,u) -> modIter#(x,y,z,u)
    if2#(true(),x,y,z,u) -> modIter#(x,y,z,0())
   TRS:
    le(0(),y) -> true()
    le(s(x),0()) -> false()
    le(s(x),s(y)) -> le(x,y)
    mod(x,0()) -> modZeroErro()
    mod(x,s(y)) -> modIter(x,s(y),0(),0())
    modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
    if(true(),x,y,z,u) -> u
    if(false(),x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
    if2(false(),x,y,z,u) -> modIter(x,y,z,u)
    if2(true(),x,y,z,u) -> modIter(x,y,z,0())
   graph:
    if2#(false(),x,y,z,u) -> modIter#(x,y,z,u) ->
    modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u)
    if2#(false(),x,y,z,u) -> modIter#(x,y,z,u) ->
    modIter#(x,s(y),z,u) -> le#(x,z)
    if2#(true(),x,y,z,u) -> modIter#(x,y,z,0()) ->
    modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u)
    if2#(true(),x,y,z,u) -> modIter#(x,y,z,0()) ->
    modIter#(x,s(y),z,u) -> le#(x,z)
    if#(false(),x,y,z,u) -> if2#(le(y,s(u)),x,y,s(z),s(u)) ->
    if2#(true(),x,y,z,u) -> modIter#(x,y,z,0())
    if#(false(),x,y,z,u) -> if2#(le(y,s(u)),x,y,s(z),s(u)) ->
    if2#(false(),x,y,z,u) -> modIter#(x,y,z,u)
    if#(false(),x,y,z,u) -> le#(y,s(u)) ->
    le#(s(x),s(y)) -> le#(x,y)
    modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u) ->
    if#(false(),x,y,z,u) -> if2#(le(y,s(u)),x,y,s(z),s(u))
    modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u) ->
    if#(false(),x,y,z,u) -> le#(y,s(u))
    modIter#(x,s(y),z,u) -> le#(x,z) ->
    le#(s(x),s(y)) -> le#(x,y)
    mod#(x,s(y)) -> modIter#(x,s(y),0(),0()) ->
    modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u)
    mod#(x,s(y)) -> modIter#(x,s(y),0(),0()) ->
    modIter#(x,s(y),z,u) -> le#(x,z)
    le#(s(x),s(y)) -> le#(x,y) -> le#(s(x),s(y)) -> le#(x,y)
   SCC Processor:
    #sccs: 2
    #rules: 5
    #arcs: 13/64
    DPs:
     if2#(false(),x,y,z,u) -> modIter#(x,y,z,u)
     modIter#(x,s(y),z,u) -> if#(le(x,z),x,s(y),z,u)
     if#(false(),x,y,z,u) -> if2#(le(y,s(u)),x,y,s(z),s(u))
     if2#(true(),x,y,z,u) -> modIter#(x,y,z,0())
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     mod(x,0()) -> modZeroErro()
     mod(x,s(y)) -> modIter(x,s(y),0(),0())
     modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
     if(true(),x,y,z,u) -> u
     if(false(),x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
     if2(false(),x,y,z,u) -> modIter(x,y,z,u)
     if2(true(),x,y,z,u) -> modIter(x,y,z,0())
    Open
    
    DPs:
     le#(s(x),s(y)) -> le#(x,y)
    TRS:
     le(0(),y) -> true()
     le(s(x),0()) -> false()
     le(s(x),s(y)) -> le(x,y)
     mod(x,0()) -> modZeroErro()
     mod(x,s(y)) -> modIter(x,s(y),0(),0())
     modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
     if(true(),x,y,z,u) -> u
     if(false(),x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
     if2(false(),x,y,z,u) -> modIter(x,y,z,u)
     if2(true(),x,y,z,u) -> modIter(x,y,z,0())
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),y) -> true()
       le(s(x),0()) -> false()
       le(s(x),s(y)) -> le(x,y)
       mod(x,0()) -> modZeroErro()
       mod(x,s(y)) -> modIter(x,s(y),0(),0())
       modIter(x,s(y),z,u) -> if(le(x,z),x,s(y),z,u)
       if(true(),x,y,z,u) -> u
       if(false(),x,y,z,u) -> if2(le(y,s(u)),x,y,s(z),s(u))
       if2(false(),x,y,z,u) -> modIter(x,y,z,u)
       if2(true(),x,y,z,u) -> modIter(x,y,z,0())
     Qed