MAYBE Problem: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Proof: DP Processor: DPs: minus#(s(x),y) -> gt#(s(x),y) minus#(s(x),y) -> if#(gt(s(x),y),x,y) if#(true(),x,y) -> minus#(x,y) ge#(s(x),s(y)) -> ge#(x,y) gt#(s(x),s(y)) -> gt#(x,y) div#(x,y) -> ge#(x,y) div#(x,y) -> if1#(ge(x,y),x,y) if1#(true(),x,y) -> gt#(y,0()) if1#(true(),x,y) -> if2#(gt(y,0()),x,y) if2#(true(),x,y) -> minus#(x,y) if2#(true(),x,y) -> div#(minus(x,y),y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() TDG Processor: DPs: minus#(s(x),y) -> gt#(s(x),y) minus#(s(x),y) -> if#(gt(s(x),y),x,y) if#(true(),x,y) -> minus#(x,y) ge#(s(x),s(y)) -> ge#(x,y) gt#(s(x),s(y)) -> gt#(x,y) div#(x,y) -> ge#(x,y) div#(x,y) -> if1#(ge(x,y),x,y) if1#(true(),x,y) -> gt#(y,0()) if1#(true(),x,y) -> if2#(gt(y,0()),x,y) if2#(true(),x,y) -> minus#(x,y) if2#(true(),x,y) -> div#(minus(x,y),y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() graph: if2#(true(),x,y) -> div#(minus(x,y),y) -> div#(x,y) -> if1#(ge(x,y),x,y) if2#(true(),x,y) -> div#(minus(x,y),y) -> div#(x,y) -> ge#(x,y) if2#(true(),x,y) -> minus#(x,y) -> minus#(s(x),y) -> if#(gt(s(x),y),x,y) if2#(true(),x,y) -> minus#(x,y) -> minus#(s(x),y) -> gt#(s(x),y) if1#(true(),x,y) -> if2#(gt(y,0()),x,y) -> if2#(true(),x,y) -> div#(minus(x,y),y) if1#(true(),x,y) -> if2#(gt(y,0()),x,y) -> if2#(true(),x,y) -> minus#(x,y) if1#(true(),x,y) -> gt#(y,0()) -> gt#(s(x),s(y)) -> gt#(x,y) div#(x,y) -> if1#(ge(x,y),x,y) -> if1#(true(),x,y) -> if2#(gt(y,0()),x,y) div#(x,y) -> if1#(ge(x,y),x,y) -> if1#(true(),x,y) -> gt#(y,0()) div#(x,y) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y) ge#(s(x),s(y)) -> ge#(x,y) -> ge#(s(x),s(y)) -> ge#(x,y) if#(true(),x,y) -> minus#(x,y) -> minus#(s(x),y) -> if#(gt(s(x),y),x,y) if#(true(),x,y) -> minus#(x,y) -> minus#(s(x),y) -> gt#(s(x),y) gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y) minus#(s(x),y) -> if#(gt(s(x),y),x,y) -> if#(true(),x,y) -> minus#(x,y) minus#(s(x),y) -> gt#(s(x),y) -> gt#(s(x),s(y)) -> gt#(x,y) SCC Processor: #sccs: 4 #rules: 7 #arcs: 16/121 DPs: if2#(true(),x,y) -> div#(minus(x,y),y) div#(x,y) -> if1#(ge(x,y),x,y) if1#(true(),x,y) -> if2#(gt(y,0()),x,y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Open DPs: minus#(s(x),y) -> if#(gt(s(x),y),x,y) if#(true(),x,y) -> minus#(x,y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Subterm Criterion Processor: simple projection: pi(minus#) = 0 pi(if#) = 1 problem: DPs: if#(true(),x,y) -> minus#(x,y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1 DPs: gt#(s(x),s(y)) -> gt#(x,y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Subterm Criterion Processor: simple projection: pi(gt#) = 1 problem: DPs: TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Qed DPs: ge#(s(x),s(y)) -> ge#(x,y) TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Subterm Criterion Processor: simple projection: pi(ge#) = 1 problem: DPs: TRS: minus(s(x),y) -> if(gt(s(x),y),x,y) if(true(),x,y) -> s(minus(x,y)) if(false(),x,y) -> 0() ge(x,0()) -> true() ge(0(),s(x)) -> false() ge(s(x),s(y)) -> ge(x,y) gt(0(),y) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) div(x,y) -> if1(ge(x,y),x,y) if1(true(),x,y) -> if2(gt(y,0()),x,y) if1(false(),x,y) -> 0() if2(true(),x,y) -> s(div(minus(x,y),y)) if2(false(),x,y) -> 0() Qed