YES Problem: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Proof: DP Processor: DPs: g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) g#(s(x),s(y)) -> n#(s(x),s(y)) g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) g#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> m#(x,y) g#(s(x),s(y)) -> minus#(m(x,y),n(x,y)) g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) g#(s(x),s(y)) -> f#(s(y)) g#(s(x),s(y)) -> f#(s(x)) g#(s(x),s(y)) -> and#(f(s(x)),f(s(y))) g#(s(x),s(y)) -> if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n#(s(x),s(y)) -> n#(x,y) m#(s(x),s(y)) -> m#(x,y) k#(s(x),s(y)) -> minus#(x,y) k#(s(x),s(y)) -> k#(minus(x,y),s(y)) t#(x) -> p#(x,x) p#(s(x),s(y)) -> id#(y) p#(s(x),s(y)) -> id#(x) p#(s(x),s(y)) -> not#(gt(x,y)) p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) p#(s(x),s(y)) -> gt#(x,y) p#(s(x),s(y)) -> if#(gt(x,y),x,y) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),x) -> id#(x) p#(s(x),x) -> gt#(x,x) p#(s(x),x) -> if#(gt(x,x),id(x),id(x)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) p#(id(x),s(y)) -> gt#(s(y),y) p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) minus#(s(x),s(y)) -> minus#(x,y) not#(x) -> if#(x,false(),true()) f#(s(x)) -> h#(x) h#(s(x)) -> f#(x) gt#(s(x),s(y)) -> gt#(x,y) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) TDG Processor: DPs: g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) g#(s(x),s(y)) -> n#(s(x),s(y)) g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) g#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> m#(x,y) g#(s(x),s(y)) -> minus#(m(x,y),n(x,y)) g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) g#(s(x),s(y)) -> f#(s(y)) g#(s(x),s(y)) -> f#(s(x)) g#(s(x),s(y)) -> and#(f(s(x)),f(s(y))) g#(s(x),s(y)) -> if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n#(s(x),s(y)) -> n#(x,y) m#(s(x),s(y)) -> m#(x,y) k#(s(x),s(y)) -> minus#(x,y) k#(s(x),s(y)) -> k#(minus(x,y),s(y)) t#(x) -> p#(x,x) p#(s(x),s(y)) -> id#(y) p#(s(x),s(y)) -> id#(x) p#(s(x),s(y)) -> not#(gt(x,y)) p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) p#(s(x),s(y)) -> gt#(x,y) p#(s(x),s(y)) -> if#(gt(x,y),x,y) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),x) -> id#(x) p#(s(x),x) -> gt#(x,x) p#(s(x),x) -> if#(gt(x,x),id(x),id(x)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) p#(id(x),s(y)) -> gt#(s(y),y) p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) minus#(s(x),s(y)) -> minus#(x,y) not#(x) -> if#(x,false(),true()) f#(s(x)) -> h#(x) h#(s(x)) -> f#(x) gt#(s(x),s(y)) -> gt#(x,y) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) graph: h#(s(x)) -> f#(x) -> f#(s(x)) -> h#(x) gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y) p#(id(x),s(y)) -> gt#(s(y),y) -> gt#(s(x),s(y)) -> gt#(x,y) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(id(x),s(y)) -> gt#(s(y),y) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),x) -> if#(gt(x,x),id(x),id(x)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),x) -> gt#(x,x) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),x) -> id#(x) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> if#(gt(x,y),x,y) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> gt#(x,y) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> not#(gt(x,y)) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> id#(x) p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) -> p#(s(x),s(y)) -> id#(y) p#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y) p#(s(x),s(y)) -> not#(gt(x,y)) -> not#(x) -> if#(x,false(),true()) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(id(x),s(y)) -> gt#(s(y),y) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),x) -> if#(gt(x,x),id(x),id(x)) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),x) -> gt#(x,x) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),x) -> id#(x) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> if#(gt(x,y),x,y) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> gt#(x,y) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> not#(gt(x,y)) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> id#(x) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> p#(s(x),s(y)) -> id#(y) p#(s(x),x) -> gt#(x,x) -> gt#(s(x),s(y)) -> gt#(x,y) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(id(x),s(y)) -> gt#(s(y),y) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),x) -> if#(gt(x,x),id(x),id(x)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),x) -> gt#(x,x) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),x) -> id#(x) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> if#(gt(x,y),x,y) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> gt#(x,y) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> not#(gt(x,y)) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> id#(x) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) -> p#(s(x),s(y)) -> id#(y) f#(s(x)) -> h#(x) -> h#(s(x)) -> f#(x) t#(x) -> p#(x,x) -> p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) t#(x) -> p#(x,x) -> p#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) t#(x) -> p#(x,x) -> p#(id(x),s(y)) -> gt#(s(y),y) t#(x) -> p#(x,x) -> p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) t#(x) -> p#(x,x) -> p#(s(x),x) -> if#(gt(x,x),id(x),id(x)) t#(x) -> p#(x,x) -> p#(s(x),x) -> gt#(x,x) t#(x) -> p#(x,x) -> p#(s(x),x) -> id#(x) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> if#(gt(x,y),x,y) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> gt#(x,y) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> not#(gt(x,y)) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> id#(x) t#(x) -> p#(x,x) -> p#(s(x),s(y)) -> id#(y) minus#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) m#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y) k#(s(x),s(y)) -> minus#(x,y) -> minus#(s(x),s(y)) -> minus#(x,y) k#(s(x),s(y)) -> k#(minus(x,y),s(y)) -> k#(s(x),s(y)) -> k#(minus(x,y),s(y)) k#(s(x),s(y)) -> k#(minus(x,y),s(y)) -> k#(s(x),s(y)) -> minus#(x,y) n#(s(x),s(y)) -> n#(x,y) -> n#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> f#(s(y)) -> f#(s(x)) -> h#(x) g#(s(x),s(y)) -> f#(s(x)) -> f#(s(x)) -> h#(x) g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) -> t#(x) -> p#(x,x) g#(s(x),s(y)) -> minus#(m(x,y),n(x,y)) -> minus#(s(x),s(y)) -> minus#(x,y) g#(s(x),s(y)) -> m#(x,y) -> m#(s(x),s(y)) -> m#(x,y) g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) -> k#(s(x),s(y)) -> k#(minus(x,y),s(y)) g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) -> k#(s(x),s(y)) -> minus#(x,y) g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) -> k#(s(x),s(y)) -> k#(minus(x,y),s(y)) g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) -> k#(s(x),s(y)) -> minus#(x,y) g#(s(x),s(y)) -> n#(s(x),s(y)) -> n#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> n#(x,y) -> n#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> and#(f(s(x)),f(s(y))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> f#(s(x)) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> f#(s(y)) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> minus#(m(x,y),n(x,y)) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> m#(x,y) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> n#(s(x),s(y)) g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) -> g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> if#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> and#(f(s(x)),f(s(y))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> f#(s(x)) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> f#(s(y)) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> t#(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> k#(minus(m(x,y),n(x,y)),s(s(0()))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> minus#(m(x,y),n(x,y)) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> m#(x,y) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> n#(x,y) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> k#(n(s(x),s(y)),s(s(0()))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> n#(s(x),s(y)) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) -> g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) SCC Processor: #sccs: 8 #rules: 12 #arcs: 106/1369 DPs: g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) -> g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) TRS: n(s(x),s(y)) -> s(n(x,y)) n(0(),y) -> 0() n(x,0()) -> 0() k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) Arctic Interpretation Processor: dimension: 1 usable rules: n(s(x),s(y)) -> s(n(x,y)) n(0(),y) -> 0() n(x,0()) -> 0() k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) interpretation: [g#](x0, x1) = 2x0 + x1 + 0, [k](x0, x1) = 1x0 + 0, [0] = 0, [minus](x0, x1) = x0 + 0, [n](x0, x1) = x0 + 0, [m](x0, x1) = 2x0 + x1 + 2, [s](x0) = 3x0 + 3 orientation: g#(s(x),s(y)) = 5x + 3y + 5 >= 5x + 3y + 5 = g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) g#(s(x),s(y)) = 5x + 3y + 5 >= 4x + 2y + 4 = g#(minus(m(x,y),n(x,y)),n(s(x),s(y))) n(s(x),s(y)) = 3x + 3 >= 3x + 3 = s(n(x,y)) n(0(),y) = 0 >= 0 = 0() n(x,0()) = x + 0 >= 0 = 0() k(0(),s(y)) = 1 >= 0 = 0() k(s(x),s(y)) = 4x + 4 >= 4x + 4 = s(k(minus(x,y),s(y))) minus(x,0()) = x + 0 >= x = x minus(s(x),s(y)) = 3x + 3 >= x + 0 = minus(x,y) m(0(),y) = y + 2 >= y = y m(x,0()) = 2x + 2 >= x = x m(s(x),s(y)) = 5x + 3y + 5 >= 5x + 3y + 5 = s(m(x,y)) problem: DPs: g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) TRS: n(s(x),s(y)) -> s(n(x,y)) n(0(),y) -> 0() n(x,0()) -> 0() k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) Restore Modifier: DPs: g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: g#(s(x),s(y)) -> g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) TRS: n(s(x),s(y)) -> s(n(x,y)) n(0(),y) -> 0() n(x,0()) -> 0() k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) Arctic Interpretation Processor: dimension: 1 usable rules: n(s(x),s(y)) -> s(n(x,y)) n(0(),y) -> 0() n(x,0()) -> 0() k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) interpretation: [g#](x0, x1) = 2x0 + x1 + 0, [k](x0, x1) = x0 + 0, [0] = 0, [minus](x0, x1) = x0 + 1, [n](x0, x1) = x0 + 1, [m](x0, x1) = 2x0 + x1 + 3, [s](x0) = 3x0 + 4 orientation: g#(s(x),s(y)) = 5x + 3y + 6 >= 4x + 2y + 5 = g#(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0())))) n(s(x),s(y)) = 3x + 4 >= 3x + 4 = s(n(x,y)) n(0(),y) = 1 >= 0 = 0() n(x,0()) = x + 1 >= 0 = 0() k(0(),s(y)) = 0 >= 0 = 0() k(s(x),s(y)) = 3x + 4 >= 3x + 4 = s(k(minus(x,y),s(y))) minus(x,0()) = x + 1 >= x = x minus(s(x),s(y)) = 3x + 4 >= x + 1 = minus(x,y) m(0(),y) = y + 3 >= y = y m(x,0()) = 2x + 3 >= x = x m(s(x),s(y)) = 5x + 3y + 6 >= 5x + 3y + 6 = s(m(x,y)) problem: DPs: TRS: n(s(x),s(y)) -> s(n(x,y)) n(0(),y) -> 0() n(x,0()) -> 0() k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) Qed DPs: n#(s(x),s(y)) -> n#(x,y) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(n#) = 1 problem: DPs: TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed DPs: k#(s(x),s(y)) -> k#(minus(x,y),s(y)) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: k#(s(x),s(y)) -> k#(minus(x,y),s(y)) TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) Arctic Interpretation Processor: dimension: 1 usable rules: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) interpretation: [k#](x0, x1) = 3x0 + -16, [0] = 8, [minus](x0, x1) = x0 + -11, [s](x0) = 1x0 + -3 orientation: k#(s(x),s(y)) = 4x + 0 >= 3x + -8 = k#(minus(x,y),s(y)) minus(x,0()) = x + -11 >= x = x minus(s(x),s(y)) = 1x + -3 >= x + -11 = minus(x,y) problem: DPs: TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) Qed DPs: m#(s(x),s(y)) -> m#(x,y) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(m#) = 1 problem: DPs: TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed DPs: minus#(s(x),s(y)) -> minus#(x,y) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(minus#) = 1 problem: DPs: TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),s(y)) -> p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(0(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x not(x) -> if(x,false(),true()) Arctic Interpretation Processor: dimension: 1 usable rules: if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x interpretation: [p#](x0, x1) = 1x0 + x1 + 0, [false] = 3, [true] = 2, [id](x0) = 1x0, [not](x0) = 5, [gt](x0, x1) = 2x1 + 0, [if](x0, x1, x2) = 1x1 + x2 + 0, [0] = 1, [s](x0) = 2x0 + 4 orientation: p#(id(x),s(y)) = 2x + 2y + 4 >= 1x + 2y + 4 = p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),s(y)) = 3x + 2y + 5 >= 2x + 1y + 1 = p#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) p#(s(x),x) = 3x + 5 >= 3x + 4 = p#(if(gt(x,x),id(x),id(x)),s(x)) gt(s(x),0()) = 3 >= 2 = true() gt(s(x),s(y)) = 4y + 6 >= 2y + 0 = gt(x,y) gt(0(),y) = 2y + 0 >= 3 = false() if(true(),x,y) = 1x + y + 0 >= x = x if(false(),x,y) = 1x + y + 0 >= y = y id(x) = 1x >= x = x not(x) = 5 >= 4 = if(x,false(),true()) problem: DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(0(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x not(x) -> if(x,false(),true()) Restore Modifier: DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) p#(s(x),x) -> p#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(0(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x LPO Processor: argument filtering: pi(s) = [0] pi(0) = [] pi(if) = [1,2] pi(gt) = [] pi(id) = 0 pi(true) = [] pi(false) = [] pi(p#) = 0 usable rules: if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x precedence: s > p# ~ false ~ true ~ id ~ gt ~ if ~ 0 problem: DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) TRS: gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(0(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x Restore Modifier: DPs: p#(id(x),s(y)) -> p#(x,if(gt(s(y),y),y,s(y))) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(p#) = 0 problem: DPs: TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))), k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed DPs: gt#(s(x),s(y)) -> gt#(x,y) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(gt#) = 1 problem: DPs: TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed DPs: h#(s(x)) -> f#(x) f#(s(x)) -> h#(x) TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(f#) = 0 pi(h#) = 0 problem: DPs: TRS: g(s(x),s(y)) -> if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0()))),k(n(s(x),s(y)),s(s(0()))))), g(minus(m(x,y),n(x,y)),n(s(x),s(y)))) n(0(),y) -> 0() n(x,0()) -> 0() n(s(x),s(y)) -> s(n(x,y)) m(0(),y) -> y m(x,0()) -> x m(s(x),s(y)) -> s(m(x,y)) k(0(),s(y)) -> 0() k(s(x),s(y)) -> s(k(minus(x,y),s(y))) t(x) -> p(x,x) p(s(x),s(y)) -> s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) p(s(x),x) -> p(if(gt(x,x),id(x),id(x)),s(x)) p(0(),y) -> y p(id(x),s(y)) -> s(p(x,if(gt(s(y),y),y,s(y)))) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) and(x,false()) -> false() and(true(),true()) -> true() f(0()) -> true() f(s(x)) -> h(x) h(0()) -> false() h(s(x)) -> f(x) gt(s(x),0()) -> true() gt(0(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed