MAYBE Problem: a__fact(X) -> a__if(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__prod(0(),X) -> 0() a__prod(s(X),Y) -> a__add(mark(Y),a__prod(mark(X),mark(Y))) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) a__zero(0()) -> true() a__zero(s(X)) -> false() a__p(s(X)) -> mark(X) mark(fact(X)) -> a__fact(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(zero(X)) -> a__zero(mark(X)) mark(prod(X1,X2)) -> a__prod(mark(X1),mark(X2)) mark(p(X)) -> a__p(mark(X)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(true()) -> true() mark(false()) -> false() a__fact(X) -> fact(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__zero(X) -> zero(X) a__prod(X1,X2) -> prod(X1,X2) a__p(X) -> p(X) a__add(X1,X2) -> add(X1,X2) Proof: DP Processor: DPs: a__fact#(X) -> mark#(X) a__fact#(X) -> a__zero#(mark(X)) a__fact#(X) -> a__if#(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__add#(0(),X) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) a__add#(s(X),Y) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__prod#(s(X),Y) -> mark#(X) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) a__prod#(s(X),Y) -> mark#(Y) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) a__p#(s(X)) -> mark#(X) mark#(fact(X)) -> mark#(X) mark#(fact(X)) -> a__fact#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(zero(X)) -> mark#(X) mark#(zero(X)) -> a__zero#(mark(X)) mark#(prod(X1,X2)) -> mark#(X2) mark#(prod(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(p(X)) -> mark#(X) mark#(p(X)) -> a__p#(mark(X)) mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) TRS: a__fact(X) -> a__if(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__prod(0(),X) -> 0() a__prod(s(X),Y) -> a__add(mark(Y),a__prod(mark(X),mark(Y))) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) a__zero(0()) -> true() a__zero(s(X)) -> false() a__p(s(X)) -> mark(X) mark(fact(X)) -> a__fact(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(zero(X)) -> a__zero(mark(X)) mark(prod(X1,X2)) -> a__prod(mark(X1),mark(X2)) mark(p(X)) -> a__p(mark(X)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(true()) -> true() mark(false()) -> false() a__fact(X) -> fact(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__zero(X) -> zero(X) a__prod(X1,X2) -> prod(X1,X2) a__p(X) -> p(X) a__add(X1,X2) -> add(X1,X2) EDG Processor: DPs: a__fact#(X) -> mark#(X) a__fact#(X) -> a__zero#(mark(X)) a__fact#(X) -> a__if#(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__add#(0(),X) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) a__add#(s(X),Y) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__prod#(s(X),Y) -> mark#(X) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) a__prod#(s(X),Y) -> mark#(Y) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) a__p#(s(X)) -> mark#(X) mark#(fact(X)) -> mark#(X) mark#(fact(X)) -> a__fact#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(zero(X)) -> mark#(X) mark#(zero(X)) -> a__zero#(mark(X)) mark#(prod(X1,X2)) -> mark#(X2) mark#(prod(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(p(X)) -> mark#(X) mark#(p(X)) -> a__p#(mark(X)) mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) TRS: a__fact(X) -> a__if(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__prod(0(),X) -> 0() a__prod(s(X),Y) -> a__add(mark(Y),a__prod(mark(X),mark(Y))) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) a__zero(0()) -> true() a__zero(s(X)) -> false() a__p(s(X)) -> mark(X) mark(fact(X)) -> a__fact(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(zero(X)) -> a__zero(mark(X)) mark(prod(X1,X2)) -> a__prod(mark(X1),mark(X2)) mark(p(X)) -> a__p(mark(X)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(true()) -> true() mark(false()) -> false() a__fact(X) -> fact(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__zero(X) -> zero(X) a__prod(X1,X2) -> prod(X1,X2) a__p(X) -> p(X) a__add(X1,X2) -> add(X1,X2) graph: a__p#(s(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X) a__p#(s(X)) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) a__p#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__p#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__p#(s(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X) a__p#(s(X)) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) a__p#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) a__p#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) a__p#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__p#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) a__p#(s(X)) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) a__p#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__p#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__p#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__p#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) -> a__prod#(s(X),Y) -> mark#(X) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) -> a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) -> a__prod#(s(X),Y) -> mark#(Y) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) -> a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) -> a__add#(0(),X) -> mark#(X) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) -> a__add#(s(X),Y) -> mark#(Y) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) -> a__add#(s(X),Y) -> mark#(X) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) -> a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__prod#(s(X),Y) -> mark#(Y) -> mark#(fact(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(Y) -> mark#(fact(X)) -> a__fact#(mark(X)) a__prod#(s(X),Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__prod#(s(X),Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__prod#(s(X),Y) -> mark#(Y) -> mark#(zero(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(Y) -> mark#(zero(X)) -> a__zero#(mark(X)) a__prod#(s(X),Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> mark#(X2) a__prod#(s(X),Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> mark#(X1) a__prod#(s(X),Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__prod#(s(X),Y) -> mark#(Y) -> mark#(p(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(Y) -> mark#(p(X)) -> a__p#(mark(X)) a__prod#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X2) a__prod#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X1) a__prod#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__prod#(s(X),Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(X) -> mark#(fact(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) a__prod#(s(X),Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__prod#(s(X),Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__prod#(s(X),Y) -> mark#(X) -> mark#(zero(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) a__prod#(s(X),Y) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) a__prod#(s(X),Y) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) a__prod#(s(X),Y) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__prod#(s(X),Y) -> mark#(X) -> mark#(p(X)) -> mark#(X) a__prod#(s(X),Y) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) a__prod#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__prod#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__prod#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__prod#(s(X),Y) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(0(),X) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(s(X),Y) -> mark#(Y) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(s(X),Y) -> mark#(X) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) -> a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__add#(s(X),Y) -> mark#(Y) -> mark#(fact(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) -> mark#(fact(X)) -> a__fact#(mark(X)) a__add#(s(X),Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__add#(s(X),Y) -> mark#(Y) -> mark#(zero(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) -> mark#(zero(X)) -> a__zero#(mark(X)) a__add#(s(X),Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(Y) -> mark#(p(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(Y) -> mark#(p(X)) -> a__p#(mark(X)) a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(Y) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(X) -> mark#(fact(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) a__add#(s(X),Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__add#(s(X),Y) -> mark#(X) -> mark#(zero(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) a__add#(s(X),Y) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(X) -> mark#(p(X)) -> mark#(X) a__add#(s(X),Y) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__add#(s(X),Y) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(s(X),Y) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__add#(0(),X) -> mark#(X) -> mark#(fact(X)) -> mark#(X) a__add#(0(),X) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) a__add#(0(),X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__add#(0(),X) -> mark#(X) -> mark#(zero(X)) -> mark#(X) a__add#(0(),X) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) a__add#(0(),X) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) a__add#(0(),X) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__add#(0(),X) -> mark#(X) -> mark#(p(X)) -> mark#(X) a__add#(0(),X) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__add#(0(),X) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(0(),X) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) -> mark#(fact(X)) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) -> mark#(fact(X)) -> a__fact#(mark(X)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__if#(false(),X,Y) -> mark#(Y) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) -> mark#(Y) -> mark#(zero(X)) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) -> mark#(zero(X)) -> a__zero#(mark(X)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> mark#(X2) a__if#(false(),X,Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> mark#(X1) a__if#(false(),X,Y) -> mark#(Y) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(p(X)) -> mark#(X) a__if#(false(),X,Y) -> mark#(Y) -> mark#(p(X)) -> a__p#(mark(X)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X2) a__if#(false(),X,Y) -> mark#(Y) -> mark#(add(X1,X2)) -> mark#(X1) a__if#(false(),X,Y) -> mark#(Y) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__if#(false(),X,Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X) a__if#(true(),X,Y) -> mark#(X) -> mark#(fact(X)) -> mark#(X) a__if#(true(),X,Y) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__if#(true(),X,Y) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__if#(true(),X,Y) -> mark#(X) -> mark#(zero(X)) -> mark#(X) a__if#(true(),X,Y) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) a__if#(true(),X,Y) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) a__if#(true(),X,Y) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) a__if#(true(),X,Y) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__if#(true(),X,Y) -> mark#(X) -> mark#(p(X)) -> mark#(X) a__if#(true(),X,Y) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) a__if#(true(),X,Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__if#(true(),X,Y) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__if#(true(),X,Y) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__if#(true(),X,Y) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(0(),X) -> mark#(X) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(s(X),Y) -> mark#(Y) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(s(X),Y) -> mark#(X) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) -> a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(add(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> a__p#(mark(X)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fact(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(add(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> a__p#(mark(X)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(add(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(zero(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X) mark#(zero(X)) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(zero(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(zero(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(zero(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X) mark#(zero(X)) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(zero(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(zero(X)) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) mark#(zero(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(zero(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) -> a__if#(true(),X,Y) -> mark#(X) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) -> a__if#(false(),X,Y) -> mark#(Y) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(fact(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(p(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(p(X)) -> a__p#(mark(X)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) -> a__prod#(s(X),Y) -> mark#(X) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) -> a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) -> a__prod#(s(X),Y) -> mark#(Y) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) -> a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(p(X)) -> a__p#(mark(X)) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X2) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(prod(X1,X2)) -> mark#(X2) -> mark#(s(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(fact(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> mark#(X) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(p(X)) -> a__p#(mark(X)) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X2) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(prod(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) mark#(fact(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X) mark#(fact(X)) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(fact(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(fact(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(fact(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X) mark#(fact(X)) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(fact(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(fact(X)) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) mark#(fact(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(fact(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(fact(X)) -> a__fact#(mark(X)) -> a__fact#(X) -> mark#(X) mark#(fact(X)) -> a__fact#(mark(X)) -> a__fact#(X) -> a__zero#(mark(X)) mark#(fact(X)) -> a__fact#(mark(X)) -> a__fact#(X) -> a__if#(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) mark#(p(X)) -> a__p#(mark(X)) -> a__p#(s(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(p(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(p(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(p(X)) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) mark#(p(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(p(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) a__fact#(X) -> a__if#(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) -> a__if#(true(),X,Y) -> mark#(X) a__fact#(X) -> a__if#(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) -> a__if#(false(),X,Y) -> mark#(Y) a__fact#(X) -> mark#(X) -> mark#(fact(X)) -> mark#(X) a__fact#(X) -> mark#(X) -> mark#(fact(X)) -> a__fact#(mark(X)) a__fact#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) a__fact#(X) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__fact#(X) -> mark#(X) -> mark#(zero(X)) -> mark#(X) a__fact#(X) -> mark#(X) -> mark#(zero(X)) -> a__zero#(mark(X)) a__fact#(X) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X2) a__fact#(X) -> mark#(X) -> mark#(prod(X1,X2)) -> mark#(X1) a__fact#(X) -> mark#(X) -> mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__fact#(X) -> mark#(X) -> mark#(p(X)) -> mark#(X) a__fact#(X) -> mark#(X) -> mark#(p(X)) -> a__p#(mark(X)) a__fact#(X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X2) a__fact#(X) -> mark#(X) -> mark#(add(X1,X2)) -> mark#(X1) a__fact#(X) -> mark#(X) -> mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__fact#(X) -> mark#(X) -> mark#(s(X)) -> mark#(X) SCC Processor: #sccs: 1 #rules: 27 #arcs: 298/841 DPs: a__p#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) mark#(add(X1,X2)) -> a__add#(mark(X1),mark(X2)) a__add#(s(X),Y) -> a__add#(mark(X),mark(Y)) a__add#(s(X),Y) -> mark#(X) mark#(add(X1,X2)) -> mark#(X1) mark#(add(X1,X2)) -> mark#(X2) mark#(p(X)) -> a__p#(mark(X)) mark#(p(X)) -> mark#(X) mark#(prod(X1,X2)) -> a__prod#(mark(X1),mark(X2)) a__prod#(s(X),Y) -> a__add#(mark(Y),a__prod(mark(X),mark(Y))) a__add#(s(X),Y) -> mark#(Y) mark#(prod(X1,X2)) -> mark#(X1) mark#(prod(X1,X2)) -> mark#(X2) mark#(zero(X)) -> mark#(X) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) -> mark#(Y) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(fact(X)) -> a__fact#(mark(X)) a__fact#(X) -> a__if#(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__if#(true(),X,Y) -> mark#(X) mark#(fact(X)) -> mark#(X) a__fact#(X) -> mark#(X) a__add#(0(),X) -> mark#(X) a__prod#(s(X),Y) -> mark#(Y) a__prod#(s(X),Y) -> a__prod#(mark(X),mark(Y)) a__prod#(s(X),Y) -> mark#(X) TRS: a__fact(X) -> a__if(a__zero(mark(X)),s(0()),prod(X,fact(p(X)))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(a__add(mark(X),mark(Y))) a__prod(0(),X) -> 0() a__prod(s(X),Y) -> a__add(mark(Y),a__prod(mark(X),mark(Y))) a__if(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) a__zero(0()) -> true() a__zero(s(X)) -> false() a__p(s(X)) -> mark(X) mark(fact(X)) -> a__fact(mark(X)) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(zero(X)) -> a__zero(mark(X)) mark(prod(X1,X2)) -> a__prod(mark(X1),mark(X2)) mark(p(X)) -> a__p(mark(X)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(s(X)) -> s(mark(X)) mark(0()) -> 0() mark(true()) -> true() mark(false()) -> false() a__fact(X) -> fact(X) a__if(X1,X2,X3) -> if(X1,X2,X3) a__zero(X) -> zero(X) a__prod(X1,X2) -> prod(X1,X2) a__p(X) -> p(X) a__add(X1,X2) -> add(X1,X2) Open