MAYBE

Problem:
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 lt(0(),s(y)) -> true()
 lt(x,0()) -> false()
 lt(s(x),s(y)) -> lt(x,y)
 fib(x) -> fibiter(x,0(),0(),s(0()))
 fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
 if(false(),b,c,x,y) -> x
 if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))

Proof:
 DP Processor:
  DPs:
   plus#(s(x),y) -> plus#(x,y)
   lt#(s(x),s(y)) -> lt#(x,y)
   fib#(x) -> fibiter#(x,0(),0(),s(0()))
   fibiter#(b,c,x,y) -> lt#(c,b)
   fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y)
   if#(true(),b,c,x,y) -> plus#(x,y)
   if#(true(),b,c,x,y) -> fibiter#(b,s(c),y,plus(x,y))
  TRS:
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   lt(0(),s(y)) -> true()
   lt(x,0()) -> false()
   lt(s(x),s(y)) -> lt(x,y)
   fib(x) -> fibiter(x,0(),0(),s(0()))
   fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
   if(false(),b,c,x,y) -> x
   if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
  TDG Processor:
   DPs:
    plus#(s(x),y) -> plus#(x,y)
    lt#(s(x),s(y)) -> lt#(x,y)
    fib#(x) -> fibiter#(x,0(),0(),s(0()))
    fibiter#(b,c,x,y) -> lt#(c,b)
    fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y)
    if#(true(),b,c,x,y) -> plus#(x,y)
    if#(true(),b,c,x,y) -> fibiter#(b,s(c),y,plus(x,y))
   TRS:
    plus(0(),y) -> y
    plus(s(x),y) -> s(plus(x,y))
    lt(0(),s(y)) -> true()
    lt(x,0()) -> false()
    lt(s(x),s(y)) -> lt(x,y)
    fib(x) -> fibiter(x,0(),0(),s(0()))
    fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
    if(false(),b,c,x,y) -> x
    if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
   graph:
    if#(true(),b,c,x,y) -> fibiter#(b,s(c),y,plus(x,y)) ->
    fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y)
    if#(true(),b,c,x,y) -> fibiter#(b,s(c),y,plus(x,y)) ->
    fibiter#(b,c,x,y) -> lt#(c,b)
    if#(true(),b,c,x,y) -> plus#(x,y) ->
    plus#(s(x),y) -> plus#(x,y)
    fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y) ->
    if#(true(),b,c,x,y) -> fibiter#(b,s(c),y,plus(x,y))
    fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y) ->
    if#(true(),b,c,x,y) -> plus#(x,y)
    fibiter#(b,c,x,y) -> lt#(c,b) ->
    lt#(s(x),s(y)) -> lt#(x,y)
    fib#(x) -> fibiter#(x,0(),0(),s(0())) ->
    fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y)
    fib#(x) -> fibiter#(x,0(),0(),s(0())) ->
    fibiter#(b,c,x,y) -> lt#(c,b)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
    plus#(s(x),y) -> plus#(x,y) -> plus#(s(x),y) -> plus#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 10/49
    DPs:
     if#(true(),b,c,x,y) -> fibiter#(b,s(c),y,plus(x,y))
     fibiter#(b,c,x,y) -> if#(lt(c,b),b,c,x,y)
    TRS:
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     fib(x) -> fibiter(x,0(),0(),s(0()))
     fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
     if(false(),b,c,x,y) -> x
     if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
    Open
    
    DPs:
     plus#(s(x),y) -> plus#(x,y)
    TRS:
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     fib(x) -> fibiter(x,0(),0(),s(0()))
     fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
     if(false(),b,c,x,y) -> x
     if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(plus#) = 0
     problem:
      DPs:
       
      TRS:
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       fib(x) -> fibiter(x,0(),0(),s(0()))
       fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
       if(false(),b,c,x,y) -> x
       if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
     Qed
    
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
    TRS:
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     lt(0(),s(y)) -> true()
     lt(x,0()) -> false()
     lt(s(x),s(y)) -> lt(x,y)
     fib(x) -> fibiter(x,0(),0(),s(0()))
     fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
     if(false(),b,c,x,y) -> x
     if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
    Subterm Criterion Processor:
     simple projection:
      pi(lt#) = 1
     problem:
      DPs:
       
      TRS:
       plus(0(),y) -> y
       plus(s(x),y) -> s(plus(x,y))
       lt(0(),s(y)) -> true()
       lt(x,0()) -> false()
       lt(s(x),s(y)) -> lt(x,y)
       fib(x) -> fibiter(x,0(),0(),s(0()))
       fibiter(b,c,x,y) -> if(lt(c,b),b,c,x,y)
       if(false(),b,c,x,y) -> x
       if(true(),b,c,x,y) -> fibiter(b,s(c),y,plus(x,y))
     Qed