YES Problem: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Proof: DP Processor: DPs: times#(x,plus(y,1())) -> times#(1(),0()) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) plus#(s(x),s(y)) -> id#(y) plus#(s(x),s(y)) -> id#(x) plus#(s(x),s(y)) -> not#(gt(x,y)) plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) plus#(s(x),s(y)) -> gt#(x,y) plus#(s(x),s(y)) -> if#(gt(x,y),x,y) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),x) -> id#(x) plus#(s(x),x) -> gt#(x,x) plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) plus#(id(x),s(y)) -> gt#(s(y),y) plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) not#(x) -> if#(x,false(),true()) gt#(s(x),s(y)) -> gt#(x,y) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) TDG Processor: DPs: times#(x,plus(y,1())) -> times#(1(),0()) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) plus#(s(x),s(y)) -> id#(y) plus#(s(x),s(y)) -> id#(x) plus#(s(x),s(y)) -> not#(gt(x,y)) plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) plus#(s(x),s(y)) -> gt#(x,y) plus#(s(x),s(y)) -> if#(gt(x,y),x,y) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),x) -> id#(x) plus#(s(x),x) -> gt#(x,x) plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) plus#(id(x),s(y)) -> gt#(s(y),y) plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) not#(x) -> if#(x,false(),true()) gt#(s(x),s(y)) -> gt#(x,y) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) graph: gt#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y) plus#(id(x),s(y)) -> gt#(s(y),y) -> gt#(s(x),s(y)) -> gt#(x,y) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(id(x),s(y)) -> gt#(s(y),y) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),x) -> gt#(x,x) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),x) -> id#(x) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> if#(gt(x,y),x,y) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> gt#(x,y) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> not#(gt(x,y)) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> id#(x) plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) -> plus#(s(x),s(y)) -> id#(y) plus#(s(x),s(y)) -> gt#(x,y) -> gt#(s(x),s(y)) -> gt#(x,y) plus#(s(x),s(y)) -> not#(gt(x,y)) -> not#(x) -> if#(x,false(),true()) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(id(x),s(y)) -> gt#(s(y),y) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),x) -> gt#(x,x) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),x) -> id#(x) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> if#(gt(x,y),x,y) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> gt#(x,y) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> not#(gt(x,y)) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> id#(x) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) -> plus#(s(x),s(y)) -> id#(y) plus#(s(x),x) -> gt#(x,x) -> gt#(s(x),s(y)) -> gt#(x,y) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(id(x),s(y)) -> gt#(s(y),y) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),x) -> gt#(x,x) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),x) -> id#(x) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> if#(gt(x,y),x,y) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> gt#(x,y) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> not#(gt(x,y)) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> id#(x) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) -> plus#(s(x),s(y)) -> id#(y) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(id(x),s(y)) -> gt#(s(y),y) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),x) -> gt#(x,x) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),x) -> id#(x) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> if#(gt(x,y),x,y) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> gt#(x,y) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> not#(gt(x,y)) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> id#(x) times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) -> plus#(s(x),s(y)) -> id#(y) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(id(x),s(y)) -> if#(gt(s(y),y),y,s(y)) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(id(x),s(y)) -> gt#(s(y),y) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),x) -> if#(gt(x,x),id(x),id(x)) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),x) -> gt#(x,x) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),x) -> id#(x) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> if#(gt(x,y),x,y) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> gt#(x,y) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> if#(not(gt(x,y)),id(x),id(y)) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> not#(gt(x,y)) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> id#(x) times#(x,plus(y,1())) -> plus#(y,times(1(),0())) -> plus#(s(x),s(y)) -> id#(y) times#(x,plus(y,1())) -> times#(1(),0()) -> times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) times#(x,plus(y,1())) -> times#(1(),0()) -> times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) times#(x,plus(y,1())) -> times#(1(),0()) -> times#(x,plus(y,1())) -> plus#(y,times(1(),0())) times#(x,plus(y,1())) -> times#(1(),0()) -> times#(x,plus(y,1())) -> times#(1(),0()) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) -> times#(x,plus(y,1())) -> plus#(times(x,plus(y,times(1(),0()))),x) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) -> times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) -> times#(x,plus(y,1())) -> plus#(y,times(1(),0())) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) -> times#(x,plus(y,1())) -> times#(1(),0()) SCC Processor: #sccs: 3 #rules: 6 #arcs: 83/400 DPs: times#(x,plus(y,1())) -> times#(1(),0()) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) EDG Processor: DPs: times#(x,plus(y,1())) -> times#(1(),0()) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) graph: times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) -> times#(x,plus(y,1())) -> times#(1(),0()) times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) -> times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: times#(x,plus(y,1())) -> times#(x,plus(y,times(1(),0()))) TRS: times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) if(true(),x,y) -> x if(false(),x,y) -> y Matrix Interpretation Processor: dim=1 usable rules: times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) interpretation: [times#](x0, x1) = 4x1 + 1, [false] = 0, [true] = 1, [zero] = 7, [id](x0) = 0, [not](x0) = x0, [if](x0, x1, x2) = 4x0 + 1, [gt](x0, x1) = 2x1 + 2, [s](x0) = 0, [0] = 0, [times](x0, x1) = 0, [plus](x0, x1) = 2x1, [1] = 1 orientation: times#(x,plus(y,1())) = 9 >= 1 = times#(x,plus(y,times(1(),0()))) times(x,0()) = 0 >= 0 = 0() plus(s(x),s(y)) = 0 >= 0 = s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) = 2x >= 0 = plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) = 2y >= y = y plus(id(x),s(y)) = 0 >= 0 = s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) = 0 >= x = x not(x) = x >= 4x + 1 = if(x,false(),true()) gt(s(x),zero()) = 16 >= 1 = true() gt(zero(),y) = 2y + 2 >= 0 = false() gt(s(x),s(y)) = 2 >= 2y + 2 = gt(x,y) if(true(),x,y) = 5 >= x = x if(false(),x,y) = 1 >= y = y problem: DPs: TRS: times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) if(true(),x,y) -> x if(false(),x,y) -> y Qed DPs: plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),s(y)) -> plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),zero()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(zero(),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: [plus#](x0, x1) = 1x0 + x1 + 0, [false] = 3, [true] = 2, [zero] = 1, [id](x0) = 1x0, [not](x0) = 5, [if](x0, x1, x2) = 1x1 + x2 + 0, [gt](x0, x1) = 2x1 + 0, [s](x0) = 2x0 + 4 orientation: plus#(id(x),s(y)) = 2x + 2y + 4 >= 1x + 2y + 4 = plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),s(y)) = 3x + 2y + 5 >= 2x + 1y + 1 = plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) plus#(s(x),x) = 3x + 5 >= 3x + 4 = plus#(if(gt(x,x),id(x),id(x)),s(x)) gt(s(x),zero()) = 3 >= 2 = true() gt(s(x),s(y)) = 4y + 6 >= 2y + 0 = gt(x,y) gt(zero(),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: plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),zero()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(zero(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x not(x) -> if(x,false(),true()) Restore Modifier: DPs: plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: plus#(id(x),s(y)) -> plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),zero()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(zero(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x Arctic Interpretation Processor: dimension: 1 usable rules: if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x interpretation: [plus#](x0, x1) = x0, [false] = 4, [true] = 1, [zero] = 2, [id](x0) = 1x0, [if](x0, x1, x2) = x1 + x2, [gt](x0, x1) = 3x1 + 1, [s](x0) = 1x0 orientation: plus#(id(x),s(y)) = 1x >= x = plus#(x,if(gt(s(y),y),y,s(y))) plus#(s(x),x) = 1x >= 1x = plus#(if(gt(x,x),id(x),id(x)),s(x)) gt(s(x),zero()) = 5 >= 1 = true() gt(s(x),s(y)) = 4y + 1 >= 3y + 1 = gt(x,y) gt(zero(),y) = 3y + 1 >= 4 = false() if(true(),x,y) = x + y >= x = x if(false(),x,y) = x + y >= y = y id(x) = 1x >= x = x problem: DPs: plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: gt(s(x),zero()) -> true() gt(s(x),s(y)) -> gt(x,y) gt(zero(),y) -> false() if(true(),x,y) -> x if(false(),x,y) -> y id(x) -> x Restore Modifier: DPs: plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Usable Rule Processor: DPs: plus#(s(x),x) -> plus#(if(gt(x,x),id(x),id(x)),s(x)) TRS: id(x) -> x gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) if(true(),x,y) -> x if(false(),x,y) -> y Arctic Interpretation Processor: dimension: 1 usable rules: id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y interpretation: [plus#](x0, x1) = x0 + -6x1 + 0, [false] = 0, [true] = 2, [zero] = 6, [id](x0) = x0 + -4, [if](x0, x1, x2) = 2x1 + 4x2, [gt](x0, x1) = -3x0 + x1 + 2, [s](x0) = 6x0 + 6 orientation: plus#(s(x),x) = 6x + 6 >= 4x + 0 = plus#(if(gt(x,x),id(x),id(x)),s(x)) id(x) = x + -4 >= x = x gt(s(x),zero()) = 3x + 6 >= 2 = true() gt(zero(),y) = y + 3 >= 0 = false() gt(s(x),s(y)) = 3x + 6y + 6 >= -3x + y + 2 = gt(x,y) if(true(),x,y) = 2x + 4y >= x = x if(false(),x,y) = 2x + 4y >= y = y problem: DPs: TRS: id(x) -> x gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) if(true(),x,y) -> x if(false(),x,y) -> y Qed DPs: gt#(s(x),s(y)) -> gt#(x,y) TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Subterm Criterion Processor: simple projection: pi(gt#) = 1 problem: DPs: TRS: times(x,plus(y,1())) -> plus(times(x,plus(y,times(1(),0()))),x) times(x,1()) -> x times(x,0()) -> 0() plus(s(x),s(y)) -> s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) plus(s(x),x) -> plus(if(gt(x,x),id(x),id(x)),s(x)) plus(zero(),y) -> y plus(id(x),s(y)) -> s(plus(x,if(gt(s(y),y),y,s(y)))) id(x) -> x if(true(),x,y) -> x if(false(),x,y) -> y not(x) -> if(x,false(),true()) gt(s(x),zero()) -> true() gt(zero(),y) -> false() gt(s(x),s(y)) -> gt(x,y) Qed