MAYBE Problem: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) Proof: DP Processor: DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact#() -> app#(s(),0()) fact#() -> app#(rec(),mult()) fact#() -> app#(app(rec(),mult()),app(s(),0())) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) TDG Processor: DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact#() -> app#(s(),0()) fact#() -> app#(rec(),mult()) fact#() -> app#(app(rec(),mult()),app(s(),0())) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) graph: fact#() -> app#(rec(),mult()) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact#() -> app#(rec(),mult()) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) fact#() -> app#(rec(),mult()) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) fact#() -> app#(rec(),mult()) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) fact#() -> app#(rec(),mult()) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) fact#() -> app#(rec(),mult()) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) fact#() -> app#(rec(),mult()) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) fact#() -> app#(rec(),mult()) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) fact#() -> app#(rec(),mult()) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) fact#() -> app#(rec(),mult()) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) fact#() -> app#(s(),0()) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact#() -> app#(s(),0()) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) fact#() -> app#(s(),0()) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) fact#() -> app#(s(),0()) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) fact#() -> app#(s(),0()) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) fact#() -> app#(s(),0()) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) fact#() -> app#(s(),0()) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) fact#() -> app#(s(),0()) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) fact#() -> app#(s(),0()) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) fact#() -> app#(s(),0()) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) fact#() -> app#(app(rec(),mult()),app(s(),0())) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(add(),x) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) SCC Processor: #sccs: 1 #rules: 10 #arcs: 130/169 DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) EDG Processor: DPs: app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) graph: app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(mult(),x) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(add(),app(app(mult(),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(mult(),app(s(),x)),y) -> app#(app(add(),app(app(mult(),x),y)),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) -> app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(add(),x) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) -> app#(app(add(),app(s(),x)),y) -> app#(s(),app(app(add(),x),y)) SCC Processor: #sccs: 3 #rules: 5 #arcs: 33/100 DPs: app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(app(rec(),f),x),y) app#(app(app(rec(),f),x),app(s(),y)) -> app#(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) app#(app(app(rec(),f),x),app(s(),y)) -> app#(f,app(s(),y)) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) Open DPs: app#(app(mult(),app(s(),x)),y) -> app#(app(mult(),x),y) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) Open DPs: app#(app(add(),app(s(),x)),y) -> app#(app(add(),x),y) TRS: app(app(add(),0()),y) -> y app(app(add(),app(s(),x)),y) -> app(s(),app(app(add(),x),y)) app(app(mult(),0()),y) -> 0() app(app(mult(),app(s(),x)),y) -> app(app(add(),app(app(mult(),x),y)),y) app(app(app(rec(),f),x),0()) -> x app(app(app(rec(),f),x),app(s(),y)) -> app(app(f,app(s(),y)),app(app(app(rec(),f),x),y)) fact() -> app(app(rec(),mult()),app(s(),0())) Open