MAYBE Problem: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Proof: DP Processor: DPs: lt#(s(x),s(y)) -> lt#(x,y) fibo#(0()) -> fib#(0()) fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(s(x)) fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) if#(true(),c,s(s(x)),a,b) -> lt#(s(c),s(s(x))) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if#(false(),c,s(s(x)),a,b) -> fibo#(b) if#(false(),c,s(s(x)),a,b) -> fibo#(a) if#(false(),c,s(s(x)),a,b) -> sum#(fibo(a),fibo(b)) sum#(x,s(y)) -> sum#(x,y) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) TDG Processor: DPs: lt#(s(x),s(y)) -> lt#(x,y) fibo#(0()) -> fib#(0()) fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(s(x)) fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) if#(true(),c,s(s(x)),a,b) -> lt#(s(c),s(s(x))) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if#(false(),c,s(s(x)),a,b) -> fibo#(b) if#(false(),c,s(s(x)),a,b) -> fibo#(a) if#(false(),c,s(s(x)),a,b) -> sum#(fibo(a),fibo(b)) sum#(x,s(y)) -> sum#(x,y) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) graph: if#(false(),c,s(s(x)),a,b) -> sum#(fibo(a),fibo(b)) -> sum#(x,s(y)) -> sum#(x,y) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(s(x))) -> fibo#(s(x)) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(s(x))) -> fibo#(x) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(0())) -> fib#(s(0())) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(0()) -> fib#(0()) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(s(x))) -> fibo#(s(x)) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(s(x))) -> fibo#(x) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(0())) -> fib#(s(0())) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(0()) -> fib#(0()) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(false(),c,s(s(x)),a,b) -> sum#(fibo(a),fibo(b)) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(false(),c,s(s(x)),a,b) -> fibo#(a) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(false(),c,s(s(x)),a,b) -> fibo#(b) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(true(),c,s(s(x)),a,b) -> lt#(s(c),s(s(x))) if#(true(),c,s(s(x)),a,b) -> lt#(s(c),s(s(x))) -> lt#(s(x),s(y)) -> lt#(x,y) sum#(x,s(y)) -> sum#(x,y) -> sum#(x,s(y)) -> sum#(x,y) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) -> if#(false(),c,s(s(x)),a,b) -> sum#(fibo(a),fibo(b)) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) -> if#(false(),c,s(s(x)),a,b) -> fibo#(a) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) -> if#(false(),c,s(s(x)),a,b) -> fibo#(b) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) -> if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) -> if#(true(),c,s(s(x)),a,b) -> lt#(s(c),s(s(x))) fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) -> sum#(x,s(y)) -> sum#(x,y) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(s(x))) -> fibo#(s(x)) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(0()) -> fib#(0()) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(s(x))) -> sum#(fibo(s(x)),fibo(x)) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(s(x))) -> fibo#(s(x)) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(x) -> fibo#(0()) -> fib#(0()) fibo#(s(0())) -> fib#(s(0())) -> fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) fibo#(0()) -> fib#(0()) -> fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y) SCC Processor: #sccs: 3 #rules: 10 #arcs: 37/169 DPs: if#(false(),c,s(s(x)),a,b) -> fibo#(b) fibo#(0()) -> fib#(0()) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if#(false(),c,s(s(x)),a,b) -> fibo#(a) fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(s(x)) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) EDG Processor: DPs: if#(false(),c,s(s(x)),a,b) -> fibo#(b) fibo#(0()) -> fib#(0()) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if#(false(),c,s(s(x)),a,b) -> fibo#(a) fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(s(x)) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) graph: if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(0()) -> fib#(0()) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(0())) -> fib#(s(0())) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(s(x))) -> fibo#(x) if#(false(),c,s(s(x)),a,b) -> fibo#(b) -> fibo#(s(s(x))) -> fibo#(s(x)) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(0()) -> fib#(0()) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(0())) -> fib#(s(0())) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(s(x))) -> fibo#(x) if#(false(),c,s(s(x)),a,b) -> fibo#(a) -> fibo#(s(s(x))) -> fibo#(s(x)) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(false(),c,s(s(x)),a,b) -> fibo#(b) if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) -> if#(false(),c,s(s(x)),a,b) -> fibo#(a) fib#(s(s(x))) -> if#(true(),0(),s(s(x)),0(),0()) -> if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(s(x)) -> fibo#(s(s(x))) -> fibo#(s(x)) fibo#(s(s(x))) -> fibo#(x) -> fibo#(0()) -> fib#(0()) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(0())) -> fib#(s(0())) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(s(x))) -> fibo#(x) fibo#(s(s(x))) -> fibo#(x) -> fibo#(s(s(x))) -> fibo#(s(x)) SCC Processor: #sccs: 2 #rules: 3 #arcs: 19/64 DPs: if#(true(),c,s(s(x)),a,b) -> if#(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Open DPs: fibo#(s(s(x))) -> fibo#(s(x)) fibo#(s(s(x))) -> fibo#(x) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Subterm Criterion Processor: simple projection: pi(fibo#) = 0 problem: DPs: TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Qed DPs: lt#(s(x),s(y)) -> lt#(x,y) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Subterm Criterion Processor: simple projection: pi(lt#) = 1 problem: DPs: TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Qed DPs: sum#(x,s(y)) -> sum#(x,y) TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Subterm Criterion Processor: simple projection: pi(sum#) = 1 problem: DPs: TRS: lt(0(),s(x)) -> true() lt(x,0()) -> false() lt(s(x),s(y)) -> lt(x,y) fibo(0()) -> fib(0()) fibo(s(0())) -> fib(s(0())) fibo(s(s(x))) -> sum(fibo(s(x)),fibo(x)) fib(0()) -> s(0()) fib(s(0())) -> s(0()) fib(s(s(x))) -> if(true(),0(),s(s(x)),0(),0()) if(true(),c,s(s(x)),a,b) -> if(lt(s(c),s(s(x))),s(c),s(s(x)),b,c) if(false(),c,s(s(x)),a,b) -> sum(fibo(a),fibo(b)) sum(x,0()) -> x sum(x,s(y)) -> s(sum(x,y)) Qed